English
For v in the interior, the second iterated derivative of cgf equals the normalized second moment of X with weight e^{vX}, i.e.
Русский
Для v внутри области вторая итерационная производная cgf равна нормированной второй моменте X с весом e^{vX}.
LaTeX
$$$\\mathrm{iteratedDeriv}_2(\\mathrm{cgf}(X,\\mu), v) = \\dfrac{\\int X(\\omega)^2 e^{v X(\\omega)} d\\mu(\\omega)}{\\mathrm{mgf}(X,\\mu)(v)} - \\bigg(\\frac{\\int X(\\omega) e^{v X(\\omega)} d\\mu(\\omega)}{\\mathrm{mgf}(X,\\mu)(v)}\\bigg)^2$ for $v \\in \\mathrm{int}(\\mathrm{integrableExpSet}(X,\\mu)).$$$
Lean4
theorem iteratedDeriv_two_cgf (h : v ∈ interior (integrableExpSet X μ)) :
iteratedDeriv 2 (cgf X μ) v = μ[fun ω ↦ (X ω) ^ 2 * exp (v * X ω)] / mgf X μ v - deriv (cgf X μ) v ^ 2 :=
by
rw [iteratedDeriv_succ, iteratedDeriv_one]
by_cases hμ : μ = 0
· simp [hμ]
have h_mem : ∀ᶠ y in 𝓝 v, y ∈ interior (integrableExpSet X μ) := isOpen_interior.eventually_mem h
have h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ μ[fun ω ↦ X ω * exp (u * X ω)] / mgf X μ u := by
filter_upwards [h_mem] with u hu using deriv_cgf hu
have h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ μ[fun ω ↦ X ω * exp (u * X ω)] := by
filter_upwards [h_mem] with u hu using deriv_mgf hu
rw [h_d_cgf.deriv_eq]
calc
deriv (fun u ↦ (∫ ω, X ω * exp (u * X ω) ∂μ) / mgf X μ u) v
_ =
(deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
(∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
mgf X μ v ^ 2 :=
by
rw [deriv_fun_div]
· rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
exact differentiableAt_iteratedDeriv_mgf h 1
· exact differentiableAt_mgf h
· exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
_ =
(deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
(∫ ω, X ω * exp (v * X ω) ∂μ) * ∫ ω, X ω * exp (v * X ω) ∂μ) /
mgf X μ v ^ 2 :=
by rw [deriv_mgf h]
_ = deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2 :=
by
rw [sub_div]
congr 1
· rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
· rw [deriv_cgf h]
ring
_ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 :=
by
congr
convert (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1
simp
