LeanMachineLearning exposition

ProbabilityTheory.condIndepFun_fst_prod🔗

Minimal Lean file

condIndepFun_fst_prod🔗

LemmaProbabilityTheory.condIndepFun_fst_prod
Details

No docstring.

🔗theorem
ProbabilityTheory.condIndepFun_fst_prod.{u_1, u_2, u_3, u_5, u_6}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_5}
  {Ω' : Type u_6} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace Ω]
  [StandardBorelSpace Ω] [Nonempty Ω] [mΩ' : MeasurableSpace Ω']
  {X : α → β} {Y : α → Ω} {Z : α → Ω'} [MeasureTheory.IsFiniteMeasure μ]
  [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
  [StandardBorelSpace γ] (hX : Measurable X) (hY : Measurable Y)
  (hZ : Measurable Z) (ν : MeasureTheory.Measure γ)
  [MeasureTheory.IsProbabilityMeasure ν]
  (h_indep : CondIndepFun (MeasurableSpace.comap Z mΩ') ⋯ Y X μ) :
  CondIndepFun (MeasurableSpace.comap (fun ω => Z (Prod.fst ω)) mΩ') ⋯
    (fun ω => Y (Prod.fst ω)) (fun ω => X (Prod.fst ω))
    (MeasureTheory.Measure.prod μ ν)
ProbabilityTheory.condIndepFun_fst_prod.{u_1,
    u_2, u_3, u_5, u_6}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {Ω : Type u_5}
  {Ω' : Type u_6} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  [MeasurableSpace Ω]
  [StandardBorelSpace Ω] [Nonempty Ω]
  [mΩ' : MeasurableSpace Ω'] {X : α → β}
  {Y : α → Ω} {Z : α → Ω'}
  [MeasureTheory.IsFiniteMeasure μ]
  [StandardBorelSpace α]
  [StandardBorelSpace β] [Nonempty β]
  [StandardBorelSpace γ]
  (hX : Measurable X) (hY : Measurable Y)
  (hZ : Measurable Z)
  (ν : MeasureTheory.Measure γ)
  [MeasureTheory.IsProbabilityMeasure ν]
  (h_indep :
    CondIndepFun
      (MeasurableSpace.comap Z mΩ') ⋯ Y X
      μ) :
  CondIndepFun
    (MeasurableSpace.comap
      (fun ω => Z (Prod.fst ω)) mΩ')
    ⋯ (fun ω => Y (Prod.fst ω))
    (fun ω => X (Prod.fst ω))
    (MeasureTheory.Measure.prod μ ν)

Code

lemma condIndepFun_fst_prod [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
    [StandardBorelSpace γ]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (ν : Measure γ) [IsProbabilityMeasure ν]
    (h_indep : CondIndepFun (mΩ'.comap Z) hZ.comap_le Y X μ) :
    CondIndepFun (mΩ'.comap (fun ω ↦ Z ω.1)) (hZ.comp measurable_fst).comap_le
      (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib (by fun_prop)
    (by fun_prop) (by fun_prop)] at h_indep ⊢
  have h1 : 𝓛[fun ω ↦ Y ω.1 | fun ω ↦ Z ω.1; μ.prod ν] =ᵐ[μ.map Z] 𝓛[Y | Z; μ] :=
    condDistrib_fst_prod (Y := Y) (X := Z) (ν := ν) (μ := μ) (by fun_prop)
  have h2 : 𝓛[fun ω ↦ X ω.1 | fun ω ↦ Z ω.1; μ.prod ν] =ᵐ[μ.map Z] 𝓛[X | Z; μ] :=
    condDistrib_fst_prod (Y := X) (X := Z) (ν := ν) (μ := μ) (by fun_prop)
  have h_fst1 : (μ.prod ν).map (fun ω ↦ Z ω.1) = μ.map Z := by
    conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst,
      Measure.map_map (by fun_prop) (by fun_prop)]
    rfl
  have h_fst2 : (μ.prod ν).map (fun ω ↦ (Z ω.1, Y ω.1, X ω.1))
      = μ.map (fun ω ↦ (Z ω, Y ω, X ω)) := by
    conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst,
      Measure.map_map (by fun_prop) (by fun_prop)]
    rfl
  rw [h_fst1, h_fst2, h_indep]
  refine Measure.bind_congr_right ?_
  filter_upwards [h1, h2] with x hx1 hx2
  simp_rw [Kernel.prod_apply]
  rw [hx1, ← hx2]