Finite field case

theorem global_dichotomy {G : Type u} [AddCommGroup G] [Fintype G] {A C : Finset G} {γ ε : ℝ} [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.Nonempty) (hγC : γ ≤ ↑C.dens) (hγ : 0 < γ) (hAC : ε ≤ |↑(Fintype.card G) * ⟪mu A ∗ᵈ mu A, mu C⟫_[ℝ] - 1|) : ε / (2 * ↑(Fintype.card G)) ≤ ‖Fintype.balance (mu A) ○ᵈ Fintype.balance (mu A)‖_[↑(2 * ⌈1 + Real.log γ⁻¹⌉₊), mu Finset.univ]

theorem ap_in_ff {G : Type u} [AddCommGroup G] [Fintype G] {ε : ℝ} {q : ℕ} [Module (ZMod q) G] {A₁ A₂ : Finset G} (S : Finset G) {α : ℝ} [DecidableEq G] (hq : Nat.Prime q) (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁ : α ≤ ↑A₁.dens) (hαA₂ : α ≤ ↑A₂.dens) : ∃ (V : Submodule (ZMod q) G) (x : DecidablePred fun (x : G) => x ∈ V), ↑(Module.finrank (ZMod q) G - Module.finrank (ZMod q) ↥V) ≤ 2 ^ 32 * (1 + Real.log α⁻¹) ^ 2 * (1 + Real.log (ε * α)⁻¹) ^ 2 * ε⁻¹ ^ 2 ∧ |∑ x_1 ∈ S, (mu (↑V).toFinset ∗ᵈ mu A₁ ∗ᵈ mu A₂) x_1 - ∑ x ∈ S, (mu A₁ ∗ᵈ mu A₂) x| ≤ ε

theorem di_in_ff {G : Type u} [AddCommGroup G] [Fintype G] {A C : Finset G} {γ ε : ℝ} {q : ℕ} [Module (ZMod q) G] [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq : Nat.Prime q) (hε₀ : 0 < ε) (hε₁ : ε < 1) (hγC : γ ≤ ↑C.dens) (hγ : 0 < γ) (hAC : ε ≤ |↑(Fintype.card G) * ⟪mu A ∗ᵈ mu A, mu C⟫_[ℝ] - 1|) : ∃ (V : Submodule (ZMod q) G) (x : DecidablePred fun (x : G) => x ∈ V), ↑(Module.finrank (ZMod q) G - Module.finrank (ZMod q) ↥V) ≤ 2 ^ 128 * (1 + Real.log (↑A.dens)⁻¹) ^ 4 * (1 + Real.log γ⁻¹) ^ 4 / ε ^ 12 ∧ (1 + ε / 32) * ↑A.dens ≤ ‖((↑A).indicator fun (x : G) => 1) ∗ᵈ mu (↑V).toFinset‖_[⊤]

theorem ff {G : Type u} [AddCommGroup G] [Fintype G] {A : Finset G} {q : ℕ} [Module (ZMod q) G] (hq₃ : 3 ≤ q) (hq : Nat.Prime q) (hA₀ : A.Nonempty) (hA : ThreeAPFree ↑A) : ↑(Module.finrank (ZMod q) G) ≤ 2 ^ 148 * (1 + Real.log (↑A.dens)⁻¹) ^ 9