Endgame for the Torsion PFR theorem

theorem sum_of_z_eq_zero {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω' : Type u) (Y : Fin p.m × Fin p.m → Ω' → G) : ∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑i • Y (i, j) + ∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑j • Y (i, j) + ∑ i : Fin p.m, ∑ j : Fin p.m, (-↑↑i - ↑↑j) • Y (i, j) = 0

Z_1+Z_2+Z_3= 0

theorem mutual_information_le_t_12 {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (Ω' : Type u) (Y : Fin p.m × Fin p.m → Ω' → G) [hΩ' : MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] : I[∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑i • Y (i, j) : ∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑j • Y (i, j)|∑ i : Fin p.m, ∑ j : Fin p.m, Y (i, j)] ≤ 4 * ↑p.m ^ 2 * p.η * multiTau p Ω hΩ X

We have I[Z_1 : Z_2 | W], I[Z_2 : Z_3 | W], I[Z_1 : Z_3 | W] ≤ 4m^2 η k.

theorem mutual_information_le_t_13 {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (Ω' : Type u) (Y : Fin p.m × Fin p.m → Ω' → G) [hΩ' : MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] : I[∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑i • Y (i, j) : ∑ i : Fin p.m, ∑ j : Fin p.m, (-↑↑i - ↑↑j) • Y (i, j)|∑ i : Fin p.m, ∑ j : Fin p.m, Y (i, j)] ≤ 4 * ↑p.m ^ 2 * p.η * multiTau p Ω hΩ X

theorem mutual_information_le_t_23 {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (Ω' : Type u) (Y : Fin p.m × Fin p.m → Ω' → G) [hΩ' : MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] : I[∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑j • Y (i, j) : ∑ i : Fin p.m, ∑ j : Fin p.m, (-↑↑i - ↑↑j) • Y (i, j)|∑ i : Fin p.m, ∑ j : Fin p.m, Y (i, j)] ≤ 4 * ↑p.m ^ 2 * p.η * multiTau p Ω hΩ X

theorem entropy_of_W_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (Ω' : Type u) (Y : Fin p.m × Fin p.m → Ω' → G) [hΩ' : MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] {m : ℝ} : H[∑ i : Fin p.m, ∑ j : Fin p.m, Y (i, j)] ≤ (2 * ↑p.m - 1) * multiTau p Ω hΩ X + m⁻¹ * ∑ i : Fin p.m, H[X i]

We have $\text{bbH}[W]\le (2m-1)k+\frac{1}{m}\sum _{i=1}^m\text{bbH}[X_i]$.

theorem entropy_of_Z_two_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (Ω' : Type u) (Y : Fin p.m × Fin p.m → Ω' → G) [hΩ' : MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] {m : ℝ} : H[∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑j • Y (i, j)] ≤ (8 * ↑p.m ^ 2 - 16 * ↑p.m + 1) * multiTau p Ω hΩ X + m⁻¹ * ∑ i : Fin p.m, H[X i]

We have $\text{bbH}[Z_2]\le (8m^2-16m+1)k+\frac{1}{m}\sum _{i=1}^m\text{bbH}[X_i]$.

theorem mutual_of_W_Z_two_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (Ω' : Type u) (Y : Fin p.m × Fin p.m → Ω' → G) [hΩ' : MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] : I[∑ i : Fin p.m, ∑ j : Fin p.m, Y (i, j) : ∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑j • Y (i, j)] ≤ 2 * (↑p.m - 1) * multiTau p Ω hΩ X

We have $\text{bbI}[W:Z_2]\le 2(m-1)k$.

theorem sum_of_conditional_distance_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (Ω' : Type u) (Y : Fin p.m × Fin p.m → Ω' → G) [hΩ' : MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] : ∑ i : Fin p.m, d[X i # ∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑j • Y (i, j) | ∑ i : Fin p.m, ∑ j : Fin p.m, Y (i, j)] ≤ 8 * (↑p.m ^ 3 - ↑p.m ^ 2) * multiTau p Ω hΩ X

We have $\sum _{i=1}^{m}d[X_i;Z_2|W]\le 8(m^3-m^2)k$.

theorem dist_of_U_add_le {G : Type u_1} [MeasureableFinGroup G] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] (T₁ T₂ T₃ : Ω → G) (hsum : T₁ + T₂ + T₃ = 0) (n : ℕ) {Ω' : Fin n → Type u_3} (hΩ' : (i : Fin n) → MeasureTheory.MeasureSpace (Ω' i)) (Y : (i : Fin n) → Ω' i → G) {α : ℝ} (hα : α > 0) : ∃ (Ω'' : Type u_4) (hΩ'' : MeasureTheory.MeasureSpace Ω'') (U : Ω'' → G), d[U # U] + α * ∑ i : Fin n, d[Y i # U] ≤ (2 + α * ↑n / 2) * (I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]) + α * ∑ i : Fin n, d[Y i # T₂]

Let $G$ be an abelian group, let $(T_1,T_2,T_3)$ be a $G^3$-valued random variable such that $T_1+T_2+T_3=0$ holds identically, and write [ \delta := \bbI[T_1 : T_2] + \bbI[T_1 : T_3] + \bbI[T_2 : T_3]. ] Let $Y_1,\dots ,Y_n$ be some further $G$-valued random variables and let $\alpha >0$ be a constant. Then there exists a random variable $U$ such that $$d[U;U]+\alpha \sum _{i=1}^{n}d[Y_i;U]\le (2+\frac{\alpha n}{2})\delta +\alpha \sum _{i=1}^{n}d[Y_i;T_2].$$

theorem k_eq_zero {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) : multiTau p Ω hΩ X = 0

We have $k=0$.

theorem dist_of_X_U_H_le {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (m : ℕ) (hm : m ≥ 2) (htorsion : ∀ (x : G), m • x = 0) (Ω : Type u_2) [MeasureTheory.MeasureSpace Ω] (X : Ω → G) : ∃ (H : AddSubgroup G) (Ω' : Type u_3) (mΩ : MeasureTheory.MeasureSpace Ω') (U : Ω' → G), ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[X # U] ≤ 64 * ↑m ^ 3 * d[X # X]

Suppose that $G$ is a finite abelian group of torsion $m$. Suppose that $X$ is a $G$-valued random variable. Then there exists a subgroup $H\le G$ such that [ d[X;U_H] \leq 64 m^3 d[X;X].]

theorem torsion_PFR_conjecture_aux {G : Type u_1} [AddCommGroup G] [Fintype G] {m : ℕ} (hm : m ≥ 2) (htorsion : ∀ (x : G), m • x = 0) {A : Set G} [Finite ↑A] {K : ℝ} (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : AddSubgroup G) (c : Set G), ↑(Nat.card ↑c) ≤ K ^ (64 * ↑m ^ 3 + 2) * ↑(Nat.card ↑A) ^ (1 / 2) * ↑(Nat.card ↥H) ^ (-1 / 2) ∧ ↑(Nat.card ↥H) ≤ K ^ (64 * ↑m ^ 3) * ↑(Nat.card ↑A) ∧ ↑(Nat.card ↑A) ≤ K ^ (64 * ↑m ^ 3) * ↑(Nat.card ↥H) ∧ A ⊆ c + ↑H

Suppose that $G$ is a finite abelian group of torsion $m$. If $A\subset G$ is non-empty and $|A+A|\le K|A|$, then $A$ can be covered by at most $K^{(64m^3+2)/2}|A{|}^{1/2}/|H{|}^{1/2}$ translates of a subspace $H$ of $G$ with $|H|/|A|\in [K^{-64m^3},K^{64m^3}]$

theorem torsion_exists_subgroup_subset_card_le {G : Type u_1} {m : ℕ} (hm : m ≥ 2) [AddCommGroup G] [Fintype G] (htorsion : ∀ (x : G), m • x = 0) {k : ℕ} (H : AddSubgroup G) (hk : k ≤ Nat.card ↥H) (h'k : k ≠ 0) : ∃ (K : AddSubgroup G), Nat.card ↥K ≤ k ∧ k < m * Nat.card ↥K ∧ K ≤ H

Every subgroup H of a finite m-torsion abelian group G contains a subgroup H' of order between k and mk, if 0 < k < |H|.

theorem torsion_PFR {G : Type u_1} [AddCommGroup G] [Fintype G] {m : ℕ} (hm : m ≥ 2) (htorsion : ∀ (x : G), m • x = 0) {A : Set G} [Finite ↑A] {K : ℝ} (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : AddSubgroup G) (c : Set G), ↑(Nat.card ↑c) < ↑m * K ^ (96 * ↑m ^ 3 + 2) ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

Suppose that $G$ is a finite abelian group of torsion $m$. If $A\subset G$ is non-empty and $|A+A|\le K|A|$, then $A$ can be covered by most $m{K}^{64m^3+1}$ translates of a subspace $H$ of $G$ with $|H|\le |A|$.