Documentation

Mathlib.MeasureTheory.Integral.IntervalIntegral

Integral over an interval #

In this file we define ∫ x in a..b, f x ∂μ to be ∫ x in Ioc a b, f x ∂μ if a ≤ b and -∫ x in Ioc b a, f x ∂μ if b ≤ a.

Implementation notes #

Avoiding if, min, and max #

In order to avoid ifs in the definition, we define IntervalIntegrable f μ a b as integrable_on f (Ioc a b) μ ∧ integrable_on f (Ioc b a) μ. For any a, b one of these intervals is empty and the other coincides with Set.uIoc a b = Set.Ioc (min a b) (max a b).

Similarly, we define ∫ x in a..b, f x ∂μ to be ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ. Again, for any a, b one of these integrals is zero, and the other gives the expected result.

This way some properties can be translated from integrals over sets without dealing with the cases a ≤ b and b ≤ a separately.

Choice of the interval #

We use integral over Set.uIoc a b = Set.Ioc (min a b) (max a b) instead of one of the other three possible intervals with the same endpoints for two reasons:

Tags #

integral

Integrability on an interval #

def IntervalIntegrable {E : Type u_3} [NormedAddCommGroup E] (f : E) (μ : MeasureTheory.Measure ) (a : ) (b : ) :

A function f is called interval integrable with respect to a measure μ on an unordered interval a..b if it is integrable on both intervals (a, b] and (b, a]. One of these intervals is always empty, so this property is equivalent to f being integrable on (min a b, max a b].

Equations
Instances For

    Basic iff's for IntervalIntegrable #

    theorem intervalIntegrable_iff {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {μ : MeasureTheory.Measure } :

    A function is interval integrable with respect to a given measure μ on a..b if and only if it is integrable on uIoc a b with respect to μ. This is an equivalent definition of IntervalIntegrable.

    theorem IntervalIntegrable.def' {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {μ : MeasureTheory.Measure } (h : IntervalIntegrable f μ a b) :

    If a function is interval integrable with respect to a given measure μ on a..b then it is integrable on uIoc a b with respect to μ.

    If a function is integrable with respect to a given measure μ then it is interval integrable with respect to μ on uIcc a b.

    theorem intervalIntegrable_const_iff {E : Type u_3} [NormedAddCommGroup E] {a : } {b : } {μ : MeasureTheory.Measure } {c : E} :
    IntervalIntegrable (fun (x : ) => c) μ a b c = 0 μ (Ι a b) <
    @[simp]

    Basic properties of interval integrability #

    theorem IntervalIntegrable.symm {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {μ : MeasureTheory.Measure } (h : IntervalIntegrable f μ a b) :
    @[simp]
    theorem IntervalIntegrable.refl {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {μ : MeasureTheory.Measure } :
    theorem IntervalIntegrable.trans {E : Type u_3} [NormedAddCommGroup E] {f : E} {μ : MeasureTheory.Measure } {a : } {b : } {c : } (hab : IntervalIntegrable f μ a b) (hbc : IntervalIntegrable f μ b c) :
    theorem IntervalIntegrable.trans_iterate_Ico {E : Type u_3} [NormedAddCommGroup E] {f : E} {μ : MeasureTheory.Measure } {a : } {m : } {n : } (hmn : m n) (hint : kSet.Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) :
    IntervalIntegrable f μ (a m) (a n)
    theorem IntervalIntegrable.trans_iterate {E : Type u_3} [NormedAddCommGroup E] {f : E} {μ : MeasureTheory.Measure } {a : } {n : } (hint : k < n, IntervalIntegrable f μ (a k) (a (k + 1))) :
    IntervalIntegrable f μ (a 0) (a n)
    theorem IntervalIntegrable.neg {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {μ : MeasureTheory.Measure } (h : IntervalIntegrable f μ a b) :
    theorem IntervalIntegrable.norm {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {μ : MeasureTheory.Measure } (h : IntervalIntegrable f μ a b) :
    IntervalIntegrable (fun (x : ) => f x) μ a b
    theorem IntervalIntegrable.abs {a : } {b : } {μ : MeasureTheory.Measure } {f : } (h : IntervalIntegrable f μ a b) :
    IntervalIntegrable (fun (x : ) => |f x|) μ a b
    theorem IntervalIntegrable.mono {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {c : } {d : } {μ : MeasureTheory.Measure } {ν : MeasureTheory.Measure } (hf : IntervalIntegrable f ν a b) (h1 : Set.uIcc c d Set.uIcc a b) (h2 : μ ν) :
    theorem IntervalIntegrable.mono_measure {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {μ : MeasureTheory.Measure } {ν : MeasureTheory.Measure } (hf : IntervalIntegrable f ν a b) (h : μ ν) :
    theorem IntervalIntegrable.mono_set {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {c : } {d : } {μ : MeasureTheory.Measure } (hf : IntervalIntegrable f μ a b) (h : Set.uIcc c d Set.uIcc a b) :
    theorem IntervalIntegrable.mono_set_ae {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {c : } {d : } {μ : MeasureTheory.Measure } (hf : IntervalIntegrable f μ a b) (h : Ι c d ≤ᶠ[MeasureTheory.Measure.ae μ] Ι a b) :
    theorem IntervalIntegrable.mono_set' {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {c : } {d : } {μ : MeasureTheory.Measure } (hf : IntervalIntegrable f μ a b) (hsub : Ι c d Ι a b) :
    theorem IntervalIntegrable.mono_fun {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] {f : E} {a : } {b : } {μ : MeasureTheory.Measure } [NormedAddCommGroup F] {g : F} (hf : IntervalIntegrable f μ a b) (hgm : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.restrict μ (Ι a b))) (hle : (fun (x : ) => g x) ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Ι a b))] fun (x : ) => f x) :
    theorem IntervalIntegrable.smul {𝕜 : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedField 𝕜] [NormedSpace 𝕜 E] {f : E} {a : } {b : } {μ : MeasureTheory.Measure } (h : IntervalIntegrable f μ a b) (r : 𝕜) :
    IntervalIntegrable (r f) μ a b
    @[simp]
    theorem IntervalIntegrable.add {E : Type u_3} [NormedAddCommGroup E] {f : E} {g : E} {a : } {b : } {μ : MeasureTheory.Measure } (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) :
    IntervalIntegrable (fun (x : ) => f x + g x) μ a b
    @[simp]
    theorem IntervalIntegrable.sub {E : Type u_3} [NormedAddCommGroup E] {f : E} {g : E} {a : } {b : } {μ : MeasureTheory.Measure } (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) :
    IntervalIntegrable (fun (x : ) => f x - g x) μ a b
    theorem IntervalIntegrable.sum {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] {a : } {b : } {μ : MeasureTheory.Measure } (s : Finset ι) {f : ιE} (h : is, IntervalIntegrable (f i) μ a b) :
    IntervalIntegrable (Finset.sum s fun (i : ι) => f i) μ a b
    theorem IntervalIntegrable.mul_continuousOn {A : Type u_5} [NormedRing A] {a : } {b : } {μ : MeasureTheory.Measure } {f : A} {g : A} (hf : IntervalIntegrable f μ a b) (hg : ContinuousOn g (Set.uIcc a b)) :
    IntervalIntegrable (fun (x : ) => f x * g x) μ a b
    theorem IntervalIntegrable.continuousOn_mul {A : Type u_5} [NormedRing A] {a : } {b : } {μ : MeasureTheory.Measure } {f : A} {g : A} (hf : IntervalIntegrable f μ a b) (hg : ContinuousOn g (Set.uIcc a b)) :
    IntervalIntegrable (fun (x : ) => g x * f x) μ a b
    @[simp]
    theorem IntervalIntegrable.const_mul {A : Type u_5} [NormedRing A] {a : } {b : } {μ : MeasureTheory.Measure } {f : A} (hf : IntervalIntegrable f μ a b) (c : A) :
    IntervalIntegrable (fun (x : ) => c * f x) μ a b
    @[simp]
    theorem IntervalIntegrable.mul_const {A : Type u_5} [NormedRing A] {a : } {b : } {μ : MeasureTheory.Measure } {f : A} (hf : IntervalIntegrable f μ a b) (c : A) :
    IntervalIntegrable (fun (x : ) => f x * c) μ a b
    @[simp]
    theorem IntervalIntegrable.div_const {a : } {b : } {μ : MeasureTheory.Measure } {𝕜 : Type u_6} {f : 𝕜} [NormedField 𝕜] (h : IntervalIntegrable f μ a b) (c : 𝕜) :
    IntervalIntegrable (fun (x : ) => f x / c) μ a b
    theorem IntervalIntegrable.comp_mul_left {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (c : ) :
    IntervalIntegrable (fun (x : ) => f (c * x)) MeasureTheory.volume (a / c) (b / c)
    theorem IntervalIntegrable.comp_mul_left_iff {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } {c : } (hc : c 0) :
    IntervalIntegrable (fun (x : ) => f (c * x)) MeasureTheory.volume (a / c) (b / c) IntervalIntegrable f MeasureTheory.volume a b
    theorem IntervalIntegrable.comp_mul_right {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (c : ) :
    IntervalIntegrable (fun (x : ) => f (x * c)) MeasureTheory.volume (a / c) (b / c)
    theorem IntervalIntegrable.comp_add_right {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (c : ) :
    IntervalIntegrable (fun (x : ) => f (x + c)) MeasureTheory.volume (a - c) (b - c)
    theorem IntervalIntegrable.comp_add_left {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (c : ) :
    IntervalIntegrable (fun (x : ) => f (c + x)) MeasureTheory.volume (a - c) (b - c)
    theorem IntervalIntegrable.comp_sub_right {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (c : ) :
    IntervalIntegrable (fun (x : ) => f (x - c)) MeasureTheory.volume (a + c) (b + c)
    theorem IntervalIntegrable.iff_comp_neg {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } :
    IntervalIntegrable f MeasureTheory.volume a b IntervalIntegrable (fun (x : ) => f (-x)) MeasureTheory.volume (-a) (-b)
    theorem IntervalIntegrable.comp_sub_left {E : Type u_3} [NormedAddCommGroup E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (c : ) :
    IntervalIntegrable (fun (x : ) => f (c - x)) MeasureTheory.volume (c - a) (c - b)

    Continuous functions are interval integrable #

    A continuous function on is IntervalIntegrable with respect to any locally finite measure ν on ℝ.

    Monotone and antitone functions are integral integrable #

    theorem Filter.Tendsto.eventually_intervalIntegrable_ae {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] {f : E} {μ : MeasureTheory.Measure } {l : Filter } {l' : Filter } (hfm : StronglyMeasurableAtFilter f l' μ) [Filter.TendstoIxxClass Set.Ioc l l'] [Filter.IsMeasurablyGenerated l'] (hμ : MeasureTheory.Measure.FiniteAtFilter μ l') {c : E} (hf : Filter.Tendsto f (l' MeasureTheory.Measure.ae μ) (nhds c)) {u : ι} {v : ι} {lt : Filter ι} (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) :
    ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)

    Let l' be a measurably generated filter; let l be a of filter such that each s ∈ l' eventually includes Ioc u v as both u and v tend to l. Let μ be a measure finite at l'.

    Suppose that f : ℝ → E has a finite limit at l' ⊓ μ.ae. Then f is interval integrable on u..v provided that both u and v tend to l.

    Typeclass instances allow Lean to find l' based on l but not vice versa, so apply Tendsto.eventually_intervalIntegrable_ae will generate goals Filter and TendstoIxxClass Ioc ?m_1 l'.

    theorem Filter.Tendsto.eventually_intervalIntegrable {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] {f : E} {μ : MeasureTheory.Measure } {l : Filter } {l' : Filter } (hfm : StronglyMeasurableAtFilter f l' μ) [Filter.TendstoIxxClass Set.Ioc l l'] [Filter.IsMeasurablyGenerated l'] (hμ : MeasureTheory.Measure.FiniteAtFilter μ l') {c : E} (hf : Filter.Tendsto f l' (nhds c)) {u : ι} {v : ι} {lt : Filter ι} (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) :
    ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)

    Let l' be a measurably generated filter; let l be a of filter such that each s ∈ l' eventually includes Ioc u v as both u and v tend to l. Let μ be a measure finite at l'.

    Suppose that f : ℝ → E has a finite limit at l. Then f is interval integrable on u..v provided that both u and v tend to l.

    Typeclass instances allow Lean to find l' based on l but not vice versa, so apply Tendsto.eventually_intervalIntegrable will generate goals Filter and TendstoIxxClass Ioc ?m_1 l'.

    Interval integral: definition and basic properties #

    In this section we define ∫ x in a..b, f x ∂μ as ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ and prove some basic properties.

    def intervalIntegral {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] (f : E) (a : ) (b : ) (μ : MeasureTheory.Measure ) :
    E

    The interval integral ∫ x in a..b, f x ∂μ is defined as ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ. If a ≤ b, then it equals ∫ x in Ioc a b, f x ∂μ, otherwise it equals -∫ x in Ioc b a, f x ∂μ.

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Pretty printer defined by notation3 command.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Pretty printer defined by notation3 command.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem intervalIntegral.integral_zero {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {μ : MeasureTheory.Measure } :
              ∫ (x : ) in a..b, 0μ = 0
              theorem intervalIntegral.integral_of_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } (h : a b) :
              ∫ (x : ) in a..b, f xμ = ∫ (x : ) in Set.Ioc a b, f xμ
              @[simp]
              theorem intervalIntegral.integral_same {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {f : E} {μ : MeasureTheory.Measure } :
              ∫ (x : ) in a..a, f xμ = 0
              theorem intervalIntegral.integral_symm {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {μ : MeasureTheory.Measure } (a : ) (b : ) :
              ∫ (x : ) in b..a, f xμ = -∫ (x : ) in a..b, f xμ
              theorem intervalIntegral.integral_of_ge {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } (h : b a) :
              ∫ (x : ) in a..b, f xμ = -∫ (x : ) in Set.Ioc b a, f xμ
              theorem intervalIntegral.intervalIntegral_eq_integral_uIoc {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] (f : E) (a : ) (b : ) (μ : MeasureTheory.Measure ) :
              ∫ (x : ) in a..b, f xμ = (if a b then 1 else -1) ∫ (x : ) in Ι a b, f xμ
              theorem intervalIntegral.norm_intervalIntegral_eq {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] (f : E) (a : ) (b : ) (μ : MeasureTheory.Measure ) :
              ∫ (x : ) in a..b, f xμ = ∫ (x : ) in Ι a b, f xμ
              theorem intervalIntegral.abs_intervalIntegral_eq (f : ) (a : ) (b : ) (μ : MeasureTheory.Measure ) :
              |∫ (x : ) in a..b, f xμ| = |∫ (x : ) in Ι a b, f xμ|
              theorem intervalIntegral.integral_cases {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure } (f : E) (a : ) (b : ) :
              ∫ (x : ) in a..b, f xμ {∫ (x : ) in Ι a b, f xμ, -∫ (x : ) in Ι a b, f xμ}
              theorem intervalIntegral.integral_undef {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } (h : ¬IntervalIntegrable f μ a b) :
              ∫ (x : ) in a..b, f xμ = 0
              theorem intervalIntegral.intervalIntegrable_of_integral_ne_zero {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } (h : ∫ (x : ) in a..b, f xμ 0) :
              theorem intervalIntegral.norm_integral_min_max {E : Type u_3} [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.norm_integral_eq_norm_integral_Ioc {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {μ : MeasureTheory.Measure } (f : E) :
              ∫ (x : ) in a..b, f xμ = ∫ (x : ) in Ι a b, f xμ
              theorem intervalIntegral.abs_integral_eq_abs_integral_uIoc {a : } {b : } {μ : MeasureTheory.Measure } (f : ) :
              |∫ (x : ) in a..b, f xμ| = |∫ (x : ) in Ι a b, f xμ|
              theorem intervalIntegral.norm_integral_le_integral_norm_Ioc {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } :
              ∫ (x : ) in a..b, f xμ ∫ (x : ) in Ι a b, f xμ
              theorem intervalIntegral.norm_integral_le_abs_integral_norm {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } :
              ∫ (x : ) in a..b, f xμ |∫ (x : ) in a..b, f xμ|
              theorem intervalIntegral.norm_integral_le_integral_norm {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } (h : a b) :
              ∫ (x : ) in a..b, f xμ ∫ (x : ) in a..b, f xμ
              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μ|
              theorem intervalIntegral.norm_integral_le_of_norm_le_const_ae {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {C : } {f : E} (h : ∀ᵐ (x : ), x Ι a bf x C) :
              ∫ (x : ) in a..b, f x C * |b - a|
              theorem intervalIntegral.norm_integral_le_of_norm_le_const {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {C : } {f : E} (h : xΙ a b, f x C) :
              ∫ (x : ) in a..b, f x C * |b - a|
              @[simp]
              theorem intervalIntegral.integral_add {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {g : E} {μ : MeasureTheory.Measure } (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) :
              ∫ (x : ) in a..b, f x + g xμ = ∫ (x : ) in a..b, f xμ + ∫ (x : ) in a..b, g xμ
              theorem intervalIntegral.integral_finset_sum {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {μ : MeasureTheory.Measure } {ι : Type u_6} {s : Finset ι} {f : ιE} (h : is, IntervalIntegrable (f i) μ a b) :
              ∫ (x : ) in a..b, Finset.sum s fun (i : ι) => f i xμ = Finset.sum s fun (i : ι) => ∫ (x : ) in a..b, f i xμ
              @[simp]
              theorem intervalIntegral.integral_neg {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } :
              ∫ (x : ) in a..b, -f xμ = -∫ (x : ) in a..b, f xμ
              @[simp]
              theorem intervalIntegral.integral_sub {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {g : E} {μ : MeasureTheory.Measure } (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) :
              ∫ (x : ) in a..b, f x - g xμ = ∫ (x : ) in a..b, f xμ - ∫ (x : ) in a..b, g xμ
              @[simp]
              theorem intervalIntegral.integral_smul {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {μ : MeasureTheory.Measure } {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 E] (r : 𝕜) (f : E) :
              ∫ (x : ) in a..b, r f xμ = r ∫ (x : ) in a..b, f xμ
              @[simp]
              theorem intervalIntegral.integral_smul_const {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } {μ : MeasureTheory.Measure } {𝕜 : Type u_6} [RCLike 𝕜] [NormedSpace 𝕜 E] (f : 𝕜) (c : E) :
              ∫ (x : ) in a..b, f x cμ = (∫ (x : ) in a..b, f xμ) c
              @[simp]
              theorem intervalIntegral.integral_const_mul {a : } {b : } {μ : MeasureTheory.Measure } {𝕜 : Type u_6} [RCLike 𝕜] (r : 𝕜) (f : 𝕜) :
              ∫ (x : ) in a..b, r * f xμ = r * ∫ (x : ) in a..b, f xμ
              @[simp]
              theorem intervalIntegral.integral_mul_const {a : } {b : } {μ : MeasureTheory.Measure } {𝕜 : Type u_6} [RCLike 𝕜] (r : 𝕜) (f : 𝕜) :
              ∫ (x : ) in a..b, f x * rμ = (∫ (x : ) in a..b, f xμ) * r
              @[simp]
              theorem intervalIntegral.integral_div {a : } {b : } {μ : MeasureTheory.Measure } {𝕜 : Type u_6} [RCLike 𝕜] (r : 𝕜) (f : 𝕜) :
              ∫ (x : ) in a..b, f x / rμ = (∫ (x : ) in a..b, f xμ) / r
              theorem intervalIntegral.integral_const' {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } {μ : MeasureTheory.Measure } (c : E) :
              ∫ (x : ) in a..b, cμ = ((μ (Set.Ioc a b)).toReal - (μ (Set.Ioc b a)).toReal) c
              @[simp]
              theorem intervalIntegral.integral_const {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (c : E) :
              ∫ (x : ) in a..b, c = (b - a) c
              theorem intervalIntegral.integral_smul_measure {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } (c : ENNReal) :
              ∫ (x : ) in a..b, f xc μ = c.toReal ∫ (x : ) in a..b, f xμ
              theorem RCLike.interval_integral_ofReal {𝕜 : Type u_6} [RCLike 𝕜] {a : } {b : } {μ : MeasureTheory.Measure } {f : } :
              ∫ (x : ) in a..b, (f x)μ = (∫ (x : ) in a..b, f xμ)
              theorem intervalIntegral.integral_ofReal {a : } {b : } {μ : MeasureTheory.Measure } {f : } :
              ∫ (x : ) in a..b, (f x)μ = (∫ (x : ) in a..b, f xμ)
              theorem ContinuousLinearMap.intervalIntegral_apply {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {μ : MeasureTheory.Measure } [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a : } {b : } {φ : F →L[𝕜] E} (hφ : IntervalIntegrable φ μ a b) (v : F) :
              (∫ (x : ) in a..b, φ xμ) v = ∫ (x : ) in a..b, (φ x) vμ
              theorem ContinuousLinearMap.intervalIntegral_comp_comm {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } {μ : MeasureTheory.Measure } {f : E} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace F] [CompleteSpace F] (L : E →L[𝕜] F) (hf : IntervalIntegrable f μ a b) :
              ∫ (x : ) in a..b, L (f x)μ = L (∫ (x : ) in a..b, f xμ)

              Basic arithmetic #

              Includes addition, scalar multiplication and affine transformations.

              Porting note: some @[simp] attributes in this section were removed to make the simpNF linter happy. TODO: find out if these lemmas are actually good or bad simp lemmas.

              theorem intervalIntegral.integral_comp_mul_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) :
              ∫ (x : ) in a..b, f (x * c) = c⁻¹ ∫ (x : ) in a * c..b * c, f x
              theorem intervalIntegral.smul_integral_comp_mul_right {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) :
              c ∫ (x : ) in a..b, f (x * c) = ∫ (x : ) in a * c..b * c, f x
              theorem intervalIntegral.integral_comp_mul_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) :
              ∫ (x : ) in a..b, f (c * x) = c⁻¹ ∫ (x : ) in c * a..c * b, f x
              theorem intervalIntegral.smul_integral_comp_mul_left {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) :
              c ∫ (x : ) in a..b, f (c * x) = ∫ (x : ) in c * a..c * b, f x
              theorem intervalIntegral.integral_comp_div {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) :
              ∫ (x : ) in a..b, f (x / c) = c ∫ (x : ) in a / c..b / c, f x
              theorem intervalIntegral.inv_smul_integral_comp_div {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) :
              c⁻¹ ∫ (x : ) in a..b, f (x / c) = ∫ (x : ) in a / c..b / c, f x
              theorem intervalIntegral.integral_comp_add_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } (f : E) (d : ) :
              ∫ (x : ) in a..b, f (x + d) = ∫ (x : ) in a + d..b + d, f x
              theorem intervalIntegral.integral_comp_add_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } (f : E) (d : ) :
              ∫ (x : ) in a..b, f (d + x) = ∫ (x : ) in d + a..d + b, f x
              theorem intervalIntegral.integral_comp_mul_add {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) (d : ) :
              ∫ (x : ) in a..b, f (c * x + d) = c⁻¹ ∫ (x : ) in c * a + d..c * b + d, f x
              theorem intervalIntegral.smul_integral_comp_mul_add {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (d : ) :
              c ∫ (x : ) in a..b, f (c * x + d) = ∫ (x : ) in c * a + d..c * b + d, f x
              theorem intervalIntegral.integral_comp_add_mul {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) (d : ) :
              ∫ (x : ) in a..b, f (d + c * x) = c⁻¹ ∫ (x : ) in d + c * a..d + c * b, f x
              theorem intervalIntegral.smul_integral_comp_add_mul {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (d : ) :
              c ∫ (x : ) in a..b, f (d + c * x) = ∫ (x : ) in d + c * a..d + c * b, f x
              theorem intervalIntegral.integral_comp_div_add {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) (d : ) :
              ∫ (x : ) in a..b, f (x / c + d) = c ∫ (x : ) in a / c + d..b / c + d, f x
              theorem intervalIntegral.inv_smul_integral_comp_div_add {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (d : ) :
              c⁻¹ ∫ (x : ) in a..b, f (x / c + d) = ∫ (x : ) in a / c + d..b / c + d, f x
              theorem intervalIntegral.integral_comp_add_div {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) (d : ) :
              ∫ (x : ) in a..b, f (d + x / c) = c ∫ (x : ) in d + a / c..d + b / c, f x
              theorem intervalIntegral.inv_smul_integral_comp_add_div {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (d : ) :
              c⁻¹ ∫ (x : ) in a..b, f (d + x / c) = ∫ (x : ) in d + a / c..d + b / c, f x
              theorem intervalIntegral.integral_comp_mul_sub {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) (d : ) :
              ∫ (x : ) in a..b, f (c * x - d) = c⁻¹ ∫ (x : ) in c * a - d..c * b - d, f x
              theorem intervalIntegral.smul_integral_comp_mul_sub {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (d : ) :
              c ∫ (x : ) in a..b, f (c * x - d) = ∫ (x : ) in c * a - d..c * b - d, f x
              theorem intervalIntegral.integral_comp_sub_mul {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) (d : ) :
              ∫ (x : ) in a..b, f (d - c * x) = c⁻¹ ∫ (x : ) in d - c * b..d - c * a, f x
              theorem intervalIntegral.smul_integral_comp_sub_mul {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (d : ) :
              c ∫ (x : ) in a..b, f (d - c * x) = ∫ (x : ) in d - c * b..d - c * a, f x
              theorem intervalIntegral.integral_comp_div_sub {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) (d : ) :
              ∫ (x : ) in a..b, f (x / c - d) = c ∫ (x : ) in a / c - d..b / c - d, f x
              theorem intervalIntegral.inv_smul_integral_comp_div_sub {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (d : ) :
              c⁻¹ ∫ (x : ) in a..b, f (x / c - d) = ∫ (x : ) in a / c - d..b / c - d, f x
              theorem intervalIntegral.integral_comp_sub_div {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } (f : E) (hc : c 0) (d : ) :
              ∫ (x : ) in a..b, f (d - x / c) = c ∫ (x : ) in d - b / c..d - a / c, f x
              theorem intervalIntegral.inv_smul_integral_comp_sub_div {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (d : ) :
              c⁻¹ ∫ (x : ) in a..b, f (d - x / c) = ∫ (x : ) in d - b / c..d - a / c, f x
              theorem intervalIntegral.integral_comp_sub_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } (f : E) (d : ) :
              ∫ (x : ) in a..b, f (x - d) = ∫ (x : ) in a - d..b - d, f x
              theorem intervalIntegral.integral_comp_sub_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } (f : E) (d : ) :
              ∫ (x : ) in a..b, f (d - x) = ∫ (x : ) in d - b..d - a, f x
              theorem intervalIntegral.integral_comp_neg {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } (f : E) :
              ∫ (x : ) in a..b, f (-x) = ∫ (x : ) in -b..-a, f x

              Integral is an additive function of the interval #

              In this section we prove that ∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ as well as a few other identities trivially equivalent to this one. We also prove that ∫ x in a..b, f x ∂μ = ∫ x, f x ∂μ provided that support f ⊆ Ioc a b.

              theorem intervalIntegral.integral_congr {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {μ : MeasureTheory.Measure } {a : } {b : } (h : Set.EqOn f g (Set.uIcc a b)) :
              ∫ (x : ) in a..b, f xμ = ∫ (x : ) in a..b, g xμ

              If two functions are equal in the relevant interval, their interval integrals are also equal.

              theorem intervalIntegral.integral_add_adjacent_intervals_cancel {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } {f : E} {μ : MeasureTheory.Measure } (hab : IntervalIntegrable f μ a b) (hbc : IntervalIntegrable f μ b c) :
              ∫ (x : ) in a..b, f xμ + ∫ (x : ) in b..c, f xμ + ∫ (x : ) in c..a, f xμ = 0
              theorem intervalIntegral.integral_add_adjacent_intervals {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } {f : E} {μ : MeasureTheory.Measure } (hab : IntervalIntegrable f μ a b) (hbc : IntervalIntegrable f μ b c) :
              ∫ (x : ) in a..b, f xμ + ∫ (x : ) in b..c, f xμ = ∫ (x : ) in a..c, f xμ
              theorem intervalIntegral.sum_integral_adjacent_intervals_Ico {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {μ : MeasureTheory.Measure } {a : } {m : } {n : } (hmn : m n) (hint : kSet.Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) :
              (Finset.sum (Finset.Ico m n) fun (k : ) => ∫ (x : ) in a k..a (k + 1), f xμ) = ∫ (x : ) in a m..a n, f xμ
              theorem intervalIntegral.sum_integral_adjacent_intervals {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {μ : MeasureTheory.Measure } {a : } {n : } (hint : k < n, IntervalIntegrable f μ (a k) (a (k + 1))) :
              (Finset.sum (Finset.range n) fun (k : ) => ∫ (x : ) in a k..a (k + 1), f xμ) = ∫ (x : ) in a 0 ..a n, f xμ
              theorem intervalIntegral.integral_interval_sub_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } {f : E} {μ : MeasureTheory.Measure } (hab : IntervalIntegrable f μ a b) (hac : IntervalIntegrable f μ a c) :
              ∫ (x : ) in a..b, f xμ - ∫ (x : ) in a..c, f xμ = ∫ (x : ) in c..b, f xμ
              theorem intervalIntegral.integral_interval_add_interval_comm {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } {d : } {f : E} {μ : MeasureTheory.Measure } (hab : IntervalIntegrable f μ a b) (hcd : IntervalIntegrable f μ c d) (hac : IntervalIntegrable f μ a c) :
              ∫ (x : ) in a..b, f xμ + ∫ (x : ) in c..d, f xμ = ∫ (x : ) in a..d, f xμ + ∫ (x : ) in c..b, f xμ
              theorem intervalIntegral.integral_interval_sub_interval_comm {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } {d : } {f : E} {μ : MeasureTheory.Measure } (hab : IntervalIntegrable f μ a b) (hcd : IntervalIntegrable f μ c d) (hac : IntervalIntegrable f μ a c) :
              ∫ (x : ) in a..b, f xμ - ∫ (x : ) in c..d, f xμ = ∫ (x : ) in a..c, f xμ - ∫ (x : ) in b..d, f xμ
              theorem intervalIntegral.integral_interval_sub_interval_comm' {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {c : } {d : } {f : E} {μ : MeasureTheory.Measure } (hab : IntervalIntegrable f μ a b) (hcd : IntervalIntegrable f μ c d) (hac : IntervalIntegrable f μ a c) :
              ∫ (x : ) in a..b, f xμ - ∫ (x : ) in c..d, f xμ = ∫ (x : ) in d..b, f xμ - ∫ (x : ) in c..a, f xμ
              theorem intervalIntegral.integral_Iic_sub_Iic {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } (ha : MeasureTheory.IntegrableOn f (Set.Iic a) μ) (hb : MeasureTheory.IntegrableOn f (Set.Iic b) μ) :
              ∫ (x : ) in Set.Iic b, f xμ - ∫ (x : ) in Set.Iic a, f xμ = ∫ (x : ) in a..b, f xμ
              theorem intervalIntegral.integral_Iic_add_Ioi {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {b : } {f : E} {μ : MeasureTheory.Measure } (h_left : MeasureTheory.IntegrableOn f (Set.Iic b) μ) (h_right : MeasureTheory.IntegrableOn f (Set.Ioi b) μ) :
              ∫ (x : ) in Set.Iic b, f xμ + ∫ (x : ) in Set.Ioi b, f xμ = ∫ (x : ), f xμ
              theorem intervalIntegral.integral_Iio_add_Ici {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {b : } {f : E} {μ : MeasureTheory.Measure } (h_left : MeasureTheory.IntegrableOn f (Set.Iio b) μ) (h_right : MeasureTheory.IntegrableOn f (Set.Ici b) μ) :
              ∫ (x : ) in Set.Iio b, f xμ + ∫ (x : ) in Set.Ici b, f xμ = ∫ (x : ), f xμ
              theorem intervalIntegral.integral_const_of_cdf {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace E] {a : } {b : } {μ : MeasureTheory.Measure } [MeasureTheory.IsFiniteMeasure μ] (c : E) :
              ∫ (x : ) in a..b, cμ = ((μ (Set.Iic b)).toReal - (μ (Set.Iic a)).toReal) c

              If μ is a finite measure then ∫ x in a..b, c ∂μ = (μ (Iic b) - μ (Iic a)) • c.

              theorem intervalIntegral.integral_eq_integral_of_support_subset {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {μ : MeasureTheory.Measure } {a : } {b : } (h : Function.support f Set.Ioc a b) :
              ∫ (x : ) in a..b, f xμ = ∫ (x : ), f xμ
              theorem intervalIntegral.integral_congr_ae' {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {g : E} {μ : MeasureTheory.Measure } (h : ∀ᵐ (x : ) ∂μ, x Set.Ioc a bf x = g x) (h' : ∀ᵐ (x : ) ∂μ, x Set.Ioc b af x = g x) :
              ∫ (x : ) in a..b, f xμ = ∫ (x : ) in a..b, g xμ
              theorem intervalIntegral.integral_congr_ae {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {g : E} {μ : MeasureTheory.Measure } (h : ∀ᵐ (x : ) ∂μ, x Ι a bf x = g x) :
              ∫ (x : ) in a..b, f xμ = ∫ (x : ) in a..b, g xμ
              theorem intervalIntegral.integral_zero_ae {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } {f : E} {μ : MeasureTheory.Measure } (h : ∀ᵐ (x : ) ∂μ, x Ι a bf x = 0) :
              ∫ (x : ) in a..b, f xμ = 0
              theorem intervalIntegral.integral_indicator {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {μ : MeasureTheory.Measure } {a₁ : } {a₂ : } {a₃ : } (h : a₂ Set.Icc a₁ a₃) :
              ∫ (x : ) in a₁..a₃, Set.indicator {x : | x a₂} f xμ = ∫ (x : ) in a₁..a₂, f xμ
              theorem intervalIntegral.integral_pos_iff_support_of_nonneg_ae' {f : } {a : } {b : } {μ : MeasureTheory.Measure } (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Ι a b))] f) (hfi : IntervalIntegrable f μ a b) :
              0 < ∫ (x : ) in a..b, f xμ a < b 0 < μ (Function.support f Set.Ioc a b)

              If f is nonnegative and integrable on the unordered interval Set.uIoc a b, then its integral over a..b is positive if and only if a < b and the measure of Function.support f ∩ Set.Ioc a b is positive.

              theorem intervalIntegral.integral_pos_iff_support_of_nonneg_ae {f : } {a : } {b : } {μ : MeasureTheory.Measure } (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae μ] f) (hfi : IntervalIntegrable f μ a b) :
              0 < ∫ (x : ) in a..b, f xμ a < b 0 < μ (Function.support f Set.Ioc a b)

              If f is nonnegative a.e.-everywhere and it is integrable on the unordered interval Set.uIoc a b, then its integral over a..b is positive if and only if a < b and the measure of Function.support f ∩ Set.Ioc a b is positive.

              theorem intervalIntegral.intervalIntegral_pos_of_pos_on {f : } {a : } {b : } (hfi : IntervalIntegrable f MeasureTheory.volume a b) (hpos : xSet.Ioo a b, 0 < f x) (hab : a < b) :
              0 < ∫ (x : ) in a..b, f x

              If f : ℝ → ℝ is integrable on (a, b] for real numbers a < b, and positive on the interior of the interval, then its integral over a..b is strictly positive.

              theorem intervalIntegral.intervalIntegral_pos_of_pos {f : } {a : } {b : } (hfi : IntervalIntegrable f MeasureTheory.volume a b) (hpos : ∀ (x : ), 0 < f x) (hab : a < b) :
              0 < ∫ (x : ) in a..b, f x

              If f : ℝ → ℝ is strictly positive everywhere, and integrable on (a, b] for real numbers a < b, then its integral over a..b is strictly positive. (See interval_integral_pos_of_pos_on for a version only assuming positivity of f on (a, b) rather than everywhere.)

              theorem intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero {f : } {g : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hfi : IntervalIntegrable f μ a b) (hgi : IntervalIntegrable g μ a b) (hle : f ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Set.Ioc a b))] g) (hlt : (MeasureTheory.Measure.restrict μ (Set.Ioc a b)) {x : | f x < g x} 0) :
              ∫ (x : ) in a..b, f xμ < ∫ (x : ) in a..b, g xμ

              If f and g are two functions that are interval integrable on a..b, a ≤ b, f x ≤ g x for a.e. x ∈ Set.Ioc a b, and f x < g x on a subset of Set.Ioc a b of nonzero measure, then ∫ x in a..b, f x ∂μ < ∫ x in a..b, g x ∂μ.

              theorem intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt {f : } {g : } {a : } {b : } (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (hle : xSet.Ioc a b, f x g x) (hlt : ∃ c ∈ Set.Icc a b, f c < g c) :
              ∫ (x : ) in a..b, f x < ∫ (x : ) in a..b, g x

              If f and g are continuous on [a, b], a < b, f x ≤ g x on this interval, and f c < g c at some point c ∈ [a, b], then ∫ x in a..b, f x < ∫ x in a..b, g x.

              theorem intervalIntegral.integral_nonneg_of_ae_restrict {f : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Set.Icc a b))] f) :
              0 ∫ (u : ) in a..b, f uμ
              theorem intervalIntegral.integral_nonneg_of_ae {f : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae μ] f) :
              0 ∫ (u : ) in a..b, f uμ
              theorem intervalIntegral.integral_nonneg_of_forall {f : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hf : ∀ (u : ), 0 f u) :
              0 ∫ (u : ) in a..b, f uμ
              theorem intervalIntegral.integral_nonneg {f : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hf : uSet.Icc a b, 0 f u) :
              0 ∫ (u : ) in a..b, f uμ
              theorem intervalIntegral.abs_integral_le_integral_abs {f : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) :
              |∫ (x : ) in a..b, f xμ| ∫ (x : ) in a..b, |f x|μ
              theorem intervalIntegral.integral_mono_ae_restrict {f : } {g : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) (h : f ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Set.Icc a b))] g) :
              ∫ (u : ) in a..b, f uμ ∫ (u : ) in a..b, g uμ
              theorem intervalIntegral.integral_mono_ae {f : } {g : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) (h : f ≤ᶠ[MeasureTheory.Measure.ae μ] g) :
              ∫ (u : ) in a..b, f uμ ∫ (u : ) in a..b, g uμ
              theorem intervalIntegral.integral_mono_on {f : } {g : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) (h : xSet.Icc a b, f x g x) :
              ∫ (u : ) in a..b, f uμ ∫ (u : ) in a..b, g uμ
              theorem intervalIntegral.integral_mono {f : } {g : } {a : } {b : } {μ : MeasureTheory.Measure } (hab : a b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) (h : f g) :
              ∫ (u : ) in a..b, f uμ ∫ (u : ) in a..b, g uμ
              theorem intervalIntegral.integral_mono_interval {f : } {a : } {b : } {μ : MeasureTheory.Measure } {c : } {d : } (hca : c a) (hab : a b) (hbd : b d) (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Set.Ioc c d))] f) (hfi : IntervalIntegrable f μ c d) :
              ∫ (x : ) in a..b, f xμ ∫ (x : ) in c..d, f xμ
              theorem intervalIntegral.abs_integral_mono_interval {f : } {a : } {b : } {μ : MeasureTheory.Measure } {c : } {d : } (h : Ι a b Ι c d) (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Ι c d))] f) (hfi : IntervalIntegrable f μ c d) :
              |∫ (x : ) in a..b, f xμ| |∫ (x : ) in c..d, f xμ|
              theorem MeasureTheory.Integrable.hasSum_intervalIntegral {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {μ : MeasureTheory.Measure } {f : E} (hfi : MeasureTheory.Integrable f μ) (y : ) :
              HasSum (fun (n : ) => ∫ (x : ) in y + n..y + n + 1, f xμ) (∫ (x : ), f xμ)
              theorem MeasureTheory.Integrable.hasSum_intervalIntegral_comp_add_int {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hfi : MeasureTheory.Integrable f MeasureTheory.volume) :
              HasSum (fun (n : ) => ∫ (x : ) in 0 ..1, f (x + n)) (∫ (x : ), f x)