gaussianReal_map_mul_const — Mathlib

English

Multiplication by a constant on the right yields the same Gaussian shift: map (· × c) equals GaussianReal (c μ) (⟨c^2, sq_nonneg⟩ * v).

Русский

Умножение справа на константу c сохраняет гауссовость: map (× c) даёт GaussianReal (c μ) (c^2 v).

LaTeX

$$$(\mathrm{gaussianReal}(\mu, v)).map (\cdot \times c) = \mathrm{gaussianReal}(c \mu, \langle c^2, \mathrm{sq\_nonneg} \rangle * v)$$$

Lean4

/-- The map of a Gaussian distribution by multiplication by a constant is a Gaussian. -/
theorem gaussianReal_map_mul_const (c : ℝ) :
    (gaussianReal μ v).map (· * c) = gaussianReal (c * μ) (⟨c ^ 2, sq_nonneg _⟩ * v) :=
  by
  simp_rw [mul_comm _ c]
  exact gaussianReal_map_const_mul c

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