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 wheneverfis integrable on each interval; in particular, it works even if the measureμhas an atom atb; this rules outSet.IooandSet.Iccintervals; - 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
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
(f : ℝ → ε)
(μ : MeasureTheory.Measure ℝ)
(a b : ℝ)
:
A function f is called interval integrable with respect to a measure μ on an unordered
interval a..b if it is integrable on both intervals (a, b] and (b, a]. One of these
intervals is always empty, so this property is equivalent to f being integrable on
(min a b, max a b].
Equations
- IntervalIntegrable f μ a b = (MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ∧ MeasureTheory.IntegrableOn f (Set.Ioc b a) μ)
Instances For
Basic iff's for IntervalIntegrable #
theorem
intervalIntegrable_iff
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
:
A function is interval integrable with respect to a given measure μ on a..b if and
only if it is integrable on uIoc a b with respect to μ. This is an equivalent
definition of IntervalIntegrable.
theorem
IntervalIntegrable.def'
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
(h : IntervalIntegrable f μ a b)
:
MeasureTheory.IntegrableOn f (Set.uIoc 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
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{g : ℝ → ε}
(hf : IntervalIntegrable f μ a b)
(h : f =ᵐ[μ.restrict (Set.uIoc a b)] g)
:
IntervalIntegrable g μ a b
theorem
IntervalIntegrable.congr_codiscreteWithin
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{g : ℝ → ε}
[MeasureTheory.NoAtoms μ]
(h : f =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] g)
(hf : IntervalIntegrable f μ a b)
:
IntervalIntegrable g μ a b
Interval integrability is invariant when functions change along discrete sets.
theorem
intervalIntegrable_congr_codiscreteWithin
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{g : ℝ → ε}
[MeasureTheory.NoAtoms μ]
(h : f =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] g)
:
Interval integrability is invariant when functions change along discrete sets.
theorem
intervalIntegrable_iff_integrableOn_Ioc_of_le
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
(hab : a ≤ b)
:
theorem
intervalIntegrable_iff'
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[MeasureTheory.NoAtoms μ]
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
:
theorem
intervalIntegrable_iff_integrableOn_Icc_of_le
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[MeasureTheory.NoAtoms μ]
(hab : a ≤ b)
(ha : ‖f a‖ₑ ≠ ⊤ := by finiteness)
:
theorem
intervalIntegrable_iff_integrableOn_Ico_of_le
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[MeasureTheory.NoAtoms μ]
(hab : a ≤ b)
(ha : ‖f a‖ₑ ≠ ⊤ := by finiteness)
(hb : ‖f b‖ₑ ≠ ⊤ := by finiteness)
:
theorem
intervalIntegrable_iff_integrableOn_Ioo_of_le
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[MeasureTheory.NoAtoms μ]
(hab : a ≤ b)
(ha : ‖f a‖ₑ ≠ ⊤ := by finiteness)
(hb : ‖f b‖ₑ ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.Integrable.intervalIntegrable
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : Measure ℝ}
(hf : 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
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : Measure ℝ}
(hf : IntegrableOn f (Set.uIcc a b) μ)
:
IntervalIntegrable f μ a b
theorem
intervalIntegrable_const_iff
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{c : ε}
(hc : ‖c‖ₑ ≠ ⊤ := by finiteness)
:
@[simp]
theorem
intervalIntegrable_const
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{c : E}
(hc : ‖c‖ₑ ≠ ⊤ := by finiteness)
:
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
fis interval integrable, so are its absolute value and norm - arithmetic properties
theorem
IntervalIntegrable.symm
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
(h : IntervalIntegrable f μ a b)
:
IntervalIntegrable f μ b a
theorem
IntervalIntegrable.symm_iff
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
:
@[simp]
theorem
IntervalIntegrable.refl
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a : ℝ}
{μ : MeasureTheory.Measure ℝ}
:
IntervalIntegrable f μ a a
theorem
IntervalIntegrable.trans
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
{a b c : ℝ}
(hab : IntervalIntegrable f μ a b)
(hbc : IntervalIntegrable f μ b c)
:
IntervalIntegrable f μ a c
theorem
IntervalIntegrable.trans_iff
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b c : ℝ}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(h : b ∈ Set.uIcc a c)
:
theorem
IntervalIntegrable.trans_iterate_Ico
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
{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
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
{a : ℕ → ℝ}
{n : ℕ}
(hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1)))
:
IntervalIntegrable f μ (a 0) (a n)
theorem
IntervalIntegrable.neg
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{f : ℝ → E}
(h : IntervalIntegrable f μ a b)
:
IntervalIntegrable (-f) μ a b
theorem
IntervalIntegrable.enorm
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
(h : IntervalIntegrable f μ a b)
:
IntervalIntegrable (fun (x : ℝ) => ‖f x‖ₑ) μ a b
theorem
IntervalIntegrable.norm
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{f : ℝ → E}
(h : IntervalIntegrable f μ a b)
:
IntervalIntegrable (fun (x : ℝ) => ‖f x‖) μ a b
theorem
IntervalIntegrable.intervalIntegrable_enorm_iff
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
[TopologicalSpace.PseudoMetrizableSpace ε]
{μ : MeasureTheory.Measure ℝ}
{a b : ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)))
:
theorem
IntervalIntegrable.intervalIntegrable_norm_iff
{E : Type u_5}
[NormedAddCommGroup E]
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{a b : ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc 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
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b c d : ℝ}
{μ ν : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f ν a b)
(h1 : Set.uIcc c d ⊆ Set.uIcc a b)
(h2 : μ ≤ ν)
:
IntervalIntegrable f μ c d
theorem
IntervalIntegrable.mono_measure
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
{μ ν : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f ν a b)
(h : μ ≤ ν)
:
IntervalIntegrable f μ a b
theorem
IntervalIntegrable.mono_set
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b c d : ℝ}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f μ a b)
(h : Set.uIcc c d ⊆ Set.uIcc a b)
:
IntervalIntegrable f μ c d
theorem
IntervalIntegrable.mono_set_ae
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b c d : ℝ}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f μ a b)
(h : Set.uIoc c d ≤ᵐ[μ] Set.uIoc a b)
:
IntervalIntegrable f μ c d
theorem
IntervalIntegrable.mono_set'
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b c d : ℝ}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f μ a b)
(hsub : Set.uIoc c d ⊆ Set.uIoc a b)
:
IntervalIntegrable f μ c d
theorem
IntervalIntegrable.mono_fun_enorm
{ε : Type u_3}
{ε' : Type u_4}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
[TopologicalSpace ε']
[ENormedAddCommMonoid ε']
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
[TopologicalSpace.PseudoMetrizableSpace ε']
{g : ℝ → ε'}
(hf : IntervalIntegrable f μ a b)
(hgm : MeasureTheory.AEStronglyMeasurable g (μ.restrict (Set.uIoc a b)))
(hle : (fun (x : ℝ) => ‖g x‖ₑ) ≤ᵐ[μ.restrict (Set.uIoc a b)] fun (x : ℝ) => ‖f x‖ₑ)
:
IntervalIntegrable g μ a b
theorem
IntervalIntegrable.mono_fun
{E : Type u_5}
{F : Type u_6}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{f : ℝ → E}
[NormedAddCommGroup F]
{g : ℝ → F}
(hf : IntervalIntegrable f μ a b)
(hgm : MeasureTheory.AEStronglyMeasurable g (μ.restrict (Set.uIoc a b)))
(hle : (fun (x : ℝ) => ‖g x‖) ≤ᵐ[μ.restrict (Set.uIoc a b)] fun (x : ℝ) => ‖f x‖)
:
IntervalIntegrable g μ a b
theorem
IntervalIntegrable.mono_fun_enorm'
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ℝ → ε}
{g : ℝ → ENNReal}
(hg : IntervalIntegrable g μ a b)
(hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)))
(hle : (fun (x : ℝ) => ‖f x‖ₑ) ≤ᵐ[μ.restrict (Set.uIoc a b)] g)
:
IntervalIntegrable f μ a b
theorem
IntervalIntegrable.mono_fun'
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{f : ℝ → E}
{g : ℝ → ℝ}
(hg : IntervalIntegrable g μ a b)
(hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)))
(hle : (fun (x : ℝ) => ‖f x‖) ≤ᵐ[μ.restrict (Set.uIoc a b)] g)
:
IntervalIntegrable f μ a b
theorem
IntervalIntegrable.aestronglyMeasurable
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
(h : IntervalIntegrable f μ a b)
:
MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b))
theorem
IntervalIntegrable.aestronglyMeasurable'
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
(h : IntervalIntegrable f μ a b)
:
MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc b a))
theorem
IntervalIntegrable.smul
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{R : Type u_8}
[NormedAddCommGroup R]
[SMulZeroClass R E]
[IsBoundedSMul R E]
{f : ℝ → E}
(h : IntervalIntegrable f μ a b)
(r : R)
:
IntervalIntegrable (r • f) μ a b
@[simp]
theorem
IntervalIntegrable.add
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f g : ℝ → ε}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[ContinuousAdd ε]
(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_5}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{f g : ℝ → E}
(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}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[ContinuousAdd ε]
(s : Finset ι)
{f : ι → ℝ → ε}
(h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b)
:
IntervalIntegrable (∑ i ∈ s, f i) μ a b
@[simp]
theorem
IntervalIntegrable.finsum
{ι : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[ContinuousAdd ε]
[TopologicalSpace.PseudoMetrizableSpace ε]
{f : ι → ℝ → ε}
(h : ∀ (i : ι), IntervalIntegrable (f i) μ a b)
:
IntervalIntegrable (∑ᶠ (i : ι), f i) μ a b
Finsums of interval integrable functions are interval integrable.
theorem
IntervalIntegrable.mul_continuousOn
{A : Type u_7}
[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_7}
[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_7}
[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_7}
[NormedRing A]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{f : ℝ → A}
(hf : IntervalIntegrable f μ a b)
(c : A)
:
IntervalIntegrable (fun (x : ℝ) => f x * c) μ a b
theorem
IntervalIntegrable.smul_continuousOn
{𝕜 : Type u_2}
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{f : ℝ → 𝕜}
{g : ℝ → E}
[NormedRing 𝕜]
[Module 𝕜 E]
[NormSMulClass 𝕜 E]
(hf : IntervalIntegrable f μ a b)
(hg : ContinuousOn g (Set.uIcc a b))
:
IntervalIntegrable (fun (x : ℝ) => f x • g x) μ a b
theorem
IntervalIntegrable.continuousOn_smul
{𝕜 : Type u_2}
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{f : ℝ → 𝕜}
{g : ℝ → E}
[NormedRing 𝕜]
[Module 𝕜 E]
[NormSMulClass 𝕜 E]
(hg : IntervalIntegrable g μ a b)
(hf : ContinuousOn f (Set.uIcc a b))
:
IntervalIntegrable (fun (x : ℝ) => f x • g x) μ a b
@[simp]
theorem
IntervalIntegrable.div_const
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{𝕜 : Type u_8}
{f : ℝ → 𝕜}
[NormedDivisionRing 𝕜]
(h : IntervalIntegrable f μ a b)
(c : 𝕜)
:
IntervalIntegrable (fun (x : ℝ) => f x / c) μ a b
theorem
IntervalIntegrable.comp_mul_left
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f MeasureTheory.volume a b)
{c : ℝ}
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
(h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable (fun (x : ℝ) => f (c * x)) MeasureTheory.volume (a / c) (b / c)
theorem
IntervalIntegrable.comp_mul_left_iff
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{f : ℝ → E}
{c : ℝ}
(hc : c ≠ 0)
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
(h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable (fun (x : ℝ) => f (c * x)) MeasureTheory.volume (a / c) (b / c) ↔ IntervalIntegrable f MeasureTheory.volume a b
theorem
IntervalIntegrable.comp_mul_right
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f MeasureTheory.volume a b)
{c : ℝ}
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
(h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable (fun (x : ℝ) => f (x * c)) MeasureTheory.volume (a / c) (b / c)
theorem
IntervalIntegrable.comp_add_right
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f MeasureTheory.volume a b)
(c : ℝ)
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable (fun (x : ℝ) => f (x + c)) MeasureTheory.volume (a - c) (b - c)
theorem
IntervalIntegrable.comp_add_left
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f MeasureTheory.volume a b)
(c : ℝ)
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable (fun (x : ℝ) => f (c + x)) MeasureTheory.volume (a - c) (b - c)
theorem
IntervalIntegrable.comp_sub_right
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : ℝ → ε}
{a b : ℝ}
[TopologicalSpace.PseudoMetrizableSpace ε]
(hf : IntervalIntegrable f MeasureTheory.volume a b)
(c : ℝ)
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable (fun (x : ℝ) => f (x - c)) MeasureTheory.volume (a + c) (b + c)
theorem
IntervalIntegrable.iff_comp_neg
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{f : ℝ → E}
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable f MeasureTheory.volume a b ↔ IntervalIntegrable (fun (x : ℝ) => f (-x)) MeasureTheory.volume (-a) (-b)
theorem
IntervalIntegrable.comp_sub_left
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{f : ℝ → E}
(hf : IntervalIntegrable f MeasureTheory.volume a b)
(c : ℝ)
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable (fun (x : ℝ) => f (c - x)) MeasureTheory.volume (c - a) (c - b)
theorem
IntervalIntegrable.comp_sub_left_iff
{E : Type u_5}
[NormedAddCommGroup E]
{a b : ℝ}
{f : ℝ → E}
(c : ℝ)
(h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness)
:
IntervalIntegrable (fun (x : ℝ) => f (c - x)) MeasureTheory.volume (c - a) (c - b) ↔ IntervalIntegrable f MeasureTheory.volume a b
Continuous functions are interval integrable #
theorem
ContinuousOn.intervalIntegrable
{E : Type u_5}
[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_5}
[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_5}
[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_5}
[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_5}
[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_5}
[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_5}
[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_5}
[NormedAddCommGroup E]
{f : ℝ → E}
(h₁f : ∀ (x : ℝ), f x = f (-x))
(h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x)
{t : ℝ}
(ht : ‖f (min 0 t)‖ₑ ≠ ⊤ := by finiteness)
:
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_5}
[NormedAddCommGroup E]
{f : ℝ → E}
(h₁f : ∀ (x : ℝ), f x = f (-x))
(h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x)
{a b : ℝ}
(ha : ‖f (min 0 a)‖ₑ ≠ ⊤ := by finiteness)
(hb : ‖f (min 0 b)‖ₑ ≠ ⊤ := by finiteness)
:
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_5}
[NormedAddCommGroup E]
{f : ℝ → E}
(h₁f : ∀ (x : ℝ), -f x = f (-x))
(h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x)
{t : ℝ}
(ht : ‖f (min 0 t)‖ₑ ≠ ⊤ := by finiteness)
:
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_5}
[NormedAddCommGroup E]
{f : ℝ → E}
(h₁f : ∀ (x : ℝ), -f x = f (-x))
(h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x)
{a b : ℝ}
(ha : ‖f (min 0 a)‖ₑ ≠ ⊤ := by finiteness)
(hb : ‖f (min 0 b)‖ₑ ≠ ⊤ := by finiteness)
:
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_5}
[NormedAddCommGroup E]
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{l l' : Filter ℝ}
(hfm : StronglyMeasurableAtFilter f l' μ)
[TendstoIxxClass Set.Ioc l l']
[l'.IsMeasurablyGenerated]
(hμ : μ.FiniteAtFilter l')
{c : E}
(hf : Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c))
{u v : ι → ℝ}
{lt : Filter ι}
(hu : Tendsto u lt l)
(hv : 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_5}
[NormedAddCommGroup E]
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{l l' : Filter ℝ}
(hfm : StronglyMeasurableAtFilter f l' μ)
[TendstoIxxClass Set.Ioc l l']
[l'.IsMeasurablyGenerated]
(hμ : μ.FiniteAtFilter l')
{c : E}
(hf : Tendsto f l' (nhds c))
{u v : ι → ℝ}
{lt : Filter ι}
(hu : Tendsto u lt l)
(hv : 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_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(f : ℝ → E)
(a b : ℝ)
(μ : MeasureTheory.Measure ℝ)
:
E
The interval integral ∫ x in a..b, f x ∂μ is defined
as ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ. If a ≤ b, then it equals
∫ x in Ioc a b, f x ∂μ, otherwise it equals -∫ x in Ioc b a, f x ∂μ.
Equations
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
intervalIntegral.integral_zero
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
:
@[simp]
theorem
intervalIntegral.integral_same
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
:
theorem
intervalIntegral.integral_undef
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(h : ¬IntervalIntegrable f μ a b)
:
theorem
intervalIntegral.intervalIntegrable_of_integral_ne_zero
{E : Type u_5}
[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_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(hf : ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)))
:
theorem
intervalIntegral.integral_non_aestronglyMeasurable_of_le
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(h : a ≤ b)
(hf : ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b)))
:
@[deprecated intervalIntegral.norm_integral_eq_norm_integral_uIoc (since := "2025-04-19")]
theorem
intervalIntegral.norm_integral_eq_norm_integral_Ioc
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
(f : ℝ → E)
:
Alias of intervalIntegral.norm_integral_eq_norm_integral_uIoc.
@[deprecated intervalIntegral.norm_integral_le_integral_norm_uIoc (since := "2025-04-19")]
theorem
intervalIntegral.norm_integral_le_integral_norm_Ioc
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
:
Alias of intervalIntegral.norm_integral_le_integral_norm_uIoc.
theorem
intervalIntegral.norm_integral_le_abs_of_norm_le
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{g : ℝ → ℝ}
(h : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ‖f t‖ ≤ g t)
(hbound : IntervalIntegrable g μ a b)
:
theorem
intervalIntegral.norm_integral_le_of_norm_le
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{g : ℝ → ℝ}
(hab : a ≤ b)
(h : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.Ioc a b → ‖f t‖ ≤ g t)
(hbound : IntervalIntegrable g μ a b)
:
@[simp]
theorem
intervalIntegral.integral_add
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f g : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(hf : IntervalIntegrable f μ a b)
(hg : IntervalIntegrable g μ a b)
:
theorem
intervalIntegral.integral_finset_sum
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{ι : Type u_8}
{s : Finset ι}
{f : ι → ℝ → E}
(h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b)
:
@[simp]
theorem
intervalIntegral.integral_sub
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f g : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(hf : IntervalIntegrable f μ a b)
(hg : IntervalIntegrable g μ a b)
:
@[simp]
theorem
intervalIntegral.integral_smul
{𝕜 : Type u_2}
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[NormedDivisionRing 𝕜]
[Module 𝕜 E]
[NormSMulClass 𝕜 E]
[SMulCommClass ℝ 𝕜 E]
(r : 𝕜)
(f : ℝ → E)
:
Compatibility with scalar multiplication. Note this assumes 𝕜 is a division ring in order to
ensure that for c ≠ 0, c • f is integrable iff f is. For scalar multiplication by more
general rings assuming integrability, see IntervalIntegrable.integral_smul.
theorem
IntervalIntegrable.integral_smul
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
{R : Type u_8}
[NormedRing R]
[Module R E]
[IsBoundedSMul R E]
[SMulCommClass ℝ R E]
{f : ℝ → E}
(r : R)
(hf : IntervalIntegrable f μ a b)
:
@[simp]
theorem
intervalIntegral.integral_smul_const
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[CompleteSpace E]
{𝕜 : Type u_8}
[RCLike 𝕜]
[NormedSpace 𝕜 E]
(f : ℝ → 𝕜)
(c : E)
:
theorem
intervalIntegral.integral_const'
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[CompleteSpace E]
(c : E)
:
@[simp]
theorem
intervalIntegral.integral_const
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
[CompleteSpace E]
(c : E)
:
theorem
ContinuousLinearMap.intervalIntegral_apply
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure ℝ}
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{a b : ℝ}
{φ : ℝ → F →L[𝕜] E}
(hφ : IntervalIntegrable φ μ a b)
(v : F)
:
theorem
ContinuousLinearMap.intervalIntegral_comp_comm
{𝕜 : Type u_2}
{E : Type u_5}
{F : Type u_6}
[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)
:
Basic arithmetic #
Includes addition, scalar multiplication and affine transformations.
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_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f g : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{a b : ℝ}
(h : Set.EqOn f g (Set.uIcc a b))
:
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_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b c : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(hab : IntervalIntegrable f μ a b)
(hbc : IntervalIntegrable f μ b c)
:
theorem
intervalIntegral.integral_add_adjacent_intervals
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b c : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(hab : IntervalIntegrable f μ a b)
(hbc : IntervalIntegrable f μ b c)
:
theorem
intervalIntegral.sum_integral_adjacent_intervals_Ico
{E : Type u_5}
[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)))
:
theorem
intervalIntegral.sum_integral_adjacent_intervals
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{a : ℕ → ℝ}
{n : ℕ}
(hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1)))
:
theorem
intervalIntegral.integral_interval_sub_left
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b c : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(hab : IntervalIntegrable f μ a b)
(hac : IntervalIntegrable f μ a c)
:
theorem
intervalIntegral.integral_interval_add_interval_comm
{E : Type u_5}
[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)
:
theorem
intervalIntegral.integral_interval_sub_interval_comm
{E : Type u_5}
[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)
:
theorem
intervalIntegral.integral_interval_sub_interval_comm'
{E : Type u_5}
[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)
:
theorem
intervalIntegral.integral_Iic_sub_Iic
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(ha : MeasureTheory.IntegrableOn f (Set.Iic a) μ)
(hb : MeasureTheory.IntegrableOn f (Set.Iic b) μ)
:
theorem
intervalIntegral.integral_Iic_add_Ioi
{E : Type u_5}
[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) μ)
:
theorem
intervalIntegral.integral_Iio_add_Ici
{E : Type u_5}
[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) μ)
:
theorem
intervalIntegral.integral_const_of_cdf
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
[CompleteSpace E]
[MeasureTheory.IsFiniteMeasure μ]
(c : E)
:
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_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{a b : ℝ}
(h : Function.support f ⊆ Set.Ioc a b)
:
theorem
intervalIntegral.integral_congr_ae_restrict
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a b : ℝ}
{f g : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
(h : f =ᵐ[μ.restrict (Set.uIoc a b)] g)
:
Integrals are equal for functions that agree almost everywhere for the restricted measure.
theorem
intervalIntegral.integral_pos_iff_support_of_nonneg_ae'
{f : ℝ → ℝ}
{a b : ℝ}
{μ : MeasureTheory.Measure ℝ}
(hf : 0 ≤ᵐ[μ.restrict (Set.uIoc a b)] f)
(hfi : IntervalIntegrable f μ 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)
:
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)
:
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)
:
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)
:
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)
:
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_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)
:
theorem
MeasureTheory.Integrable.hasSum_intervalIntegral_comp_add_int
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
(hfi : Integrable f volume)
: