eq_dirac_of_variance_eq_zero — Mathlib

English

If the variance vanishes in the strong Dual sense, μ is a Dirac measure at its mean.

Русский

Если вариация нулевая в смысле сильного двойственного, μ — дираковская мера по своему среднему.

LaTeX

$$$(\\forall L, Var[L; μ] = 0) \\Rightarrow μ = \\mathrm{dirac}(\\int x\, dμ)$$$

Lean4

/-- A Gaussian measure with variance zero is a Dirac. -/
theorem eq_dirac_of_variance_eq_zero (h : ∀ L : StrongDual ℝ E, Var[L; μ] = 0) : μ = Measure.dirac (∫ x, x ∂μ) :=
  by
  refine Measure.ext_of_charFunDual ?_
  ext L
  rw [charFunDual_dirac, charFunDual_eq L, h L, integral_complex_ofReal, integral_dual L]
  simp

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