LeanMachineLearning exposition

ProbabilityTheory.cond_of_indepFun🔗

Minimal Lean file

cond_of_indepFun🔗

LemmaProbabilityTheory.cond_of_indepFun
Details

No docstring.

🔗theorem
ProbabilityTheory.cond_of_indepFun.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ)
  (hX : Measurable X) (hT : Measurable T) {s : Set β}
  (hs : MeasurableSet s) (hμs : μ (X ⁻¹' s) ≠ 0) :
  𝓛[T | X in s; μ] = MeasureTheory.Measure.map T μ
ProbabilityTheory.cond_of_indepFun.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {X : α → β}
  {T : α → γ}
  [MeasureTheory.IsZeroOrProbabilityMeasure
      μ]
  (h : IndepFun X T μ) (hX : Measurable X)
  (hT : Measurable T) {s : Set β}
  (hs : MeasurableSet s)
  (hμs : μ (X ⁻¹' s) ≠ 0) :
  𝓛[T | X in s; μ] =
    MeasureTheory.Measure.map T μ

Code

lemma cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ)
    (hX : Measurable X) (hT : Measurable T) {s : Set β} (hs : MeasurableSet s)
    (hμs : μ (X ⁻¹' s) ≠ 0) :
    (μ[|X ⁻¹' s]).map T = μ.map T
Used by (4)

Actions: Source · Open Issue

Proof
by
  ext t ht
  rw [Measure.map_apply (by fun_prop) ht, Measure.map_apply (by fun_prop) ht, cond_apply (hX hs),
    IndepSet.measure_inter_eq_mul, ← mul_assoc, ENNReal.inv_mul_cancel, one_mul]
  · exact hμs
  · simp
  · rw [indepFun_iff_indepSet_preimage hX hT] at h
    exact h s t hs ht