Endgame for the Torsion PFR theorem

theorem Q_eq {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : MeasureTheory.MeasureSpace Ωₒ] {p : multiRefPackage G Ωₒ} {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} (j : Fin p.m) : (fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j = ∑ i : Fin p.m, Y (i, j)

theorem sum_of_z_eq_zero {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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 indep_yj {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : MeasureTheory.MeasureSpace Ωₒ] {p : multiRefPackage G Ωₒ} {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} [hΩ' : MeasureTheory.MeasureSpace Ω'] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (j : Fin p.m) : ProbabilityTheory.iIndepFun (fun (i : Fin p.m) => Y (i, j)) MeasureTheory.volume

theorem mutual_information_le_t_12 {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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} (h_min : multiTauMinimizes p Ω hΩ X) {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} [hΩ' : MeasureTheory.MeasureSpace Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume 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)] ≤ ↑p.m * (4 * ↑p.m + 1) * p.η * D[X; hΩ]

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

theorem torsion_mul_eq {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : MeasureTheory.MeasureSpace Ωₒ] {p : multiRefPackage G Ωₒ} {i j : ℤ} (x : G) (h : i ≡ j [ZMOD ↑p.m]) : i • x = j • x

theorem mutual_information_le_t_23 {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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} (h_min : multiTauMinimizes p Ω hΩ X) {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} [hΩ' : MeasureTheory.MeasureSpace Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume 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)] ≤ ↑p.m * (4 * ↑p.m + 1) * p.η * D[X; hΩ]

theorem mutual_information_le_t_13 {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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} (h_min : multiTauMinimizes p Ω hΩ X) {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} [hΩ' : MeasureTheory.MeasureSpace Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume 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)] ≤ ↑p.m * (4 * ↑p.m + 1) * p.η * D[X; hΩ]

theorem Q_ident {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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 Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume MeasureTheory.volume) (j j' : Fin p.m) : ProbabilityTheory.IdentDistrib ((fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j) ((fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j') MeasureTheory.volume MeasureTheory.volume

theorem Q_mes {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : MeasureTheory.MeasureSpace Ωₒ] {p : multiRefPackage G Ωₒ} {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} [hΩ' : MeasureTheory.MeasureSpace Ω'] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (j : Fin p.m) : Measurable (-(fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j)

theorem Q_dist {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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 Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume MeasureTheory.volume) (j j' : Fin p.m) : d[(fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j # -(fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j'] ≤ 2 * D[X; hΩ]

theorem Q_ent {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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 Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume MeasureTheory.volume) (j : Fin p.m) : H[(fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j] = D[X; hΩ] + (↑p.m)⁻¹ * ∑ i : Fin p.m, H[X i]

theorem Q_indep {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : MeasureTheory.MeasureSpace Ωₒ] {p : multiRefPackage G Ωₒ} {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} [hΩ' : MeasureTheory.MeasureSpace Ω'] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) {j j' : Fin p.m} (h : j ≠ j') : ProbabilityTheory.IndepFun ((fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j) (-(fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j') MeasureTheory.volume

theorem entropy_of_W_le {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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 Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume MeasureTheory.volume) : H[∑ i : Fin p.m, ∑ j : Fin p.m, Y (i, j)] ≤ (2 * ↑p.m - 1) * D[X; hΩ] + (↑p.m)⁻¹ * ∑ i : Fin p.m, H[X i]

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

theorem Z2_eq {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : MeasureTheory.MeasureSpace Ωₒ] {p : multiRefPackage G Ωₒ} {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} : ∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑j • Y (i, j) = ∑ j ∈ Finset.univ.erase ⟨0, ⋯⟩, ↑j • (fun (j : Fin p.m) => ∑ i : Fin p.m, Y (i, j)) j

theorem entropy_of_Z_two_le {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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 Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume MeasureTheory.volume) : H[∑ i : Fin p.m, ∑ j : Fin p.m, ↑↑j • Y (i, j)] ≤ (8 * ↑p.m ^ 2 - 16 * ↑p.m + 1) * D[X; hΩ] + (↑p.m)⁻¹ * ∑ i : Fin p.m, H[X i]

We have $\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} [MeasurableFinGroup G] [hΩ₀ : 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 Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume 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) * D[X; hΩ]

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

theorem sum_of_conditional_distance_le {G Ωₒ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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} (hΩ_prob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) (hX_mes : ∀ (i : Fin p.m), Measurable (X i)) {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} [hΩ' : MeasureTheory.MeasureSpace Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume 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)] ≤ 4 * (↑p.m ^ 3 - ↑p.m ^ 2) * D[X; hΩ]

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

theorem pigeonhole {G : Type u_1} [MeasureTheory.MeasureSpace G] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Finite G] [MeasurableSingletonClass G] (f : G → ℝ) : ∃ (x : G), f x ≤ ∫ (z : G), f z ∧ MeasureTheory.volume {x} ≠ 0

theorem dist_of_U_add_le {G : Type u_1} [MeasurableFinGroup G] {Ω : Type u} [hΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ T₂ T₃ : Ω → G} (hsum : T₁ + T₂ + T₃ = 0) (hmes₁ : Measurable T₁) (hmes₂ : Measurable T₂) (hmes₃ : Measurable T₃) {n : ℕ} {Ω' : Fin n → Type u_2} (hΩ' : (i : Fin n) → MeasureTheory.MeasureSpace (Ω' i)) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Y : (i : Fin n) → Ω' i → G} (hY : ∀ (i : Fin n), Measurable (Y i)) {α : ℝ} (hα : α > 0) : ∃ (Ω'' : Type u) (hΩ'' : MeasureTheory.MeasureSpace Ω'') (U : Ω'' → G), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ 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] \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} [MeasurableFinGroup G] [hΩ₀ : 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} (h_min : multiTauMinimizes p Ω hΩ X) (hΩ_prob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) (hX_mes : ∀ (i : Fin p.m), Measurable (X i)) {Ω' : Type u} {Y : Fin p.m × Fin p.m → Ω' → G} [hΩ' : MeasureTheory.MeasureSpace Ω'] [hΩ'_prob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (h_mes : ∀ (i j : Fin p.m), Measurable (Y (i, j))) (h_indep : ProbabilityTheory.iIndepFun Y MeasureTheory.volume) (hident : ∀ (i j : Fin p.m), ProbabilityTheory.IdentDistrib (Y (i, j)) (X i) MeasureTheory.volume MeasureTheory.volume) (hη_eq : p.η = 1 / (32 * ↑p.m ^ 3)) : D[X; hΩ] = 0

We have $k = 0$.

theorem dist_of_X_U_H_le {G : Type u} [AddCommGroup G] [Finite G] [MeasurableSpace G] [MeasurableSingletonClass G] {m : ℕ} (hm : m ≥ 2) (htorsion : ∀ (x : G), m • x = 0) {Ω : Type u} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω → G} (hX : Measurable X) : ∃ (H : AddSubgroup G) (Ω' : Type u) (mΩ : MeasureTheory.MeasureSpace Ω'), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ ∃ (U : Ω' → G), ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ Measurable U ∧ 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 rdist_le_of_isUniform_of_card_add_le' {G : Type u_1} [AddCommGroup G] {A : Set G} {K : ℝ} [Countable G] [A_fin : Finite ↑A] [MeasurableSpace G] [MeasurableSingletonClass G] (h₀A : A.Nonempty) (hA : ↑(A + A).ncard ≤ K * ↑A.ncard) {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {U₀ : Ω → G} (U₀unif : ProbabilityTheory.IsUniform A U₀ MeasureTheory.volume) (U₀meas : Measurable U₀) : d[U₀ # -U₀] ≤ Real.log K

A uniform distribution on a set with doubling constant K has self Rusza distance at most log K.

theorem torsion_PFR_conjecture_aux {G : Type u_1} [AddCommGroup G] [Finite G] {m : ℕ} (hm : m ≥ 2) (htorsion : ∀ (x : G), m • x = 0) {A : Set G} [A_fin : Finite ↑A] {K : ℝ} (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑A.ncard) : ∃ (H : AddSubgroup G) (c : Set G), ↑c.ncard ≤ K ^ (128 * m ^ 3 + 1) * ↑A.ncard ^ (1 / 2) * ↑(↑H).ncard ^ (-1 / 2) ∧ ↑(↑H).ncard ≤ K ^ (256 * m ^ 3) * ↑A.ncard ∧ ↑A.ncard ≤ K ^ (256 * m ^ 3) * ↑(↑H).ncard ∧ 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_exists_subgroup_subset_card_le {G : Type u_1} {m : ℕ} (hm : m ≥ 2) [AddCommGroup G] [Finite G] (htorsion : ∀ (x : G), m • x = 0) {k : ℕ} (H : AddSubgroup G) (hk : k ≤ (↑H).ncard) (h'k : k ≠ 0) : ∃ (K : AddSubgroup G), (↑K).ncard ≤ k ∧ k < m * (↑K).ncard ∧ 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] [Finite 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 * ↑A.ncard) : ∃ (H : AddSubgroup G) (c : Set G), ↑(Nat.card ↑c) < ↑m * K ^ (256 * m ^ 3 + 1) ∧ (↑H).ncard ≤ A.ncard ∧ 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|$.