Unnecessary absolute value in intervalIntegral.norm_integral

Stream: mathlib4

[Geoffrey Irving]

Is there a reason docs#intervalIntegral.norm_integral_le_of_norm_le has an absolute value on the RHS?

theorem intervalIntegral.norm_integral_le_of_norm_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ℝ} (h : ∀ᵐ (t : ℝ) ∂MeasureTheory.Measure.restrict μ (Ι a b), ‖f t‖ ≤ g t) (hbound : IntervalIntegrable g μ a b) :
‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|

We know g is a.e. nonnegative from the hypotheses, and the absolute value makes it slightly harder to work with in the case I am using right now.

[Sébastien Gouëzel]

If b < a, then the right hand side without the absolute value is negative, so one definitely needs the absolute value.

[Geoffrey Irving]

Aha, I'd forgotten about reversed integrals. Thanks!

[Sébastien Gouëzel]

If you want to remove the absolute value, you could use instead docs#MeasureTheory.norm_integral_le_of_norm_le.