charFunDual_eq_of_integral_eq_zero

English

If μ[id] = 0, then the characteristic function of μ is exp(-Var[L; μ]/2) for every dual L.

Русский

Если μ[id] = 0, то характеристическая функция μ равна exp(-Var[L; μ]/2) для каждого двойственного функционала L.

LaTeX

$$$(μ[id] = 0) \\Rightarrow ∀ L,\\ charFunDual μ L = \\exp(-Var[L; μ]/2)$$$

Lean4

/-- Characteristic function of a centered Gaussian measure. -/
theorem charFunDual_eq_of_integral_eq_zero (hμ : μ[id] = 0) (L : StrongDual ℝ E) :
    charFunDual μ L = exp (-Var[L; μ] / 2) :=
  by
  refine charFunDual_eq_of_forall_strongDual_eq_zero (fun L ↦ ?_) L
  simp only [id_eq] at hμ
  simp [integral_dual, hμ]

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