condExp_ae_eq_integral_condDistrib_id

English

For X: α → β and Y: α → Ω with appropriate measurability, the conditional expectation of f(X(a), Y(a)) given X equals the conditional expectation of f(Y(a)) with respect to condDistrib id X.

Русский

Условное ожидание f(X(a), Y(a)) по X равно условному экспоненту f(Y(a)) относительно condDistrib id X.

LaTeX

$$$$ \\mu[ f(X a, Y a) \\mid X] =^{}_{μ} \\int_y f(y) \\; d(\\operatorname{condDistrib}(Y,X,μ)(y)). $$$$

Lean4

theorem condExp_ae_eq_integral_condDistrib_id [NormedSpace ℝ F] [CompleteSpace F] {X : Ω → β} {μ : Measure Ω}
    [IsFiniteMeasure μ] (hX : Measurable X) {f : Ω → F} (hf_int : Integrable f μ) :
    μ[f|mβ.comap X] =ᵐ[μ] fun a => ∫ y, f y ∂condDistrib id X μ (X a) :=
  condExp_prod_ae_eq_integral_condDistrib' hX aemeasurable_id (hf_int.comp_snd_map_prodMk X)

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