English
The complex moment-generating function of a Gaussian distribution with mean μ and variance v is exp(z μ + v z^2 / 2).
Русский
Комплексная моментогенерирующая функция гауссового распределения с параметрами μ и v равна exp(z μ + v z^2 / 2).
LaTeX
$$$\text{complexMGF}(X, p, z) = \exp\left(z \cdot \mu + v \cdot z^2 / 2\right)$$$
Lean4
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `c * X`
has Gaussian law with mean `c * μ` and variance `c^2 * v`. -/
theorem gaussianReal_const_mul {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (c : ℝ) :
Measure.map (fun ω ↦ c * X ω) ℙ = gaussianReal (c * μ) (⟨c ^ 2, sq_nonneg _⟩ * v) :=
by
have hXm : AEMeasurable X := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)
change Measure.map ((fun ω ↦ c * ω) ∘ X) ℙ = gaussianReal (c * μ) (⟨c ^ 2, sq_nonneg _⟩ * v)
rw [← AEMeasurable.map_map_of_aemeasurable (measurable_id'.const_mul c).aemeasurable hXm, hX]
exact gaussianReal_map_const_mul c
