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 IntegrableOn f (Ioc a b) μ ∧ IntegrableOn 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:

• this way ∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ holds whenever f is integrable on each interval; in particular, it works even if the measure μ has an atom at b; this rules out Set.Ioo and Set.Icc intervals;
• with this definition for a probability measure μ, the integral ∫ x in a..b, 1 ∂μ equals the difference $F_μ(b)-F_μ(a)$, where $F_μ(a)=μ(-∞, a]$ is the cumulative distribution function of μ.

Tags

integral

Integrability on an interval

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

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

• IntervalIntegrable f μ a b = (MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ∧ MeasureTheory.IntegrableOn f (Set.Ioc b a) μ)

Basic iff's for IntervalIntegrable

theorem intervalIntegrable_iff {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} : IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Ι a b) μ

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) : MeasureTheory.IntegrableOn 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 μ.

theorem IntervalIntegrable.congr {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → E} (hf : IntervalIntegrable f μ a b) (h : f =ᵐ[μ.restrict (Ι a b)] g) : IntervalIntegrable g μ a b

theorem intervalIntegrable_iff_integrableOn_Ioc_of_le {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) : IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ

theorem intervalIntegrable_iff' {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NoAtoms μ] : IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.uIcc a b) μ

theorem intervalIntegrable_iff_integrableOn_Icc_of_le {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} (hab : a ≤ b) {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NoAtoms μ] : IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Icc a b) μ

theorem intervalIntegrable_iff_integrableOn_Ico_of_le {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NoAtoms μ] (hab : a ≤ b) : IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ

theorem intervalIntegrable_iff_integrableOn_Ioo_of_le {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NoAtoms μ] (hab : a ≤ b) : IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ

theorem MeasureTheory.Integrable.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : MeasureTheory.Integrable f μ) : IntervalIntegrable f μ a b

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

theorem MeasureTheory.IntegrableOn.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : MeasureTheory.IntegrableOn f (Set.uIcc a b) μ) : IntervalIntegrable f μ 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]

theorem intervalIntegrable_const {E : Type u_3} [NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {c : E} : IntervalIntegrable (fun (x : ℝ) => c) μ a b

Basic properties of interval integrability

• interval integrability is symmetric, reflexive, transitive
• monotonicity and strong measurability of the interval integral
• if f is interval integrable, so are its absolute value and norm
• arithmetic properties

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

@[simp]

theorem IntervalIntegrable.refl {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a : ℝ} {μ : MeasureTheory.Measure ℝ} : IntervalIntegrable f μ a a

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) : IntervalIntegrable f μ a c

theorem IntervalIntegrable.trans_iterate_Ico {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {a : ℕ → ℝ} {m n : ℕ} (hmn : m ≤ n) (hint : ∀ k ∈ Set.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) : 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.intervalIntegrable_norm_iff {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Ι a b))) : IntervalIntegrable (fun (t : ℝ) => ‖f t‖) μ a b ↔ IntervalIntegrable f μ 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 ℝ} (hf : IntervalIntegrable f ν a b) (h1 : Set.uIcc c d ⊆ Set.uIcc a b) (h2 : μ ≤ ν) : IntervalIntegrable f μ c d

theorem IntervalIntegrable.mono_measure {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ ν : MeasureTheory.Measure ℝ} (hf : IntervalIntegrable f ν a b) (h : μ ≤ ν) : IntervalIntegrable f μ 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) (h : Set.uIcc c d ⊆ Set.uIcc a b) : IntervalIntegrable f μ c d

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 ≤ᵐ[μ] Ι a b) : IntervalIntegrable f μ c d

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) : IntervalIntegrable f μ c d

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 (μ.restrict (Ι a b))) (hle : (fun (x : ℝ) => ‖g x‖) ≤ᵐ[μ.restrict (Ι a b)] fun (x : ℝ) => ‖f x‖) : IntervalIntegrable g μ a b

theorem IntervalIntegrable.mono_fun' {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ℝ} (hg : IntervalIntegrable g μ a b) (hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Ι a b))) (hle : (fun (x : ℝ) => ‖f x‖) ≤ᵐ[μ.restrict (Ι a b)] g) : IntervalIntegrable f μ a b

theorem IntervalIntegrable.aestronglyMeasurable {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (h : IntervalIntegrable f μ a b) : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b))

theorem IntervalIntegrable.aestronglyMeasurable' {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (h : IntervalIntegrable f μ a b) : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc b a))

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 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 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 : ∀ i ∈ s, IntervalIntegrable (f i) μ a b) : IntervalIntegrable (∑ i ∈ s, f i) μ a b

theorem IntervalIntegrable.mul_continuousOn {A : Type u_5} [NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f 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 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

theorem ContinuousOn.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {u : ℝ → E} {a b : ℝ} (hu : ContinuousOn u (Set.uIcc a b)) : IntervalIntegrable u μ a b

theorem ContinuousOn.intervalIntegrable_of_Icc {E : Type u_3} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {u : ℝ → E} {a b : ℝ} (h : a ≤ b) (hu : ContinuousOn u (Set.Icc a b)) : IntervalIntegrable u μ a b

theorem Continuous.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {u : ℝ → E} (hu : Continuous u) (a b : ℝ) : IntervalIntegrable u μ a b

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

Monotone and antitone functions are integral integrable

theorem MonotoneOn.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ} (hu : MonotoneOn u (Set.uIcc a b)) : IntervalIntegrable u μ a b

theorem AntitoneOn.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ} (hu : AntitoneOn u (Set.uIcc a b)) : IntervalIntegrable u μ a b

theorem Monotone.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ} (hu : Monotone u) : IntervalIntegrable u μ a b

theorem Antitone.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ} (hu : Antitone u) : IntervalIntegrable u μ a b

Interval integrability of functions with even or odd parity

theorem intervalIntegrable_of_even₀ {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} (h₁f : ∀ (x : ℝ), f x = f (-x)) (h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) (t : ℝ) : IntervalIntegrable f MeasureTheory.volume 0 t

An even function is interval integrable (with respect to the volume measure) on every interval of the form 0..x if it is interval integrable (with respect to the volume measure) on every interval of the form 0..x, for positive x.

See intervalIntegrable_of_even for a stronger result.

theorem intervalIntegrable_of_even {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} (h₁f : ∀ (x : ℝ), f x = f (-x)) (h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) (a b : ℝ) : IntervalIntegrable f MeasureTheory.volume a b

An even function is interval integrable (with respect to the volume measure) on every interval if it is interval integrable (with respect to the volume measure) on every interval of the form 0..x, for positive x.

theorem intervalIntegrable_of_odd₀ {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} (h₁f : ∀ (x : ℝ), -f x = f (-x)) (h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) (t : ℝ) : IntervalIntegrable f MeasureTheory.volume 0 t

An odd function is interval integrable (with respect to the volume measure) on every interval of the form 0..x if it is interval integrable (with respect to the volume measure) on every interval of the form 0..x, for positive x.

See intervalIntegrable_of_odd for a stronger result.

theorem intervalIntegrable_of_odd {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} (h₁f : ∀ (x : ℝ), -f x = f (-x)) (h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) (a b : ℝ) : IntervalIntegrable f MeasureTheory.volume a b

An odd function is interval integrable (with respect to the volume measure) on every interval iff it is interval integrable (with respect to the volume measure) on every interval of the form 0..x, for positive x.

Limits of intervals

theorem Filter.Tendsto.eventually_intervalIntegrable_ae {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {l l' : Filter ℝ} (hfm : StronglyMeasurableAtFilter f l' μ) [Filter.TendstoIxxClass Set.Ioc l l'] [l'.IsMeasurablyGenerated] (hμ : μ.FiniteAtFilter l') {c : E} (hf : Filter.Tendsto f (l' ⊓ MeasureTheory.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 l' : Filter ℝ} (hfm : StronglyMeasurableAtFilter f l' μ) [Filter.TendstoIxxClass Set.Ioc l l'] [l'.IsMeasurablyGenerated] (hμ : μ.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

• intervalIntegral f a b μ = ∫ (x : ℝ) in Set.Ioc a b, f x ∂μ - ∫ (x : ℝ) in Set.Ioc b a, f x ∂μ

def «term∫_In_.._,_∂_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «term∫_In_.._,_∂_» : Lean.ParserDescr

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

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

def «term∫_In_.._,_» : Lean.ParserDescr

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

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

def «term∫_In_.._,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

@[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) : IntervalIntegrable f μ a b

theorem intervalIntegral.integral_non_aestronglyMeasurable {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} (hf : ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Ι a b))) : ∫ (x : ℝ) in a..b, f x ∂μ = 0

theorem intervalIntegral.integral_non_aestronglyMeasurable_of_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} (h : a ≤ b) (hf : ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b))) : ∫ (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 a ⊓ b..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 : ℝ) ∂μ.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 b → ‖f 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 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 : ∀ i ∈ s, IntervalIntegrable (f i) μ a b) : ∫ (x : ℝ) in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ (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 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] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [CompleteSpace E] {𝕜 : 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] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [CompleteSpace E] (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] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] (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 x ∂c • μ = c.toReal • ∫ (x : ℝ) in a..b, f x ∂μ

theorem RCLike.intervalIntegral_ofReal {𝕜 : Type u_6} [RCLike 𝕜] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} : ∫ (x : ℝ) in a..b, ↑(f x) ∂μ = ↑(∫ (x : ℝ) in a..b, f x ∂μ)

@[deprecated RCLike.intervalIntegral_ofReal (since := "2024-04-06")]

theorem intervalIntegral.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 ∂μ)

Alias of RCLike.intervalIntegral_ofReal.

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] [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] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace F] [CompleteSpace E] (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.

@[simp]

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

@[simp]

theorem intervalIntegral.smul_integral_comp_mul_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c : ℝ) : c • ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x

@[simp]

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

@[simp]

theorem intervalIntegral.smul_integral_comp_mul_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c : ℝ) : c • ∫ (x : ℝ) in a..b, f (c * x) = ∫ (x : ℝ) in c * a..c * b, f x

@[simp]

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

@[simp]

theorem intervalIntegral.inv_smul_integral_comp_div {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c : ℝ) : c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c) = ∫ (x : ℝ) in a / c..b / c, f x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem intervalIntegral.smul_integral_comp_mul_add {E : Type u_3} [NormedAddCommGroup 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

@[simp]

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

@[simp]

theorem intervalIntegral.smul_integral_comp_add_mul {E : Type u_3} [NormedAddCommGroup 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

@[simp]

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

@[simp]

theorem intervalIntegral.inv_smul_integral_comp_div_add {E : Type u_3} [NormedAddCommGroup 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

@[simp]

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

@[simp]

theorem intervalIntegral.inv_smul_integral_comp_add_div {E : Type u_3} [NormedAddCommGroup 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

@[simp]

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

@[simp]

theorem intervalIntegral.smul_integral_comp_mul_sub {E : Type u_3} [NormedAddCommGroup 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

@[simp]

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

@[simp]

theorem intervalIntegral.smul_integral_comp_sub_mul {E : Type u_3} [NormedAddCommGroup 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

@[simp]

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

@[simp]

theorem intervalIntegral.inv_smul_integral_comp_div_sub {E : Type u_3} [NormedAddCommGroup 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

@[simp]

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

@[simp]

theorem intervalIntegral.inv_smul_integral_comp_sub_div {E : Type u_3} [NormedAddCommGroup 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

@[simp]

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

@[simp]

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

@[simp]

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 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 : ∀ k ∈ Set.Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) : ∑ k ∈ Finset.Ico m n, ∫ (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))) : ∑ k ∈ Finset.range n, ∫ (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] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [CompleteSpace E] [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 g : ℝ → E} {μ : MeasureTheory.Measure ℝ} (h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Ioc a b → f x = g x) (h' : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Ioc b a → f 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 g : ℝ → E} {μ : MeasureTheory.Measure ℝ} (h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → f 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 b → f 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₃, {x : ℝ | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ

theorem intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Set.Ioc a b)] f) (hfi : IntervalIntegrable f μ a b) : ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Set.Ioc a b)] 0

theorem intervalIntegral.integral_eq_zero_iff_of_nonneg_ae {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : 0 ≤ᵐ[μ.restrict (Set.Ioc a b ∪ Set.Ioc b a)] f) (hfi : IntervalIntegrable f μ a b) : ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Set.Ioc a b ∪ Set.Ioc b a)] 0

theorem intervalIntegral.integral_pos_iff_support_of_nonneg_ae' {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : 0 ≤ᵐ[μ.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 ≤ᵐ[μ] 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 : ∀ x ∈ Set.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 intervalIntegral_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 ≤ᵐ[μ.restrict (Set.Ioc a b)] g) (hlt : (μ.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 : ∀ x ∈ Set.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 ≤ᵐ[μ.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 ≤ᵐ[μ] 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 : ∀ u ∈ Set.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_pos {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hle : ∀ x ∈ Set.Ioc a b, 0 ≤ f x) (hlt : ∃ c ∈ Set.Icc a b, 0 < f c) : 0 < ∫ (x : ℝ) in a..b, f x

theorem intervalIntegral.integral_mono_interval {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c d : ℝ} (hca : c ≤ a) (hab : a ≤ b) (hbd : b ≤ d) (hf : 0 ≤ᵐ[μ.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 ≤ᵐ[μ.restrict (Ι c d)] f) (hfi : IntervalIntegrable f μ c d) : |∫ (x : ℝ) in a..b, f x ∂μ| ≤ |∫ (x : ℝ) in c..d, 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 ≤ᵐ[μ.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 ≤ᵐ[μ] 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 : ∀ x ∈ Set.Icc a b, f x ≤ g x) : ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

theorem intervalIntegral.integral_mono_on_of_le_Ioo {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) [MeasureTheory.NoAtoms μ] (h : ∀ x ∈ Set.Ioo 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 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)