LeanMachineLearning exposition

ProbabilityTheory.condDistrib_ae_eq_cond🔗

Minimal Lean file

condDistrib_ae_eq_cond🔗

LemmaProbabilityTheory.condDistrib_ae_eq_cond
Details

No docstring.

🔗theorem
ProbabilityTheory.condDistrib_ae_eq_cond.{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 : α → Ω} [Countable β] [MeasurableSingletonClass β]
  [MeasureTheory.IsFiniteMeasure μ] (hX : Measurable X)
  (hY : Measurable Y) :
  ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ] fun b =>
    𝓛[Y | X in {b}; μ]
ProbabilityTheory.condDistrib_ae_eq_cond.{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 : α → Ω} [Countable β]
  [MeasurableSingletonClass β]
  [MeasureTheory.IsFiniteMeasure μ]
  (hX : Measurable X)
  (hY : Measurable Y) :
  ⇑𝓛[Y | X;
        μ] =ᵐ[MeasureTheory.Measure.map X
      μ]
    fun b => 𝓛[Y | X in {b}; μ]

Code

lemma condDistrib_ae_eq_cond [Countable β] [MeasurableSingletonClass β]
    [IsFiniteMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) :
    condDistrib Y X μ =ᵐ[μ.map X] fun b ↦ (μ[|X ⁻¹' {b}]).map Y
Used by (5)

Actions: Source · Open Issue

Proof
by
  rw [Filter.EventuallyEq, ae_iff_of_countable]
  intro b hb
  ext s hs
  rw [condDistrib_apply_of_ne_zero hY,
    Measure.map_apply hX (measurableSet_singleton _), Measure.map_apply hY hs,
    Measure.map_apply (hX.prodMk hY) ((measurableSet_singleton _).prod hs),
    cond_apply (hX (measurableSet_singleton _))]
  · congr
  · exact hb