English
If X =ᵐ[μ] Y, then evariance(X; μ) = evariance(Y; μ).
Русский
Если X равномерно эквивалентен Y по ae-свойству относительно μ, то evariance(X; μ) = evariance(Y; μ).
LaTeX
$$$eVar[X; \\mu] = eVar[Y; \\mu]$ if $X =_{ae}^{\\mu} Y$$$
Lean4
/-- The variance of `X` under the tilted measure `μ.tilted (t * X ·)` is the second derivative of
the cumulant-generating function of `X` at `t`. -/
theorem variance_tilted_mul (ht : t ∈ interior (integrableExpSet X μ)) :
Var[X; μ.tilted (t * X ·)] = iteratedDeriv 2 (cgf X μ) t :=
by
rw [variance_eq_integral]
swap; · exact (memLp_tilted_mul ht 1).aestronglyMeasurable.aemeasurable
rw [integral_tilted_mul_self ht, iteratedDeriv_two_cgf_eq_integral ht, integral_tilted_mul_eq_mgf, ← integral_div]
simp only [smul_eq_mul]
congr with ω
ring
