ι : 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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂Measure.restrict volume (Ioc a₀ 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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ IntegrableOn f (Ioc a₀ b₀)
refine (aecover_Ioc_of_Ioc ha hb).integrable_of_integral_norm_bounded I
  (fun i => (hfi i).restrict measurableSet_Ioc) (h.mono fun i hi ↦ ?_)
ι : 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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ (∫ (x : ℝ) in Ioc (a i) (b i) ∩ Ioc a₀ b₀, ‖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 a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂Measure.restrict volume (Ioc a₀ b₀)) ≤ I
rw [Measure.restrict_restrict measurableSet_Ioc]
case refine'_1.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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ ∀ (a : ℝ), OfNat.ofNat 0 a ≤ (fun x => ‖f x‖) a

case refine'_2.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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ ∀ (a_1 : ℝ), (Ioc (a i) (b i) ∩ Ioc a₀ b₀) a_1 ≤ Ioc (a i) (b i) a_1
ι : 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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ (∫ (x : ℝ) in Ioc (a i) (b i) ∩ Ioc a₀ b₀, ‖f x‖) ≤ I
refine' le_trans (set_integral_mono_set (hfi i).norm _ _) hi <;> apply ae_of_all
no goals
case refine'_1.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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ ∀ (a : ℝ), OfNat.ofNat 0 a ≤ (fun x => ‖f x‖) a
simp only [Pi.zero_apply, norm_nonneg, forall_const]
case refine'_2.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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
c : ℝ
hc : (Ioc (a i) (b i) ∩ Ioc a₀ b₀) c
⊢ Ioc (a i) (b i) c
case refine'_2.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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
⊢ ∀ (a_1 : ℝ), (Ioc (a i) (b i) ∩ Ioc a₀ b₀) a_1 ≤ Ioc (a i) (b i) a_1
intro c hc
no goals
case refine'_2.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₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
i : ι
hi : (∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖) ≤ I
c : ℝ
hc : (Ioc (a i) (b i) ∩ Ioc a₀ b₀) c
⊢ Ioc (a i) (b i) c
exact hc.1