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:

• 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))

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_iff_integrable_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_integrable_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 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

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 : ℕ), 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 : ℕ), 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 (MeasureTheory.Measure.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 ℝ} {ν : 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 ℝ} {ν : 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 ≤ᶠ[MeasureTheory.Measure.ae μ] Ι 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 (MeasureTheory.Measure.restrict μ (Ι a b))) (hle : (fun x => ‖g x‖) ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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 (MeasureTheory.Measure.restrict μ (Ι a b))) (hle : (fun x => ‖f x‖) ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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 (MeasureTheory.Measure.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 (MeasureTheory.Measure.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 : ℝ → 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 : ∀ (i : ι), i ∈ s → 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)

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 ℝ.

theorem MonotoneOn.intervalIntegrable {E : Type u_3} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [ConditionallyCompleteLinearOrder E] [OrderTopology E] [TopologicalSpace.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] [TopologicalSpace.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] [TopologicalSpace.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] [TopologicalSpace.SecondCountableTopology E] {u : ℝ → E} {a : ℝ} {b : ℝ} (hu : Antitone u) : IntervalIntegrable u μ a b

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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 (MeasureTheory.Measure.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 (MeasureTheory.Measure.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 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 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 : ℝ), 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 : ∀ (i : ι), i ∈ s → 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} [IsROrC 𝕜] [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} [IsROrC 𝕜] (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} [IsROrC 𝕜] (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} [IsROrC 𝕜] (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 ∂μ = (ENNReal.toReal (↑↑μ (Set.Ioc a b)) - ENNReal.toReal (↑↑μ (Set.Ioc b a))) • 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 x ∂c • μ = ENNReal.toReal c • ∫ (x : ℝ) in a..b, f x ∂μ

theorem IsROrC.interval_integral_ofReal {𝕜 : Type u_6} [IsROrC 𝕜] {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 ℝ} [IsROrC 𝕜] [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} [IsROrC 𝕜] [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 ∂μ)

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 : ∀ (k : ℕ), k ∈ Set.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 : ℕ), 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_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 ∂μ = (ENNReal.toReal (↑↑μ (Set.Iic b)) - ENNReal.toReal (↑↑μ (Set.Iic a))) • 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 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 : ℝ → E} {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₃, Set.indicator {x | x ≤ a₂} f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ

theorem intervalIntegral.tendsto_integral_filter_of_dominated_convergence {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {ι : Type u_6} {l : Filter ι} [Filter.IsCountablyGenerated l] {F : ι → ℝ → E} (bound : ℝ → ℝ) (hF_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x) (bound_integrable : IntervalIntegrable bound μ a b) (h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Filter.Tendsto (fun n => F n x) l (nhds (f x))) : Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))

Lebesgue dominated convergence theorem for filters with a countable basis

theorem intervalIntegral.hasSum_integral_of_dominated_convergence {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {ι : Type u_6} [Countable ι] {F : ι → ℝ → E} (bound : ι → ℝ → ℝ) (hF_meas : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t) (bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Summable fun n => bound n t) (bound_integrable : IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b) (h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasSum (fun n => F n t) (f t)) : HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)

Lebesgue dominated convergence theorem for series.

theorem intervalIntegral.hasSum_intervalIntegral_of_summable_norm {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} [Countable ι] {f : ι → C(ℝ, E)} (hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := (_ : IsCompact (Set.uIcc a b)) }) (f i)‖) : HasSum (fun i => ∫ (x : ℝ) in a..b, ↑(f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), ↑(f i) x)

Interval integrals commute with countable sums, when the supremum norms are summable (a special case of the dominated convergence theorem).

theorem intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} [Countable ι] {f : ι → C(ℝ, E)} (hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := (_ : IsCompact (Set.uIcc a b)) }) (f i)‖) : ∑' (i : ι), ∫ (x : ℝ) in a..b, ↑(f i) x = ∫ (x : ℝ) in a..b, ∑' (i : ι), ↑(f i) x

theorem intervalIntegral.continuousWithinAt_of_dominated_interval {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_6} [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a : ℝ} {b : ℝ} {s : Set X} (hF_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousWithinAt (fun x => F x t) s x₀) : ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) s x₀

Continuity of interval integral with respect to a parameter, at a point within a set. Given F : X → ℝ → E, assume F x is ae-measurable on [a, b] for x in a neighborhood of x₀ within s and at x₀, and assume it is bounded by a function integrable on [a, b] independent of x in a neighborhood of x₀ within s. If (fun x ↦ F x t) is continuous at x₀ within s for almost every t in [a, b] then the same holds for (fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀.

theorem intervalIntegral.continuousAt_of_dominated_interval {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_6} [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a : ℝ} {b : ℝ} (hF_meas : ∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousAt (fun x => F x t) x₀) : ContinuousAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) x₀

Continuity of interval integral with respect to a parameter at a point. Given F : X → ℝ → E, assume F x is ae-measurable on [a, b] for x in a neighborhood of x₀, and assume it is bounded by a function integrable on [a, b] independent of x in a neighborhood of x₀. If (fun x ↦ F x t) is continuous at x₀ for almost every t in [a, b] then the same holds for (fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀.

theorem intervalIntegral.continuous_of_dominated_interval {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_6} [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] {F : X → ℝ → E} {bound : ℝ → ℝ} {a : ℝ} {b : ℝ} (hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Continuous fun x => F x t) : Continuous fun x => ∫ (t : ℝ) in a..b, F x t ∂μ

Continuity of interval integral with respect to a parameter. Given F : X → ℝ → E, assume each F x is ae-measurable on [a, b], and assume it is bounded by a function integrable on [a, b] independent of x. If (fun x ↦ F x t) is continuous for almost every t in [a, b] then the same holds for (fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀.

theorem intervalIntegral.continuousWithinAt_primitive {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b₀ : ℝ} {b₁ : ℝ} {b₂ : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} (hb₀ : ↑↑μ {b₀} = 0) (h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)) : ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.Icc b₁ b₂) b₀

theorem intervalIntegral.continuousOn_primitive {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NoAtoms μ] (h_int : MeasureTheory.IntegrableOn f (Set.Icc a b)) : ContinuousOn (fun x => ∫ (t : ℝ) in Set.Ioc a x, f t ∂μ) (Set.Icc a b)

theorem intervalIntegral.continuousOn_primitive_Icc {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NoAtoms μ] (h_int : MeasureTheory.IntegrableOn f (Set.Icc a b)) : ContinuousOn (fun x => ∫ (t : ℝ) in Set.Icc a x, f t ∂μ) (Set.Icc a b)

theorem intervalIntegral.continuousOn_primitive_interval' {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b₁ : ℝ} {b₂ : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NoAtoms μ] (h_int : IntervalIntegrable f μ b₁ b₂) (ha : a ∈ Set.uIcc b₁ b₂) : ContinuousOn (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.uIcc b₁ b₂)

Note: this assumes that f is IntervalIntegrable, in contrast to some other lemmas here.

theorem intervalIntegral.continuousOn_primitive_interval {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NoAtoms μ] (h_int : MeasureTheory.IntegrableOn f (Set.uIcc a b)) : ContinuousOn (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Set.uIcc a b)

theorem intervalIntegral.continuousOn_primitive_interval_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NoAtoms μ] (h_int : MeasureTheory.IntegrableOn f (Set.uIcc a b)) : ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) (Set.uIcc a b)

theorem intervalIntegral.continuous_primitive {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NoAtoms μ] (h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b) (a : ℝ) : Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ

theorem MeasureTheory.Integrable.continuous_primitive {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NoAtoms μ] (h_int : MeasureTheory.Integrable f) (a : ℝ) : Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ

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

theorem intervalIntegral.integral_eq_zero_iff_of_nonneg_ae {f : ℝ → ℝ} {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : 0 ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Set.Ioc a b ∪ Set.Ioc b a))] f) (hfi : IntervalIntegrable f μ a b) : ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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 ≤ᶠ[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 : ∀ (x : ℝ), 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 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 : ∀ (x : ℝ), x ∈ Set.Ioc a b → f x ≤ g x) (hlt : ∃ c, 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 : ∀ (u : ℝ), 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_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 : ∀ (x : ℝ), 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 {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) : HasSum (fun n => ∫ (x : ℝ) in 0 ..1, f (x + ↑n)) (∫ (x : ℝ), f x)