English
For a Gaussian measure μ and a StrongDual L, the dual characteristic function charFunDual μ L equals exp( μ[L] I − Var[L; μ] / 2 ).
Русский
Для гауссовой меры μ и линейного функционала L двойственная характеристическая функция равна exp( μ[L] I − Var[L; μ] / 2 ).
LaTeX
$$$\text{charFunDual}(\mu, L) = \exp\big(\mu[L] \; I \, - \, \dfrac{\mathrm{Var}[L;\mu]}{2}\big)$$$
Lean4
instance isGaussian_conv [SecondCountableTopology E] {μ ν : Measure E} [IsGaussian μ] [IsGaussian ν] :
IsGaussian (μ ∗ ν) where
map_eq_gaussianReal
L :=
by
have : (μ ∗ ν)[L] = ∫ x, x ∂((μ.map L).conv (ν.map L)) := by
rw [← Measure.map_conv_continuousLinearMap L, integral_map (φ := L) (by fun_prop) (by fun_prop)]
rw [Measure.map_conv_continuousLinearMap L, this, ← variance_id_map (by fun_prop),
Measure.map_conv_continuousLinearMap L, IsGaussian.map_eq_gaussianReal L, IsGaussian.map_eq_gaussianReal L,
gaussianReal_conv_gaussianReal]
congr <;> simp [variance_nonneg]
