ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
⊢ Integrable f
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
⊢ Integrable f
have hφ : AECover μ l _ := aecover_Ioc ha hb
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
⊢ ∀ᶠ (x : ι) in l, (∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ) ≤ I → (∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ) ≤ I
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
⊢ Integrable f
refine' hφ.integrable_of_integral_norm_bounded I hfi (h.mp _)
case h
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
ht : (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
⊢ (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ) ≤ I
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
⊢ ∀ᶠ (x : ι) in l, (∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ) ≤ I → (∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ) ≤ I
filter_upwards [ha.eventually (eventually_le_atBot 0),
  hb.eventually (eventually_ge_atTop 0)] with i hai hbi ht
no goals
case h
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
ht : (∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) ≤ I
⊢ (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ) ≤ I
rwa [← intervalIntegral.integral_of_le (hai.trans hbi)]