Vitali's convergence theorem for maps into a pseudometric space

Let μ be a finite measure on X and let T n, T₀ : X → Y be almost-everywhere measurable maps into a second-countable pseudometric space. Mathlib's Vitali convergence theorem MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite characterises Lᵖ convergence of vector-valued functions as convergence in measure together with uniform integrability. This file transports it to Y-valued maps through the real-valued distances: for 1 ≤ p < ∞ and maps with finite p-th moment about a basepoint y₀, the distances dist (T n x) (T₀ x) converge to 0 in Lᵖ(μ) exactly when T n converges to T₀ in measure and the family dist (T n ·) y₀ is uniformly integrable in Lᵖ(μ).

The uniform integrability of dist (T n ·) y₀ does not depend on the basepoint y₀: by the triangle inequality, changing the basepoint changes each distance by at most the constant dist y₀ y₁, and constants are uniformly integrable over a finite measure. Uniform integrability is Mathlib's MeasureTheory.UnifIntegrable, the predicate its Vitali theorem uses. Mathlib's stronger MeasureTheory.UniformIntegrable adds a uniform Lᵖ bound on the family. The convergence theorem is stated with either predicate: when the Lᵖ convergence of the distances is assumed, the convergent sequence of their finite Lᵖ norms is bounded, and this bound upgrades MeasureTheory.UnifIntegrable to MeasureTheory.UniformIntegrable.

Main statements

• TauCeti.memLp_dist_of_memLp_dist — two maps with finite p-th moment about a basepoint have a distance with finite p-th moment;
• TauCeti.eLpNorm_dist_le_eLpNorm_dist_add, MeasureTheory.UnifIntegrable.dist_of_memLp_dist and MeasureTheory.UniformIntegrable.dist_of_memLp_dist — the triangle inequality lifted to Lᵖ norms of distances and to uniform integrability, with and without the uniform Lᵖ bound;
• TauCeti.unifIntegrable_dist_iff_dist and TauCeti.uniformIntegrable_dist_iff_dist — uniform integrability of the distances to a basepoint does not depend on the basepoint;
• TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_unifIntegrable — Vitali's theorem for maps into a pseudometric space: for 1 ≤ p < ∞, Lᵖ convergence of dist (T n ·) (T₀ ·) to 0 is convergence in measure together with uniform integrability of dist (T n ·) y₀;
• TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_uniformIntegrable — the same with MeasureTheory.UniformIntegrable, which also records the uniform Lᵖ bound.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, second edition, Birkhäuser 2008, Lemma 5.4.1, whose Lᵖ refinement is the statement proved here.

theorem TauCeti.memLp_dist_of_memLp_dist {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : MeasureTheory.Measure X} {p : ENNReal} {T T₀ : X → Y} {y₀ : Y} (hT : AEMeasurable T μ) (hT₀ : AEMeasurable T₀ μ) (hTp : MeasureTheory.MemLp (fun (x : X) => dist (T x) y₀) p μ) (hT₀p : MeasureTheory.MemLp (fun (x : X) => dist (T₀ x) y₀) p μ) : MeasureTheory.MemLp (fun (x : X) => dist (T x) (T₀ x)) p μ

Two almost-everywhere measurable maps with finite p-th moment about a basepoint y₀ have a distance with finite p-th moment.

theorem TauCeti.eLpNorm_dist_le_eLpNorm_dist_add {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : MeasureTheory.Measure X} {p : ENNReal} {T S S' : X → Y} (hp : 1 ≤ p) (hT : AEMeasurable T μ) (hS' : AEMeasurable S' μ) : MeasureTheory.eLpNorm (fun (x : X) => dist (T x) (S' x)) p μ ≤ MeasureTheory.eLpNorm (fun (x : X) => dist (T x) (S x)) p μ + MeasureTheory.eLpNorm (fun (x : X) => dist (S x) (S' x)) p μ

The triangle inequality for Lᵖ norms of distances: for 1 ≤ p, a map S : X → Y and almost-everywhere measurable maps T S' : X → Y, the Lᵖ(μ) norm of dist (T ·) (S' ·) is at most the sum of those of dist (T ·) (S ·) and dist (S ·) (S' ·).

theorem MeasureTheory.UnifIntegrable.dist_of_memLp_dist {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : Measure X} {p : ENNReal} {ι : Type u_3} {T : ι → X → Y} {S S' : X → Y} (h : UnifIntegrable (fun (i : ι) (x : X) => dist (T i x) (S x)) p μ) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hT : ∀ (i : ι), AEMeasurable (T i) μ) (hS' : AEMeasurable S' μ) (hSS' : MemLp (fun (x : X) => dist (S x) (S' x)) p μ) : UnifIntegrable (fun (i : ι) (x : X) => dist (T i x) (S' x)) p μ

Uniform integrability in Lᵖ(μ) of the distances dist (T i ·) (S ·) to a reference map S passes to any almost-everywhere measurable reference map S' with dist (S ·) (S' ·) of finite p-th moment, for 1 ≤ p < ∞: by the triangle inequality, changing the reference map changes each distance by at most the fixed Lᵖ function dist (S ·) (S' ·), and a single Lᵖ function is uniformly integrable.

theorem MeasureTheory.UniformIntegrable.dist_of_memLp_dist {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : Measure X} {p : ENNReal} {ι : Type u_3} {T : ι → X → Y} {S S' : X → Y} (h : UniformIntegrable (fun (i : ι) (x : X) => dist (T i x) (S x)) p μ) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hT : ∀ (i : ι), AEMeasurable (T i) μ) (hS' : AEMeasurable S' μ) (hSS' : MemLp (fun (x : X) => dist (S x) (S' x)) p μ) : UniformIntegrable (fun (i : ι) (x : X) => dist (T i x) (S' x)) p μ

Uniform integrability in Lᵖ(μ) with a uniform Lᵖ bound of the distances dist (T i ·) (S ·) to a reference map S passes to any almost-everywhere measurable reference map S' with dist (S ·) (S' ·) of finite p-th moment, for 1 ≤ p < ∞: the uniform bound grows by the Lᵖ norm of dist (S ·) (S' ·).

theorem TauCeti.unifIntegrable_dist_iff_dist {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : MeasureTheory.Measure X} {p : ENNReal} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_3} {T : ι → X → Y} {y₀ y₁ : Y} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hT : ∀ (i : ι), AEMeasurable (T i) μ) : MeasureTheory.UnifIntegrable (fun (i : ι) (x : X) => dist (T i x) y₀) p μ ↔ MeasureTheory.UnifIntegrable (fun (i : ι) (x : X) => dist (T i x) y₁) p μ

Uniform integrability in Lᵖ(μ) of the distances dist (T i ·) y₀ does not depend on the basepoint y₀, for 1 ≤ p < ∞ and a finite measure μ: changing the basepoint changes each distance by at most the constant dist y₀ y₁.

theorem TauCeti.uniformIntegrable_dist_iff_dist {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : MeasureTheory.Measure X} {p : ENNReal} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_3} {T : ι → X → Y} {y₀ y₁ : Y} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hT : ∀ (i : ι), AEMeasurable (T i) μ) : MeasureTheory.UniformIntegrable (fun (i : ι) (x : X) => dist (T i x) y₀) p μ ↔ MeasureTheory.UniformIntegrable (fun (i : ι) (x : X) => dist (T i x) y₁) p μ

Uniform integrability in Lᵖ(μ) with a uniform Lᵖ bound of the distances dist (T i ·) y₀ does not depend on the basepoint y₀, for 1 ≤ p < ∞ and a finite measure μ.

theorem TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_unifIntegrable {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : MeasureTheory.Measure X} {p : ENNReal} [MeasureTheory.IsFiniteMeasure μ] {T : ℕ → X → Y} {T₀ : X → Y} {y₀ : Y} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hT : ∀ (n : ℕ), AEMeasurable (T n) μ) (hT₀ : AEMeasurable T₀ μ) (hTp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : X) => dist (T n x) y₀) p μ) (hT₀p : MeasureTheory.MemLp (fun (x : X) => dist (T₀ x) y₀) p μ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : X) => dist (T n x) (T₀ x)) p μ) Filter.atTop (nhds 0) ↔ MeasureTheory.TendstoInMeasure μ T Filter.atTop T₀ ∧ MeasureTheory.UnifIntegrable (fun (n : ℕ) (x : X) => dist (T n x) y₀) p μ

Vitali's convergence theorem for maps into a pseudometric space. Let 1 ≤ p < ∞, let μ be a finite measure, and let the almost-everywhere measurable maps T n, T₀ : X → Y have finite p-th moment about a point y₀. Then dist (T n x) (T₀ x) tends to 0 in Lᵖ(μ) if and only if T n converges to T₀ in μ-measure and the family dist (T n ·) y₀ is uniformly integrable in Lᵖ(μ).

theorem TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_uniformIntegrable {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : MeasureTheory.Measure X} {p : ENNReal} [MeasureTheory.IsFiniteMeasure μ] {T : ℕ → X → Y} {T₀ : X → Y} {y₀ : Y} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hT : ∀ (n : ℕ), AEMeasurable (T n) μ) (hT₀ : AEMeasurable T₀ μ) (hTp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : X) => dist (T n x) y₀) p μ) (hT₀p : MeasureTheory.MemLp (fun (x : X) => dist (T₀ x) y₀) p μ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : X) => dist (T n x) (T₀ x)) p μ) Filter.atTop (nhds 0) ↔ MeasureTheory.TendstoInMeasure μ T Filter.atTop T₀ ∧ MeasureTheory.UniformIntegrable (fun (n : ℕ) (x : X) => dist (T n x) y₀) p μ

Vitali's convergence theorem for maps into a pseudometric space, with MeasureTheory.UniformIntegrable: under the hypotheses of TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_unifIntegrable, dist (T n x) (T₀ x) tends to 0 in Lᵖ(μ) if and only if T n converges to T₀ in μ-measure and the family dist (T n ·) y₀ is uniformly integrable in Lᵖ(μ) with a uniform Lᵖ bound.