Commit 2025-05-16 10:47 fe66a272

feat: define Gaussian measures in normed spaces (#24900)

• Add IsGaussian, property that a measure is Gaussian (its map by any continuous linear form is a real Gaussian measure)
• Prove that a finite measure µ is Gaussian iff its characteristic function has value exp (μ[L] * I - Var[L; μ] / 2) for every continuous linear form L : Dual ℝ E.