English
Symmetric statement to the right-hand version: the left endpoint analogue yields a similar little-o behavior as u,v approach the left limit.
Русский
Аналогично слева: для левой границы действует аналогичное поведение little-o при приближении u,v к левому пределу.
LaTeX
$$$(\\text{hab}) \\Rightarrow (\\text{hmeas}) \\Rightarrow (\\text{hf}) \\Rightarrow (\\text{hu}) \\Rightarrow (\\text{hv}) :\\; (\\int_{v}^{b} f) - (\\int_{u}^{b} f) + (v-u)\\, c = o_{lt}(v-u).$$$
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 `f` has a finite limit `c` almost surely at `la'`, then
`(∫ x in v..b, f x) - ∫ x in u..b, f x = -(v - u) • c + o(‖v - u‖)` as `u` and `v` tend to `la`.
This lemma could've been formulated using `HasStrictDerivAtFilter` if we had this definition. -/
theorem integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left (hab : IntervalIntegrable f volume a b)
(hmeas : StronglyMeasurableAtFilter f la') (hf : Tendsto f (la' ⊓ ae volume) (𝓝 c)) (hu : Tendsto u lt la)
(hv : Tendsto v lt la) : (fun t => ((∫ x in v t..b, f x) - ∫ x in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u) :=
by
simpa only [integral_const, smul_eq_mul, mul_one] using
measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left hab hmeas hf hu hv
