English
Let f: R → E be Lebesgue integrable on [a,b], and suppose that the limits ca = lim_{x→a} f(x) and cb = lim_{x→b} f(x) exist (ae-almost surely). Then the map F: R^2 → E given by F(u,v) = ∫_{u}^{v} f(x) dx is strictly differentiable at (a,b) with differential dF_{(a,b)}(h,k) = k·cb − h·ca; i.e., the derivative in the (u,v) variables is the linear map that sends (h,k) to k cb − h ca.
Русский
Пусть f: R → E интегрируема на отрезке [a,b], и существуют конечные пределы ca = lim_{x→a} f(x) и cb = lim_{x→b} f(x) почти surely. Тогда отображение F: R^2 → E, F(u,v) = ∫_{u}^{v} f(x) dx, строго гладко в окрестности точки (a,b); его производная в точке (a,b) по направлению (h,k) равна k·cb − h·ca.
LaTeX
$$$F(u,v) = \\int_{u}^{v} f(x)\\,dx,\\quad F:\\mathbb{R}^{2}\\to E,$\n$\\text{ IntervalIntegrable on }[a,b],\\ ca = \\lim_{x\\to a} f(x),\\ cb = \\lim_{x\\to b} f(x),$ \n$\\text{ then } F \\text{ is strictly differentiable at } (a,b) \\text{ with } dF_{(a,b)}(h,k) = k\\,c_b - h\\,c_a.$$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict differentiability in both endpoints.
If `f : ℝ → E` is integrable on `a..b` and `f x` has finite limits `ca` and `cb` almost surely as
`x` tends to `a` and `b`, respectively, then
`(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)`
in the sense of strict differentiability. -/
theorem integral_hasStrictFDerivAt_of_tendsto_ae (hf : IntervalIntegrable f volume a b)
(hmeas_a : StronglyMeasurableAtFilter f (𝓝 a)) (hmeas_b : StronglyMeasurableAtFilter f (𝓝 b))
(ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)) (hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)) :
HasStrictFDerivAt (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca)
(a, b) :=
by
have :=
integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hf hmeas_a hmeas_b ha hb
(continuous_snd.fst.tendsto ((a, b), (a, b))) (continuous_fst.fst.tendsto ((a, b), (a, b)))
(continuous_snd.snd.tendsto ((a, b), (a, b))) (continuous_fst.snd.tendsto ((a, b), (a, b)))
refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_
· simp [sub_smul]
· exact isBigO_fst_prod.norm_left.add isBigO_snd_prod.norm_left
