no goals
ι : Type u_2
𝕜 : Type ?u.1353399
E : Type u_1
F : Type ?u.1353405
A : Type ?u.1353408
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
c ca cb : E
l l' la la' lb lb' : Filter ℝ
lt : Filter ι
μ : MeasureTheory.Measure ℝ
u v ua va ub vb : ι → ℝ
inst✝² : FTCFilter a la la'
inst✝¹ : FTCFilter b lb lb'
inst✝ : IsLocallyFiniteMeasure μ
hab : IntervalIntegrable f μ a b
hmeas : StronglyMeasurableAtFilter f lb'
hf : Tendsto f (lb' ⊓ Measure.ae μ) (𝓝 c)
hu : Tendsto u lt lb
hv : Tendsto v lt lb
⊢ (fun t => ((∫ (x : ℝ) in a..v t, f x ∂μ) - ∫ (x : ℝ) in a..u t, f x ∂μ) - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t =>
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
simpa using
  measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab stronglyMeasurableAt_bot
    hmeas ((tendsto_bot : Tendsto _ ⊥ (𝓝 (0 : E))).mono_left inf_le_left) hf
    (tendsto_const_pure : Tendsto _ _ (pure a)) tendsto_const_pure hu hv