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 \leq G$ such that $d[X_1^0;U_H] + d[X_2^0;U_H] \le 11 d[X_1^0;X_2^0]$, and both $d[X_1^0;U_H]$ and $d[X_2^0;U_H]$ are at most $6 d[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] [Finite G] [MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (h_min : TauMinimizes 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, X'_2$ such that $\tau[X'_1;X'_2] < \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] [Finite 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₀₂] ∧ d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧ d[p.X₀₂ # U] ≤ 6 * 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 \leq G$ such that $d[X_1^0;U_H] + d[X_2^0;U_H] \le 11 d[X_1^0;X_2^0]$, and both $d[X_1^0; U_H]$ and $d[X_2^0; U_H]$ are at most $6 d[X_1^0;X_2^0]$.