ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
⊢ IntegrableOn f (Ioi a)
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
⊢ IntegrableOn f (Ioi a)
have hφ : AECover (μ.restrict <| Ioi a) l _ := aecover_Iic 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 a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
⊢ IntegrableOn f (Ioi a)
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
⊢ IntegrableOn f (Ioi a)
have hfi : ∀ i, IntegrableOn f (Iic (b i)) (μ.restrict <| Ioi a) := by
  intro i
  rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
  exact hfi 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 a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
⊢ ∀ᶠ (x : ι) in l, (∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ) ≤ I → (∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂Measure.restrict μ (Ioi a)) ≤ 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 a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
⊢ IntegrableOn f (Ioi a)
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 a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
i : ι
hbi : a ≤ b i
⊢ (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I → (∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂Measure.restrict μ (Ioi a)) ≤ 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 a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
⊢ ∀ᶠ (x : ι) in l, (∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ) ≤ I → (∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂Measure.restrict μ (Ioi a)) ≤ I
filter_upwards [hb.eventually (eventually_ge_atTop a)] with i hbi
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 a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
i : ι
hbi : a ≤ b i
⊢ (∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ) ≤ I → (∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ) ≤ I
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 a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
i : ι
hbi : a ≤ b i
⊢ (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I → (∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂Measure.restrict μ (Ioi a)) ≤ I
rw [intervalIntegral.integral_of_le hbi, Measure.restrict_restrict (hφ.measurableSet i),
  inter_comm]
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 a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
i : ι
hbi : a ≤ b i
⊢ (∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ) ≤ I → (∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ) ≤ I
exact id
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
i : ι
⊢ IntegrableOn f (Iic (b 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 a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
⊢ ∀ (i : ι), IntegrableOn f (Iic (b i))
intro 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 a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
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 a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
i : ι
⊢ IntegrableOn f (Iic (b i))
rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
no goals
ι : Type u_2
E : Type u_1
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
i : ι
⊢ Integrable f
exact hfi i