LeanMachineLearning exposition

ProbabilityTheory.CondIndepFun.of_measurable🔗

Minimal Lean file

of_measurable🔗

LemmaProbabilityTheory.CondIndepFun.of_measurable
Details

No docstring.

🔗theorem
ProbabilityTheory.CondIndepFun.of_measurable.{u_1, u_2, u_3, u_4, u_5,
    u_6}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4}
  {γ' : Type u_5} {δ' : Type u_6} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {mγ' : MeasurableSpace γ'}
  {mδ' : MeasurableSpace δ'} [StandardBorelSpace δ'] [Nonempty δ']
  [StandardBorelSpace γ'] [Nonempty γ'] {μ : MeasureTheory.Measure α}
  {X : α → β} {hX : Measurable X} {Y : α → γ} {Z : α → δ} {Y' : α → γ'}
  {Z' : α → δ'} [StandardBorelSpace α] [MeasureTheory.IsFiniteMeasure μ]
  (h_indep :
    CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z μ)
  (hY_meas : Measurable Y') (hZ_meas : Measurable Z') :
  CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y' Z' μ
ProbabilityTheory.CondIndepFun.of_measurable.{u_1,
    u_2, u_3, u_4, u_5, u_6}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {δ : Type u_4}
  {γ' : Type u_5} {δ' : Type u_6}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {mγ' : MeasurableSpace γ'}
  {mδ' : MeasurableSpace δ'}
  [StandardBorelSpace δ'] [Nonempty δ']
  [StandardBorelSpace γ'] [Nonempty γ']
  {μ : MeasureTheory.Measure α}
  {X : α → β} {hX : Measurable X}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'}
  {Z' : α → δ'} [StandardBorelSpace α]
  [MeasureTheory.IsFiniteMeasure μ]
  (h_indep :
    CondIndepFun
      (MeasurableSpace.comap X
        inferInstance)
      ⋯ Y Z μ)
  (hY_meas : Measurable Y')
  (hZ_meas : Measurable Z') :
  CondIndepFun
    (MeasurableSpace.comap X
      inferInstance)
    ⋯ Y' Z' μ

Code

lemma CondIndepFun.of_measurable (h_indep : Y ⟂ᵢ[X, hX; μ] Z)
    (hY_meas : Measurable[mγ.comap Y] Y') (hZ_meas : Measurable[mδ.comap Z] Z') :
    Y' ⟂ᵢ[X, hX; μ] Z'

Actions: Source · Open Issue

Proof
by
  obtain ⟨φ, hφ_meas, h_eqY⟩ : ∃ φ, Measurable φ ∧ Y' = φ ∘ Y := hY_meas.exists_eq_measurable_comp
  obtain ⟨ψ, hψ_meas, h_eqZ⟩ : ∃ ψ, Measurable ψ ∧ Z' = ψ ∘ Z := hZ_meas.exists_eq_measurable_comp
  rw [h_eqY, h_eqZ]
  exact h_indep.comp hφ_meas hψ_meas