no goals
ι : Type u_2
𝕜 : Type ?u.1613008
E : Type u_1
F : Type ?u.1613014
A : Type ?u.1613017
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'
inst✝ : FTCFilter a l l'
hfm : StronglyMeasurableAtFilter f l'
hf : Tendsto f (l' ⊓ Measure.ae volume) (𝓝 c)
u v : ι → ℝ
hu : Tendsto u lt l
hv : Tendsto v lt l
⊢ (fun t => (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)
simpa [integral_const] using measure_integral_sub_linear_isLittleO_of_tendsto_ae hfm hf hu hv