English
Translation by a constant y preserves Gaussian form: the GaussianReal μ v, after mapping by x ↦ x + y, becomes GaussianReal (μ + y) v.
Русский
Сдвиг на константу y сохраняет гауссовость: after mapping by x ↦ x + y, гауссова мера имеет параметры μ + y и v.
LaTeX
$$$(\mathrm{gaussianReal}(\mu, v)).map (\lambda x. x + y) = \mathrm{gaussianReal}(\mu + y, v)$$$
Lean4
/-- The map of a Gaussian distribution by addition of a constant is a Gaussian. -/
theorem gaussianReal_map_add_const (y : ℝ) : (gaussianReal μ v).map (· + y) = gaussianReal (μ + y) v :=
by
by_cases hv : v = 0
· simp only [hv, gaussianReal_zero_var]
exact Measure.map_dirac (measurable_id'.add_const _) _
let e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
have he' : ∀ x, HasDerivAt e ((fun _ ↦ 1) x) x := fun _ ↦ (hasDerivAt_id _).sub_const y
change (gaussianReal μ v).map e.symm = gaussianReal (μ + y) v
ext s' hs'
rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs']
simp only [abs_one, one_mul]
rw [gaussianReal_apply_eq_integral _ hv s']
simp [e, gaussianPDFReal_sub _ y, Homeomorph.addRight, ← sub_eq_add_neg]
