condExp_bot — Mathlib

English

If μ is a probability measure, condExp on bottom equals the function x ↦ ∫ f, under normalization by μ(univ).

Русский

Если μ — вероятность, condExp на дне равен функции x ↦ ∫ f, нормированному на μ(univ).

LaTeX

$$$$\\operatorname{condExp}_{\\mathcal{F}_{\\bot}}(μ,f) = \\operatorname{const}(x) \\cdot \\int f \\, dμ.$$$$

Lean4

theorem condExp_bot [IsProbabilityMeasure μ] (f : α → E) : μ[f|⊥] = fun _ => ∫ x, f x ∂μ :=
  by
  refine (condExp_bot' f).trans ?_
  rw [measureReal_univ_eq_one, inv_one, one_smul]

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