Polynomial Freiman-Ruzsa conjecture

Here we prove the polynomial Freiman-Ruzsa conjecture.

theorem ProbabilityTheory.IsUniform.measureReal_preimage_sub_zero {G : Type u_1} {Ω : Type u_2} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {A : Finset G} {B : Finset G} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {U : Ω → G} {V : Ω → G} (Uunif : ProbabilityTheory.IsUniform (↑A) U MeasureTheory.volume) (Umeas : Measurable U) (Vunif : ProbabilityTheory.IsUniform (↑B) V MeasureTheory.volume) (Vmeas : Measurable V) (h_indep : ProbabilityTheory.IndepFun U V MeasureTheory.volume) : MeasureTheory.volume.real ((U - V) ⁻¹' {0}) = ↑(Nat.card ↑(↑A ∩ ↑B)) / (↑(Nat.card { x : G // x ∈ A }) * ↑(Nat.card { x : G // x ∈ B }))

Given two independent random variables U and V uniformly distributed respectively on A and B, then U = V with probability #(A ∩ B) / #A ⬝ #B.

theorem ProbabilityTheory.IsUniform.measureReal_preimage_sub {G : Type u_1} {Ω : Type u_2} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {A : Finset G} {B : Finset G} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {U : Ω → G} {V : Ω → G} (Uunif : ProbabilityTheory.IsUniform (↑A) U MeasureTheory.volume) (Umeas : Measurable U) (Vunif : ProbabilityTheory.IsUniform (↑B) V MeasureTheory.volume) (Vmeas : Measurable V) (h_indep : ProbabilityTheory.IndepFun U V MeasureTheory.volume) (x : G) : MeasureTheory.volume.real ((U - V) ⁻¹' {x}) = ↑(Nat.card ↑(↑A ∩ (↑B + {x}))) / (↑(Nat.card { x : G // x ∈ A }) * ↑(Nat.card { x : G // x ∈ B }))

Given two independent random variables U and V uniformly distributed respectively on A and B, then U = V + x with probability # (A ∩ (B + x)) / #A ⬝ #B.

theorem PFR_conjecture_pos_aux {G : Type u_1} [AddCommGroup G] {A : Set G} [Finite ↑A] {K : ℝ} (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A - A)) ≤ K * ↑(Nat.card ↑A)) : 0 < ↑(Nat.card ↑A) ∧ 0 < ↑(Nat.card ↑(A - A)) ∧ 0 < K

Record positivity results that are useful in the proof of PFR.

theorem PFR_conjecture_pos_aux' {G : Type u_1} [AddCommGroup G] {A : Set G} [Finite ↑A] {K : ℝ} (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : 0 < ↑(Nat.card ↑A) ∧ 0 < ↑(Nat.card ↑(A + A)) ∧ 0 < K

theorem rdist_le_of_isUniform_of_card_add_le {G : Type u_1} [AddCommGroup G] {A : Set G} {K : ℝ} [Countable G] [A_fin : Finite ↑A] [MeasurableSpace G] [MeasurableSingletonClass G] (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A - A)) ≤ K * ↑(Nat.card ↑A)) {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {U₀ : Ω → G} (U₀unif : ProbabilityTheory.IsUniform A U₀ MeasureTheory.volume) (U₀meas : Measurable U₀) : d[U₀ # U₀] ≤ Real.log K

A uniform distribution on a set with doubling constant K has self Rusza distance at most log K.

theorem sumset_eq_sub {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (A : Set G) : A + A = A - A

theorem PFR_conjecture_aux {G : Type u_1} [AddCommGroup G] {A : Set G} {K : ℝ} [Countable G] [Module (ZMod 2) G] [Fintype G] (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), ↑(Nat.card ↑c) ≤ K ^ (13 / 2) * ↑(Nat.card ↑A) ^ (1 / 2) * ↑(Nat.card ↥H) ^ (-1 / 2) ∧ ↑(Nat.card ↥H) ≤ K ^ 11 * ↑(Nat.card ↑A) ∧ ↑(Nat.card ↑A) ≤ K ^ 11 * ↑(Nat.card ↥H) ∧ A ⊆ c + ↑H

Auxiliary statement towards the polynomial Freiman-Ruzsa (PFR) conjecture: if A is a subset of an elementary abelian 2-group of doubling constant at most $K$, then there exists a subgroup H such that A can be covered by at most K^(13/2) |A|^(1/2) / |H|^(1/2) cosets of H, and H has the same cardinality as A up to a multiplicative factor K^11.

theorem PFR_conjecture {G : Type u_1} [AddCommGroup G] {A : Set G} {K : ℝ} [Countable G] [Module (ZMod 2) G] [Fintype G] (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), ↑(Nat.card ↑c) < 2 * K ^ 12 ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

The polynomial Freiman-Ruzsa (PFR) conjecture: if A is a subset of an elementary abelian 2-group of doubling constant at most K, then A can be covered by at most 2 * K ^ 12 cosets of a subgroup of cardinality at most |A|.

theorem PFR_conjecture' {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (Afin : A.Finite) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (↑H).Finite ∧ ↑(Nat.card ↑c) < 2 * K ^ 12 ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

Corollary of PFR_conjecture in which the ambient group is not required to be finite (but) then H and c are finite.