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^0_1, X^0_2$, there is some subgroup $H \leq G$ such that $d[X^0_1;U_H] + d[X^0_2;U_H] \le 11 d[X^0_1;X^0_2]$.
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₁ : Ω → G}
{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, 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]
[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^0_1, X^0_2$, there is some
subgroup $H \leq G$ such that $d[X^0_1;U_H] + d[X^0_2;U_H] \le 11 d[X^0_1;X^0_2]$.
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)
: