English
Left-endpoint version: the left-endpoint analogue of the FTC sub-integral statement holds with o(μ(I)) precision.
Русский
Левая граница: аналогично левому концу иллюстрации FTC.
LaTeX
$$$(∫_{v}^{b} f - ∫_{u}^{b} f) + ∫_{u}^{v} c = o( ∫_{u}^{v} 1 )$$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict derivative in left endpoint for a locally finite
measure.
Let `f` be a measurable function integrable on `a..b`. Let `(la, la')` be a pair of
`intervalIntegral.FTCFilter`s around `a`. Suppose that `f` has a finite limit `c` at `la' ⊓ ae μ`.
Then `∫ x in v..b, f x ∂μ - ∫ x in u..b, f x ∂μ = -∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ)`
as `u` and `v` tend to `la`.
-/
theorem measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left (hab : IntervalIntegrable f μ a b)
(hmeas : StronglyMeasurableAtFilter f la' μ) (hf : Tendsto f (la' ⊓ ae μ) (𝓝 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 ∂μ) + ∫ _ in u t..v t, c ∂μ) =o[lt] fun t =>
∫ _ in u t..v t, (1 : ℝ) ∂μ :=
by
simpa using
measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab hmeas stronglyMeasurableAt_bot hf
((tendsto_bot : Tendsto _ ⊥ (𝓝 (0 : E))).mono_left inf_le_left) hu hv (tendsto_const_pure : Tendsto _ _ (pure b))
tendsto_const_pure
