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] [Finite G] [MeasurableSpace G] [MeasurableSingletonClass G] {A B : Finset G} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {U V : Ω → G} [DecidableEq G] (Uunif : IsUniform (↑A) U MeasureTheory.volume) (Umeas : Measurable U) (Vunif : IsUniform (↑B) V MeasureTheory.volume) (Vmeas : Measurable V) (h_indep : IndepFun U V MeasureTheory.volume) : MeasureTheory.volume.real ((U - V) ⁻¹' {0}) = ↑(A ∩ B).card / (↑A.card * ↑B.card)

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] [Finite G] [MeasurableSpace G] [MeasurableSingletonClass G] {A B : Finset G} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {U V : Ω → G} [DecidableEq G] (Uunif : IsUniform (↑A) U MeasureTheory.volume) (Umeas : Measurable U) (Vunif : IsUniform (↑B) V MeasureTheory.volume) (Vmeas : Measurable V) (h_indep : IndepFun U V MeasureTheory.volume) (x : G) : MeasureTheory.volume.real ((U - V) ⁻¹' {x}) = ↑(A ∩ (B + {x})).card / (↑A.card * ↑B.card)

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} (hA : A.Finite) {K : ℝ} (hA₀ : A.Nonempty) (hAK : ↑(A - A).ncard ≤ K * ↑A.ncard) : 0 < ↑A.ncard ∧ 0 < ↑(A - A).ncard ∧ 0 < K

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

theorem PFR_conjecture_pos_aux' {G : Type u_1} [AddCommGroup G] {A : Set G} (hA : A.Finite) {K : ℝ} (hA₀ : A.Nonempty) (hAK : ↑(A + A).ncard ≤ K * ↑A.ncard) : 0 < ↑A.ncard ∧ 0 < ↑(A + A).ncard ∧ 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] (hA₀ : A.Nonempty) (hA : ↑(A - A).ncard ≤ K * ↑A.ncard) {Ω : 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] [Finite G] (hA₀ : A.Nonempty) (hA : ↑(A + A).ncard ≤ K * ↑A.ncard) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), ↑(Nat.card ↑c) ≤ K ^ (13 / 2) * ↑A.ncard ^ (1 / 2) * ↑(↑H).ncard ^ (-1 / 2) ∧ ↑(↑H).ncard ≤ K ^ 11 * ↑A.ncard ∧ ↑A.ncard ≤ K ^ 11 * ↑(↑H).ncard ∧ 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] [Finite G] (hA₀ : A.Nonempty) (hA : ↑(A + A).ncard ≤ K * ↑A.ncard) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), ↑(Nat.card ↑c) < 2 * K ^ 12 ∧ (↑H).ncard ≤ A.ncard ∧ 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 : ℝ} (hA₀ : A.Nonempty) (Afin : A.Finite) (hA : ↑(A + A).ncard ≤ K * ↑A.ncard) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (↑H).Finite ∧ ↑(Nat.card ↑c) < 2 * K ^ 12 ∧ (↑H).ncard ≤ A.ncard ∧ 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.