gaussianReal_map_neg — Mathlib

English

Negation corresponds to negating the mean: map (−) yields gaussianReal (−μ) v.

Русский

Отрицание переменной соответствует изменению знака матожидания: GaussianReal(μ,v) под отрицанием имеет вид GaussianReal(−μ, v).

LaTeX

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

Lean4

theorem gaussianReal_map_neg : (gaussianReal μ v).map (fun x ↦ -x) = gaussianReal (-μ) v := by
  simpa using gaussianReal_map_const_mul (μ := μ) (v := v) (-1)

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