gaussianReal_const_add — Mathlib

English

If X has GaussianReal μ v, then c · X has GaussianReal (c μ) (⟨c^2, sq_nonneg⟩ · v).

Русский

Если X имеет гауссово распределение μ, v, то c · X имеет GaussianReal(c μ) и дисперсию умноженную на c^2.

LaTeX

$$$\text{If } \mathrm{map} X = \mathrm{gaussianReal}(\mu, v) \text{, then } \mathrm{map}(c \cdot X) = \mathrm{gaussianReal}(c \mu, \langle c^2, \mathrm{sq\_nonneg} \rangle \cdot v)$$$

Lean4

/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `y + X`
has Gaussian law with mean `μ + y` and variance `v`. -/
theorem gaussianReal_const_add {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (y : ℝ) :
    Measure.map (fun ω ↦ y + X ω) ℙ = gaussianReal (μ + y) v :=
  by
  simp_rw [add_comm y]
  exact gaussianReal_add_const hX y

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