gaussianReal_map_sub_const — Mathlib

English

Subtracting a constant from the variable corresponds to subtracting that constant from the mean: gaussianReal μ v mapped by (x ↦ x − y) equals gaussianReal (μ − y) v.

Русский

Вычитание константы из переменной эквивалентно вычитанию константы из среднего: гауссовоReal μ v под (x−y) даёт GaussianReal(μ−y, v).

LaTeX

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

Lean4

theorem gaussianReal_map_sub_const (y : ℝ) : (gaussianReal μ v).map (· - y) = gaussianReal (μ - y) v := by
  simp_rw [sub_eq_add_neg, gaussianReal_map_add_const]

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