ff done 🎉

LeanAPAP.lean

@@ -11,6 +11,7 @@ import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
 import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
+import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Basic

LeanAPAP/FiniteField/Basic.lean

@@ -1,6 +1,7 @@
 import Mathlib.FieldTheory.Finite.Basic
 import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
 import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
+import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Physics.AlmostPeriodicity
@@ -216,7 +217,17 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
     rw [dLinftyNorm_eq_iSup_norm, ← Finset.sup'_univ_eq_ciSup, Finset.le_sup'_iff] at hv'
     obtain ⟨x, -, hx⟩ := hv'
     let B' : Finset V' := (-x +ᵥ B).preimage (↑) Set.injOn_subtype_val
-    have hβ : (1 + 64⁻¹ : ℝ) * B.dens ≤ B'.dens := sorry
+    have hβ := by
+      calc
+        ((1 + 64⁻¹ : ℝ) * B.dens : ℝ) = (1 + 2⁻¹ / 32) * B.dens := by ring
+        _ ≤ ‖(𝟭_[ℝ] B ∗ μ (V' : Set V).toFinset) x‖ := hx
+        _ = B'.dens := ?_
+      rw [mu, conv_smul, Pi.smul_apply, indicate_conv_indicate_eq_card_vadd_inter_neg,
+        norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div]
+      congr 2
+      · congr 1 with x
+        simp
+      · simp
     simp at hx
     refine ⟨V', inferInstance, inferInstance, inferInstance, inferInstance, B', ?_, ?_, ?_,
       fun h ↦ ?_⟩
@@ -227,7 +238,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
         _ ≤ finrank (ZMod q) V' + 2 ^ 171 * 𝓛 B.dens ^ 4 * 𝓛 α ^ 4 / 2⁻¹ ^ 24 +
             2 ^ 195 * i * 𝓛 α ^ 8 := by gcongr
         _ ≤ finrank (ZMod q) V' + 2 ^ 171 * 𝓛 α ^ 4 * 𝓛 α ^ 4 / 2⁻¹ ^ 24 +
-            2 ^ 195 * i * 𝓛 α ^ 8 := by gcongr; sorry
+            2 ^ 195 * i * 𝓛 α ^ 8 := by have := hα₀.trans_le hαβ; gcongr
         _ = _ := by push_cast; ring
     · exact .of_image .subtypeVal Set.injOn_subtype_val (Set.subset_univ _)
         (hB.vadd_set (a := -x) |>.mono $ by simp [B'])

LeanAPAP/Mathlib/Data/Finset/Preimage.lean

@@ -0,0 +1,10 @@
+import Mathlib.Data.Finset.Preimage
+
+namespace Finset
+variable {α β : Type*} {f : α → β} {s : Finset β}
+
+lemma card_preimage (s : Finset β) (f : α → β) (hf) [DecidablePred (· ∈ Set.range f)] :
+    (s.preimage f hf).card = {x ∈ s | x ∈ Set.range f}.card :=
+  card_nbij f (by simp) (by simpa) (fun b hb ↦ by aesop)
+
+end Finset

LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean

@@ -50,7 +50,7 @@ In this section, we define the convolution `f ∗ g` and difference convolution
 section CommSemiring
 variable [CommSemiring R] {f g : G → R}
 
-lemma indicate_conv_indicate_apply (s t : Finset G) (a : G) :
+lemma indicate_conv_indicate_eq_sum (s t : Finset G) (a : G) :
     (𝟭_[R] s ∗ 𝟭 t) a = ((s ×ˢ t).filter fun x : G × G ↦ x.1 + x.2 = a).card := by
   simp only [conv_apply, indicate_apply, ← ite_and, filter_comm, boole_mul, sum_boole]
   simp_rw [← mem_product, filter_univ_mem]
@@ -61,6 +61,12 @@ lemma indicate_conv (s : Finset G) (f : G → R) : 𝟭 s ∗ f = ∑ a ∈ s, 
 lemma conv_indicate (f : G → R) (s : Finset G) : f ∗ 𝟭 s = ∑ a ∈ s, τ a f := by
   ext; simp [conv_eq_sum_sub, indicate_apply]
 
+lemma indicate_conv_indicate_eq_card_vadd_inter_neg (s t : Finset G) (a : G) :
+    (𝟭_[R] s ∗ 𝟭 t) a = ((-a +ᵥ s) ∩ -t).card := by
+  rw [← card_neg, neg_inter]
+  simp [conv_indicate, indicate, inter_comm, ← filter_mem_eq_inter, ← neg_vadd_mem_iff,
+    ← sub_eq_add_neg]
+
 variable [StarRing R]
 
 lemma indicate_dconv_indicate_apply (s t : Finset G) (a : G) :

blueprint/src/chapter/ff.tex

@@ -195,7 +195,7 @@ \chapter{Finite field model}
 \end{theorem}
 \begin{proof}
   \uses{no3aps_inner_prod, di_in_ff}
-  % \leanok
+  \leanok
 
   Let $t\geq 0$ be maximal such that there is a sequence of subspaces $\bbf_q^n=V_0\geq \cdots \geq V_t$ and associated $A_i\subseteq V_i$ with $A_0=A$ such that
   \begin{enumerate}