FourVariables.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

23 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

PFR.Mathlib.Probability.Independence.Basic

Imported by 2 files

lemma ProbabilityTheory.iIndepFun.reindex_four_abcd line 18 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
4 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.iIndepFun.reindex_four_abdc line 21 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_acbd line 33 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_acdb line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_adbc line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_adcb line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_bacd line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_badc line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_bcad line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_bcda line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_bdac line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_bdca line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_cadb line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_cabd line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_cbad line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_dabc line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_dacb line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_dbac line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.iIndepFun.reindex_four_dbca line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume
Proof uses: Equiv, Equiv.mk, List, List.Mem, Eq, 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.refl, eq_of_heq, List.Mem.tail and 12 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
abbrev ProbabilityTheory.iIndepFun.κ line 237 source
Distinct definitions of this name: PFR/ForMathlib/ThreeVariables.lean:82 (different declaration text). Qualify references as ProbabilityTheory.iIndepFun.κ@path.
def ProbabilityTheory.iIndepFun.κ_equiv line 241 source
Distinct definitions of this name: PFR/ForMathlib/ThreeVariables.lean:86 (different declaration text). Qualify references as ProbabilityTheory.iIndepFun.κ_equiv@path.
instance ProbabilityTheory.iIndepFun.fintype_kappa line 252 source
Distinct definitions of this name: PFR/ForMathlib/ThreeVariables.lean:96 (different declaration text). Qualify references as ProbabilityTheory.iIndepFun.fintype_kappa@path.
lemma ProbabilityTheory.iIndepFun.apply_two_last If (Z₁, Z₂, Z₃, Z₄) are independent, so are (Z₁, Z₂, φ Z₃ Z₄) for any measurable φ line 256 source
Source documentation
If (Z₁, Z₂, Z₃, Z₄) are independent, so are (Z₁, Z₂, φ Z₃ Z₄) for any measurable φ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, MeasureTheory.MeasureSpace.volume, Measurable, Prod, Function.uncurry
Proof uses: Equiv, Sigma, Sigma.mk, ProbabilityTheory.iIndepFun.pi', List, List.Mem, Eq, 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 and 23 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma apply_two_last
    (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) (hZ₄ : Measurable Z₄)
    {phi : G → G → G} (hphi : Measurable phi.uncurry) :
    iIndepFun ![Z₁, Z₂, (fun ω ↦ phi (Z₃ ω) (Z₄ ω))] := by
…
```
Mentions: phi