ι : Type ?u.12289686
𝕜 : Type ?u.12289689
E : Type u_1
F : Type ?u.12289695
A : Type ?u.12289698
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in Ι a b, f x‖ ≤ C * abs (b - a)
ι : Type ?u.12289686
𝕜 : Type ?u.12289689
E : Type u_1
F : Type ?u.12289695
A : Type ?u.12289698
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * abs (b - a)
rw [norm_integral_eq_norm_integral_Ioc]
case h.e'_4
ι : Type ?u.12289686
𝕜 : Type ?u.12289689
E : Type u_1
F : Type ?u.12289695
A : Type ?u.12289698
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * abs (b - a) = C * ENNReal.toReal (↑↑volume (Ioc (min a b) (max a b)))

ι : Type ?u.12289686
𝕜 : Type ?u.12289689
E : Type u_1
F : Type ?u.12289695
A : Type ?u.12289698
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ↑↑volume (Ioc (min a b) (max a b)) < ⊤
ι : Type ?u.12289686
𝕜 : Type ?u.12289689
E : Type u_1
F : Type ?u.12289695
A : Type ?u.12289698
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in Ι a b, f x‖ ≤ C * abs (b - a)
convert norm_set_integral_le_of_norm_le_const_ae'' _ measurableSet_Ioc h using 1
no goals
case h.e'_4
ι : Type ?u.12289686
𝕜 : Type ?u.12289689
E : Type u_1
F : Type ?u.12289695
A : Type ?u.12289698
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * abs (b - a) = C * ENNReal.toReal (↑↑volume (Ioc (min a b) (max a b)))
rw [Real.volume_Ioc, max_sub_min_eq_abs, ENNReal.toReal_ofReal (abs_nonneg _)]
no goals
ι : Type ?u.12289686
𝕜 : Type ?u.12289689
E : Type u_1
F : Type ?u.12289695
A : Type ?u.12289698
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ↑↑volume (Ioc (min a b) (max a b)) < ⊤
simp only [Real.volume_Ioc, ENNReal.ofReal_lt_top]