Source indexedtheorem · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.IndepFun.identDistrib_cond

PFR.ForMathlib.ConditionalIndependence · PFR/ForMathlib/ConditionalIndependence.lean:22 to 31

Source documentation

If A is independent from B, then conditioning on an event given by B does not change the distribution of A.

Exact Lean statement

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])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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  refine ⟨hA.aemeasurable, hA.aemeasurable, ?_⟩  ext t ht  rw [Measure.map_apply hA ht, Measure.map_apply hA ht, cond_apply (hB hs), Set.inter_comm,    hi.measure_inter_preimage_eq_mul _ _ ht hs, mul_comm, mul_assoc,    ENNReal.mul_inv_cancel h (by finiteness), mul_one]