English
Scaling a random variable by a real constant c scales its evariance by c^2. Precisely, evariance(cX)μ = ENNReal.ofReal(c^2) · evariance(X) μ.
Русский
Умножение случайной величины на константу c масштабирует e-variance на c^2, то есть evariance(cX)μ = ENNReal.ofReal(c^2) · evariance(X) μ.
LaTeX
$$$$ \mathrm{evariance}(cX, \mu) = \mathrm{ENNReal}.ofReal(c^2) \cdot \mathrm{evariance}(X, \mu). $$$$
Lean4
theorem evariance_mul (c : ℝ) (X : Ω → ℝ) (μ : Measure Ω) :
evariance (fun ω => c * X ω) μ = ENNReal.ofReal (c ^ 2) * evariance X μ :=
by
rw [evariance, evariance, ← lintegral_const_mul' _ _ ENNReal.ofReal_lt_top.ne]
congr with ω
rw [integral_const_mul, ← mul_sub, enorm_mul, mul_pow, ← enorm_pow, Real.enorm_of_nonneg (sq_nonneg _)]
