instIsGaussianMapHSub_1 — Mathlib

English

If μ is Gaussian and c ∈ E, then the map x ↦ c − x yields a Gaussian image.

Русский

Если μ гауссова и c ∈ E, то изображение x ↦ c − x гауссово.

LaTeX

$$$\\forall c \\in E,\\ IsGaussian(\\mu.map (fun x \\mapsto c - x))$$$

Lean4

instance (c : E) : IsGaussian (μ.map (fun x ↦ c - x)) :=
  by
  simp_rw [sub_eq_add_neg]
  suffices IsGaussian ((μ.map (fun x ↦ -x)).map (fun x ↦ c + x))
    by
    rw [Measure.map_map (by fun_prop) (by fun_prop)] at this
    convert this using 1
  infer_instance

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