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 integral
• MeasureTheory.hasSum_integral_of_dominated_convergence: the Lebesgue dominated convergence theorem for series
• MeasureTheory.integral_tsum, MeasureTheory.integral_tsum_of_summable_integral_norm: the integral and tsums commute, if the norms of the functions form a summable series
• intervalIntegral.hasSum_integral_of_dominated_convergence: the Lebesgue dominated convergence theorem for parametric interval integrals
• intervalIntegral.continuous_of_dominated_interval: continuity of the interval integral w.r.t. a parameter
• intervalIntegral.continuous_primitive and 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 ι} [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 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) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t) (bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Summable fun (n : ι) => bound n t) (bound_integrable : IntervalIntegrable (fun (t : ℝ) => ∑' (n : ι), bound n t) μ a b) (h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasSum (fun (n : ι) => F n t) (f t)) : HasSum (fun (n : ι) => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)

Lebesgue dominated convergence theorem for 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 : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a : ℝ} {b : ℝ} {s : Set X} (hF_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousWithinAt (fun (x : 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) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousAt (fun (x : 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) (MeasureTheory.Measure.restrict μ (Ι a b))) (h_bound : ∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Continuous fun (x : 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) (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 ∂μ