Radon–Riesz property

TheoremRadon–Riesz theorem, inner-product form#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), not necessarily complete, let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(H\) and let \(x \in H\). If \(\langle u_n, y \rangle \to \langle x, y \rangle\) for every \(y \in H\) and \(\|u_n\| \to \|x\|\), then \(u_n \to x\) in norm.

theorem tendsto_of_tendsto_inner_and_tendsto_norm {u : ℕ → H} {x : H}
    (hinner : ∀ y : H, Tendsto (fun n => ⟪u n, y⟫_𝕜) atTop (𝓝 ⟪x, y⟫_𝕜))
    (hnorm : Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖)) :
    Tendsto u atTop (𝓝 x)

Used by 1

Used byRadon–Riesz characterization of norm convergence

TheoremRadon–Riesz theorem, dual-functionals form#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), not necessarily complete, let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(H\) and let \(x \in H\). If \(f(u_n) \to f(x)\) for every continuous linear functional \(f : H \to \mathbb{K}\) and \(\|u_n\| \to \|x\|\), then \(u_n \to x\) in norm.

theorem tendsto_of_forall_tendsto_and_tendsto_norm {u : ℕ → H} {x : H}
    (h : ∀ f : StrongDual 𝕜 H, Tendsto (fun n => f (u n)) atTop (𝓝 (f x)))
    (hnorm : Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖)) :
    Tendsto u atTop (𝓝 x)

Used by 1

Used byRadon–Riesz theorem, weak-topology form

TheoremRadon–Riesz theorem, weak-topology form#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), not necessarily complete, let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(H\) and let \(x \in H\). If \(u_n \to x\) in the weak topology of \(H\) (the coarsest topology making every continuous linear functional \(H \to \mathbb{K}\) continuous) and \(\|u_n\| \to \|x\|\), then \(u_n \to x\) in norm.

theorem tendsto_of_tendsto_weakSpace_and_tendsto_norm {u : ℕ → H} {x : H}
    (h : Tendsto (fun n => toWeakSpace 𝕜 H (u n)) atTop (𝓝 (toWeakSpace 𝕜 H x)))
    (hnorm : Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖)) :
    Tendsto u atTop (𝓝 x)

Uses 1

Proof usesRadon–Riesz theorem, dual-functionals form

TheoremRadon–Riesz characterization of norm convergence#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), not necessarily complete, let \((u_n)_{n \in \mathbb{N}}\) be a sequence in \(H\) and let \(x \in H\). Then \(u_n \to x\) in norm if and only if \(\langle u_n, y \rangle \to \langle x, y \rangle\) for every \(y \in H\) and \(\|u_n\| \to \|x\|\).

theorem tendsto_iff_tendsto_inner_and_tendsto_norm {u : ℕ → H} {x : H} :
    Tendsto u atTop (𝓝 x) ↔
      (∀ y : H, Tendsto (fun n => ⟪u n, y⟫_𝕜) atTop (𝓝 ⟪x, y⟫_𝕜)) ∧
        Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖)

Uses 1

Proof usesRadon–Riesz theorem, inner-product form

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.