gaussianReal_map_const_sub — Mathlib

English

Constant subtraction from the left is equivalent to subtracting from the mean: (y − X) has GaussianReal (y − μ) v.

Русский

Левое вычитание константы аналогично вычитанию константы из среднего: y − X имеет GaussianReal( y − μ ) v.

LaTeX

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

Lean4

theorem gaussianReal_map_const_sub (y : ℝ) : (gaussianReal μ v).map (y - ·) = gaussianReal (y - μ) v :=
  by
  simp_rw [sub_eq_add_neg]
  have : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x := by ext; simp
  rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), gaussianReal_map_neg, gaussianReal_map_const_add, add_comm]

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