integral_dual

Mathlib.Probability.Distributions.Gaussian.Fernique

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.IsGaussian.integral_dual

English

A Gaussian measure with variance zero is a Dirac delta at its mean.

Русский

Гауссова мера с нулевой дисперсией есть дираковская мера в среднем.

LaTeX

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

Lean4

theorem integral_dual (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) :=
  L.integral_comp_comm ((memLp_id μ 1 (by simp)).integrable le_rfl)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru