instIsGaussianMapNeg

Mathlib.Probability.Distributions.Gaussian.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.instIsGaussianMapNeg

English

If μ is Gaussian, then its image under x ↦ −x is Gaussian.

Русский

Если μ гауссова, то образ μ под x ↦ −x гауссов.

LaTeX

$$$\\forall \\mu,\\ IsGaussian(\\mu) \\Rightarrow IsGaussian(\\mu.map (fun x \\mapsto -x))$$$

Lean4

instance : IsGaussian (μ.map (fun x ↦ -x)) :=
  by
  change IsGaussian (μ.map (ContinuousLinearEquiv.neg ℝ))
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru