LeanMachineLearning exposition

ProbabilityTheory.IndepFun.of_measurable_left🔗

Minimal Lean file

of_measurable_left🔗

LemmaProbabilityTheory.IndepFun.of_measurable_left
Details

No docstring.

🔗theorem
ProbabilityTheory.IndepFun.of_measurable_left.{u_1, u_3, u_4, u_5}
  {α : Type u_1} {γ : Type u_3} {δ : Type u_4} {γ' : Type u_5}
  {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {mγ' : MeasurableSpace γ'}
  [StandardBorelSpace γ'] [Nonempty γ'] {μ : MeasureTheory.Measure α}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'} (h_indep : IndepFun Y Z μ)
  (hY_meas : Measurable Y') : IndepFun Y' Z μ
ProbabilityTheory.IndepFun.of_measurable_left.{u_1,
    u_3, u_4, u_5}
  {α : Type u_1} {γ : Type u_3}
  {δ : Type u_4} {γ' : Type u_5}
  {mα : MeasurableSpace α}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {mγ' : MeasurableSpace γ'}
  [StandardBorelSpace γ'] [Nonempty γ']
  {μ : MeasureTheory.Measure α}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'}
  (h_indep : IndepFun Y Z μ)
  (hY_meas : Measurable Y') :
  IndepFun Y' Z μ

Code

lemma IndepFun.of_measurable_left
    (h_indep : Y ⟂ᵢ[μ] Z) (hY_meas : Measurable[mγ.comap Y] Y') :
    Y' ⟂ᵢ[μ] Z

Actions: Source · Open Issue

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