LeanMachineLearning exposition

ProbabilityTheory.hasCondDistrib_fst_prod🔗

Minimal Lean file

hasCondDistrib_fst_prod🔗

LemmaProbabilityTheory.hasCondDistrib_fst_prod
Details

No docstring.

🔗theorem
ProbabilityTheory.hasCondDistrib_fst_prod.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_4}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mΩ : MeasurableSpace Ω} {Y : α → Ω}
  {X : α → β} {κ : Kernel β Ω} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure γ} [MeasureTheory.IsProbabilityMeasure ν]
  (h : HasCondDistrib Y X κ μ) :
  HasCondDistrib (fun ω => Y (Prod.fst ω)) (fun ω => X (Prod.fst ω)) κ
    (MeasureTheory.Measure.prod μ ν)
ProbabilityTheory.hasCondDistrib_fst_prod.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {Ω : Type u_4}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mΩ : MeasurableSpace Ω} {Y : α → Ω}
  {X : α → β} {κ : Kernel β Ω}
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure γ}
  [MeasureTheory.IsProbabilityMeasure ν]
  (h : HasCondDistrib Y X κ μ) :
  HasCondDistrib (fun ω => Y (Prod.fst ω))
    (fun ω => X (Prod.fst ω)) κ
    (MeasureTheory.Measure.prod μ ν)

Code

lemma hasCondDistrib_fst_prod {Y : α → Ω} {X : α → β} {κ : Kernel β Ω}
    {μ : Measure α} {ν : Measure γ} [IsProbabilityMeasure ν]
    (h : HasCondDistrib Y X κ μ) :
    HasCondDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) κ (μ.prod ν) where
  aemeasurable

Actions: Source · Open Issue

Proof
by fun_prop
  map_eq := by
    have h_rhs : Measure.map (fun ω ↦ X ω.1) (μ.prod ν) ⊗ₘ κ = (μ.map X) ⊗ₘ κ := by
      conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst]
      rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)]
      · rfl
      · have := h.aemeasurable_fst
        simpa
    rw [h_rhs, ← h.map_eq]
    conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst]
    rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)]
    · rfl
    · have := h.aemeasurable
      simpa