integral_condDistrib — Mathlib

English

The conditional expectation of f(X, Y) given X is almost everywhere equal to the integral of f(X, y) against condDistrib(Y, X, μ).

Русский

Условное ожидание функции f(X, Y) по X равно почти наверняка интегралу по y от f(X, y) против condDistrib(Y, X, μ).

LaTeX

$$$\\mu[ f(X, Y) \\mid m\\beta\\backslash\\!\\!\\!\\!\\! \\! X] =^{\\mathrm{a.e.}} \\int_y f(X(·), y) \\, d(\\operatorname{condDistrib}(Y,X,μ) X(·)).$$$

Lean4

theorem _root_.MeasureTheory.Integrable.integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ :=
  (hf_int.integral_condDistrib_map hY).comp_aemeasurable hX

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