`PFR/Endgame.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

20 declarations, 0 contain sorry, 0 declared as axioms

Endgame

The endgame on tau-minimizers.

Assumptions:

$X_1, X_2$ are tau-minimizers
$X_1, X_2, \tilde X_1, \tilde X_2$ be independent random variables, with $X_1,\tilde X_1$ copies of $X_1$ and $X_2,\tilde X_2$ copies of $X_2$.
$d[X_1;X_2] = k$
$U := X_1 + X_2$
$V := \tilde X_1 + X_2$
$W := X_1 + \tilde X_1$
$S := X_1 + X_2 + \tilde X_1 + \tilde X_2$.
$I_1 := I[U : V | S]$
$I_2 := I[U : W | S]$
$I_3 := I[V : W | S]$ (not explicitly defined in Lean)

Main results:

sum_condMutual_le : An upper bound on the total conditional mutual information $I_1+I_2+I_3$.
sum_dist_diff_le: A sum of the "costs" of $U$, $V$, $W$.
construct_good: A construction of two random variables with small Ruzsa distance between them given some random variables with control on total cost, as well as total mutual information.

Imports (2)

Imported by 2 files

lemma hmeas2 (Mantas) this times out in the proof below line 80 source

Source comment

(Mantas) this times out in the proof below

private lemma hmeas2 {G : Type*} [AddCommGroup G] [Finite G] [hG : MeasurableSpace G]
    [MeasurableSingletonClass G] :
    Measurable fun p : Fin 4 → G => ((p 0 + p 1, p 0 + p 2), p 0 + p 1 + p 2 + p 3) := by
…

lemma I₃_eq The quantity I_3 = I[V:W|S] is equal to I_2 line 87 source
Source documentation
The quantity I_3 = I[V:W|S] is equal to I_2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.IsProbabilityMeasure, Eq, Real, ProbabilityTheory.condMutualInfo, HAdd.hAdd
Proof uses: ProbabilityTheory.iIndepFun.reindex_four_cbad, ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Eq.mpr, id, congrArg, propext, measurable_pi_iff, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt and 54 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma I₃_eq [IsProbabilityMeasure (ℙ : Measure Ω)] : I[V : W | S] = I₂ := by
…
```
lemma sum_condMutual_le I[U : V | S] + I[V : W | S] + I[W : U | S] is less than or equal to 6 * η * k - (1 - 5 * η) / (1 - η) * (2 * η * k - I₁) line 136 source
Source documentation
I[U : V | S] + I[V : W | S] + I[W : U | S] is less than or equal to 6 * η * k - (1 - 5 * η) / (1 - η) * (2 * η * k - I₁).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, Measurable, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, TauMinimizes, Module, ZMod and 9 more
Proof uses: Eq, ProbabilityTheory.condMutualInfo_comm, Measurable.add, Prod, Eq.mpr, id, congrArg, I₃_eq, second_estimate, LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring and 100 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma sum_condMutual_le [Module (ZMod 2) G] [IsProbabilityMeasure (ℙ : Measure Ω)] :
    I[U : V | S] + I[V : W | S] + I[W : U | S]
      ≤ 6 * p.η * k - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * k - I₁) := by
…
```
lemma hU line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.IsProbabilityMeasure, Eq, Real, ProbabilityTheory.entropy, HAdd.hAdd
Proof uses: ProbabilityTheory.IdentDistrib.entropy_congr, ProbabilityTheory.IdentDistrib.add, Prod, ProbabilityTheory.iIndepFun.indepFun, Ne, id, of_decide_eq_true, Not, Bool, Decidable.decide, Bool.true, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma independenceCondition1 line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume, HAdd.hAdd
Proof uses: ProbabilityTheory.iIndepFun.apply_two_last, Add, MeasurableAdd₂.measurable_add, Prod
20 instances, coercions and auxiliary constants left out.
lemma hV line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.IsProbabilityMeasure, Eq, Real, ProbabilityTheory.entropy, HAdd.hAdd
Proof uses: ProbabilityTheory.IdentDistrib.entropy_congr, ProbabilityTheory.IdentDistrib.add, Prod, ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.iIndepFun.indepFun, Ne, id, of_decide_eq_true, Not, Bool, Decidable.decide, Bool.true, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma independenceCondition2 line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume, HAdd.hAdd
Proof uses: independenceCondition1, ProbabilityTheory.iIndepFun.reindex_four_bacd
10 instances, coercions and auxiliary constants left out.
lemma independenceCondition3 line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume, HAdd.hAdd
Proof uses: independenceCondition1, ProbabilityTheory.iIndepFun.reindex_four_cbad
10 instances, coercions and auxiliary constants left out.
lemma independenceCondition4 line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume, HAdd.hAdd
Proof uses: independenceCondition1, ProbabilityTheory.iIndepFun.reindex_four_bcad
10 instances, coercions and auxiliary constants left out.
lemma independenceCondition5 line 194 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume, HAdd.hAdd
Proof uses: independenceCondition1, ProbabilityTheory.iIndepFun.reindex_four_acbd
10 instances, coercions and auxiliary constants left out.
lemma independenceCondition6 line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume, HAdd.hAdd
Proof uses: independenceCondition1, ProbabilityTheory.iIndepFun.reindex_four_bdca
10 instances, coercions and auxiliary constants left out.
lemma sum_dist_diff_le $$ \sum_{i=1}^2 \sum_{A\in\{U,V,W\}} \big(d[X^0_i;A|S] - d[X^0_i;X_i]\big)$$ is less than or equal to $$ \leq (6 - 3\eta) k + 3(2 \eta k - I_1).$$ line 210 source
Source documentation
$$ \sum_{i=1}^2 \sum_{A\in\{U,V,W\}} \big(d[X^0_i;A|S] - d[X^0_i;X_i]\big)$$ is less than or equal to $$ \leq (6 - 3\eta) k + 3(2 \eta k - I_1).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, Measurable, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, TauMinimizes, Module, ZMod and 11 more
Proof uses: HDiv.hDiv, ProbabilityTheory.entropy, Eq, Eq.mpr, id, congrArg, hU, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 150 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
```
lemma sum_dist_diff_le [IsProbabilityMeasure (ℙ : Measure Ω)] [Module (ZMod 2) G] :
    c[U|S # U|S] + c[V|S # V|S] + c[W|S # W|S] ≤ (6 - 3 * p.η)*k + 3 * (2*p.η*k - I₁) := by
…
```
lemma sum_uvw_eq_zero U + V + W = 0 line 312 source
Source documentation
U + V + W = 0.

standard axioms: Quot.sound, propext what this means
Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, congr, Eq.symm, ZModModule.sub_eq_add, add_assoc, add_sub_cancel, sub_sub_cancel, ZModModule.add_self, eq_self
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma sum_uvw_eq_zero [Module (ZMod 2) G] : U + V + W = 0 := by
…
```
lemma cond_c_eq_integral line 319 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, refPackage, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Eq, Real, HAdd.hAdd, HSub.hSub, condRuzsaDist', refPackage.X₀₁, rdist, refPackage.X₀₂, MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.cond and 3 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.sum, Finset.univ, HSMul.hSMul, MeasureTheory.Measure.real, id, congrArg, Eq.trans, NormedAddCommGroup, NormedSpace, CompleteSpace, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, MeasureTheory.integral_fintype, MeasureTheory.Integrable.of_finite, Finset.sum_congr and 19 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma construct_good_prelim Documented declaration: construct_good_prelim line 351 source
Source documentation
If $T_1, T_2, T_3$ are $G$-valued random variables with $T_1+T_2+T_3=0$ holds identically and $$ \delta := \sum_{1 \leq i < j \leq 3} I[T_i;T_j]$$ Then there exist random variables $T'_1, T'_2$ such that $$ d[T'_1;T'_2] + \eta (d[X_1^0;T'_1] - d[X_1^0;X_1]) + \eta(d[X_2^0;T'_2] - d[X_2^0;X_2]) $$ is at most $$ \delta + \eta ( d[X^0_1;T_1]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2]-d[X^0_2;X_2]) $$ $$ + \tfrac12 \eta I[T_1: T_3] + \tfrac12 \eta I[T_2: T_3].$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, TauMinimizes, Eq, HAdd.hAdd, OfNat.ofNat, Measurable, Module, ZMod, Nat, LE.le, Real, rdist, ProbabilityTheory.mutualInfo and 6 more
Proof uses: MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, 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.sub_congr and 148 more
201 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
lemma construct_good_prelim :
    k ≤ δ + p.η * c[T₁ # T₂] + p.η * (I[T₁: T₃] + I[T₂ : T₃])/2 := by
…
```
lemma construct_good Documented declaration: construct_good line 414 source
Source documentation
If $T_1, T_2, T_3$ are $G$-valued random variables with $T_1+T_2+T_3=0$ holds identically and
$$ \delta := \sum_{1 \leq i < j \leq 3} I[T_i;T_j]$$
Then there exist random variables $T'_1, T'_2$ such that
$$ d[T'_1;T'_2] + \eta (d[X_1^0;T'_1] - d[X_1^0;X _1]) + \eta(d[X_2^0;T'_2] - d[X_2^0;X_2])$$
is at most
$$\delta + \frac{\eta}{3} \biggl( \delta + \sum_{i=1}^2 \sum_{j = 1}^3 (d[X^0_i;T_j] - d[X^0_i; X_i]) \biggr).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, TauMinimizes, Eq, HAdd.hAdd, OfNat.ofNat, Measurable, Module, ZMod, Nat, LE.le, Real, rdist, ProbabilityTheory.mutualInfo and 6 more
Proof uses: construct_good_prelim, Eq.mpr, id, congrArg, Eq.symm, ProbabilityTheory.entropy, Prod, prod, congr, MeasureTheory.Measure, ProbabilityTheory.entropy_comm, congrFun', le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq and 72 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma construct_good :
    k ≤ δ + (p.η/3) * (δ + c[T₁ # T₁] + c[T₂ # T₂] + c[T₃ # T₃]) := by
…
```
lemma construct_good' line 425 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, TauMinimizes, Eq, HAdd.hAdd, OfNat.ofNat, Measurable, Module, ZMod, Nat, MeasureTheory.Measure, LE.le, Real, rdist and 7 more
Proof uses: MeasureTheory.MeasureSpace.mk, construct_good
49 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma delta'_eq_integral line 434 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Eq, Real, HAdd.hAdd, ProbabilityTheory.condMutualInfo, MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.mutualInfo, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, id, Eq.mpr, Finset.sum, Finset.univ, HSMul.hSMul, MeasureTheory.Measure.real, congr, congrArg, NormedAddCommGroup, NormedSpace, CompleteSpace, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, MeasureTheory.integral_fintype, MeasureTheory.Integrable.of_finite, Finset.sum_congr and 10 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma cond_construct_good line 441 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, TauMinimizes, Eq, HAdd.hAdd, OfNat.ofNat, Measurable, Module, ZMod, Nat, LE.le, Real, rdist, ProbabilityTheory.condMutualInfo and 7 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.mutualInfo, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, id, congrArg, delta'_eq_integral, cond_c_eq_integral, Finset.sum, Finset.univ, HSMul.hSMul, MeasureTheory.Measure.real and 37 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
theorem tau_strictly_decreases_aux If d[X₁ ; X₂] > 0 then there are G-valued random variables X₁', X₂' such that Phrased in the contrapositive form for convenience of proof line 468 source
Source documentation
If d[X₁ ; X₂] > 0 then there are G-valued random variables X₁', X₂' such that Phrased in the contrapositive form for convenience of proof.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, Measurable, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, TauMinimizes, Module, ZMod and 5 more
Proof uses: LE.le, HAdd.hAdd, ProbabilityTheory.condMutualInfo, HMul.hMul, HSub.hSub, condRuzsaDist', refPackage.X₀₁, refPackage.X₀₂, cond_construct_good, sum_uvw_eq_zero, Measurable.add, Prod, sum_condMutual_le, sum_dist_diff_le, Equiv, Equiv.mk, List, List.Mem, List.finRange, HEq and 115 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
theorem tau_strictly_decreases_aux [IsProbabilityMeasure (ℙ : Measure Ω)] [Module (ZMod 2) G]
    (hpη : p.η = 1 / 9) : d[X₁ # X₂] = 0 := by
…
```

PFR/Endgame.lean

Endgame

Main results:

If $T_1, T_2, T_3$ are $G$-valued random variables with $T_1+T_2+T_3=0$ holds identically and

`PFR/Endgame.lean`