Documentation

PFR.TorsionEndgame

Endgame for the Torsion PFR theorem #

Main definitions: #

Main results #

theorem sum_of_z_eq_zero {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω' : Type u) (Y : Fin p.m × Fin p.mΩ'G) :
(((Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => i Y (i, j)) + Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => j Y (i, j)) + -Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (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} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.mType u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω iG) (Ω' : Type u) [hΩ' : MeasureTheory.MeasureSpace Ω'] (Y : Fin p.m × Fin p.mΩ'G) :
I[Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => i Y (i, j) : Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => j Y (i, j)|Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => Y (i, j)] 4 * p.m ^ 2 * p * multiTau p Ω 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} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.mType u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω iG) (Ω' : Type u) [hΩ' : MeasureTheory.MeasureSpace Ω'] (Y : Fin p.m × Fin p.mΩ'G) :
I[Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => i Y (i, j) : -Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => (i + j) Y (i, j)|Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => Y (i, j)] 4 * p.m ^ 2 * p * multiTau p Ω X
theorem mutual_information_le_t_23 {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.mType u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω iG) (Ω' : Type u) [hΩ' : MeasureTheory.MeasureSpace Ω'] (Y : Fin p.m × Fin p.mΩ'G) :
I[Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => j Y (i, j) : -Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => (i + j) Y (i, j)|Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => Y (i, j)] 4 * p.m ^ 2 * p * multiTau p Ω X
theorem entropy_of_W_le {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.mType u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω iG) (Ω' : Type u) [hΩ' : MeasureTheory.MeasureSpace Ω'] (Y : Fin p.m × Fin p.mΩ'G) {m : } :
H[Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => Y (i, j)] (2 * p.m - 1) * multiTau p Ω X + m⁻¹ * Finset.univ.sum fun (i : Fin p.m) => H[X i]

We let $\bbH[W] \leq (2m-1)k + \frac1m \sum_{i=1}^m \bbH[X_i]$.

theorem entropy_of_Z_two_le {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.mType u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω iG) (Ω' : Type u) [hΩ' : MeasureTheory.MeasureSpace Ω'] (Y : Fin p.m × Fin p.mΩ'G) {m : } :
H[Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => j Y (i, j)] (8 * p.m ^ 2 - 16 * p.m + 1) * multiTau p Ω X + m⁻¹ * Finset.univ.sum fun (i : Fin p.m) => H[X i]

We let $\bbH[Z_2] \leq (8m^2-16m+1) k + \frac{1}{m} \sum_{i=1}^m \bbH[X_i]$.

theorem mutual_of_W_Z_two_le {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.mType u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω iG) (Ω' : Type u) [hΩ' : MeasureTheory.MeasureSpace Ω'] (Y : Fin p.m × Fin p.mΩ'G) :
I[Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => Y (i, j) : Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => j Y (i, j)] 2 * (p.m - 1) * multiTau p Ω X

We let $\bbI[W : Z_2] \leq 2 (m-1) k$.

theorem sum_of_conditional_distance_le {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.mType u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω iG) (Ω' : Type u) [hΩ' : MeasureTheory.MeasureSpace Ω'] (Y : Fin p.m × Fin p.mΩ'G) [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] :
(Finset.univ.sum fun (i : Fin p.m) => d[X i # Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => j Y (i, j) | Finset.univ.sum fun (i : Fin p.m) => Finset.univ.sum fun (j : Fin p.m) => Y (i, j)]) 8 * (p.m ^ 3 - p.m ^ 2) * multiTau p Ω X

We let $\sum_{i=1}^m d[X_i;Z_2|W] \leq 8(m^3-m^2) k$.

theorem dist_of_U_add_le {G : Type u_1} [MeasureableFinGroup G] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] (T₁ : ΩG) (T₂ : ΩG) (T₃ : ΩG) (hsum : T₁ + T₂ + T₃ = 0) (n : ) {Ω' : Fin nType u_3} (hΩ' : (i : Fin n) → MeasureTheory.MeasureSpace (Ω' i)) (Y : (i : Fin n) → Ω' iG) {α : } (hα : α > 0) :
∃ (Ω'' : Type u_4) (hΩ'' : MeasureTheory.MeasureSpace Ω'') (U : Ω''G), (d[U # U] + α * Finset.univ.sum fun (i : Fin n) => d[Y i # U]) (2 + α * n / 2) * (I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]) + α * Finset.univ.sum fun (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] \leq \Bigl(2 + \frac{\alpha n}{2} \Bigr) \delta + \alpha \sum_{i=1}^n d[Y_i;T_2]. $$

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

We let $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) ( : 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 \leq 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| \leq 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_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 ^ (64 * m ^ 3 + 1) 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| \leq K|A|$, then $A$ can be covered by most $mK^{64m^3+1}$ translates of a subspace $H$ of $G$ with $|H| \leq |A|$.