Mazur's lemma

A weak limit in a locally convex space belongs to the closure of the convex hull of the range. In a seminormed space, finite convex combinations from successive tails of a weakly convergent sequence converge in norm to the weak limit. The coefficients are real and nonnegative even for complex spaces.

exists_sum_smul_norm_sub_lt_of_tendsto_weak gives a finite combination from any specified tail with any positive error tolerance. exists_tendsto_sum_smul_of_tendsto_weak chooses such combinations as a norm-convergent sequence. In both statements, the indices in the nth tail are written as n + i, so no coefficient can involve an earlier term.

Convex.mem_of_tendsto_weak deduces that a closed real-convex set contains weak limits of families in it.

These results require neither completeness nor separability. They use Mathlib's Convex.toWeakSpace_closure to pass from weak convergence to norm approximation, and convexHull_range_eq_exists_affineCombination to extract the finite coefficients.

References

• R. E. Megginson, An Introduction to Banach Space Theory, §2.5 (Mazur's theorem).

theorem TauCeti.mem_closure_convexHull_range_of_tendsto_weak {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {ι : Type u_3} {l : Filter ι} [l.NeBot] {u : ι → E} {x : E} (hu : Filter.Tendsto (fun (n : ι) => (toWeakSpace 𝕜 E) (u n)) l (nhds ((toWeakSpace 𝕜 E) x))) : x ∈ closure ((convexHull ℝ) (Set.range u))

A weak limit along a nontrivial filter in a locally convex space lies in the closure of the real convex hull of the range, taken in the original topology.

theorem Convex.mem_of_tendsto_weak {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {ι : Type u_3} {s : Set E} (hs : Convex ℝ s) (hsc : IsClosed s) {l : Filter ι} [l.NeBot] {u : ι → E} {x : E} (hu : ∀ (i : ι), u i ∈ s) (hlim : Filter.Tendsto (fun (i : ι) => (toWeakSpace 𝕜 E) (u i)) l (nhds ((toWeakSpace 𝕜 E) x))) : x ∈ s

A closed real-convex set in a locally convex space contains every weak limit of a family in it, along any nontrivial filter.

theorem TauCeti.exists_sum_smul_norm_sub_lt_of_tendsto_weak {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {u : ℕ → E} {x : E} (hu : Filter.Tendsto (fun (n : ℕ) => (toWeakSpace 𝕜 E) (u n)) Filter.atTop (nhds ((toWeakSpace 𝕜 E) x))) (n : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset ℕ) (w : ℕ → ℝ), (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ ‖∑ i ∈ s, w i • u (n + i) - x‖ < ε

Mazur's lemma, with explicit finite coefficients: every tail of a weakly convergent sequence admits a convex combination within any positive norm distance of its weak limit.

theorem TauCeti.exists_tendsto_sum_smul_of_tendsto_weak {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {u : ℕ → E} {x : E} (hu : Filter.Tendsto (fun (n : ℕ) => (toWeakSpace 𝕜 E) (u n)) Filter.atTop (nhds ((toWeakSpace 𝕜 E) x))) : ∃ (s : ℕ → Finset ℕ) (w : ℕ → ℕ → ℝ), (∀ (n i : ℕ), i ∈ s n → 0 ≤ w n i) ∧ (∀ (n : ℕ), ∑ i ∈ s n, w n i = 1) ∧ Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ s n, w n i • u (n + i)) Filter.atTop (nhds x)

Mazur's lemma, in sequential form: choose a finite real convex combination from the nth tail for every n, so that the combinations converge in norm to the weak limit.