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

9 declarations, 0 contain sorry, 0 declared as axioms

First estimate

The first estimate on tau-minimizers.

Assumptions:

$X_1, X_2$ are tau-minimizers
$X_1, X_2, \tilde X_1, \tilde X_2$ are independent random variables, with $X_1,\tilde X_1$ copies of $X_1$ and $X_2,\tilde X_2$ copies of $X_2$.
$k := d[X_1;X_2]$
$I_1 := I [X_1+X_2 : \tilde X_1 + X_2 | X_1+X_2+\tilde X_1+\tilde X_2]$

Main results

first_estimate : $I_1 ≤ 2 η k$
ent_ofsum_le : $H[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} H[X_1]+\tfrac{1}{2} H[X_2] + (2 + \eta) k - I_1.$

Imports (2)

Imported by 3 files

lemma rdist_add_rdist_add_condMutual_eq Documented declaration: rdist_add_rdist_add_condMutual_eq line 59 source
Source documentation
The sum of $$ d[X_1+\tilde X_2;X_2+\tilde X_1] + d[X_1|X_1+\tilde X_2; X_2|X_2+\tilde X_1] $$ and $$ I[X_1+ X_2 : \tilde X_1 + X_2 \,|\, X_1 + X_2 + \tilde X_1 + \tilde X_2] $$ is equal to $2k$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Module, ZMod, Eq, Real and 5 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, rfl, sum_of_rdist_eq_char_2, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil and 40 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_add_rdist_add_condMutual_eq [Module (ZMod 2) G] :
    d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁']
      + I[X₁ + X₂ : X₁' + X₂ | X₁ + X₂ + X₁' + X₂'] = 2 * k := by
…
```
lemma rdist_of_sums_ge The distance $d[X_1+\tilde X_2; X_2+\tilde X_1]$ is at least $$k - \eta (d[X^0_1; X_1+\tilde X_2] - d[X^0_1; X_1]) - \eta (d[X^0_2; X_2+\tilde X_1] - d[X^0_2; X_2]).$$ line 82 source
Source documentation
The distance $d[X_1+\tilde X_2; X_2+\tilde X_1]$ is at least $$k - \eta (d[X^0_1; X_1+\tilde X_2] - d[X^0_1; X_1]) - \eta (d[X^0_2; X_2+\tilde X_1] - d[X^0_2; X_2]).$$

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, TauMinimizes, GE.ge, Real, rdist, HAdd.hAdd, HSub.hSub, HMul.hMul, refPackage.η, refPackage.X₀₁, refPackage.X₀₂
Proof uses: distance_ge_of_min, Measurable.add, Prod
25 instances, coercions and auxiliary constants left out.
```
lemma rdist_of_sums_ge :
    d[X₁ + X₂' # X₂ + X₁'] ≥
      k - p.η * (d[p.X₀₁ # X₁ + X₂'] - d[p.X₀₁ # X₁])
        - p.η * (d[p.X₀₂ # X₂ + X₁'] - d[p.X₀₂ # X₂]) :=
…
```
lemma condRuzsaDist_of_sums_ge Documented declaration: condRuzsaDist_of_sums_ge line 93 source
Source documentation
The distance $d[X_1|X_1+\tilde X_2; X_2|X_2+\tilde X_1]$ is at least $$ k - \eta (d[X^0_1; X_1 | X_1 + \tilde X_2] - d[X^0_1; X_1]) - \eta(d[X^0_2; X_2 | X_2 + \tilde X_1] - d[X^0_2; X_2]).$$

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, TauMinimizes, GE.ge, Real, condRuzsaDist, HAdd.hAdd, HSub.hSub, rdist, HMul.hMul, refPackage.η, condRuzsaDist', refPackage.X₀₁ and 1 more
Proof uses: condRuzsaDistance_ge_of_min, Measurable.add, Prod
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist_of_sums_ge :
    d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] ≥
      k - p.η * (d[p.X₀₁ # X₁ | X₁ + X₂'] - d[p.X₀₁ # X₁])
        - p.η * (d[p.X₀₂ # X₂ | X₂ + X₁'] - d[p.X₀₂ # X₂]) :=
…
```
lemma diff_rdist_le_1 d[X₀₁ # X₁ + X₂'] - d[X₀₁ # X₁] ≤ k/2 + H[X₂]/4 - H[X₁]/4 line 103 source
Source documentation
d[X₀₁ # X₁ + X₂'] - d[X₀₁ # X₁] ≤ k/2 + H[X₂]/4 - H[X₁]/4.

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, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Module, ZMod, LE.le and 7 more
Proof uses: ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun, Ne, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, eq_of_heq, LE, HEq, HEq.refl, Eq.symm, outParam, HSub, HAdd, HDiv and 5 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma diff_rdist_le_1 [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] :
    d[p.X₀₁ # X₁ + X₂'] - d[p.X₀₁ # X₁] ≤ k/2 + H[X₂]/4 - H[X₁]/4 := by
…
```
lemma diff_rdist_le_2 $$ d[X^0_2;X_2+\tilde X_1] - d[X^0_2; X_2] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$ line 113 source
Source documentation
$$ d[X^0_2;X_2+\tilde X_1] - d[X^0_2; X_2] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$

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, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Module, ZMod, LE.le and 7 more
Proof uses: ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun, Ne, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, eq_of_heq, LE, HEq, HEq.refl, Eq.symm, outParam, HSub, HAdd, HDiv and 7 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma diff_rdist_le_2 [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
    d[p.X₀₂ # X₂ + X₁'] - d[p.X₀₂ # X₂] ≤ k/2 + H[X₁]/4 - H[X₂]/4 := by
…
```
lemma diff_rdist_le_3 $$ d[X_1^0;X_1|X_1+\tilde X_2] - d[X_1^0;X_1] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$ line 124 source
Source documentation
$$ d[X_1^0;X_1|X_1+\tilde X_2] - d[X_1^0;X_1] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$

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, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Module, ZMod, LE.le and 8 more
Proof uses: ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun, Ne, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, eq_of_heq, LE, HEq, HEq.refl, Eq.symm, outParam, HSub, HAdd, congrArg and 6 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma diff_rdist_le_3 [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] :
    d[p.X₀₁ # X₁ | X₁ + X₂'] - d[p.X₀₁ # X₁] ≤ k/2 + H[X₁]/4 - H[X₂]/4 := by
…
```
lemma diff_rdist_le_4 $$ d[X_2^0; X_2|X_2+\tilde X_1] - d[X_2^0; X_2] \leq \tfrac{1}{2}k + \tfrac{1}{4} \mathbb{H}[X_2] - \tfrac{1}{4} \mathbb{H}[X_1].$$ line 134 source
Source documentation
$$ d[X_2^0; X_2|X_2+\tilde X_1] - d[X_2^0; X_2] \leq \tfrac{1}{2}k + \tfrac{1}{4} \mathbb{H}[X_2] - \tfrac{1}{4} \mathbb{H}[X_1].$$

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, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Module, ZMod, LE.le and 8 more
Proof uses: ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun, Ne, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, eq_of_heq, LE, HEq, HEq.refl, Eq.symm, outParam, HSub, HAdd, congrArg and 7 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma diff_rdist_le_4 [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
    d[p.X₀₂ # X₂ | X₂ + X₁'] - d[p.X₀₂ # X₂] ≤ k/2 + H[X₂]/4 - H[X₁]/4 := by
…
```
lemma first_estimate We have $I_1 \leq 2 \eta k$ line 143 source
Source documentation
We have $I_1 \leq 2 \eta k$

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, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, TauMinimizes, Module, ZMod and 7 more
Proof uses: Eq, condRuzsaDist, rdist_add_rdist_add_condMutual_eq, GE.ge, HSub.hSub, refPackage.X₀₁, refPackage.X₀₂, rdist_of_sums_ge, condRuzsaDist', condRuzsaDist_of_sums_ge, HDiv.hDiv, ProbabilityTheory.entropy, mul_le_mul_of_nonneg_left, diff_rdist_le_1, LT.lt.le, refPackage.hη, diff_rdist_le_2, diff_rdist_le_3, diff_rdist_le_4, le_of_not_gt and 86 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma first_estimate
    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
    I₁ ≤ 2 * p.η * k := by
…
```
lemma ent_ofsum_le $$\mathbb{H}[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} \mathbb{H}[X_1]+\tfrac{1}{2} \mathbb{H}[X_2] + (2 + \eta) k - I_1.$$ line 158 source
Source documentation
$$\mathbb{H}[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} \mathbb{H}[X_1]+\tfrac{1}{2} \mathbb{H}[X_2] + (2 + \eta) k - I_1.$$

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, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, TauMinimizes, Module, ZMod and 10 more
Proof uses: condRuzsaDist, refPackage.X₀₁, condRuzsaDist', refPackage.X₀₂, Eq, rdist_add_rdist_add_condMutual_eq, GE.ge, condRuzsaDist_of_sums_ge, diff_rdist_le_3, diff_rdist_le_4, Trans.trans, 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 and 145 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
```
lemma ent_ofsum_le
    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
    H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁]/2 + H[X₂]/2 + (2+p.η)*k - I₁ := by
…
```