LeanMachineLearning exposition

ProbabilityTheory.ae_eq_of_condDistrib_eq_deterministic🔗

Minimal Lean file

ae_eq_of_condDistrib_eq_deterministic🔗

LemmaProbabilityTheory.ae_eq_of_condDistrib_eq_deterministic
Details

No docstring.

🔗theorem
ProbabilityTheory.ae_eq_of_condDistrib_eq_deterministic.{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 μ] {f : β → Ω}
  (hf : Measurable f) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
  (h :
    ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ]
      ⇑(Kernel.deterministic f hf)) :
  Y =ᵐ[μ] f ∘ X
ProbabilityTheory.ae_eq_of_condDistrib_eq_deterministic.{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 μ]
  {f : β → Ω} (hf : Measurable f)
  (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ)
  (h :
    ⇑𝓛[Y | X;
          μ] =ᵐ[MeasureTheory.Measure.map
        X μ]
      ⇑(Kernel.deterministic f hf)) :
  Y =ᵐ[μ] f ∘ X

Code

lemma ae_eq_of_condDistrib_eq_deterministic {f : β → Ω} (hf : Measurable f) (hX : AEMeasurable X μ)
    (hY : AEMeasurable Y μ) (h : condDistrib Y X μ =ᵐ[μ.map X] Kernel.deterministic f hf) :
    Y =ᵐ[μ] f ∘ X
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  have hfX := condDistrib_comp_self (μ := μ) X hf
  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h hfX
  exact ae_eq_of_map_prodMk_eq hf hX hY (hfX ▸ h)