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

14 declarations, 0 contain sorry, 0 declared as axioms

The tau functional for multidistance

Definition of the tau functional and basic facts

Main definitions:

Main results

Imports (3)

Imported by 3 files

class MeasurableFinGroup We will frequently be working with finite additive groups with the discrete sigma-algebra line 25 source

Source documentation

We will frequently be working with finite additive groups with the discrete sigma-algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means

class MeasurableFinGroup (G : Type*)
extends AddCommGroup G, Fintype G,
          MeasurableSpace G, MeasurableSingletonClass G

/-
May need an instance lemma here that [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] follows
automatically from [MeasurableFinGroup G]
-/

/-- A structure that packages all the fixed information in the main argument. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Problem.20when.20instances.20are.20inside.20a.20structure for more discussion of the design choices here. -/

structure multiRefPackage A structure that packages all the fixed information in the main argument line 35 source
Source documentation
A structure that packages all the fixed information in the main argument. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Problem.20when.20instances.20are.20inside.20a.20structure for more discussion of the design choices here.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace
```
structure multiRefPackage (G Ω₀ : Type u) [MeasurableFinGroup G] [MeasureSpace Ω₀] where
…
```
Mentions: MeasurableFinGroup
def multiTau If $(X_i)_{1 \leq i \leq m}$ is a tuple, we define its $\tau$-functional $$ \tau[ (X_i)_{1 \leq i \leq m}] := D[(X_i)_{1 \leq i \leq m}] + \eta \sum_{i=1}^m d[X_i; X^0].$$ line 52 source
Source documentation
If $(X_i)_{1 \leq i \leq m}$ is a tuple, we define its $\tau$-functional $$ \tau[ (X_i)_{1 \leq i \leq m}] := D[(X_i)_{1 \leq i \leq m}] + \eta \sum_{i=1}^m d[X_i; X^0].$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, Real
Proof uses: HAdd.hAdd, multiDist, HMul.hMul, multiRefPackage.η, Finset.sum, Finset.univ, rdist, multiRefPackage.X₀, MeasureTheory.MeasureSpace.volume
9 instances, coercions and auxiliary constants left out.
```
noncomputable def multiTau {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]
    (p : multiRefPackage G Ω₀) (Ω : Fin p.m → Type*) (hΩ : ∀ i, MeasureSpace (Ω i))
    (X : ∀ i, Ω i → G) : ℝ :=
…
```
Mentions: MeasurableFinGroup, multiRefPackage
lemma multiTau_of_ident line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, Eq, Real, multiTau
Proof uses: id, HAdd, Eq.rec, HAdd.hAdd, Eq.refl, multiDist, multiDist_copy, HMul.hMul, multiRefPackage.η, Finset.sum, Finset.univ, rdist, multiRefPackage.X₀, HMul, AddCommMonoid, Finset, funext, Measurable, multiRefPackage.hmeas, ProbabilityTheory.IdentDistrib.rdist_congr_left and 1 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def multiTauMinimizes A $\tau$-minimizer is a tuple $(X_i)_{1 \leq i \leq m}$ that minimizes the $\tau$-functional among all tuples of $G$-valued random variables line 77 source
Source documentation
A $\tau$-minimizer is a tuple $(X_i)_{1 \leq i \leq m}$ that minimizes the $\tau$-functional among all tuples of $G$-valued random variables.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m
Proof uses: MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, LE.le, Real, multiTau
3 instances, coercions and auxiliary constants left out.
```
def multiTauMinimizes {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]
    (p : multiRefPackage G Ω₀) (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i))
    (X : ∀ i, Ω i → G) : Prop :=
…
```
Mentions: MeasurableFinGroup, multiRefPackage
lemma multiTauMinimizes_of_ident line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Fin, multiRefPackage.m, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, multiTauMinimizes
Proof uses: MeasureTheory.IsProbabilityMeasure, Measurable, Eq.mpr, LE.le, Real, multiTau, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, multiTau_of_ident, ProbabilityTheory.IdentDistrib.symm
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma multiTau_continuous If $G$ is finite, then $\tau$ is continuous line 96 source
Source documentation
If $G$ is finite, then $\tau$ is continuous.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, TopologicalSpace, DiscreteTopology, BorelSpace, MeasureTheory.MeasureSpace, multiRefPackage, Continuous, Fin, multiRefPackage.m, MeasureTheory.ProbabilityMeasure, Real, multiTau, MeasureTheory.MeasureSpace.mk, id
Proof uses: Eq.mpr, HAdd.hAdd, HSub.hSub, ProbabilityTheory.entropy, Finset.sum, Finset.univ, MeasureTheory.Measure.pi, MeasureTheory.MeasureSpace.volume, HMul.hMul, Inv.inv, multiRefPackage.η, rdist, multiRefPackage.X₀, Eq, congrArg, funext, multiDist, congr, MeasureTheory.Measure.map, MeasureTheory.Measure and 24 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma multiTau_continuous {G Ω₀ : Type u} [MeasurableFinGroup G] [TopologicalSpace G]
    [DiscreteTopology G] [BorelSpace G] [MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) :
    Continuous (fun (μ : Fin p.m → ProbabilityMeasure G) ↦
      multiTau p (fun _ ↦ G) (fun i ↦ ⟨μ i⟩) (fun _ ↦ id)) := by
…
```
Mentions: MeasurableFinGroup, multiRefPackage, multiTau
lemma multiTau_min_exists_measure If $G$ is finite, then a $\tau$-minimizer exists line 121 source
Source documentation
If $G$ is finite, then a $\tau$-minimizer exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Exists, Fin, multiRefPackage.m, MeasureTheory.Measure, And, MeasureTheory.IsProbabilityMeasure, LE.le, Real, multiTau, MeasureTheory.MeasureSpace.mk, id
Proof uses: TopologicalSpace, Bot.bot, DiscreteTopology, DiscreteTopology.mk, rfl, MeasureTheory.ProbabilityMeasure, Continuous, multiTau_continuous, Inhabited, Inhabited.mk, OfNat.ofNat, Membership.mem, Set, Set.univ, IsMinOn, IsCompact.exists_isMinOn, isCompact_univ, of_eq_true, Set.Nonempty, Continuous.continuousOn and 8 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma multiTau_min_exists_measure {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]
    (p : multiRefPackage G Ω₀) :
    ∃ (μ : Fin p.m → Measure G), (∀ i, IsProbabilityMeasure (μ i)) ∧
    ∀ (ν : Fin p.m → Measure G) [∀ i, IsProbabilityMeasure (ν i)],
    multiTau p (fun _ ↦ G) (fun i ↦ ⟨μ i⟩) (fun _ ↦ id) ≤
      multiTau p (fun _ ↦ G) (fun i ↦ ⟨ν i⟩) (fun _ ↦ id) := by
…
```
Mentions: MeasurableFinGroup, multiRefPackage, multiTau
lemma multiTau_min_exists If $G$ is finite, then a $\tau$-minimizer exists line 141 source
Source documentation
If $G$ is finite, then a $\tau$-minimizer exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableFinGroup, MeasureTheory.MeasureSpace, multiRefPackage, Exists, Fin, multiRefPackage.m, And, Measurable, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, multiTauMinimizes
Proof uses: MeasureTheory.Measure, Exists.choose, LE.le, Real, multiTau, MeasureTheory.MeasureSpace.mk, id, multiTau_min_exists_measure, Exists.intro, And.intro, measurable_id, And.left, Exists.choose_spec, Eq, MeasureTheory.Measure.map, multiTau_of_ident, ProbabilityTheory.identDistrib_map, Eq.mpr, congrArg, Eq.symm and 1 more
6 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma multiTau_min_exists {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]
    (p : multiRefPackage G Ω₀) :
    ∃ (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G),
    (∀ i, Measurable (X i)) ∧ (∀ i, IsProbabilityMeasure (hΩ i).volume)
    ∧ multiTauMinimizes p Ω hΩ X := by
…
```
Mentions: MeasurableFinGroup, multiRefPackage, multiTauMinimizes
lemma multiTau_min_sum_le If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, then $\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0]$ line 159 source
Source documentation
If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, then $\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0]$.

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, multiTauMinimizes, LE.le, Real, Finset.sum, Finset.univ, rdist, multiRefPackage.X₀, HMul.hMul, OfNat.ofNat, Nat, Inv.inv, multiRefPackage.η
Proof uses: GT.gt, multiRefPackage.hη, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, LT.lt, HAdd.hAdd, 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 130 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma multiTau_min_sum_le {G Ω₀ : Type u} [hG : MeasurableFinGroup G] [hΩ₀ : MeasureSpace Ω₀]
    (p : multiRefPackage G Ω₀) (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i))
    (hprobΩ : ∀ i, IsProbabilityMeasure (ℙ : Measure (Ω i))) (X : ∀ i, Ω i → G)
    (hX : ∀ i, Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X) :
  ∑ i, d[X i # p.X₀] ≤ 2 * p.m * p.η⁻¹ * d[p.X₀ # p.X₀] := by
…
```
Mentions: MeasurableFinGroup, multiRefPackage, multiTauMinimizes
lemma sub_multiDistance_le Documented declaration: sub_multiDistance_le line 200 source
Source documentation
If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, and $k := D[(X_i)_{1 \leq i \leq m}]$, then for any other tuple $(X'_i)_{1 \leq i \leq m}$, one has $$ k - D[(X'_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i].$$

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, multiTauMinimizes, LE.le, Real, HSub.hSub, multiDist, HMul.hMul, multiRefPackage.η, Finset.sum, Finset.univ, rdist
Proof uses: HAdd.hAdd, multiRefPackage.X₀, Trans.trans, multiTau, GT.gt, OfNat.ofNat, multiRefPackage.hη, multiRefPackage.hprob, Eq.mpr, id, Eq, congrArg, Eq.symm, mul_add, Finset.sum_add_distrib, add_le_add, le_refl, mul_le_mul_of_nonneg_left, Finset.sum_le_sum, Membership.mem and 59 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma sub_multiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [hΩ₀ : MeasureSpace Ω₀]
    {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : ∀ i, MeasureSpace (Ω i)}
    (hΩprob : ∀ i, IsProbabilityMeasure (hΩ i).volume) {X : ∀ i, Ω i → G}
    (hmeasX : ∀ i, Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X)
    {Ω' : Fin p.m → Type u} {hΩ' : ∀ i, MeasureSpace (Ω' i)}
    (hΩprob' : ∀ i, IsProbabilityMeasure (hΩ' i).volume)
    {X' : ∀ i, Ω' i → G} (hmeasX' : ∀ i, Measurable (X' i)) :
    D[X; hΩ] - D[X'; hΩ'] ≤ p.η * ∑ i, d[X i ; (hΩ i).volume # X' i; (hΩ' i).volume ] := by
…
```
Mentions: MeasurableFinGroup, multiRefPackage, multiTauMinimizes
lemma sub_multiDistance_le' line 222 source
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, multiTauMinimizes, Equiv.Perm, LE.le, Real, HSub.hSub, multiDist, HMul.hMul, multiRefPackage.η, Finset.sum, Finset.univ, rdist
Proof uses: Trans.trans, Eq, HSub, Eq.rec, Eq.refl, Eq.mpr, id, congrArg, multiDist_of_perm, sub_multiDistance_le, multiTau, HAdd, HAdd.hAdd, multiRefPackage.X₀, HMul, Fintype.sum_equiv, rfl
33 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma sub_condMultiDistance_le Documented declaration: sub_condMultiDistance_le line 257 source
Source documentation
If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, and $k := D[(X_i)_{1 \leq i \leq m}]$, then for any other tuples $(X'_i)_{1 \leq i \leq m}$ and $(Y_i)_{1 \leq i \leq m}$ with the $X'_i$ G$-valued, one has $$ k - D[(X'_i)_{1 \leq i \leq m} | (Y_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i|Y_i].$$

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, multiTauMinimizes, Fintype, MeasurableSpace, MeasurableSingletonClass, LE.le, Real, HSub.hSub, multiDist, condMultiDist, HMul.hMul, multiRefPackage.η, Finset.sum and 2 more
Proof uses: Finset.prod, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, Eq, OfNat.ofNat, Eq.mpr, MeasureTheory.Measure.map, Finset, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Membership.mem, MeasureTheory.map_measureReal_apply, MeasurableSet.singleton, id and 82 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
lemma sub_condMultiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]
    {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : ∀ i, MeasureSpace (Ω i)}
    (hΩprob : ∀ i, IsProbabilityMeasure (hΩ i).volume) {X : ∀ i, Ω i → G}
    (hmeasX : ∀ i, Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X)
    {Ω' : Fin p.m → Type u} {hΩ' : ∀ i, MeasureSpace (Ω' i)}
    (hΩ'prob : ∀ i, IsProbabilityMeasure (hΩ' i).volume)
    {X' : ∀ i, Ω' i → G} (hmeasX' : ∀ i, Measurable (X' i))
    {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S]
    {Y : ∀ i, Ω' i → S} (hY : ∀ i, Measurable (Y i)) :
    D[X; hΩ] - D[X'|Y; hΩ'] ≤ p.η * ∑ i, d[X i ; (hΩ i).volume # X' i | Y i; (hΩ' i).volume] := by
…
```
Mentions: MeasurableFinGroup, multiRefPackage, multiTauMinimizes
lemma sub_condMultiDistance_le' Documented declaration: sub_condMultiDistance_le' line 339 source
Source documentation
With the notation of the previous lemma, we have \begin{equation}\label{5.3-conv} k - D[ X'{[m]} | Y{[m]} ] \leq \eta \sum_{i=1}^m d[X_{\sigma(i)};X'_i|Y_i] \end{equation} for any permutation $\sigma : \{1,\dots,m\} \rightarrow \{1,\dots,m\}$.

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, multiTauMinimizes, Fintype, MeasurableSpace, MeasurableSingletonClass, Equiv.Perm, LE.le, Real, HSub.hSub, multiDist, condMultiDist, HMul.hMul, multiRefPackage.η and 3 more
Proof uses: Trans.trans, Eq, HSub, Eq.rec, Eq.refl, Eq.mpr, id, congrArg, multiDist_of_perm, sub_condMultiDistance_le, multiTau, HAdd, HAdd.hAdd, rdist, multiRefPackage.X₀, HMul, Fintype.sum_equiv, rfl
41 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma sub_condMultiDistance_le' {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]
    {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : ∀ i, MeasureSpace (Ω i)}
    (hΩprob : ∀ i, IsProbabilityMeasure (hΩ i).volume)
    {X : ∀ i, Ω i → G} (hmeasX : ∀ i, Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X)
    {Ω' : Fin p.m → Type u} {hΩ' : ∀ i, MeasureSpace (Ω' i)}
    (hΩ'prob : ∀ i, IsProbabilityMeasure (hΩ' i).volume) {X' : ∀ i, Ω' i → G}
    (hmeasX' : ∀ i, Measurable (X' i))
    {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S]
    {Y : ∀ i, Ω' i → S} (hY : ∀ i, Measurable (Y i)) (φ : Equiv.Perm (Fin p.m)) :
    D[X; hΩ] - D[X'|Y; hΩ'] ≤
      p.η * ∑ i, d[X (φ i) ; (hΩ (φ i)).volume # X' i | Y i; (hΩ' i).volume ] := by
…
```
Mentions: MeasurableFinGroup, multiRefPackage, multiTauMinimizes