LeanMachineLearning exposition

ProbabilityTheory.map_swap_compProd_map_condDistrib🔗

Minimal Lean file

map_swap_compProd_map_condDistrib🔗

LemmaProbabilityTheory.map_swap_compProd_map_condDistrib
Details

No docstring.

🔗theorem
ProbabilityTheory.map_swap_compProd_map_condDistrib.{u_1, u_2, u_5}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_5} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β}
  [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {X : α → β}
  {Y : α → Ω} [MeasureTheory.IsFiniteMeasure μ]
  (hY : AEMeasurable Y μ) :
  MeasureTheory.Measure.map Prod.swap
      (MeasureTheory.Measure.compProd (MeasureTheory.Measure.map X μ)
        𝓛[Y | X; μ]) =
    MeasureTheory.Measure.map (fun a => (Y a, X a)) μ
ProbabilityTheory.map_swap_compProd_map_condDistrib.{u_1,
    u_2, u_5}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_5} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace Ω]
  [StandardBorelSpace Ω] [Nonempty Ω]
  {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  (hY : AEMeasurable Y μ) :
  MeasureTheory.Measure.map Prod.swap
      (MeasureTheory.Measure.compProd
        (MeasureTheory.Measure.map X μ)
        𝓛[Y | X; μ]) =
    MeasureTheory.Measure.map
      (fun a => (Y a, X a)) μ

Code

lemma map_swap_compProd_map_condDistrib (hY : AEMeasurable Y μ) :
    (μ.map X ⊗ₘ condDistrib Y X μ).map Prod.swap = μ.map (fun a ↦ (Y a, X a))
Used by (1)

Actions: Source · Open Issue

Proof
by
  by_cases hX : AEMeasurable X μ
  · rw [compProd_map_condDistrib hY,
      AEMeasurable.map_map_of_aemeasurable measurable_swap.aemeasurable (hX.prodMk hY)]
    rfl
  · have hYX : ¬ AEMeasurable (fun a ↦ (Y a, X a)) μ :=
      fun h ↦ hX (measurable_snd.comp_aemeasurable h)
    simp [hX, hYX]