Convergence and measurability for set-to-function extensions #
This file proves norm estimates and dominated-convergence results for MeasureTheory.setToFun.
It includes sequential and filter versions of dominated convergence, applications to infinite
sums, strong measurability for parameterized families, and continuity results for families
dominated by an integrable function.
theorem
MeasureTheory.norm_setToFun_le_mul_norm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp E 1 μ))
(hC : 0 ≤ C)
:
theorem
MeasureTheory.norm_setToFun_le_mul_norm'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.norm_setToFun_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : Integrable f μ)
(hC : 0 ≤ C)
:
theorem
MeasureTheory.norm_setToFun_le'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : Integrable f μ)
:
theorem
MeasureTheory.enorm_setToFun_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
:
theorem
MeasureTheory.norm_setToFun_le_toReal
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
:
theorem
MeasureTheory.tendsto_setToFun_of_dominated_convergence
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{fs : ℕ → α → E}
{f : α → E}
(bound : α → ℝ)
(fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ)
(bound_integrable : Integrable bound μ)
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => fs n a) Filter.atTop (nhds (f a)))
:
Filter.Tendsto (fun (n : ℕ) => setToFun μ T hT (fs n)) Filter.atTop (nhds (setToFun μ T hT f))
Lebesgue dominated convergence theorem provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
setToFun.
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_setToFun_filter_of_dominated_convergence
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{ι : Type u_4}
{l : Filter ι}
[l.IsCountablyGenerated]
{fs : ι → α → E}
{f : α → E}
(bound : α → ℝ)
(hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ)
(h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ι) => fs n a) l (nhds (f a)))
:
Filter.Tendsto (fun (n : ι) => setToFun μ T hT (fs n)) l (nhds (setToFun μ T hT f))
Lebesgue dominated convergence theorem for filters with a countable basis
theorem
MeasureTheory.hasSum_setToFun_of_dominated_convergence
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{ι : Type u_4}
[Countable ι]
{F✝ : ι → α → E}
{f : α → E}
(bound : ι → α → ℝ)
(hF_meas : ∀ (n : ι), AEStronglyMeasurable (F✝ n) μ)
(h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F✝ n a‖ ≤ bound n a)
(bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun (n : ι) => bound n a)
(bound_integrable : Integrable (fun (a : α) => ∑' (n : ι), bound n a) μ)
(h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) => F✝ n a) (f a))
:
Lebesgue dominated convergence theorem for series.
theorem
MeasureTheory.setToFun_tsum
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
[CompleteSpace E]
(hT : DominatedFinMeasAdditive μ T C)
{ι : Type u_4}
[Countable ι]
{f : ι → α → E}
(hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ)
(hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤)
:
theorem
MeasureTheory.tendsto_setToFun_filter_of_norm_le_const
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{ι : Type u_4}
{l : Filter ι}
[l.IsCountablyGenerated]
{F✝ : ι → α → E}
[IsFiniteMeasure μ]
{f : α → E}
(h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F✝ n) μ)
(h_bound : ∃ (C : ℝ), ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F✝ n ω‖ ≤ C)
(h_lim : ∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun (n : ι) => F✝ n ω) l (nhds (f ω)))
:
Filter.Tendsto (fun (n : ι) => setToFun μ T hT (F✝ n)) l (nhds (setToFun μ T hT f))
Corollary of the Lebesgue dominated convergence theorem: If a sequence of functions F n is
(eventually) uniformly bounded by a constant and converges (eventually) pointwise to a
function f, then the integrals of F n with respect to a finite measure μ converge
to the integral of f.
theorem
measurableSet_integrable
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_4}
{mβ : MeasurableSpace β}
[MeasureTheory.SFinite μ]
⦃f : β → α → E⦄
(hf : MeasureTheory.StronglyMeasurable (Function.uncurry f))
:
MeasurableSet {x : β | MeasureTheory.Integrable (f x) μ}
theorem
MeasureTheory.StronglyMeasurable.setToFun_prod_right
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{β : Type u_4}
{mβ : MeasurableSpace β}
[SFinite μ]
(hT : DominatedFinMeasAdditive μ T C)
(h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun (x : β) => T (Prod.mk x ⁻¹' s))
⦃f : β → α → E⦄
(hf : StronglyMeasurable (Function.uncurry f))
:
StronglyMeasurable fun (x : β) => setToFun μ T hT (f x)
The setToFun operation is measurable. This shows that the integrand of (the right-hand-side
of) Fubini's theorem is measurable. This version has f in curried form.
theorem
MeasureTheory.continuousWithinAt_setToFun_of_dominated
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_4}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{x₀ : X}
{bound : α → ℝ}
{s : Set X}
(hfs_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun (x : X) => fs x a) s x₀)
:
ContinuousWithinAt (fun (x : X) => setToFun μ T hT (fs x)) s x₀
theorem
MeasureTheory.continuousAt_setToFun_of_dominated
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_4}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{x₀ : X}
{bound : α → ℝ}
(hfs_meas : ∀ᶠ (x : X) in nhds x₀, AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun (x : X) => fs x a) x₀)
:
ContinuousAt (fun (x : X) => setToFun μ T hT (fs x)) x₀
theorem
MeasureTheory.continuousOn_setToFun_of_dominated
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_4}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{bound : α → ℝ}
{s : Set X}
(hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun (x : X) => fs x a) s)
:
ContinuousOn (fun (x : X) => setToFun μ T hT (fs x)) s
theorem
MeasureTheory.continuous_setToFun_of_dominated
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_4}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{bound : α → ℝ}
(hfs_meas : ∀ (x : X), AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun (x : X) => fs x a)
:
Continuous fun (x : X) => setToFun μ T hT (fs x)