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

8 declarations, 0 contain sorry, 0 declared as axioms

The fibring identity

The proof of the fibring identity, which is a key component of the proof of PFR.

Main statement

sum_of_rdist_eq: If $Y_1,Y_2,Y_3,Y_4$ are independent, then $d[Y_1; Y_2] + d[Y_3; Y_4]$ is equal to the sum of $$d[Y_1+Y_3; Y_2+Y_4] + d[Y_1|Y_1+Y_3; Y_2|Y_2+Y_4] $$ and $$ I[Y_1+Y_2 : Y_2 + Y_4 | Y_1+Y_2+Y_3+Y_4].$$

Imports (1)

PFR.ForMathlib.Entropy.RuzsaDist

Imported by 2 files

lemma rdist_of_indep_eq_sum_fibre Documented declaration: rdist_of_indep_eq_sum_fibre line 38 source
Source documentation
If $Z_1, Z_2$ are independent, then $d[Z_1; Z_2]$ is equal to $$ d[\pi(Z_1);\pi(Z_2)] + d[Z_1|\pi(Z_1); Z_2 |\pi(Z_2)]$$ plus $$I( Z_1 - Z_2 : (\pi(Z_1), \pi(Z_2)) | \pi(Z_1 - Z_2) ).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Countable, MeasurableSpace, MeasurableSingletonClass, AddMonoidHom, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IndepFun, Measurable, FiniteRange, Eq, Real, rdist, HAdd.hAdd, Function.comp, condRuzsaDist, ProbabilityTheory.condMutualInfo, Prod, HSub.hSub, prod
Proof uses: Measurable.of_discrete, ProbabilityTheory.condEntropy, HDiv.hDiv, OfNat.ofNat, Nat, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy_comp_self, Measurable.sub, Eq.mpr, id, congrArg, ProbabilityTheory.IndepFun.rdist_eq, ProbabilityTheory.IndepFun.comp, Measurable.comp, map_comp_sub, of_eq_true, Eq.trans, HMul.hMul, Neg.neg, True and 87 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_of_indep_eq_sum_fibre {Z_1 Z_2 : Ω → H} (h : IndepFun Z_1 Z_2 μ)
    (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] :
    d[Z_1; μ # Z_2; μ] = d[π ∘ Z_1; μ # π ∘ Z_2; μ] + d[Z_1|π∘Z_1; μ # Z_2|π∘Z_2; μ]
      + I[Z_1-Z_2 : ⟨π∘Z_1, π∘Z_2⟩ | π∘(Z_1 - Z_2); μ] := by
…
```
Mentions: FiniteRange
lemma rdist_le_sum_fibre line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Countable, MeasurableSpace, MeasurableSingletonClass, AddMonoidHom, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, HAdd.hAdd, rdist, Function.comp, condRuzsaDist
Proof uses: Prod, Exists, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies_finiteRange, Measurable.of_discrete, Prod.mk, prod, ProbabilityTheory.IdentDistrib.comp, ProbabilityTheory.IdentDistrib.symm, Eq.mpr, id, Eq, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.condMutualInfo, HSub.hSub, rdist_of_indep_eq_sum_fibre and 7 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma rdist_of_hom_le \[d[X;Y]\geq d[\pi(X);\pi(Y)].\] line 80 source
Source documentation
\[d[X;Y]\geq d[\pi(X);\pi(Y)].\]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Countable, MeasurableSpace, MeasurableSingletonClass, AddMonoidHom, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, rdist, Function.comp
Proof uses: le_trans, HAdd.hAdd, condRuzsaDist, Eq.mpr, OfNat.ofNat, id, Eq, congrArg, propext, le_add_iff_nonneg_right, condRuzsaDist_nonneg, Measurable.fun_comp, Measurable.of_discrete, rdist_le_sum_fibre
38 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_of_hom_le {Z_1 : Ω → H} {Z_2 : Ω' → H}
    (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] :
    d[π ∘ Z_1; μ # π ∘ Z_2; μ'] ≤ d[Z_1; μ # Z_2; μ'] := by
…
```
Mentions: FiniteRange
lemma sum_of_rdist_eq_step_condRuzsaDist The conditional Ruzsa Distance step of sum_of_rdist_eq line 94 source
Source documentation
The conditional Ruzsa Distance step of sum_of_rdist_eq

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Fin, OfNat.ofNat, Nat, ProbabilityTheory.iIndepFun, Measurable, Eq, Real, condRuzsaDist, Prod, prod, HSub.hSub
Proof uses: Unit, Prod.mk, Measurable.of_discrete, ProbabilityTheory.IndepFun, ProbabilityTheory.IndepFun.comp, ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk, of_decide_eq_true, Ne, id, Bool, Decidable.decide, Bool.true, Eq.refl, Measurable.sub, of_eq_true, Eq.trans, True, congrArg, sub_sub_cancel, eq_self and 12 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma sum_of_rdist_eq_step_condRuzsaDist {Y : Fin 4 → Ω → G} (h_indep : iIndepFun Y μ)
    (h_meas : ∀ i, Measurable (Y i)) :
    d[⟨Y 0, Y 2⟩ | Y 0 - Y 2 ; μ # ⟨Y 1, Y 3⟩ | Y 1 - Y 3 ; μ]
      = d[Y 0 | Y 0 - Y 2 ; μ # Y 1 | Y 1 - Y 3 ; μ] := by
…
```
lemma sum_of_rdist_eq_step_condMutualInfo The conditional mutual information step of sum_of_rdist_eq line 120 source
Source documentation
The conditional mutual information step of sum_of_rdist_eq

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Fin, OfNat.ofNat, Nat, Measurable, Eq, Real, ProbabilityTheory.condMutualInfo, Prod, prod, HSub.hSub, HAdd.hAdd
Proof uses: Eq.symm, Function.comp, Function.uncurry, Measurable.fun_comp, Prod.fst, Prod.snd, Prod.mk, Measurable.of_discrete, Measurable.prodMk, Measurable.sub, Eq.mpr, id, congrArg, ProbabilityTheory.condMutualInfo_of_inj_map, And.left, Iff.mp, And, Prod.ext_iff, ProbabilityTheory.condMutualInfo_comm, And.right and 15 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma sum_of_rdist_eq_step_condMutualInfo {Y : Fin 4 → Ω → G}
    (h_meas : ∀ i, Measurable (Y i)) :
    I[⟨Y 0 - Y 1, Y 2 - Y 3⟩:⟨Y 0 - Y 2, Y 1 - Y 3⟩|Y 0 - Y 1 - (Y 2 - Y 3);μ] =
    I[Y 0 - Y 1 : Y 1 - Y 3|Y 0 - Y 1 - Y 2 + Y 3;μ] := by
…
```
lemma sum_of_rdist_eq Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables line 153 source
Source documentation
Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables. Then $$d[Y_1-Y_3; Y_2-Y_4] + d[Y_1|Y_1-Y_3; Y_2|Y_2-Y_4] $$ $$ + I[Y_1-Y_2 : Y_2 - Y_4 | Y_1-Y_2-Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Fin, OfNat.ofNat, Nat, ProbabilityTheory.iIndepFun, Measurable, Eq, Real, HAdd.hAdd, rdist, HSub.hSub, condRuzsaDist, ProbabilityTheory.condMutualInfo
Proof uses: AddMonoidHom, Prod, AddMonoidHom.fst, AddMonoidHom.snd, Function.comp, prod, rfl, Measurable.prodMk, ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun, of_decide_eq_true, Ne, id, Bool, Decidable.decide, Bool.true, Eq.refl, ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk, ProbabilityTheory.iIndepFun.indepFun_sub_sub, Measurable.sub and 74 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma sum_of_rdist_eq (Y : Fin 4 → Ω → G) (h_indep : iIndepFun Y μ)
  (h_meas : ∀ i, Measurable (Y i)) :
    d[Y 0; μ # Y 1; μ] + d[Y 2; μ # Y 3; μ]
      = d[(Y 0) - (Y 2); μ # (Y 1) - (Y 3); μ]
        + d[Y 0 | (Y 0) - (Y 2); μ # Y 1 | (Y 1) - (Y 3); μ]
        + I[(Y 0) - (Y 1) : (Y 1) - (Y 3) | (Y 0) - (Y 1) - (Y 2) + (Y 3); μ] := by
…
```
lemma sum_of_rdist_eq_char_2 Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables line 190 source
Source documentation
Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables. Then $$d[Y_1+Y_3; Y_2+Y_4] + d[Y_1|Y_1+Y_3; Y_2|Y_2+Y_4] $$ $$ + I[Y_1+Y_2 : Y_2 + Y_4 | Y_1+Y_2+Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Module, ZMod, OfNat.ofNat, Nat, Fin, ProbabilityTheory.iIndepFun, Measurable, Eq, Real, HAdd.hAdd, rdist, condRuzsaDist, ProbabilityTheory.condMutualInfo
Proof uses: Eq.mp, HSub.hSub, congrArg, congr, congrFun', autoParam, ZModModule.sub_eq_add, condRuzsaDist.congr_simp, Eq.refl, Eq.trans, sum_of_rdist_eq
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma sum_of_rdist_eq_char_2
  [Module (ZMod 2) G] (Y : Fin 4 → Ω → G) (h_indep : iIndepFun Y μ)
  (h_meas : ∀ i, Measurable (Y i)) :
    d[Y 0; μ # Y 1; μ] + d[Y 2; μ # Y 3; μ]
      = d[(Y 0) + (Y 2); μ # (Y 1) + (Y 3); μ]
        + d[Y 0 | (Y 0) + (Y 2); μ # Y 1 | (Y 1) + (Y 3); μ]
        + I[(Y 0) + (Y 1) : (Y 1) + (Y 3) | (Y 0) + (Y 1) + (Y 2) + (Y 3); μ] := by
…
```
lemma sum_of_rdist_eq_char_2' line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Module, ZMod, OfNat.ofNat, Nat, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Measurable, Eq, Real, HAdd.hAdd, rdist and 2 more
Proof uses: 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, eq_of_heq, List.Mem.tail, False.elim, noConfusion_of_Nat, List.ctorIdx and 2 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.