Documentation

Mathlib.MeasureTheory.Integral.DominatedConvergence

The dominated convergence theorem #

This file collects various results related to the Lebesgue dominated convergence theorem for the Bochner integral.

Main results #

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 ι} [Filter.IsCountablyGenerated l] {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_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μ))

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 ι} [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 bF n x bound x) (bound_integrable : IntervalIntegrable bound μ a b) (h_lim : ∀ᵐ (x : ) ∂μ, x Ι a bFilter.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) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ (n : ι), ∀ᵐ (t : ) ∂μ, t Ι a bF n t bound n t) (bound_summable : ∀ᵐ (t : ) ∂μ, t Ι a bSummable fun (n : ι) => bound n t) (bound_integrable : IntervalIntegrable (fun (t : ) => ∑' (n : ι), bound n t) μ a b) (h_lim : ∀ᵐ (t : ) ∂μ, t Ι a bHasSum (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 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)) :
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' := }) (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_5} [TopologicalSpace X] [FirstCountableTopology X] {F : XE} {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 bF x t bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ) ∂μ, t Ι a bContinuousWithinAt (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 : XE} {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 bF x t bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ) ∂μ, t Ι a bContinuousAt (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 : XE} {bound : } {a : } {b : } (hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ (x : X), ∀ᵐ (t : ) ∂μ, t Ι a bF x t bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ) ∂μ, t Ι a bContinuous 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 : XE} (bound : ) (a : ) (b : ) {a₀ : } {b₀ : } {x₀ : X} (hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ) ∂MeasureTheory.Measure.restrict μ (Ι a b), F x t bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ) ∂MeasureTheory.Measure.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μ