LeanMachineLearning exposition

ProbabilityTheory.HasCondDistrib.condDistrib_eq🔗

Minimal Lean file

condDistrib_eq🔗

LemmaProbabilityTheory.HasCondDistrib.condDistrib_eq
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.condDistrib_eq.{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 : α → Ω} {κ : Kernel β Ω}
  [StandardBorelSpace Ω] [Nonempty Ω] [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ) :
  ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ
ProbabilityTheory.HasCondDistrib.condDistrib_eq.{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 : α → Ω} {κ : Kernel β Ω}
  [StandardBorelSpace Ω] [Nonempty Ω]
  [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ]
  (h : HasCondDistrib Y X κ μ) :
  ⇑𝓛[Y | X;
        μ] =ᵐ[MeasureTheory.Measure.map X
      μ]
    ⇑κ

Code

lemma HasCondDistrib.condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]
    (h : HasCondDistrib Y X κ μ) :
    condDistrib Y X μ =ᵐ[μ.map X] κ
Used by (13)

Actions: Source · Open Issue

Proof
by
  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h.map_eq]