comp_snd_map_prod_id — Mathlib

English

For X: Ω → β and μ finite on Ω, the conditional expectation of f( X ) with respect to comap of id on β equals the integral of f against condDistrib id X μ.

Русский

Условное ожидание f(X) относительно comap id на β равно интегралу по condDistrib id X μ.

LaTeX

$$$$ \\mu[f|mβ.comap X] =^{}_{μ} \\int_y f(y) \\; d( condDistrib(id, X, μ) )(y). $$$$

Lean4

theorem _root_.MeasureTheory.Integrable.comp_snd_map_prod_id [NormedAddCommGroup F] (hm : m ≤ mΩ)
    (hf : Integrable f μ) :
    Integrable (fun x : Ω × Ω => f x.2) (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω => (id ω, id ω)) μ) :=
  by
  rw [← integrable_comp_snd_map_prodMk_iff (measurable_id'' hm)] at hf
  simp_rw [id] at hf ⊢
  exact hf

Похожие утверждения