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

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)

Imported by 2 files

lemma ProbabilityTheory.Kernel.iIndepFun.finsets Documented declaration: finsets line 26 source
Source documentation
If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint finite index sets, then the tuples formed by f i for i ∈ S j are mutually independent, when seen as a family indexed by J.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, MeasureTheory.Measure, Finset, Set.PairwiseDisjoint, Set.univ, ProbabilityTheory.Kernel.iIndepFun, Measurable, Subtype, Membership.mem
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Set, Set.image, Set.pi, Set.ofPred, MeasurableSet, ProbabilityTheory.Kernel.iIndepSets.iIndep, MeasurableSpace.comap, LE.le, Eq.symm, propext, measurable_iff_comap_le, measurable_pi_iff, Exists, And, Set.preimage and 92 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 122 steps
Open to load the checked before-and-after goal states.
```
lemma iIndepFun.finsets {J : Type*}
    (S : J → Finset ι) (h_disjoint : Set.PairwiseDisjoint Set.univ S)
    (hf_Indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (f i)) :
    iIndepFun (fun (j : J) ↦ fun a (i : S j) ↦ f i a) κ μ := by
…
```
lemma ProbabilityTheory.Kernel.iIndepFun.finsets_comp Documented declaration: finsets_comp line 138 source
Source documentation
If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint finite index sets, and φ j is a function that maps the tuple formed by f i for i ∈ S j to a measurable space γ j, then the family of random variables formed by φ j (f i)_{i ∈ S j} and indexed by J is iIndep.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, MeasureTheory.Measure, Finset, Set.PairwiseDisjoint, Set.univ, ProbabilityTheory.Kernel.iIndepFun, Measurable, Subtype, Membership.mem
Proof uses: ProbabilityTheory.Kernel.iIndepFun.comp, ProbabilityTheory.Kernel.iIndepFun.finsets
12 instances, coercions and auxiliary constants left out.
```
lemma iIndepFun.finsets_comp {J : Type*}
    (S : J → Finset ι) (h_disjoint : Set.PairwiseDisjoint Set.univ S)
    (hf_Indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (f i))
    (γ : J → Type*) {mγ : ∀ j, MeasurableSpace (γ j)}
    (φ : (j : J) → ((i : S j) → β i) → γ j) (hφ : ∀ j, Measurable (φ j)) :
    iIndepFun (fun (j : J) ↦ fun a ↦ φ j (fun (i : S j) ↦ f i a)) κ μ :=
…
```