gaussianReal_mul_const — Mathlib

English

If X is Gaussian with mean μ and v, then the complex MGF of X with measure p is exp(z μ + v z^2/2).

Русский

Если X гауссово распределена с μ и v, то её комплексная MGF равна exp(z μ + v z^2/2).

LaTeX

$$$\text{complexMGF } X p z = \exp\left(z \mu + v z^2 / 2\right)$$$

Lean4

/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `X * c`
has Gaussian law with mean `c * μ` and variance `c^2 * v`. -/
theorem gaussianReal_mul_const {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (c : ℝ) :
    Measure.map (fun ω ↦ X ω * c) ℙ = gaussianReal (c * μ) (⟨c ^ 2, sq_nonneg _⟩ * v) :=
  by
  simp_rw [mul_comm _ c]
  exact gaussianReal_const_mul hX c

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