English
Right-endpoint version of the strict FTC-1 result with finite limits; the error term is little-o relative to the interval length.
Русский
Правая граница: аналогично, ошибка мала-o по длине интервала.
LaTeX
$$...$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict differentiability at filter in both endpoints.
If `f` is a measurable function integrable on `a..b`, `(la, la')` is an `intervalIntegral.FTCFilter`
pair around `a`, and `(lb, lb')` is an `intervalIntegral.FTCFilter` pair around `b`, and `f` has
finite limits `ca` and `cb` almost surely at `la'` and `lb'`, respectively, then
`(∫ x in va..vb, f x) - ∫ x in ua..ub, f x = (vb - ub) • cb - (va - ua) • ca +
o(‖va - ua‖ + ‖vb - ub‖)` as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`.
This lemma could've been formulated using `HasStrictFDerivAtFilter` if we had this
definition. -/
theorem integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae (hab : IntervalIntegrable f volume a b)
(hmeas_a : StronglyMeasurableAtFilter f la') (hmeas_b : StronglyMeasurableAtFilter f lb')
(ha_lim : Tendsto f (la' ⊓ ae volume) (𝓝 ca)) (hb_lim : Tendsto f (lb' ⊓ ae volume) (𝓝 cb)) (hua : Tendsto ua lt la)
(hva : Tendsto va lt la) (hub : Tendsto ub lt lb) (hvb : Tendsto vb lt lb) :
(fun t => ((∫ x in va t..vb t, f x) - ∫ x in ua t..ub t, f x) - ((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt]
fun t => ‖va t - ua t‖ + ‖vb t - ub t‖ :=
by
simpa [integral_const] using
measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab hmeas_a hmeas_b ha_lim hb_lim hua hva hub hvb
