English
If X is Gaussian with mean μ and variance v, then X + y has Gaussian law with mean μ + y and variance v.
Русский
Если X имеет гауссово распределение с параметрами μ и v, то X + y имеет гауссово распределение с параметрами μ + y и v.
LaTeX
$$$\text{If } \mathrm{map}(X, \mathbb{P}) = \mathrm{gaussianReal}(\mu, v) \text{, then } \mathrm{map}(X + y, \mathbb{P}) = \mathrm{gaussianReal}(\mu + y, v)$$$
Lean4
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `X + y`
has Gaussian law with mean `μ + y` and variance `v`. -/
theorem gaussianReal_add_const {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (y : ℝ) :
Measure.map (fun ω ↦ X ω + y) ℙ = gaussianReal (μ + y) v :=
by
have hXm : AEMeasurable X := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)
change Measure.map ((fun ω ↦ ω + y) ∘ X) ℙ = gaussianReal (μ + y) v
rw [← AEMeasurable.map_map_of_aemeasurable (measurable_id'.add_const _).aemeasurable hXm, hX,
gaussianReal_map_add_const y]
