`PFR/TorsionEndgame.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 9 curated AI-written annotations and 485 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2

25 declarations, 0 contain sorry, 0 declared as axioms

Endgame for the Torsion PFR theorem

dist_of_X_U_H_le: entropy form, with explicit constant 64 m^3.
torsion_PFR_conjecture_aux: covering by K^(128 m^3 + 1) |A|^{1/2}/|H|^{1/2} cosets, with |H|/|A| in [K^{-256 m^3}, K^{256 m^3}].
torsion_PFR: covering by fewer than m * K^(256 m^3 + 1) cosets of a finite subgroup no larger than A (ambient group need not be finite).

The extra factors of 2 relative to the entropy form comes from the lack of 2-torsion: d[U_A; U_A] ≤ 2 d[U_A; -U_A] ≤ 2 log K.

Imports (6)

Imported by 3 files

lemma Q_eq line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Prod, Fin, multiRefPackage.m, Eq, Finset.sum, Finset.univ, Prod.mk
Proof uses: Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma sum_of_z_eq_zero Z_1+Z_2+Z_3= 0 line 52 source
Source documentation
Z_1+Z_2+Z_3= 0

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Prod, Fin, multiRefPackage.m, Eq, HAdd.hAdd, Finset.sum, Finset.univ, HSMul.hSMul, Int, Prod.mk, HSub.hSub, Neg.neg, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Finset.sum_add_distrib, Finset.sum_eq_zero, Membership.mem, Finset, add_zsmul, eq_of_heq, HEq, Eq.refl, HEq.refl, outParam, HSMul, of_eq_true, Eq.trans, True, congrFun', add_add_sub_cancel and 3 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma sum_of_z_eq_zero :Z1 + Z2 + Z3 = 0 := by
…
```
lemma indep_yj line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Prod, Fin, multiRefPackage.m, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, MeasureTheory.MeasureSpace.volume
Proof uses: Finset, Singleton.singleton, Subtype, Membership.mem, Subtype.mk, of_eq_true, Eq.trans, Eq, True, eq_self, Eq.mpr, Eq.refl, ProbabilityTheory.iIndepFun.finsets_comp, Set.PairwiseDisjoint, Set.univ, Set, Finset.Nonempty, Inter.inter, id, congrArg and 11 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma mutual_information_le_t_12 We have I[Z_1 : Z_2 | W], I[Z_2 : Z_3 | W], I[Z_1 : Z_3 | W] ≤ 4m^2 η k line 79 source
Source documentation
We have I[Z_1 : Z_2 | W], I[Z_2 : Z_3 | W], I[Z_1 : Z_3 | W] ≤ 4m^2 η k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, multiTauMinimizes, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, LE.le, Real, ProbabilityTheory.condMutualInfo, Finset.sum, Finset.univ, HSMul.hSMul, Int and 6 more
Proof uses: GE.ge, multiRefPackage.hm, Fin.mk, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 89 more
155 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma mutual_information_le_t_12 : I[Z1 : Z2 | W] ≤ p.m * (4*p.m+1) * p.η * k := by
…
```
lemma torsion_mul_eq line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Int, Int.ModEq, multiRefPackage.m, Eq, HSMul.hSMul
Proof uses: HAdd.hAdd, HMul.hMul, Exists, Eq.mp, congrArg, propext, Int.modEq_iff_add_fac, of_eq_true, Eq.trans, True, congrFun', mul_comm, add_smul, OfNat.ofNat, mul_zsmul, Nat, natCast_zsmul, multiRefPackage.htorsion, smul_zero, add_zero and 2 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma mutual_information_le_t_23 line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, multiTauMinimizes, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, LE.le, Real, ProbabilityTheory.condMutualInfo, Finset.sum, Finset.univ, HSMul.hSMul, Int and 8 more
Proof uses: GE.ge, multiRefPackage.hm, NeZero, Eq.mpr, Ne, id, Eq, congrArg, propext, neZero_iff, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 130 more
197 instances, coercions and auxiliary constants left out.

Tactic trace: 88 steps
Open to load the checked before-and-after goal states.
lemma mutual_information_le_t_13 line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, multiTauMinimizes, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, LE.le, Real, ProbabilityTheory.condMutualInfo, Finset.sum, Finset.univ, HSMul.hSMul, Int and 8 more
Proof uses: GE.ge, multiRefPackage.hm, NeZero, Eq.mpr, Ne, id, Eq, congrArg, propext, neZero_iff, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 129 more
197 instances, coercions and auxiliary constants left out.

Tactic trace: 83 steps
Open to load the checked before-and-after goal states.
lemma Q_ident line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, Finset.sum, Finset.univ
Proof uses: Eq.mpr, Function.comp, eq_of_heq, MeasurableSpace, Eq, autoParam, MeasureTheory.Measure, HEq, Eq.refl, HEq.refl, Eq.symm, funext, of_eq_true, Eq.trans, True, congr, congrArg, Finset.sum_apply, Finset.sum_congr, Finset and 19 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Q_mes line 255 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Prod, Fin, multiRefPackage.m, Measurable, Prod.mk, Neg.neg, Finset.sum, Finset.univ
Proof uses: Measurable.neg, Finset.measurable_sum'', Membership.mem, Finset, Measurable.fun_comp, Prod.snd, Measurable.snd, measurable_id'
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Q_dist line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, LE.le, Real, rdist, Finset.sum, Finset.univ, Neg.neg, HMul.hMul, OfNat.ofNat and 2 more
Proof uses: Q_ident, Q_mes, Trans.trans, Eq, ProbabilityTheory.IdentDistrib.rdist_congr_left, AEMeasurable.neg, Finset.aemeasurable_sum, Membership.mem, Finset, Measurable.aemeasurable, Eq.mpr, inferInstance, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HMul and 6 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Q_ent line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, Eq, Real, ProbabilityTheory.entropy, Finset.sum, Finset.univ, HAdd.hAdd, multiDist, HMul.hMul and 1 more
Proof uses: Eq.mpr, id, congrArg, Q_eq, HDiv.hDiv, inv_mul_eq_div, HSub.hSub, multiDist_indep, indep_yj, multiDist_copy, ProbabilityTheory.IdentDistrib.entropy_congr, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Tactic.Ring.of_eq and 71 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Q_indep line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Prod, Fin, multiRefPackage.m, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, MeasureTheory.MeasureSpace.volume, Ne, ProbabilityTheory.IndepFun, Finset.sum, Finset.univ, Neg.neg
Proof uses: Finset, Finset.filter, Eq, Prod.snd, Subtype, Membership.mem, Subtype.mk, of_eq_true, Eq.trans, And, True, congr, congrArg, eq_self, and_self, Eq.mpr, eq_of_heq, MeasurableSpace, autoParam, MeasureTheory.Measure and 27 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma entropy_of_W_le We have $\bbH[W] \leq (2m-1)k + \frac1m \sum_{i=1}^m \bbH[X_i]$ line 297 source
Source documentation
We have $\bbH[W] \leq (2m-1)k + \frac1m \sum_{i=1}^m \bbH[X_i]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, LE.le, Real, ProbabilityTheory.entropy, Finset.sum, Finset.univ, HAdd.hAdd, HMul.hMul, HSub.hSub and 4 more
Proof uses: GE.ge, multiRefPackage.hm, NeZero, NeZero.mk, Trans.trans, Eq, Finset.Ioi, Eq.mpr, id, congrArg, Finset.sum_comm, Eq.refl, of_eq_true, Eq.trans, True, congr, congrFun', MeasureTheory.Measure, autoParam, Finset.sum_congr and 146 more
201 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_of_W_le : H[W] ≤ (2*p.m - 1) * k + (p.m:ℝ)⁻¹ * ∑ i, H[X i] := by
…
```
lemma Z2_eq line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Prod, Fin, multiRefPackage.m, Eq, Finset.sum, Finset.univ, HSMul.hSMul, Int, Prod.mk, Finset.erase, Fin.mk, OfNat.ofNat, Nat
Proof uses: Trans.trans, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 55 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma entropy_of_Z_two_le We have $\bbH[Z_2] \leq (8m^2-16m+1) k + \frac{1}{m} \sum_{i=1}^m \bbH[X_i]$ line 339 source
Source documentation
We have $\bbH[Z_2] \leq (8m^2-16m+1) k + \frac{1}{m} \sum_{i=1}^m \bbH[X_i]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, LE.le, Real, ProbabilityTheory.entropy, Finset.sum, Finset.univ, HSMul.hSMul, Int, HAdd.hAdd and 7 more
Proof uses: GE.ge, multiRefPackage.hm, Fin.mk, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 172 more
271 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_of_Z_two_le : H[Z2] ≤ (8 * p.m^2 - 16 * p.m + 1) * k + (p.m:ℝ)⁻¹ * ∑ i, H[X i] := by
…
```
lemma mutual_of_W_Z_two_le We have $\bbI[W : Z_2] \leq 2(m-1) k$ line 390 source
Source documentation
We have $\bbI[W : Z_2] \leq 2(m-1) k$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, Prod, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, LE.le, Real, ProbabilityTheory.mutualInfo, Finset.sum, Finset.univ, HSMul.hSMul, Int, HMul.hMul and 4 more
Proof uses: Eq.mpr, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy, id, Eq, congrArg, ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy, Finset.measurable_sum'', Membership.mem, Finset, Prod.snd, Measurable.fun_comp, Measurable.snd, measurable_id', Measurable.smul, measurable_const, NatCast.natCast, GE.ge, multiRefPackage.hm, Fin.mk and 151 more
221 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
```
lemma mutual_of_W_Z_two_le : I[W : Z2] ≤ 2 * (p.m-1) * k := by
…
```
lemma sum_of_conditional_distance_le We have $\sum_{i=1}^m d[X_i;Z_2|W] \leq 4(m^3-m^2) k$ line 432 source
Source documentation
We have $\sum_{i=1}^m d[X_i;Z_2|W] \leq 4(m^3-m^2) k$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, LE.le, Real, Finset.sum, Finset.univ, condRuzsaDist', HSMul.hSMul, Int, HMul.hMul and 5 more
Proof uses: GE.ge, multiRefPackage.hm, Fin.mk, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 252 more
301 instances, coercions and auxiliary constants left out.

Tactic trace: 90 steps
Open to load the checked before-and-after goal states.
```
lemma sum_of_conditional_distance_le : ∑ i, d[ X i # Z2 | W] ≤ 4 * (p.m^3 - p.m^2)*k := by
…
```
lemma pigeonhole line 502 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Finite, MeasurableSingletonClass, Real, Exists, And, LE.le, MeasureTheory.integral, Ne, ENNReal, MeasureTheory.Measure, Set, Singleton.singleton, OfNat.ofNat
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Eq.mpr, id, congrArg, rfl, Decidable.byContradiction, Not, GT.gt, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Finset.sum_lt_sum, Membership.mem, Finset, dite and 47 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma dist_of_U_add_le Documented declaration: dist_of_U_add_le line 535 source
Source documentation
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].$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Eq, HAdd.hAdd, OfNat.ofNat, Measurable, Nat, Fin, Real, GT.gt, Exists, And, LE.le, rdist, HMul.hMul, Finset.sum, Finset.univ, HDiv.hDiv and 1 more
Proof uses: MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, HSub.hSub, ProbabilityTheory.entropy, ent_bsg, Prod, prod, ProbabilityTheory.mutualInfo_def, Eq.mpr, Neg.neg, id, congrArg, Eq.symm, ProbabilityTheory.entropy_neg, Measurable.add, MeasurableSpace and 169 more
245 instances, coercions and auxiliary constants left out.

Tactic trace: 113 steps
Open to load the checked before-and-after goal states.
```
lemma dist_of_U_add_le {G : Type*} [MeasurableFinGroup G] {Ω : Type u} [hΩ : MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)] {T₁ T₂ T₃ : Ω → G} (hsum : T₁ + T₂ + T₃ = 0)
    (hmes₁ : Measurable T₁) (hmes₂ : Measurable T₂) (hmes₃ : Measurable T₃) {n : ℕ}
    {Ω' : Fin n → Type*} (hΩ' : ∀ i, MeasureSpace (Ω' i)) [∀ i, IsProbabilityMeasure (hΩ' i).volume]
    {Y : ∀ i, (Ω' i) → G} (hY : ∀ i, Measurable (Y i)) {α : ℝ} (hα : α > 0) :
    ∃ (Ω'' : Type u) (hΩ'': MeasureSpace Ω'') (U: Ω'' → G),
      IsProbabilityMeasure hΩ''.volume ∧ Measurable U ∧
        d[U # U] + α * ∑ i, d[Y i # U] ≤
          (2 + α * n / 2) * (I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]) + α * ∑ i, d[Y i # T₂] := by
…
```
Mentions: MeasurableFinGroup
lemma k_eq_zero We have $k = 0$ line 631 source
Source documentation
We have $k = 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, multiTauMinimizes, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Prod, Prod.mk, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, Eq, Real, multiRefPackage.η, HDiv.hDiv, OfNat.ofNat, HMul.hMul, Nat and 2 more
Proof uses: GE.ge, multiRefPackage.hm, LT.lt, multiRefPackage.hη, Fin.mk, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat and 237 more
283 instances, coercions and auxiliary constants left out.

Tactic trace: 102 steps
Open to load the checked before-and-after goal states.
```
lemma k_eq_zero (hη_eq : p.η = 1 / (32 * p.m ^ 3)) : k = 0 := by
…
```
lemma dist_of_X_U_H_le Suppose that $G$ is a finite abelian group of torsion $m$ line 721 source
Source documentation
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]. \]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Nat, GE.ge, OfNat.ofNat, Eq, HSMul.hSMul, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Exists, AddSubgroup, And, ProbabilityTheory.IsUniform, LE.le, Real, rdist and 2 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, MeasurableFinGroup, MeasurableFinGroup.mk, multiRefPackage, multiRefPackage.mk, inferInstance, HDiv.hDiv, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, mul_pos, Mathlib.Meta.NormNum.instAtLeastTwo, pow_pos and 192 more
231 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
```
lemma 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}
    [MeasureSpace Ω] [IsProbabilityMeasure (ℙ:Measure Ω)] {X: Ω → G} (hX: Measurable X) :
    ∃ H : AddSubgroup G, ∃ Ω' : Type u, ∃ mΩ : MeasureSpace Ω', IsProbabilityMeasure mΩ.volume ∧
      ∃ U : Ω' → G, IsUniform H U ∧ Measurable U ∧ d[X # U] ≤ 64 * m^3 * d[X # X] := by
…
```
theorem rdist_le_of_isUniform_of_card_add_le' A uniform distribution on a set with doubling constant K has self Rusza distance at most log K line 777 source
Source documentation
A uniform distribution on a set with doubling constant K has self Rusza distance at most log K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, Real, Countable, Finite, MeasurableSpace, MeasurableSingletonClass, Set.Nonempty, LE.le, Set.ncard, HAdd.hAdd, HMul.hMul, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IsUniform, Measurable, rdist, Neg.neg, Real.log
Proof uses: LT.lt, OfNat.ofNat, And, PFR_conjecture_pos_aux', Exists, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies_two, ProbabilityTheory.IsUniform.of_identDistrib, ProbabilityTheory.IdentDistrib.symm, MeasurableSet.of_discrete, ProbabilityTheory.entropy, HSub.hSub, Eq.mpr, id, Eq, congrFun', congrArg, MeasureTheory.Measure, autoParam and 127 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
theorem rdist_le_of_isUniform_of_card_add_le' {G : Type*} [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*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}
    (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # -U₀] ≤ log K := by
…
```
lemma torsion_PFR_conjecture_aux Suppose that $G$ is a finite abelian group of torsion $m$ line 816 source
Source documentation
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^{128 m^3+1} |A|^{1/2}/|H|^{1/2}$ translates of a subspace $H$ of $G$ with $|H|/|A| \in [K^{-256 m^3}, K^{256 m^3}]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, Nat, GE.ge, OfNat.ofNat, Eq, HSMul.hSMul, Set, Real, Set.Nonempty, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Set.ncard, Exists, AddSubgroup, And, HPow.hPow, HDiv.hDiv and 1 more
Proof uses: MeasurableSpace, Top.top, MeasurableSingletonClass, MeasurableSingletonClass.mk, trivial, LT.lt, PFR_conjecture_pos_aux', Finset, Set.Finite.toFinset, Set.toFinite, Finset.Nonempty, Eq.mpr, Membership.mem, id, congrArg, funext, Set.Finite.coe_toFinset, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume and 235 more
279 instances, coercions and auxiliary constants left out.

Tactic trace: 98 steps
Open to load the checked before-and-after goal states.
```
lemma torsion_PFR_conjecture_aux {G : Type*} [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 : Set G).ncard ^ (-1/2 : ℝ)
      ∧ (H : Set G).ncard ≤ K ^ (256 * m^3) * A.ncard
      ∧ A.ncard ≤ K ^ (256 * m^3) * (H : Set G).ncard ∧ A ⊆ c + H := by
…
```
lemma torsion_exists_subgroup_subset_card_le 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| line 930 source
Source documentation
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|.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, AddCommGroup, Finite, Eq, HSMul.hSMul, AddSubgroup, LE.le, Set.ncard, Ne, Exists, And, LT.lt, HMul.hMul
Proof uses: Set, Set.ofPred, Set.Nonempty, Exists.intro, Membership.mem, Bot.bot, Eq.mpr, id, Eq.trans, True, congr, congrArg, congrFun', Set.ncard_singleton, true_and, Decidable.byContradiction, Not, MaximalFor, Set.Finite.exists_maximalFor, Set.toFinite and 46 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma torsion_exists_subgroup_subset_card_le {G : Type*} {m : ℕ} (hm : m ≥ 2)
    [AddCommGroup G] [Finite G] (htorsion : ∀ x:G, m • x = 0)
    {k : ℕ} (H : AddSubgroup G) (hk : k ≤ (H : Set G).ncard) (h'k : k ≠ 0) :
    ∃ (K : AddSubgroup G), (K : Set G).ncard ≤ k ∧ k < m * (K : Set G).ncard ∧ K ≤ H := by
…
```
theorem torsion_PFR Suppose that $G$ is an abelian group of torsion $m$ (not necessarily finite) line 974 source
Source documentation
Suppose that $G$ is an abelian group of torsion $m$ (not necessarily finite). If $A \subset G$ is a finite non-empty set with $|A+A| \leq K|A|$, then $A$ can be covered by at most $m K^{256 m^3+1}$ translates of a finite subspace $H$ of $G$ with $|H| \leq |A|$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Nat, GE.ge, OfNat.ofNat, Eq, HSMul.hSMul, Set, Set.Finite, Real, Set.Nonempty, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Set.ncard, Exists, AddSubgroup, And, LT.lt, HPow.hPow
Proof uses: Classical.byCases, Finite, Set.Finite.to_subtype, PFR_conjecture_pos_aux', HDiv.hDiv, Neg.neg, torsion_PFR_conjecture_aux, Nat.card_pos, Membership.mem, Iff.mpr, Nat.cast_pos', Or, le_or_gt, Exists.intro, And.intro, Set.toFinite, Trans.trans, mul_le_mul_of_nonneg_right, mul_le_mul_of_nonneg_left, Real.rpow_le_rpow and 238 more
269 instances, coercions and auxiliary constants left out.

Tactic trace: 99 steps
Open to load the checked before-and-after goal states.
```
theorem torsion_PFR {G : Type*} [AddCommGroup G] {m : ℕ} (hm : m ≥ 2)
    (htorsion : ∀ x : G, m • x = 0) {A : Set G} (Afin : A.Finite) {K : ℝ} (h₀A : A.Nonempty)
    (hA : Nat.card (A + A) ≤ K * A.ncard) :
    ∃ (H : AddSubgroup G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
      Nat.card c < m * K ^ (256 * m ^ 3 + 1) ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by
…
```