no goals
ι : Type u_2
𝕜 : Type ?u.1622147
E : Type u_1
F : Type ?u.1622153
A : Type ?u.1622156
inst✝⁴ : NormedAddCommGroup E
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c ca cb : E
l l' la la' lb lb' : Filter ℝ
lt : Filter ι
a b z : ℝ
u v ua ub va vb : ι → ℝ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f la'
hmeas_b : StronglyMeasurableAtFilter f lb'
ha_lim : Tendsto f (la' ⊓ Measure.ae volume) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ Measure.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‖
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