English
Analogous to the previous one, with a different orientation of the interval endpoints.
Русский
Аналогично предыдущему, но с иной ориентацией концов интервала.
LaTeX
$$$\\text{IsLittleO}_{lt}( \\text{difference}, \\mu) $$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict derivative in both limits 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`; let `(lb, lb')` be a pair of `intervalIntegral.FTCFilter`s
around `b`. Suppose that `f` has finite limits `ca` and `cb` at `la' ⊓ ae μ` and `lb' ⊓ ae μ`,
respectively.
Then `∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ =
∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ +
o(‖∫ x in ua..va, (1:ℝ) ∂μ‖ + ‖∫ x in ub..vb, (1:ℝ) ∂μ‖)`
as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`.
-/
theorem measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae (hab : IntervalIntegrable f μ a b)
(hmeas_a : StronglyMeasurableAtFilter f la' μ) (hmeas_b : StronglyMeasurableAtFilter f lb' μ)
(ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)) (hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 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 ∂μ) -
((∫ _ in ub t..vb t, cb ∂μ) - ∫ _ in ua t..va t, ca ∂μ)) =o[lt]
fun t => ‖∫ _ in ua t..va t, (1 : ℝ) ∂μ‖ + ‖∫ _ in ub t..vb t, (1 : ℝ) ∂μ‖ :=
by
haveI := FTCFilter.meas_gen la; haveI := FTCFilter.meas_gen lb
refine
((measure_integral_sub_linear_isLittleO_of_tendsto_ae hmeas_a ha_lim hua hva).neg_left.add_add
(measure_integral_sub_linear_isLittleO_of_tendsto_ae hmeas_b hb_lim hub hvb)).congr'
?_ EventuallyEq.rfl
have A : ∀ᶠ t in lt, IntervalIntegrable f μ (ua t) (va t) :=
ha_lim.eventually_intervalIntegrable_ae hmeas_a (FTCFilter.finiteAt_inner la) hua hva
have A' : ∀ᶠ t in lt, IntervalIntegrable f μ a (ua t) :=
ha_lim.eventually_intervalIntegrable_ae hmeas_a (FTCFilter.finiteAt_inner la)
(tendsto_const_pure.mono_right FTCFilter.pure_le) hua
have B : ∀ᶠ t in lt, IntervalIntegrable f μ (ub t) (vb t) :=
hb_lim.eventually_intervalIntegrable_ae hmeas_b (FTCFilter.finiteAt_inner lb) hub hvb
have B' : ∀ᶠ t in lt, IntervalIntegrable f μ b (ub t) :=
hb_lim.eventually_intervalIntegrable_ae hmeas_b (FTCFilter.finiteAt_inner lb)
(tendsto_const_pure.mono_right FTCFilter.pure_le) hub
filter_upwards [A, A', B, B'] with _ ua_va a_ua ub_vb b_ub
rw [← integral_interval_sub_interval_comm']
· abel
exacts [ub_vb, ua_va, b_ub.symm.trans <| hab.symm.trans a_ua]
