ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
let φ i := Ioc (a i) (b i)
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
have hφ : AECover μ l φ := aecover_Ioc ha hb
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ (fun i => ∫ (x : ℝ) in φ i, f x ∂μ) =ᶠ[l] fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
refine' (hφ.integral_tendsto_of_countably_generated hfi).congr' _
case h
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
⊢ (∫ (x : ℝ) in Ioc (a i) (b i), f x ∂μ) = ∫ (x : ℝ) in a i..b i, f x ∂μ
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ (fun i => ∫ (x : ℝ) in φ i, f x ∂μ) =ᶠ[l] fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ
filter_upwards [ha.eventually (eventually_le_atBot 0),
  hb.eventually (eventually_ge_atTop 0)] with i hai hbi
no goals
case h
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
⊢ (∫ (x : ℝ) in Ioc (a i) (b i), f x ∂μ) = ∫ (x : ℝ) in a i..b i, f x ∂μ
exact (intervalIntegral.integral_of_le (hai.trans hbi)).symm