Entropic version of polynomial Freiman-Ruzsa conjecture

Here we prove the entropic version of the polynomial Freiman-Ruzsa conjecture.

Main results

• entropic_PFR_conjecture: For two $G$-valued random variables $X_1^0,X_2^0$, there is some subgroup $H\le G$ such that $d[X_1^0;U_H]+d[X_2^0;U_H]\le 11d[X_1^0;X_2^0]$.

theorem tau_strictly_decreases {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {Ω : Type u_3} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (h_min : tau_minimizes p X₁ X₂) (hpη : p.η = 1 / 9) : d[X₁ # X₂] = 0

If $d[X_1;X_2]>0$ then there are $G$-valued random variables $X_1^{\prime },X_2^{\prime }$ such that $\tau [X_1^{\prime };X_2^{\prime }]<\tau [X_1;X_2]$. Phrased in the contrapositive form for convenience of proof.

theorem entropic_PFR_conjecture {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) (hpη : p.η = 1 / 9) : ∃ (H : Submodule (ZMod 2) G) (Ω : Type uG) (mΩ : MeasureTheory.MeasureSpace Ω) (U : Ω → G), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂]

entropic_PFR_conjecture: For two $G$-valued random variables $X_1^0,X_2^0$, there is some subgroup $H\le G$ such that $d[X_1^0;U_H]+d[X_2^0;U_H]\le 11d[X_1^0;X_2^0]$.

theorem entropic_PFR_conjecture' {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) (hpη : p.η = 1 / 9) : ∃ (H : Submodule (ZMod 2) G) (Ω : Type uG) (mΩ : MeasureTheory.MeasureSpace Ω) (U : Ω → G), ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧ d[p.X₀₂ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂]