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