theorem intervalIntegral.enorm_integral_min_max {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (f : ℝ → E) : ‖∫ (x : ℝ) in min a b..max a b, f x ∂μ‖ₑ = ‖∫ (x : ℝ) in a..b, f x ∂μ‖ₑ

theorem intervalIntegral.enorm_integral_eq_enorm_integral_uIoc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (f : ℝ → E) : ‖∫ (x : ℝ) in a..b, f x ∂μ‖ₑ = ‖∫ (x : ℝ) in Set.uIoc a b, f x ∂μ‖ₑ

theorem intervalIntegral.enorm_integral_le_lintegral_enorm_uIoc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} : ‖∫ (x : ℝ) in a..b, f x ∂μ‖ₑ ≤ ∫⁻ (x : ℝ) in Set.uIoc a b, ‖f x‖ₑ ∂μ