instIsGaussianMapHAdd_1 — Mathlib

English

If μ is Gaussian and c ∈ E, then the pushforward of μ under the map x ↦ c + x is Gaussian.

Русский

Если μ гауссова и c ∈ E, то образ μ по отображению x ↦ c + x является гауссовой мерой.

LaTeX

$$$\\forall c \\in E,\\ IsGaussian(\\mu) \\Rightarrow IsGaussian(\\mu\\circ T_{c}^{-1})$ with $T_c(x)=c+x$.$$

Lean4

instance (c : E) : IsGaussian (μ.map (fun x ↦ c + x)) := by simp_rw [add_comm c]; infer_instance

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