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

12 declarations, 0 contain sorry, 0 declared as axioms

The tau functional

Definition of the tau functional and basic facts

Main definitions:

η: $1/9$
τ: The tau functional $\tau[X_1; X_2] = d[X_1; X_2] + \eta d[X^0_1; X_1] + \eta d[X^0_2; X_2].$

Main results

tau_minimizer_exists: A pair of random variables minimizing $\tau$ exists.
condRuzsaDistance_ge_of_min: If $X_1,X_2$ is a tau-minimizer with $k = d[X_1;X_2]$, then $d[X'_1|Z, X'_2|W]$ is at least $$k - \eta (d[X^0_1;X'_1|Z] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2|W] - d[X^0_2;X_2] )$$ for any $X'_1, Z, X'_2, W$.

Imports (2)

Imported by 3 files

structure refPackage A structure that packages all the fixed information in the main argument line 41 source
Source documentation
A structure that packages all the fixed information in the main argument. In this way, when defining the τ functional, we will only only need to refer to the package once in the notation instead of stating the reference spaces, the reference measures and the reference random variables.
The η parameter has now been incorporated into the package, in preparation for being able to manipulate the package.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace
```
structure refPackage where
…
```
def tau Documented declaration: tau line 68 source
Source documentation
If $X_1,X_2$ are two $G$-valued random variables, then $$ \tau[X_1; X_2] := d[X_1; X_2] + \eta d[X^0_1; X_1] + \eta d[X^0_2; X_2].$$ Here, $X^0_1$ and $X^0_2$ are two random variables fixed once and for all in most of the argument. To lighten notation, We package X^0_1 and X^0_2 in a single object named p.
We denote it as τ[X₁ ; μ₁ # X₂ ; μ₂ | p] where p is a fixed package containing the information of the reference random variables. When the measurable spaces have a canonical measure ℙ, we can use τ[X₁ # X₂ | p]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, AddCommGroup, MeasurableSpace, refPackage, MeasureTheory.Measure, Real
Proof uses: HAdd.hAdd, rdist, HMul.hMul, refPackage.η, refPackage.X₀₁, MeasureTheory.MeasureSpace.volume, refPackage.X₀₂
5 instances, coercions and auxiliary constants left out.
```
noncomputable def tau {Ω₁ Ω₂ : Type*} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂]
    (X₁ : Ω₁ → G) (X₂ : Ω₂ → G) (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) : ℝ :=
…
```
lemma continuous_tau_restrict_probabilityMeasure line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, AddCommGroup, Finite, MeasurableSpace, refPackage, TopologicalSpace, DiscreteTopology, BorelSpace, Continuous, Prod, MeasureTheory.ProbabilityMeasure, Real, tau, id, Prod.fst, Prod.snd
Proof uses: rdist, refPackage.X₀₂, Continuous.comp, continuous_rdist_restrict_probabilityMeasure₁', refPackage.hmeas2, continuous_snd, continuous_rdist_restrict_probabilityMeasure, refPackage.X₀₁, refPackage.hmeas1, continuous_fst, Continuous.fun_add, HAdd.hAdd, HMul.hMul, refPackage.η, Continuous.comp', continuous_const_mul
30 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IdentDistrib.tau_eq If $X'_1, X'_2$ are copies of $X_1,X_2$, then $\tau[X'_1;X'_2] = \tau[X_1;X_2]$ line 97 source
Source documentation
If $X'_1, X'_2$ are copies of $X_1,X_2$, then $\tau[X'_1;X'_2] = \tau[X_1;X_2]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, AddCommGroup, MeasurableSpace, refPackage, MeasureTheory.Measure, ProbabilityTheory.IdentDistrib, Eq, Real, tau
Proof uses: id, Eq.mpr, HAdd.hAdd, rdist, HMul.hMul, refPackage.η, refPackage.X₀₁, MeasureTheory.MeasureSpace.volume, refPackage.X₀₂, congrArg, ProbabilityTheory.IdentDistrib.rdist_congr_right, Measurable.aemeasurable, refPackage.hmeas1, refPackage.hmeas2, ProbabilityTheory.IdentDistrib.rdist_congr, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma ProbabilityTheory.IdentDistrib.tau_eq [MeasurableSpace Ω₁] [MeasurableSpace Ω₂]
    [MeasurableSpace Ω'₁] [MeasurableSpace Ω'₂]
    {μ₁ : Measure Ω₁} {μ₂ : Measure Ω₂} {μ'₁ : Measure Ω'₁} {μ'₂ : Measure Ω'₂}
    {X₁ : Ω₁ → G} {X₂ : Ω₂ → G} {X₁' : Ω'₁ → G} {X₂' : Ω'₂ → G}
    (h₁ : IdentDistrib X₁ X₁' μ₁ μ'₁) (h₂ : IdentDistrib X₂ X₂' μ₂ μ'₂) :
    τ[X₁ ; μ₁ # X₂ ; μ₂ | p] = τ[X₁' ; μ'₁ # X₂' ; μ'₂ | p] := by
…
```
def TauMinimizes Property recording the fact that two random variables minimize the tau functional line 111 source
Source documentation
Property recording the fact that two random variables minimize the tau functional. Expressed in terms of measures on the group to avoid quantifying over all spaces, but this implies comparison with any pair of random variables, see Lemma is_tau_min.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, AddCommGroup, MeasurableSpace, refPackage
Proof uses: MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, LE.le, Real, tau, MeasureTheory.MeasureSpace.volume, id
2 instances, coercions and auxiliary constants left out.
```
def TauMinimizes {Ω : Type*} [MeasureSpace Ω] (X₁ : Ω → G) (X₂ : Ω → G) : Prop :=
…
```
lemma ProbabilityTheory.IdentDistrib.tauMinimizes If $X'_1, X'_2$ are copies of $X_1,X_2$, then $X_1, X_2$ minimize $\tau$ iff $X_1', X_2'$ do line 118 source
Source documentation
If $X'_1, X'_2$ are copies of $X_1,X_2$, then $X_1, X_2$ minimize $\tau$ iff $X_1', X_2'$ do.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, AddCommGroup, MeasurableSpace, refPackage, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, Iff, TauMinimizes
Proof uses: id, of_eq_true, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, LE.le, Real, tau, Eq.trans, True, congrFun', congrArg, forall_congr, implies_congr, Eq.refl, ProbabilityTheory.IdentDistrib.tau_eq, iff_self
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma ProbabilityTheory.IdentDistrib.tauMinimizes [MeasureSpace Ω]
    [MeasureSpace Ω']
    {X₁ X₂ : Ω → G} {X₁' X₂' : Ω' → G}
    (h₁ : IdentDistrib X₁ X₁') (h₂ : IdentDistrib X₂ X₂') :
    TauMinimizes p X₁ X₂ ↔ TauMinimizes p X₁' X₂' := by
…
```
Mentions: TauMinimizes
lemma tau_min_exists_measure A pair of measures minimizing $\tau$ exists line 126 source
Source documentation
A pair of measures minimizing $\tau$ exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, AddCommGroup, Finite, MeasurableSpace, refPackage, MeasurableSingletonClass, Exists, Prod, MeasureTheory.Measure, And, Prod.fst, Prod.snd, LE.le, Real, tau, id
Proof uses: TopologicalSpace, Bot.bot, DiscreteTopology, DiscreteTopology.mk, rfl, MeasureTheory.ProbabilityMeasure, Continuous, continuous_tau_restrict_probabilityMeasure, Inhabited, Inhabited.mk, OfNat.ofNat, Membership.mem, Set, Set.univ, IsMinOn, IsCompact.exists_isMinOn, isCompact_univ, Exists.intro, Inhabited.default, trivial and 9 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma tau_min_exists_measure [MeasurableSingletonClass G] :
    ∃ (μ : Measure G × Measure G),
    IsProbabilityMeasure μ.1 ∧ IsProbabilityMeasure μ.2 ∧
    ∀ (ν₁ : Measure G) [IsProbabilityMeasure ν₁] (ν₂ : Measure G) [IsProbabilityMeasure ν₂],
      τ[id ; μ.1 # id ; μ.2 | p] ≤ τ[id ; ν₁ # id ; ν₂ | p] := by
…
```
lemma tau_minimizer_exists A pair of random variables minimizing $τ$ exists line 147 source
Source documentation
A pair of random variables minimizing $τ$ exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, AddCommGroup, Finite, MeasurableSpace, refPackage, MeasurableSingletonClass, Exists, And, Measurable, TauMinimizes
Proof uses: Prod, MeasureTheory.Measure, Exists.choose, Prod.fst, Prod.snd, LE.le, Real, tau, id, tau_min_exists_measure, And.left, Exists.choose_spec, And.right, MeasureTheory.Measure.prod, inferInstance, MeasureTheory.MeasureSpace.mk, Exists.intro, And.intro, measurable_fst, measurable_snd and 11 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma tau_minimizer_exists [MeasurableSingletonClass G] :
    ∃ (Ω : Type uG) (_ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),
    Measurable X₁ ∧ Measurable X₂ ∧ IsProbabilityMeasure (ℙ : Measure Ω) ∧
    TauMinimizes p X₁ X₂ := by
…
```
Mentions: TauMinimizes
lemma is_tau_min line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, AddCommGroup, MeasurableSpace, refPackage, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, TauMinimizes, Measurable, LE.le, Real, tau
Proof uses: MeasureTheory.Measure, MeasureTheory.Measure.map, Eq, id, ProbabilityTheory.IdentDistrib.tau_eq, ProbabilityTheory.identDistrib_id_right, Measurable.aemeasurable, Eq.mpr, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma distance_ge_of_min Documented declaration: distance_ge_of_min line 184 source
Source documentation
Let X₁ and X₂ be tau-minimizers associated to p, with $d[X_1,X_2]=k$, then $$ d[X'_1;X'_2] \geq k - \eta (d[X^0_1;X'_1] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2] - d[X^0_2;X_2] )$$ for any $G$-valued random variables $X'_1,X'_2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, AddCommGroup, MeasurableSpace, refPackage, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, TauMinimizes, Measurable, LE.le, Real, HSub.hSub, rdist, HMul.hMul, refPackage.η, refPackage.X₀₁, refPackage.X₀₂
Proof uses: tau, is_tau_min, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr and 43 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma distance_ge_of_min (h : TauMinimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂') :
    d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁'] - d[p.X₀₁ # X₁]) - p.η * (d[p.X₀₂ # X₂'] - d[p.X₀₂ # X₂])
      ≤ d[X₁' # X₂'] := by
…
```
Mentions: TauMinimizes
lemma distance_ge_of_min' Version of distance_ge_of_min with the measures made explicit line 194 source
Source documentation
Version of distance_ge_of_min with the measures made explicit.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, AddCommGroup, MeasurableSpace, refPackage, TauMinimizes, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, LE.le, Real, HSub.hSub, rdist, MeasureTheory.MeasureSpace.volume, HMul.hMul, refPackage.η, refPackage.X₀₁, refPackage.X₀₂
Proof uses: MeasureTheory.MeasureSpace.mk, distance_ge_of_min
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma distance_ge_of_min' {Ω'₁ Ω'₂ : Type*} (h : TauMinimizes p X₁ X₂)
    [MeasurableSpace Ω'₁] [MeasurableSpace Ω'₂] {μ : Measure Ω'₁} {μ' : Measure Ω'₂}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] {X₁' : Ω'₁ → G} {X₂' : Ω'₂ → G}
    (h1 : Measurable X₁') (h2 : Measurable X₂') :
    d[X₁ # X₂] - p.η * (d[p.X₀₁; ℙ # X₁'; μ] - d[p.X₀₁ # X₁])
      - p.η * (d[p.X₀₂; ℙ # X₂'; μ'] - d[p.X₀₂ # X₂]) ≤ d[X₁'; μ # X₂'; μ'] := by
…
```
Mentions: TauMinimizes
lemma condRuzsaDistance_ge_of_min Documented declaration: condRuzsaDistance_ge_of_min line 210 source
Source documentation
For any $G$-valued random variables $X'_1,X'_2$ and random variables $Z,W$, one can lower bound $d[X'_1|Z;X'_2|W]$ by $$k - \eta (d[X^0_1;X'_1|Z] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2|W] - d[X^0_2;X_2] ).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, AddCommGroup, Finite, MeasurableSpace, refPackage, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, MeasurableSingletonClass, TauMinimizes, Measurable, LE.le, Real, HSub.hSub, rdist, HMul.hMul, refPackage.η, condRuzsaDist', refPackage.X₀₁, refPackage.X₀₂, condRuzsaDist
Proof uses: Eq, Finset.sum, FiniteRange.toFinset, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, Eq.mpr, id, congrArg, MeasureTheory.Measure.map, congrFun', Finset.sum_congr, Eq.refl, Finset, Membership.mem, MeasureTheory.Measure, Eq.symm, MeasureTheory.map_measureReal_apply, MeasurableSet.singleton and 73 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDistance_ge_of_min [MeasurableSingletonClass G]
    [Finite S] [MeasurableSpace S] [MeasurableSingletonClass S]
    [Finite T] [MeasurableSpace T] [MeasurableSingletonClass T]
    (h : TauMinimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂')
    (Z : Ω'₁ → S) (W : Ω'₂ → T) (hZ : Measurable Z) (hW : Measurable W) :
    d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁' | Z] - d[p.X₀₁ # X₁])
      - p.η * (d[p.X₀₂ # X₂' | W] - d[p.X₀₂ # X₂]) ≤ d[X₁' | Z # X₂' | W] := by
…
```
Mentions: TauMinimizes