English
If μ is a Gaussian measure on a normed space E and c is a fixed vector in E, then the translated measure μ mapped by x ↦ x + c is again Gaussian.
Русский
Если μ — гауссовая мера на нормированном пространстве E и c — фиксированный вектор в E, то сдвинутая по x ↦ x + c мера μ снова гауссова.
LaTeX
$$$\\forall c \\in E,\\ IsGaussian(\\mu) \\Rightarrow IsGaussian(\\mu\\circ T_c^{-1})$, where $T_c(x)=x+c$.$$
Lean4
instance (c : E) : IsGaussian (μ.map (fun x ↦ x + c)) :=
by
refine isGaussian_of_charFunDual_eq fun L ↦ ?_
rw [charFunDual_map_add_const, IsGaussian.charFunDual_eq, ← exp_add]
have hL_comp : L ∘ (fun x ↦ x + c) = fun x ↦ L x + L c := by ext; simp
rw [variance_map (by fun_prop) (by fun_prop), integral_map (by fun_prop) (by fun_prop), hL_comp,
variance_add_const (by fun_prop), integral_complex_ofReal, integral_complex_ofReal]
simp only [map_add]
rw [integral_add (by fun_prop) (by fun_prop)]
congr
simp only [integral_const, measureReal_univ_eq_one, smul_eq_mul, one_mul, ofReal_add]
ring
