The dominated convergence theorem #
This file collects various results related to the Lebesgue dominated convergence theorem for the Bochner integral.
Main results #
MeasureTheory.tendsto_integral_of_dominated_convergence: the Lebesgue dominated convergence theorem for the Bochner integralMeasureTheory.hasSum_integral_of_dominated_convergence: the Lebesgue dominated convergence theorem for seriesMeasureTheory.integral_tsum,MeasureTheory.integral_tsum_of_summable_integral_norm: the integral andtsums commute, if the norms of the functions form a summable seriesintervalIntegral.hasSum_integral_of_dominated_convergence: the Lebesgue dominated convergence theorem for parametric interval integralsintervalIntegral.continuous_of_dominated_interval: continuity of the interval integral w.r.t. a parameterintervalIntegral.continuous_primitiveand friends: primitives of interval integrable measurable functions are continuous
The Lebesgue dominated convergence theorem for the Bochner integral #
theorem
MeasureTheory.tendsto_integral_of_dominated_convergence
{α : Type u_1}
{G : Type u_3}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{F : ℕ → α → G}
{f : α → G}
(bound : α → ℝ)
(F_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ)
(bound_integrable : MeasureTheory.Integrable bound μ)
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a)))
:
Filter.Tendsto (fun (n : ℕ) => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))
Lebesgue dominated convergence theorem provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their integrals.
We could weaken the condition bound_integrable to require HasFiniteIntegral bound μ instead
(i.e. not requiring that bound is measurable), but in all applications proving integrability
is easier.
theorem
MeasureTheory.tendsto_integral_filter_of_dominated_convergence
{α : Type u_1}
{G : Type u_3}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_4}
{l : Filter ι}
[l.IsCountablyGenerated]
{F : ι → α → G}
{f : α → G}
(bound : α → ℝ)
(hF_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) μ)
(h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(bound_integrable : MeasureTheory.Integrable bound μ)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ι) => F n a) l (nhds (f a)))
:
Filter.Tendsto (fun (n : ι) => ∫ (a : α), F n a ∂μ) l (nhds (∫ (a : α), f a ∂μ))
Lebesgue dominated convergence theorem for filters with a countable basis
theorem
MeasureTheory.hasSum_integral_of_dominated_convergence
{α : Type u_1}
{G : Type u_3}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_4}
[Countable ι]
{F : ι → α → G}
{f : α → G}
(bound : ι → α → ℝ)
(hF_meas : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) μ)
(h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a)
(bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun (n : ι) => bound n a)
(bound_integrable : MeasureTheory.Integrable (fun (a : α) => ∑' (n : ι), bound n a) μ)
(h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) => F n a) (f a))
:
HasSum (fun (n : ι) => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
Lebesgue dominated convergence theorem for series.
theorem
MeasureTheory.integral_tsum
{α : Type u_1}
{G : Type u_3}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_4}
[Countable ι]
{f : ι → α → G}
(hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ)
(hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤)
:
∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ
theorem
MeasureTheory.hasSum_integral_of_summable_integral_norm
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_4}
[Countable ι]
{F : ι → α → E}
(hF_int : ∀ (i : ι), MeasureTheory.Integrable (F i) μ)
(hF_sum : Summable fun (i : ι) => ∫ (a : α), ‖F i a‖ ∂μ)
:
HasSum (fun (x : ι) => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
theorem
MeasureTheory.integral_tsum_of_summable_integral_norm
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_4}
[Countable ι]
{F : ι → α → E}
(hF_int : ∀ (i : ι), MeasureTheory.Integrable (F i) μ)
(hF_sum : Summable fun (i : ι) => ∫ (a : α), ‖F i a‖ ∂μ)
:
∑' (i : ι), ∫ (a : α), F i a ∂μ = ∫ (a : α), ∑' (i : ι), F i a ∂μ
theorem
Antitone.tendsto_setIntegral
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : ℕ → Set α}
{f : α → E}
(hsm : ∀ (i : ℕ), MeasurableSet (s i))
(h_anti : Antitone s)
(hfi : MeasureTheory.IntegrableOn f (s 0) μ)
:
Filter.Tendsto (fun (i : ℕ) => ∫ (a : α) in s i, f a ∂μ) Filter.atTop (nhds (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
@[deprecated Antitone.tendsto_setIntegral]
theorem
Antitone.tendsto_set_integral
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : ℕ → Set α}
{f : α → E}
(hsm : ∀ (i : ℕ), MeasurableSet (s i))
(h_anti : Antitone s)
(hfi : MeasureTheory.IntegrableOn f (s 0) μ)
:
Filter.Tendsto (fun (i : ℕ) => ∫ (a : α) in s i, f a ∂μ) Filter.atTop (nhds (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
Alias of Antitone.tendsto_setIntegral.
The Lebesgue dominated convergence theorem for interval integrals #
As an application, we show continuity of parametric integrals.
theorem
intervalIntegral.tendsto_integral_filter_of_dominated_convergence
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a : ℝ}
{b : ℝ}
{f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}
{ι : Type u_5}
{l : Filter ι}
[l.IsCountablyGenerated]
{F : ι → ℝ → E}
(bound : ℝ → ℝ)
(hF_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) (μ.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_5}
[Countable ι]
{F : ι → ℝ → E}
(bound : ι → ℝ → ℝ)
(hF_meas : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) (μ.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))
:
Lebesgue dominated convergence theorem for parametric interval integrals.
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' := ⋯ }) (f i)‖)
:
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' := ⋯ }) (f i)‖)
:
theorem
intervalIntegral.continuousWithinAt_of_dominated_interval
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure ℝ}
{X : Type u_5}
[TopologicalSpace X]
[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) (μ.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 : X) => F x t) s x₀)
:
ContinuousWithinAt (fun (x : 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_5}
[TopologicalSpace X]
[FirstCountableTopology X]
{F : X → ℝ → E}
{x₀ : X}
{bound : ℝ → ℝ}
{a : ℝ}
{b : ℝ}
(hF_meas : ∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.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 : X) => F x t) x₀)
:
ContinuousAt (fun (x : 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_5}
[TopologicalSpace X]
[FirstCountableTopology X]
{F : X → ℝ → E}
{bound : ℝ → ℝ}
{a : ℝ}
{b : ℝ}
(hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.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 : X) => F x t)
:
Continuous fun (x : 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_1}
[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.continuousAt_parametric_primitive_of_dominated
{μ : MeasureTheory.Measure ℝ}
{X : Type u_2}
[TopologicalSpace X]
[FirstCountableTopology X]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : X → ℝ → E}
(bound : ℝ → ℝ)
(a : ℝ)
(b : ℝ)
{a₀ : ℝ}
{b₀ : ℝ}
{x₀ : X}
(hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
(h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t)
(bound_integrable : IntervalIntegrable bound μ a b)
(h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun (x : X) => F x t) x₀)
(ha₀ : a₀ ∈ Set.Ioo a b)
(hb₀ : b₀ ∈ Set.Ioo a b)
(hμb₀ : ↑↑μ {b₀} = 0)
:
ContinuousAt (fun (p : X × ℝ) => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
theorem
intervalIntegral.continuousOn_primitive
{E : Type u_1}
[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_1}
[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_1}
[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_1}
[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_1}
[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_1}
[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_1}
[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 ∂μ