LeanMachineLearning exposition

ProbabilityTheory.HasCondDistrib.const_map_of_const🔗

Minimal Lean file

const_map_of_const🔗

LemmaProbabilityTheory.HasCondDistrib.const_map_of_const
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.const_map_of_const.{u_1, u_2, u_4}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {Q : MeasureTheory.Measure Ω}
  [MeasureTheory.SFinite Q]
  (h : HasCondDistrib Y X (Kernel.const β Q) μ) :
  HasCondDistrib X Y (Kernel.const Ω (MeasureTheory.Measure.map X μ)) μ
ProbabilityTheory.HasCondDistrib.const_map_of_const.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {Q : MeasureTheory.Measure Ω}
  [MeasureTheory.SFinite Q]
  (h :
    HasCondDistrib Y X (Kernel.const β Q)
      μ) :
  HasCondDistrib X Y
    (Kernel.const Ω
      (MeasureTheory.Measure.map X μ))
    μ

Code

lemma HasCondDistrib.const_map_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q]
    (h : HasCondDistrib Y X (Kernel.const β Q) μ) :
    HasCondDistrib X Y (Kernel.const Ω (μ.map X)) μ where
  aemeasurable
Used by (1)

Actions: Source · Open Issue

Proof
by fun_prop
  map_eq := by
    calc μ.map (fun ω ↦ (Y ω, X ω))
    _ = (μ.map (fun ω ↦ (X ω, Y ω))).map Prod.swap := by
      rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
      rfl
    _ = (μ.map X ⊗ₘ Kernel.const β Q).map Prod.swap := by rw [h.map_eq]
    _ = μ.map Y ⊗ₘ Kernel.const Ω (μ.map X) := by simp [h.hasLaw_of_const.map_eq, Measure.prod_swap]