English
If t>0 and X has zero mean under μ and t lies in a suitable interval, there exists a point u in (0,t) such that cgf(X, μ; t) equals (iteratedDeriv_2 (cgf X μ) u) t^2/2.
Русский
Если t>0 и μ[X]=0, тогда существует u∈(0,t) такое, что cgf(X,μ)(t) = (iteratedDeriv_2 (cgf X μ) u) t^2/2.
LaTeX
$$$\\exists u\\in(0,t),\\quad \\mathrm{cgf}(X,\\mu)(t) = (\\mathrm{iteratedDeriv}_2(\\mathrm{cgf}(X,\\mu), u)) \\frac{t^2}{2}.$$$
Lean4
theorem exists_cgf_eq_iteratedDeriv_two_cgf_mul [IsZeroOrProbabilityMeasure μ] (ht : 0 < t) (hc : μ[X] = 0)
(hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)) :
∃ u ∈ Set.Ioo 0 t, cgf X μ t = (iteratedDeriv 2 (cgf X μ) u) * t ^ 2 / 2 :=
by
have hu : UniqueDiffOn ℝ (Set.Icc 0 t) := uniqueDiffOn_Icc ht
rw [← sub_zero (cgf X μ t)]
nth_rw 3 [← sub_zero t]
convert taylor_mean_remainder_lagrange_iteratedDeriv ht ((analyticOn_cgf.mono hs).contDiffOn hu)
have hd : derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0 :=
by
convert (analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _
· simpa [hc] using (deriv_cgf_zero (hs ⟨le_refl 0, le_of_lt ht⟩)).symm
· exact hu 0 ⟨le_refl 0, le_of_lt ht⟩
simp [hd]
