Documentation

PFR.EntropyPFR

Entropic version of polynomial Freiman-Ruzsa conjecture #

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

Main results #

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, 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) ( : 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) :
∃ (H : Submodule (ZMod 2) G) (Ω : Type uG) ( : 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₀₂]