English
Multiplying a Gaussian variable by a constant c scales the mean and variance: map (·) by c gives GaussianReal (c μ) (⟨c^2, sq_nonneg ⟩ * v).
Русский
Умножение гауссова случайного переменного на константу c масштабирует матожидание и дисперсию: новое распределение GaussianReal (c μ) (c^2 v).
LaTeX
$$$(\mathrm{gaussianReal}(\mu, v)).map (\cdot \cdot c) = \mathrm{gaussianReal}(c \mu, \langle c^2, \mathrm{sq\_nonneg} \rangle * v)$$$
Lean4
/-- The map of a Gaussian distribution by multiplication by a constant is a Gaussian. -/
theorem gaussianReal_map_const_mul (c : ℝ) :
(gaussianReal μ v).map (c * ·) = gaussianReal (c * μ) (⟨c ^ 2, sq_nonneg _⟩ * v) :=
by
by_cases hv : v = 0
· simp only [hv, mul_zero, gaussianReal_zero_var]
exact Measure.map_dirac (measurable_id'.const_mul c) μ
by_cases hc : c = 0
· simp only [hc, zero_mul]
rw [Measure.map_const]
simp only [measure_univ, one_smul]
convert (gaussianReal_zero_var 0).symm
simp only [ne_eq, zero_pow, mul_eq_zero, hv, or_false, not_false_eq_true, reduceCtorEq, NNReal.mk_zero]
let e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
have he' : ∀ x, HasDerivAt e ((fun _ ↦ c⁻¹) x) x :=
by
suffices ∀ x, HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x by rwa [mul_one] at this
exact fun _ ↦ HasDerivAt.const_mul _ (hasDerivAt_id _)
change (gaussianReal μ v).map e.symm = gaussianReal (c * μ) (⟨c ^ 2, sq_nonneg _⟩ * v)
ext s' hs'
rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs', gaussianReal_apply_eq_integral _ _ s']
swap
· simp only [ne_eq, mul_eq_zero, hv, or_false]
rw [← NNReal.coe_inj]
simp [hc]
simp only [e, Homeomorph.mulLeft₀, Equiv.mulLeft₀_symm_apply, Homeomorph.toMeasurableEquiv_coe,
Homeomorph.homeomorph_mk_coe_symm, gaussianPDFReal_inv_mul hc]
congr with x
suffices |c⁻¹| * |c| = 1 by rw [← mul_assoc, this, one_mul]
rw [abs_inv, inv_mul_cancel₀]
rwa [ne_eq, abs_eq_zero]
