LeanMachineLearning exposition

ProbabilityTheory.IndepFun.of_measurable_right🔗

Minimal Lean file

of_measurable_right🔗

LemmaProbabilityTheory.IndepFun.of_measurable_right
Details

No docstring.

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

Code

lemma IndepFun.of_measurable_right
    (h_indep : Y ⟂ᵢ[μ] Z) (hZ_meas : Measurable[mδ.comap Z] Z') :
    Y ⟂ᵢ[μ] Z'
Used by (3)

Actions: Source · Open Issue

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