LeanMachineLearning exposition

ProbabilityTheory.HasCondDistrib.prod_right🔗

Minimal Lean file

prod_right🔗

LemmaProbabilityTheory.HasCondDistrib.prod_right
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.prod_right.{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 Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ]
  (h : HasCondDistrib Y X κ μ) {f : β → γ} (hf : Measurable f) :
  HasCondDistrib Y (fun a => (X a, f (X a))) (Kernel.prodMkRight γ κ) μ
ProbabilityTheory.HasCondDistrib.prod_right.{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 Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ]
  (h : HasCondDistrib Y X κ μ) {f : β → γ}
  (hf : Measurable f) :
  HasCondDistrib Y
    (fun a => (X a, f (X a)))
    (Kernel.prodMkRight γ κ) μ

Code

lemma HasCondDistrib.prod_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ)
    {f : β → γ} (hf : Measurable f) :
    HasCondDistrib Y (fun a ↦ (X a, f (X a))) (κ.prodMkRight _) μ
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine ⟨by fun_prop, ?_⟩
  have h_eq := h.map_eq
  calc μ.map (fun x ↦ ((X x, f (X x)), Y x))
  _ = (μ.map (fun ω ↦ (X ω, Y ω))).map (fun p ↦ ((p.1, f p.1), p.2)) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    congr
  _ = (μ.map X ⊗ₘ κ).map (fun p ↦ ((p.1, f p.1), p.2)) := by rw [h_eq]
  _ = (μ.map X).map (fun a ↦ (a, f a)) ⊗ₘ κ.prodMkRight γ := by
    rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod,
      ← Measure.deterministic_comp_eq_map (f := fun a ↦ (a, f a)),
      ← Measure.deterministic_comp_eq_map, Measure.comp_assoc, Measure.comp_assoc]
    swap; · fun_prop
    swap; · fun_prop
    congr 1
    ext b : 1
    rw [Kernel.comp_apply, Kernel.comp_apply, Kernel.prod_apply, Kernel.deterministic_apply,
      Kernel.id_apply, Measure.dirac_bind (Kernel.measurable _), Kernel.prod_apply,
      Measure.deterministic_comp_eq_map, Kernel.prodMkRight_apply, Kernel.id_apply]
    change Measure.map (Prod.map (fun x ↦ (x, f x)) id) ((Measure.dirac b).prod (κ b)) =
      (Measure.dirac (b, f b)).prod (κ b)
    rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id,
      Measure.map_dirac' (by fun_prop)]
  _ = μ.map (fun a ↦ (X a, f (X a))) ⊗ₘ κ.prodMkRight γ := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    congr