Integral over an interval #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 interval_integrable 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 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
interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
(f : ℝ → E)
(μ : measure_theory.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
- interval_integrable f μ a b = (measure_theory.integrable_on f (set.Ioc a b) μ ∧ measure_theory.integrable_on f (set.Ioc b a) μ)
theorem
interval_integrable_iff
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ} :
interval_integrable f μ a b ↔ measure_theory.integrable_on f (set.uIoc 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 interval_integrable.
theorem
interval_integrable.def
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(h : interval_integrable f μ a b) :
measure_theory.integrable_on 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
interval_integrable_iff_integrable_Ioc_of_le
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(hab : a ≤ b) :
interval_integrable f μ a b ↔ measure_theory.integrable_on f (set.Ioc a b) μ
theorem
interval_integrable_iff'
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.has_no_atoms μ] :
interval_integrable f μ a b ↔ measure_theory.integrable_on f (set.uIcc a b) μ
theorem
interval_integrable_iff_integrable_Icc_of_le
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
(hab : a ≤ b)
{μ : measure_theory.measure ℝ}
[measure_theory.has_no_atoms μ] :
interval_integrable f μ a b ↔ measure_theory.integrable_on f (set.Icc a b) μ
theorem
measure_theory.integrable.interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(hf : measure_theory.integrable f μ) :
interval_integrable 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
measure_theory.integrable_on.interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(hf : measure_theory.integrable_on f (set.uIcc a b) μ) :
interval_integrable f μ a b
theorem
interval_integrable_const_iff
{E : Type u_3}
[normed_add_comm_group E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{c : E} :
@[simp]
theorem
interval_integrable_const
{E : Type u_3}
[normed_add_comm_group E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
{c : E} :
interval_integrable (λ (_x : ℝ), c) μ a b
@[symm]
theorem
interval_integrable.symm
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(h : interval_integrable f μ a b) :
interval_integrable f μ b a
@[refl]
theorem
interval_integrable.refl
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a : ℝ}
{μ : measure_theory.measure ℝ} :
interval_integrable f μ a a
@[trans]
theorem
interval_integrable.trans
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{a b c : ℝ}
(hab : interval_integrable f μ a b)
(hbc : interval_integrable f μ b c) :
interval_integrable f μ a c
theorem
interval_integrable.trans_iterate_Ico
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{a : ℕ → ℝ}
{m n : ℕ}
(hmn : m ≤ n)
(hint : ∀ (k : ℕ), k ∈ set.Ico m n → interval_integrable f μ (a k) (a (k + 1))) :
interval_integrable f μ (a m) (a n)
theorem
interval_integrable.trans_iterate
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{a : ℕ → ℝ}
{n : ℕ}
(hint : ∀ (k : ℕ), k < n → interval_integrable f μ (a k) (a (k + 1))) :
interval_integrable f μ (a 0) (a n)
theorem
interval_integrable.neg
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(h : interval_integrable f μ a b) :
interval_integrable (-f) μ a b
theorem
interval_integrable.norm
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(h : interval_integrable f μ a b) :
interval_integrable (λ (x : ℝ), ‖f x‖) μ a b
theorem
interval_integrable.interval_integrable_norm_iff
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{a b : ℝ}
(hf : measure_theory.ae_strongly_measurable f (μ.restrict (set.uIoc a b))) :
interval_integrable (λ (t : ℝ), ‖f t‖) μ a b ↔ interval_integrable f μ a b
theorem
interval_integrable.abs
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → ℝ}
(h : interval_integrable f μ a b) :
interval_integrable (λ (x : ℝ), |f x|) μ a b
theorem
interval_integrable.mono
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b c d : ℝ}
{μ ν : measure_theory.measure ℝ}
(hf : interval_integrable f ν a b)
(h1 : set.uIcc c d ⊆ set.uIcc a b)
(h2 : μ ≤ ν) :
interval_integrable f μ c d
theorem
interval_integrable.mono_measure
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ ν : measure_theory.measure ℝ}
(hf : interval_integrable f ν a b)
(h : μ ≤ ν) :
interval_integrable f μ a b
theorem
interval_integrable.mono_set
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b c d : ℝ}
{μ : measure_theory.measure ℝ}
(hf : interval_integrable f μ a b)
(h : set.uIcc c d ⊆ set.uIcc a b) :
interval_integrable f μ c d
theorem
interval_integrable.mono_set_ae
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b c d : ℝ}
{μ : measure_theory.measure ℝ}
(hf : interval_integrable f μ a b)
(h : set.uIoc c d ≤ᵐ[μ] set.uIoc a b) :
interval_integrable f μ c d
theorem
interval_integrable.mono_set'
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b c d : ℝ}
{μ : measure_theory.measure ℝ}
(hf : interval_integrable f μ a b)
(hsub : set.uIoc c d ⊆ set.uIoc a b) :
interval_integrable f μ c d
theorem
interval_integrable.mono_fun
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[normed_add_comm_group F]
{g : ℝ → F}
(hf : interval_integrable f μ a b)
(hgm : measure_theory.ae_strongly_measurable g (μ.restrict (set.uIoc a b)))
(hle : (λ (x : ℝ), ‖g x‖) ≤ᵐ[μ.restrict (set.uIoc a b)] λ (x : ℝ), ‖f x‖) :
interval_integrable g μ a b
theorem
interval_integrable.mono_fun'
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{g : ℝ → ℝ}
(hg : interval_integrable g μ a b)
(hfm : measure_theory.ae_strongly_measurable f (μ.restrict (set.uIoc a b)))
(hle : (λ (x : ℝ), ‖f x‖) ≤ᵐ[μ.restrict (set.uIoc a b)] g) :
interval_integrable f μ a b
@[protected]
theorem
interval_integrable.ae_strongly_measurable
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(h : interval_integrable f μ a b) :
measure_theory.ae_strongly_measurable f (μ.restrict (set.Ioc a b))
@[protected]
theorem
interval_integrable.ae_strongly_measurable'
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(h : interval_integrable f μ a b) :
measure_theory.ae_strongly_measurable f (μ.restrict (set.Ioc b a))
theorem
interval_integrable.smul
{𝕜 : Type u_2}
{E : Type u_3}
[normed_add_comm_group E]
[normed_field 𝕜]
[normed_space 𝕜 E]
{f : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(h : interval_integrable f μ a b)
(r : 𝕜) :
interval_integrable (r • f) μ a b
@[simp]
theorem
interval_integrable.add
{E : Type u_3}
[normed_add_comm_group E]
{f g : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(hf : interval_integrable f μ a b)
(hg : interval_integrable g μ a b) :
interval_integrable (λ (x : ℝ), f x + g x) μ a b
@[simp]
theorem
interval_integrable.sub
{E : Type u_3}
[normed_add_comm_group E]
{f g : ℝ → E}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(hf : interval_integrable f μ a b)
(hg : interval_integrable g μ a b) :
interval_integrable (λ (x : ℝ), f x - g x) μ a b
theorem
interval_integrable.sum
{ι : Type u_1}
{E : Type u_3}
[normed_add_comm_group E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(s : finset ι)
{f : ι → ℝ → E}
(h : ∀ (i : ι), i ∈ s → interval_integrable (f i) μ a b) :
interval_integrable (s.sum (λ (i : ι), f i)) μ a b
theorem
interval_integrable.mul_continuous_on
{A : Type u_5}
[normed_ring A]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f g : ℝ → A}
(hf : interval_integrable f μ a b)
(hg : continuous_on g (set.uIcc a b)) :
interval_integrable (λ (x : ℝ), f x * g x) μ a b
theorem
interval_integrable.continuous_on_mul
{A : Type u_5}
[normed_ring A]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f g : ℝ → A}
(hf : interval_integrable f μ a b)
(hg : continuous_on g (set.uIcc a b)) :
interval_integrable (λ (x : ℝ), g x * f x) μ a b
@[simp]
theorem
interval_integrable.const_mul
{A : Type u_5}
[normed_ring A]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → A}
(hf : interval_integrable f μ a b)
(c : A) :
interval_integrable (λ (x : ℝ), c * f x) μ a b
@[simp]
theorem
interval_integrable.mul_const
{A : Type u_5}
[normed_ring A]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → A}
(hf : interval_integrable f μ a b)
(c : A) :
interval_integrable (λ (x : ℝ), f x * c) μ a b
@[simp]
theorem
interval_integrable.div_const
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{𝕜 : Type u_1}
{f : ℝ → 𝕜}
[normed_field 𝕜]
(h : interval_integrable f μ a b)
(c : 𝕜) :
interval_integrable (λ (x : ℝ), f x / c) μ a b
theorem
interval_integrable.comp_mul_left
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
(hf : interval_integrable f measure_theory.measure_space.volume a b)
(c : ℝ) :
interval_integrable (λ (x : ℝ), f (c * x)) measure_theory.measure_space.volume (a / c) (b / c)
theorem
interval_integrable.comp_mul_right
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
(hf : interval_integrable f measure_theory.measure_space.volume a b)
(c : ℝ) :
interval_integrable (λ (x : ℝ), f (x * c)) measure_theory.measure_space.volume (a / c) (b / c)
theorem
interval_integrable.comp_add_right
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
(hf : interval_integrable f measure_theory.measure_space.volume a b)
(c : ℝ) :
interval_integrable (λ (x : ℝ), f (x + c)) measure_theory.measure_space.volume (a - c) (b - c)
theorem
interval_integrable.comp_add_left
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
(hf : interval_integrable f measure_theory.measure_space.volume a b)
(c : ℝ) :
interval_integrable (λ (x : ℝ), f (c + x)) measure_theory.measure_space.volume (a - c) (b - c)
theorem
interval_integrable.comp_sub_right
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
(hf : interval_integrable f measure_theory.measure_space.volume a b)
(c : ℝ) :
interval_integrable (λ (x : ℝ), f (x - c)) measure_theory.measure_space.volume (a + c) (b + c)
theorem
interval_integrable.iff_comp_neg
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ} :
interval_integrable f measure_theory.measure_space.volume a b ↔ interval_integrable (λ (x : ℝ), f (-x)) measure_theory.measure_space.volume (-a) (-b)
theorem
interval_integrable.comp_sub_left
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{a b : ℝ}
(hf : interval_integrable f measure_theory.measure_space.volume a b)
(c : ℝ) :
interval_integrable (λ (x : ℝ), f (c - x)) measure_theory.measure_space.volume (c - a) (c - b)
theorem
continuous_on.interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
{u : ℝ → E}
{a b : ℝ}
(hu : continuous_on u (set.uIcc a b)) :
interval_integrable u μ a b
theorem
continuous_on.interval_integrable_of_Icc
{E : Type u_3}
[normed_add_comm_group E]
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
{u : ℝ → E}
{a b : ℝ}
(h : a ≤ b)
(hu : continuous_on u (set.Icc a b)) :
interval_integrable u μ a b
theorem
continuous.interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
{u : ℝ → E}
(hu : continuous u)
(a b : ℝ) :
interval_integrable u μ a b
A continuous function on ℝ is interval_integrable with respect to any locally finite measure
ν on ℝ.
theorem
monotone_on.interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
[conditionally_complete_linear_order E]
[order_topology E]
[topological_space.second_countable_topology E]
{u : ℝ → E}
{a b : ℝ}
(hu : monotone_on u (set.uIcc a b)) :
interval_integrable u μ a b
theorem
antitone_on.interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
[conditionally_complete_linear_order E]
[order_topology E]
[topological_space.second_countable_topology E]
{u : ℝ → E}
{a b : ℝ}
(hu : antitone_on u (set.uIcc a b)) :
interval_integrable u μ a b
theorem
monotone.interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
[conditionally_complete_linear_order E]
[order_topology E]
[topological_space.second_countable_topology E]
{u : ℝ → E}
{a b : ℝ}
(hu : monotone u) :
interval_integrable u μ a b
theorem
antitone.interval_integrable
{E : Type u_3}
[normed_add_comm_group E]
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
[conditionally_complete_linear_order E]
[order_topology E]
[topological_space.second_countable_topology E]
{u : ℝ → E}
{a b : ℝ}
(hu : antitone u) :
interval_integrable u μ a b
theorem
filter.tendsto.eventually_interval_integrable_ae
{ι : Type u_1}
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{l l' : filter ℝ}
(hfm : strongly_measurable_at_filter f l' μ)
[filter.tendsto_Ixx_class set.Ioc l l']
[l'.is_measurably_generated]
(hμ : μ.finite_at_filter l')
{c : E}
(hf : filter.tendsto f (l' ⊓ μ.ae) (nhds c))
{u v : ι → ℝ}
{lt : filter ι}
(hu : filter.tendsto u lt l)
(hv : filter.tendsto v lt l) :
∀ᶠ (t : ι) in lt, interval_integrable 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_interval_integrable_ae will generate goals filter ℝ and
tendsto_Ixx_class Ioc ?m_1 l'.
theorem
filter.tendsto.eventually_interval_integrable
{ι : Type u_1}
{E : Type u_3}
[normed_add_comm_group E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{l l' : filter ℝ}
(hfm : strongly_measurable_at_filter f l' μ)
[filter.tendsto_Ixx_class set.Ioc l l']
[l'.is_measurably_generated]
(hμ : μ.finite_at_filter 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, interval_integrable 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_interval_integrable_ae will generate goals filter ℝ and
tendsto_Ixx_class 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.
noncomputable
def
interval_integral
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
(f : ℝ → E)
(a b : ℝ)
(μ : measure_theory.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 ∂μ.
@[simp]
theorem
interval_integral.integral_zero
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ} :
@[simp]
theorem
interval_integral.integral_same
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ} :
theorem
interval_integral.integral_undef
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(h : ¬interval_integrable f μ a b) :
theorem
interval_integral.interval_integrable_of_integral_ne_zero
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(h : ∫ (x : ℝ) in a..b, f x ∂μ ≠ 0) :
interval_integrable f μ a b
theorem
interval_integral.integral_non_ae_strongly_measurable
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(hf : ¬measure_theory.ae_strongly_measurable f (μ.restrict (set.uIoc a b))) :
theorem
interval_integral.integral_non_ae_strongly_measurable_of_le
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(h : a ≤ b)
(hf : ¬measure_theory.ae_strongly_measurable f (μ.restrict (set.Ioc a b))) :
theorem
interval_integral.norm_integral_min_max
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(f : ℝ → E) :
theorem
interval_integral.norm_integral_le_of_norm_le
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{g : ℝ → ℝ}
(h : ∀ᵐ (t : ℝ) ∂μ.restrict (set.uIoc a b), ‖f t‖ ≤ g t)
(hbound : interval_integrable g μ a b) :
@[simp]
theorem
interval_integral.integral_add
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f g : ℝ → E}
{μ : measure_theory.measure ℝ}
(hf : interval_integrable f μ a b)
(hg : interval_integrable g μ a b) :
theorem
interval_integral.integral_finset_sum
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{ι : Type u_1}
{s : finset ι}
{f : ι → ℝ → E}
(h : ∀ (i : ι), i ∈ s → interval_integrable (f i) μ a b) :
@[simp]
theorem
interval_integral.integral_sub
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f g : ℝ → E}
{μ : measure_theory.measure ℝ}
(hf : interval_integrable f μ a b)
(hg : interval_integrable g μ a b) :
@[simp]
theorem
interval_integral.integral_smul
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
[smul_comm_class ℝ 𝕜 E]
(r : 𝕜)
(f : ℝ → E) :
@[simp]
theorem
interval_integral.integral_smul_const
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
[normed_space 𝕜 E]
(f : ℝ → 𝕜)
(c : E) :
theorem
interval_integral.integral_const'
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(c : E) :
@[simp]
theorem
interval_integral.integral_const
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
(c : E) :
theorem
continuous_linear_map.interval_integral_apply
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{μ : measure_theory.measure ℝ}
[is_R_or_C 𝕜]
[normed_space 𝕜 E]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{a b : ℝ}
{φ : ℝ → (F →L[𝕜] E)}
(hφ : interval_integrable φ μ a b)
(v : F) :
theorem
continuous_linear_map.interval_integral_comp_comm
{𝕜 : Type u_2}
{E : Type u_3}
{F : Type u_4}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
[is_R_or_C 𝕜]
[normed_space 𝕜 E]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[normed_space ℝ F]
[complete_space F]
(L : E →L[𝕜] F)
(hf : interval_integrable f μ a b) :
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
interval_integral.integral_congr
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{f g : ℝ → E}
{μ : measure_theory.measure ℝ}
{a b : ℝ}
(h : set.eq_on f g (set.uIcc a b)) :
If two functions are equal in the relevant interval, their interval integrals are also equal.
theorem
interval_integral.integral_add_adjacent_intervals_cancel
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b c : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(hab : interval_integrable f μ a b)
(hbc : interval_integrable f μ b c) :
theorem
interval_integral.integral_add_adjacent_intervals
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b c : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(hab : interval_integrable f μ a b)
(hbc : interval_integrable f μ b c) :
theorem
interval_integral.sum_integral_adjacent_intervals_Ico
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{a : ℕ → ℝ}
{m n : ℕ}
(hmn : m ≤ n)
(hint : ∀ (k : ℕ), k ∈ set.Ico m n → interval_integrable f μ (a k) (a (k + 1))) :
theorem
interval_integral.sum_integral_adjacent_intervals
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{a : ℕ → ℝ}
{n : ℕ}
(hint : ∀ (k : ℕ), k < n → interval_integrable f μ (a k) (a (k + 1))) :
theorem
interval_integral.integral_interval_sub_left
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b c : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(hab : interval_integrable f μ a b)
(hac : interval_integrable f μ a c) :
theorem
interval_integral.integral_interval_add_interval_comm
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b c d : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(hab : interval_integrable f μ a b)
(hcd : interval_integrable f μ c d)
(hac : interval_integrable f μ a c) :
theorem
interval_integral.integral_interval_sub_interval_comm
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b c d : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(hab : interval_integrable f μ a b)
(hcd : interval_integrable f μ c d)
(hac : interval_integrable f μ a c) :
theorem
interval_integral.integral_interval_sub_interval_comm'
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b c d : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(hab : interval_integrable f μ a b)
(hcd : interval_integrable f μ c d)
(hac : interval_integrable f μ a c) :
theorem
interval_integral.integral_Iic_sub_Iic
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
(ha : measure_theory.integrable_on f (set.Iic a) μ)
(hb : measure_theory.integrable_on f (set.Iic b) μ) :
theorem
interval_integral.integral_const_of_cdf
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_finite_measure μ]
(c : E) :
If μ is a finite measure then ∫ x in a..b, c ∂μ = (μ (Iic b) - μ (Iic a)) • c.
theorem
interval_integral.integral_eq_integral_of_support_subset
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{a b : ℝ}
(h : function.support f ⊆ set.Ioc a b) :
theorem
interval_integral.tendsto_integral_filter_of_dominated_convergence
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{ι : Type u_1}
{l : filter ι}
[l.is_countably_generated]
{F : ι → ℝ → E}
(bound : ℝ → ℝ)
(hF_meas : ∀ᶠ (n : ι) in l, measure_theory.ae_strongly_measurable (F n) (μ.restrict (set.uIoc a b)))
(h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ set.uIoc a b → ‖F n x‖ ≤ bound x)
(bound_integrable : interval_integrable bound μ a b)
(h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ set.uIoc a b → filter.tendsto (λ (n : ι), F n x) l (nhds (f x))) :
Lebesgue dominated convergence theorem for filters with a countable basis
theorem
interval_integral.has_sum_integral_of_dominated_convergence
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{f : ℝ → E}
{μ : measure_theory.measure ℝ}
{ι : Type u_1}
[countable ι]
{F : ι → ℝ → E}
(bound : ι → ℝ → ℝ)
(hF_meas : ∀ (n : ι), measure_theory.ae_strongly_measurable (F n) (μ.restrict (set.uIoc a b)))
(h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → ‖F n t‖ ≤ bound n t)
(bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → summable (λ (n : ι), bound n t))
(bound_integrable : interval_integrable (λ (t : ℝ), ∑' (n : ι), bound n t) μ a b)
(h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → has_sum (λ (n : ι), F n t) (f t)) :
Lebesgue dominated convergence theorem for series.
theorem
interval_integral.has_sum_interval_integral_of_summable_norm
{ι : Type u_1}
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
[countable ι]
{f : ι → C(ℝ, E)}
(hf_sum : summable (λ (i : ι), ‖continuous_map.restrict ↑{carrier := set.uIcc a b, is_compact' := _} (f i)‖)) :
Interval integrals commute with countable sums, when the supremum norms are summable (a special case of the dominated convergence theorem).
theorem
interval_integral.tsum_interval_integral_eq_of_summable_norm
{ι : Type u_1}
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
[countable ι]
{f : ι → C(ℝ, E)}
(hf_sum : summable (λ (i : ι), ‖continuous_map.restrict ↑{carrier := set.uIcc a b, is_compact' := _} (f i)‖)) :
theorem
interval_integral.continuous_within_at_of_dominated_interval
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{μ : measure_theory.measure ℝ}
{X : Type u_6}
[topological_space X]
[topological_space.first_countable_topology X]
{F : X → ℝ → E}
{x₀ : X}
{bound : ℝ → ℝ}
{a b : ℝ}
{s : set X}
(hF_meas : ∀ᶠ (x : X) in nhds_within x₀ s, measure_theory.ae_strongly_measurable (F x) (μ.restrict (set.uIoc a b)))
(h_bound : ∀ᶠ (x : X) in nhds_within x₀ s, ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → ‖F x t‖ ≤ bound t)
(bound_integrable : interval_integrable bound μ a b)
(h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → continuous_within_at (λ (x : X), 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 (λ x, F x t)
is continuous at x₀ within s for almost every t in [a, b]
then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.
theorem
interval_integral.continuous_at_of_dominated_interval
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{μ : measure_theory.measure ℝ}
{X : Type u_6}
[topological_space X]
[topological_space.first_countable_topology X]
{F : X → ℝ → E}
{x₀ : X}
{bound : ℝ → ℝ}
{a b : ℝ}
(hF_meas : ∀ᶠ (x : X) in nhds x₀, measure_theory.ae_strongly_measurable (F x) (μ.restrict (set.uIoc a b)))
(h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → ‖F x t‖ ≤ bound t)
(bound_integrable : interval_integrable bound μ a b)
(h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → continuous_at (λ (x : X), 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 (λ x, F x t)
is continuous at x₀ for almost every t in [a, b]
then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.
theorem
interval_integral.continuous_of_dominated_interval
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{μ : measure_theory.measure ℝ}
{X : Type u_6}
[topological_space X]
[topological_space.first_countable_topology X]
{F : X → ℝ → E}
{bound : ℝ → ℝ}
{a b : ℝ}
(hF_meas : ∀ (x : X), measure_theory.ae_strongly_measurable (F x) (μ.restrict (set.uIoc a b)))
(h_bound : ∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → ‖F x t‖ ≤ bound t)
(bound_integrable : interval_integrable bound μ a b)
(h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ set.uIoc a b → continuous (λ (x : X), 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 (λ x, F x t) is continuous for almost every t in [a, b]
then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.
theorem
interval_integral.continuous_within_at_primitive
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b₀ b₁ b₂ : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
(hb₀ : ⇑μ {b₀} = 0)
(h_int : interval_integrable f μ (linear_order.min a b₁) (linear_order.max a b₂)) :
theorem
interval_integral.continuous_on_primitive
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
[measure_theory.has_no_atoms μ]
(h_int : measure_theory.integrable_on f (set.Icc a b) μ) :
theorem
interval_integral.continuous_on_primitive_Icc
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
[measure_theory.has_no_atoms μ]
(h_int : measure_theory.integrable_on f (set.Icc a b) μ) :
theorem
interval_integral.continuous_on_primitive_interval'
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b₁ b₂ : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
[measure_theory.has_no_atoms μ]
(h_int : interval_integrable f μ b₁ b₂)
(ha : a ∈ set.uIcc b₁ b₂) :
Note: this assumes that f is interval_integrable, in contrast to some other lemmas here.
theorem
interval_integral.continuous_on_primitive_interval
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
[measure_theory.has_no_atoms μ]
(h_int : measure_theory.integrable_on f (set.uIcc a b) μ) :
theorem
interval_integral.continuous_on_primitive_interval_left
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{a b : ℝ}
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
[measure_theory.has_no_atoms μ]
(h_int : measure_theory.integrable_on f (set.uIcc a b) μ) :
theorem
interval_integral.continuous_primitive
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
[measure_theory.has_no_atoms μ]
(h_int : ∀ (a b : ℝ), interval_integrable f μ a b)
(a : ℝ) :
theorem
measure_theory.integrable.continuous_primitive
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
[measure_theory.has_no_atoms μ]
(h_int : measure_theory.integrable f μ)
(a : ℝ) :
theorem
interval_integral.integral_pos_iff_support_of_nonneg_ae'
{f : ℝ → ℝ}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(hf : 0 ≤ᵐ[μ.restrict (set.uIoc a b)] f)
(hfi : interval_integrable 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
interval_integral.integral_pos_iff_support_of_nonneg_ae
{f : ℝ → ℝ}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(hf : 0 ≤ᵐ[μ] f)
(hfi : interval_integrable 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
interval_integral.interval_integral_pos_of_pos_on
{f : ℝ → ℝ}
{a b : ℝ}
(hfi : interval_integrable f measure_theory.measure_space.volume a b)
(hpos : ∀ (x : ℝ), 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
interval_integral.interval_integral_pos_of_pos
{f : ℝ → ℝ}
{a b : ℝ}
(hfi : interval_integrable f measure_theory.measure_space.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 interval_integral_pos_of_pos_on
for a version only assuming positivity of f on (a, b) rather than everywhere.)
theorem
interval_integral.integral_lt_integral_of_ae_le_of_measure_set_of_lt_ne_zero
{f g : ℝ → ℝ}
{a b : ℝ}
{μ : measure_theory.measure ℝ}
(hab : a ≤ b)
(hfi : interval_integrable f μ a b)
(hgi : interval_integrable 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
interval_integral.integral_lt_integral_of_continuous_on_of_le_of_exists_lt
{f g : ℝ → ℝ}
{a b : ℝ}
(hab : a < b)
(hfc : continuous_on f (set.Icc a b))
(hgc : continuous_on g (set.Icc a b))
(hle : ∀ (x : ℝ), x ∈ set.Ioc a b → f x ≤ g x)
(hlt : ∃ (c : ℝ) (H : 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
measure_theory.integrable.has_sum_interval_integral
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{μ : measure_theory.measure ℝ}
{f : ℝ → E}
(hfi : measure_theory.integrable f μ)
(y : ℝ) :
theorem
measure_theory.integrable.has_sum_interval_integral_comp_add_int
{E : Type u_3}
[normed_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
{f : ℝ → E}
(hfi : measure_theory.integrable f measure_theory.measure_space.volume) :