gaussianReal_map_const_add — Mathlib

English

Translation by a constant y on the left (y + X) yields Gaussian with mean μ + y and same variance v.

Русский

При добавлении константы слева y + X получается гауссово распределение с тем же v и с новым матожиданием μ + y.

LaTeX

$$$(\mathrm{gaussianReal}(\mu, v)).map (\lambda x. y + x) = \mathrm{gaussianReal}(\mu + y, v)$$$

Lean4

/-- The map of a Gaussian distribution by addition of a constant is a Gaussian. -/
theorem gaussianReal_map_const_add (y : ℝ) : (gaussianReal μ v).map (y + ·) = gaussianReal (μ + y) v :=
  by
  simp_rw [add_comm y]
  exact gaussianReal_map_add_const y

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