variance_dirac — Mathlib

English

For a measurable map Y: Ω' → Ω and X measurable with respect to μ.map Y, Var[X; μ.map Y] equals Var[X ∘ Y; μ].

Русский

Для отображения Y: Ω' → Ω и X, измеримого относительно μ.map Y, Var[X; μ.map Y] = Var[X ∘ Y; μ].

LaTeX

$$$$ \mathrm{variance}(X; \mu.map Y) = \mathrm{variance}(X \circ Y; \mu). $$$$

Lean4

@[simp]
theorem variance_dirac [MeasurableSingletonClass Ω] (x : Ω) : Var[X; Measure.dirac x] = 0 :=
  by
  rw [variance_eq_integral]
  · simp
  · exact aemeasurable_dirac

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