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

9 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)

Imported by 2 files

theorem ProbabilityTheory.IndepFun.identDistrib_cond If A is independent from B, then conditioning on an event given by B does not change the distribution of A line 22 source
Source documentation
If A is independent from B, then conditioning on an event given by B does not change the distribution of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IndepFun, Set, MeasurableSet, Measurable, Ne, ENNReal, Set.preimage, OfNat.ofNat, ProbabilityTheory.IdentDistrib, ProbabilityTheory.cond
Proof uses: ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, MeasureTheory.Measure.ext, MeasureTheory.Measure.map, Eq.mpr, Eq, id, congrArg, MeasureTheory.Measure.map_apply, HMul.hMul, Inv.inv, Inter.inter, ProbabilityTheory.cond_apply, Set.inter_comm, ProbabilityTheory.IndepFun.measure_inter_preimage_eq_mul, mul_comm, mul_assoc, ENNReal.mul_inv_cancel, MeasureTheory.measure_ne_top, mul_one and 1 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem IndepFun.identDistrib_cond [IsProbabilityMeasure μ]
    (hi : IndepFun A B μ) {s : Set β}
    (hs : MeasurableSet s) (hA : Measurable A) (hB : Measurable B)
    (h : μ (B ⁻¹' s) ≠ 0) :
    IdentDistrib A A μ (μ[|B ⁻¹' s]) := by
…
```
lemma ProbabilityTheory.IndepFun.cond_left If A is independent of B, then they remain independent when conditioning on an event of the form A ∈ s of positive probability line 35 source
Source documentation
If A is independent of B, then they remain independent when conditioning on an event of the form A ∈ s of positive probability.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.IndepFun, Set, MeasurableSet, Measurable, ProbabilityTheory.cond, Set.preimage
Proof uses: Iff.mpr, Eq, ENNReal, Inter.inter, HMul.hMul, ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul, id, Set.ext, Eq.mpr, Iff, Membership.mem, And, congr, congrArg, Eq.trans, Iff.intro, of_eq_true, True, eq_true, and_self and 27 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma IndepFun.cond_left (hi : IndepFun A B μ) {s : Set α}
    (hs : MeasurableSet s) (hA : Measurable A) :
    IndepFun A B (μ[| A⁻¹' s]) := by
…
```
lemma ProbabilityTheory.IndepFun.cond_right If A is independent of B, then they remain independent when conditioning on an event of the form B ∈ t of positive probability line 56 source
Source documentation
If A is independent of B, then they remain independent when conditioning on an event of the form B ∈ t of positive probability.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.IndepFun, Set, MeasurableSet, Measurable, ProbabilityTheory.cond, Set.preimage
Proof uses: ProbabilityTheory.IndepFun.symm, ProbabilityTheory.IndepFun.cond_left
```
lemma IndepFun.cond_right (h : IndepFun A B μ) {t : Set β}
    (ht : MeasurableSet t) (hB : Measurable B) :
    IndepFun A B (μ[| B⁻¹' t]) :=
…
```
lemma ProbabilityTheory.IndepFun.cond If A is independent of B, then they remain independent when conditioning on an event of the form A ∈ s ∩ B ∈ t of positive probability line 63 source
Source documentation
If A is independent of B, then they remain independent when conditioning on an event of the form A ∈ s ∩ B ∈ t of positive probability.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.IndepFun, Set, MeasurableSet, Measurable, ProbabilityTheory.cond, Inter.inter, Set.preimage
Proof uses: Iff.mpr, Eq, ENNReal, HMul.hMul, ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul, id, Set.ext, Eq.mpr, Iff, Membership.mem, And, congr, congrArg, Eq.trans, Iff.intro, of_eq_true, True, eq_true, and_self, Inv.inv and 60 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma IndepFun.cond (hi : IndepFun A B μ) {s : Set α} {t : Set β}
    (hs : MeasurableSet s) (ht : MeasurableSet t) (hA : Measurable A) (hB : Measurable B) :
    IndepFun A B (μ[| A ⁻¹' s ∩ B ⁻¹' t]) := by
…
```
def ProbabilityTheory.CondIndepFun The assertion that f and g are conditionally independent relative to h line 105 source
Source documentation
The assertion that f and g are conditionally independent relative to h.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure
Proof uses: Filter.Eventually, ProbabilityTheory.IndepFun, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, MeasureTheory.ae, MeasureTheory.Measure.map
4 instances, coercions and auxiliary constants left out.
```
def CondIndepFun (f : Ω → α) (g : Ω → β) (h : Ω → γ) (μ : Measure Ω := by volume_tac) : Prop :=
…
```
lemma ProbabilityTheory.condIndepFun_iff line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Iff, ProbabilityTheory.CondIndepFun, Filter.Eventually, ProbabilityTheory.IndepFun, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, MeasureTheory.ae, MeasureTheory.Measure.map
Proof uses: Iff.rfl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.CondIndepFun.comp_right Composing independent functions with a measurable embedding of conull range gives independent functions line 114 source
Source documentation
Composing independent functions with a measurable embedding of conull range gives independent functions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, MeasurableEmbedding, Filter.Eventually, Membership.mem, Set, Set.range, MeasureTheory.ae, Measurable, ProbabilityTheory.CondIndepFun, Function.comp, MeasureTheory.Measure.comap
Proof uses: Eq.mpr, ProbabilityTheory.IndepFun, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, MeasureTheory.Measure.map, id, Eq, congrArg, propext, ProbabilityTheory.condIndepFun_iff, Eq.symm, MeasureTheory.Measure.map_map, MeasurableEmbedding.measurable, MeasureTheory.Measure.restrict, MeasurableEmbedding.map_comap, MeasureTheory.Measure.restrict_eq_self_of_ae_mem, Filter.Eventually.mono, Eq.mp, Set.preimage_comp and 6 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma CondIndepFun.comp_right {i : Ω' → Ω} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂μ, a ∈ range i)
    (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) (hfg : CondIndepFun f g h μ) :
    CondIndepFun (f ∘ i) (g ∘ i) (h ∘ i) (μ.comap i) := by
…
```
Mentions: ProbabilityTheory.CondIndepFun
lemma ProbabilityTheory.condIndep_copies For X, Y random variables, there exist conditionally independent trials X_1, X_2, Y' line 133 source
Source documentation
For X, Y random variables, there exist conditionally independent trials X_1, X_2, Y'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, FiniteRange, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Exists, And, ProbabilityTheory.CondIndepFun, ProbabilityTheory.IdentDistrib, Prod, prod
Proof uses: MeasureTheory.Measure.map, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, MeasureTheory.Measure.prod, MeasureTheory.Measure.dirac, Finset.sum, FiniteRange.toFinset, HSMul.hSMul, ENNReal, Membership.mem, Filter, MeasureTheory.ae, Set.ofPred, Eq, Eq.mpr, Compl.compl, OfNat.ofNat, id and 130 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 159 steps
Open to load the checked before-and-after goal states.
```
lemma condIndep_copies (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY : Measurable Y)
    [finY : FiniteRange Y] (μ : Measure Ω) [IsProbabilityMeasure μ] :
    ∃ (Ω' : Type u) (_ : MeasurableSpace Ω') (X₁ X₂ : Ω' → α) (Y' : Ω' → β) (ν : Measure Ω'),
      IsProbabilityMeasure ν ∧ Measurable X₁ ∧ Measurable X₂ ∧ Measurable Y' ∧
      CondIndepFun X₁ X₂ Y' ν ∧ IdentDistrib (⟨X₁, Y'⟩) (⟨X, Y⟩) ν μ ∧
      IdentDistrib (⟨X₂, Y'⟩) (⟨X, Y⟩) ν μ := by
…
```
Mentions: FiniteRange, ProbabilityTheory.CondIndepFun
lemma ProbabilityTheory.condIndep_copies' For X, Y random variables, there exist conditionally independent trials X₁, X₂, Y' line 278 source
Source documentation
For X, Y random variables, there exist conditionally independent trials X₁, X₂, Y'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, FiniteRange, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Prod, Function.uncurry, Filter.Eventually, MeasureTheory.ae, Exists, And, ProbabilityTheory.CondIndepFun, ProbabilityTheory.IdentDistrib, prod
Proof uses: ProbabilityTheory.condIndep_copies, Subtype, MeasurableEmbedding, MeasurableEmbedding.subtype_coe, Measurable.setOf, Function.comp, Prod.mk, Measurable.and, Measurable.comp, Measurable.prodMk, Membership.mem, Set, Set.range, Eq.mpr, id, Eq, Eq.trans, congrFun', Filter, congrArg and 16 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma condIndep_copies' (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY : Measurable Y)
    [FiniteRange Y] (μ : Measure Ω) [IsProbabilityMeasure μ] (p : α → β → Prop)
    (hp : Measurable (uncurry p)) (hp' : ∀ᵐ ω ∂μ, p (X ω) (Y ω)) :
    ∃ (Ω' : Type u) (_ : MeasurableSpace Ω') (X₁ X₂ : Ω' → α) (Y' : Ω' → β) (ν : Measure Ω'),
      IsProbabilityMeasure ν ∧ Measurable X₁ ∧ Measurable X₂ ∧ Measurable Y' ∧
      CondIndepFun X₁ X₂ Y' ν ∧ IdentDistrib (⟨X₁, Y'⟩) (⟨X, Y⟩) ν μ ∧
       IdentDistrib (⟨X₂, Y'⟩) (⟨X, Y⟩) ν μ ∧ (∀ ω, p (X₁ ω) (Y' ω)) ∧ (∀ ω, p (X₂ ω) (Y' ω)) := by
…
```
Mentions: FiniteRange, ProbabilityTheory.CondIndepFun