LeanMachineLearning exposition

ProbabilityTheory.hasCondDistrib_of_condDistrib_eq🔗

Minimal Lean file

hasCondDistrib_of_condDistrib_eq🔗

LemmaProbabilityTheory.hasCondDistrib_of_condDistrib_eq
Details

No docstring.

🔗theorem
ProbabilityTheory.hasCondDistrib_of_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 κ] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
  (h : ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ) :
  HasCondDistrib Y X κ μ
ProbabilityTheory.hasCondDistrib_of_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 κ]
  (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ)
  (h :
    ⇑𝓛[Y | X;
          μ] =ᵐ[MeasureTheory.Measure.map
        X μ]
      ⇑κ) :
  HasCondDistrib Y X κ μ

Code

lemma hasCondDistrib_of_condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (h : condDistrib Y X μ =ᵐ[μ.map X] κ) :
    HasCondDistrib Y X κ μ where
  aemeasurable
Used by (5)

Actions: Source · Open Issue

Proof
by fun_prop
  map_eq := by rw [← compProd_map_condDistrib hY, Measure.compProd_congr h]