Mazur's lemma

TheoremMazur's lemma, hull form#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), regarded also as a real vector space by restricting scalars. If a sequence \((u_n)_{n \in \mathbb{N}}\) in \(E\) converges to \(x \in E\) in the weak topology of \(E\) (the topology induced by the continuous \(\mathbb{K}\)-linear functionals on \(E\)), then for every \(N \in \mathbb{N}\) the point \(x\) lies in the norm closure of the real convex hull of the tail \(\{u_n : n \ge N\}\).

theorem mem_closure_convexHull_of_tendsto_weakSpace {u : ℕ → E} {x : E}
    (h : Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x)))
    (N : ℕ) :
    x ∈ closure (convexHull ℝ (u '' Set.Ici N))

Used by 2

Used byMazur's lemma, explicit finite convex combinations · Mazur's lemma, hull form for the whole sequence

TheoremMazur's lemma, hull form for the whole sequence#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), regarded also as a real vector space by restricting scalars. If a sequence \((u_n)_{n \in \mathbb{N}}\) in \(E\) converges to \(x \in E\) in the weak topology of \(E\) (the topology induced by the continuous \(\mathbb{K}\)-linear functionals on \(E\)), then \(x\) lies in the norm closure of the real convex hull of the set \(\{u_n : n \in \mathbb{N}\}\).

theorem mem_closure_convexHull_range_of_tendsto_weakSpace {u : ℕ → E} {x : E}
    (h : Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x))) :
    x ∈ closure (convexHull ℝ (Set.range u))

Uses 1

Proof usesMazur's lemma, hull form

TheoremMazur's lemma, explicit finite convex combinations#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), regarded also as a real vector space by restricting scalars. If a sequence \((u_n)_{n \in \mathbb{N}}\) in \(E\) converges to \(x \in E\) in the weak topology of \(E\) (the topology induced by the continuous \(\mathbb{K}\)-linear functionals on \(E\)), then for every \(N \in \mathbb{N}\) and every real \(\varepsilon > 0\) there are a finite index set \(I\), real weights \(w_i \ge 0\) with \(\sum_{i \in I} w_i = 1\) and natural numbers \(n_i \ge N\) for \(i \in I\) such that \(\left\| \sum_{i \in I} w_i u_{n_i} - x \right\| < \varepsilon\).

theorem exists_finite_convex_combination_norm_sub_lt_of_tendsto_weakSpace
    {u : ℕ → E} {x : E}
    (h : Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x)))
    (N : ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ (ι : Type) (_ : Fintype ι) (w : ι → ℝ) (n : ι → ℕ),
      (∀ i, 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ i, N ≤ n i) ∧
        ‖∑ i, w i • u (n i) - x‖ < ε

Uses 1 · Used by 1

Proof usesMazur's lemma, hull form

Used byMazur's lemma in the textbook phrasing

TheoremMazur's lemma in the textbook phrasing#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), regarded also as a real vector space by restricting scalars. Let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(E\) and \(x \in E\) such that \(f(u_n) \to f(x)\) for every continuous \(\mathbb{K}\)-linear functional \(f \colon E \to \mathbb{K}\). Then for every \(N \in \mathbb{N}\) and every real \(\varepsilon > 0\) there are a finite index set \(I\), real weights \(w_i \ge 0\) with \(\sum_{i \in I} w_i = 1\) and natural numbers \(n_i \ge N\) for \(i \in I\) such that \(\left\| \sum_{i \in I} w_i u_{n_i} - x \right\| < \varepsilon\).

theorem exists_finite_convex_combination_norm_sub_lt_of_forall_tendsto
    {u : ℕ → E} {x : E}
    (h : ∀ f : StrongDual 𝕜 E,
      Tendsto (fun n => f (u n)) atTop (𝓝 (f x)))
    (N : ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ (ι : Type) (_ : Fintype ι) (w : ι → ℝ) (n : ι → ℕ),
      (∀ i, 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ i, N ≤ n i) ∧
        ‖∑ i, w i • u (n i) - x‖ < ε

Uses 1

Proof usesMazur's lemma, explicit finite convex combinations

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.