charFunDual_eq_of_forall_strongDual_eq_zero

English

The product μ × μ is invariant under linear rotations: applying rotation by θ to both components leaves μ × μ unchanged.

Русский

Произведение μ × μ инвариантно относительно линейных вращений: поворот на θ в обеих компонентах сохраняет μ × μ.

LaTeX

$$$(\\mu \\otimes \\mu) \\circ R_{\\theta}^{-1} = \\mu \\otimes \\mu$ for the rotation R_{\\theta}$$$

Lean4

/-- Characteristic function of a centered Gaussian measure.
For a Gaussian measure, the hypothesis `∀ L : StrongDual ℝ E, μ[L] = 0` is equivalent to the simpler
`μ[id] = 0`, but at this point we don't know yet that `μ` has a first moment so we can't use it.
See `charFunDual_eq_of_integral_eq_zero` -/
theorem charFunDual_eq_of_forall_strongDual_eq_zero (hμ : ∀ L : StrongDual ℝ E, μ[L] = 0) (L : StrongDual ℝ E) :
    charFunDual μ L = exp (-Var[L; μ] / 2) := by simp [charFunDual_eq L, integral_complex_ofReal, hμ L, neg_div]

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