evariance_eq_zero_iff — Mathlib

English

Let X be an a.e.-measurable real-valued random variable on (Ω, μ). Then the evariance of X is zero if and only if X is μ-almost surely equal to the constant μ[X].

Русский

Пусть X: Ω → ℝ измерима по мере μ и верна почти везде. Тогда evariance(X, μ) = 0, если и только если X = μ[X] μ-приближенно (а.е.).

LaTeX

$$$$ \mathrm{evariance}(X, \mu) = 0 \iff X =_{\mathrm{ae}}^{\mu} (\omega \mapsto \mu[X]). $$$$

Lean4

theorem evariance_eq_zero_iff (hX : AEMeasurable X μ) : evariance X μ = 0 ↔ X =ᵐ[μ] fun _ => μ[X] := by
  simp [evariance, lintegral_eq_zero_iff' ((hX.sub_const _).enorm.pow_const _), EventuallyEq, sub_eq_zero]

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