LeanMachineLearning exposition

ProbabilityTheory.hasCondDistrib_prod_right_iff🔗

Minimal Lean file

hasCondDistrib_prod_right_iff🔗

LemmaProbabilityTheory.hasCondDistrib_prod_right_iff
Details

No docstring.

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

Code

lemma hasCondDistrib_prod_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] (X : α → β) (Y : α → Ω)
    {f : β → γ} (hf : Measurable f) :
    HasCondDistrib Y (fun a ↦ (X a, f (X a))) (κ.prodMkRight _) μ ↔ HasCondDistrib Y X κ μ
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine ⟨fun h ↦ ?_, fun h ↦ h.prod_right hf⟩
  have hX : AEMeasurable X μ := by
    have := h.aemeasurable_snd
    have h_eq : X = (fun p ↦ p.1) ∘ (fun a ↦ (X a, f (X a))) := by ext; simp
    rw [h_eq]
    exact Measurable.comp_aemeasurable (by fun_prop) (by fun_prop)
  refine ⟨by fun_prop, ?_⟩
  have h_eq := h.map_eq
  calc μ.map (fun x ↦ (X x, Y x))
  _ = (μ.map (fun ω ↦ ((X ω, f (X ω)), Y ω))).map (fun p ↦ (p.1.1, p.2)) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    congr
  _ = (μ.map (fun a ↦ (X a, f (X a))) ⊗ₘ κ.prodMkRight γ).map (fun p ↦ (p.1.1, p.2)) := by rw [h_eq]
  _ = ((μ.map X).map (fun a ↦ (a, f a)) ⊗ₘ κ.prodMkRight γ).map (fun p ↦ (p.1.1, p.2)) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    congr
  _ = μ.map X ⊗ₘ κ := by
    simp_rw [Measure.compProd_eq_comp_prod,
      ← Measure.deterministic_comp_eq_map (f := fun a ↦ (a, f a)) (by fun_prop),
      ← Measure.deterministic_comp_eq_map (f := fun p : (β × γ) × Ω ↦ (p.1.1, p.2)) (by fun_prop),
      Measure.comp_assoc]
    congr 1
    ext b : 1
    rw [Kernel.comp_apply, Kernel.comp_apply, Kernel.prod_apply, Kernel.id_apply,
      Kernel.deterministic_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.1) id) ((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)]