Weak convergence of orthonormal sequences

TheoremFourier coefficients along an orthonormal family tend to 0#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((v_i)_{i \in \iota}\) be an orthonormal family in \(H\) and let \(x \in H\). Then the inner products \(\langle v_i, x \rangle\) tend to \(0\) along the cofinite filter on \(\iota\): for every \(\varepsilon > 0\), \(|\langle v_i, x \rangle| < \varepsilon\) for all but finitely many \(i\).

Bessel's inequality makes their squared absolute values summable, and the terms of a summable family tend to \(0\).

theorem tendsto_inner_cofinite_zero {ι : Type*} {v : ι → H} (hv : Orthonormal 𝕜 v)
    (x : H) :
    Tendsto (fun i => ⟪v i, x⟫_𝕜) cofinite (𝓝 0)
Used by 2
Used byAn orthonormal family tends weakly to 0 · Fourier coefficients along an orthonormal sequence tend to 0

TheoremAn orthonormal family tends weakly to 0#✓fully proved

Let \(H\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((v_i)_{i \in \iota}\) be an orthonormal family in \(H\) and let \(f : H \to \mathbb{K}\) be a continuous linear functional. Then \(f(v_i)\) tends to \(0\) along the cofinite filter on \(\iota\): for every \(\varepsilon > 0\), \(|f(v_i)| < \varepsilon\) for all but finitely many \(i\).

By the Riesz representation theorem, \(f\) is the inner product with a fixed vector, so this follows from the corresponding statement for Fourier coefficients.

theorem tendsto_apply_cofinite_zero [CompleteSpace H] {ι : Type*} {v : ι → H}
    (hv : Orthonormal 𝕜 v) (f : H →L[𝕜] 𝕜) :
    Tendsto (fun i => f (v i)) cofinite (𝓝 0)
Uses 1 · Used by 1
Proof usesFourier coefficients along an orthonormal family tend to 0
Used byAn orthonormal sequence tends weakly to 0

TheoremFourier coefficients along an orthonormal sequence tend to 0#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \((v_n)_{n \in \mathbb{N}}\) be an orthonormal sequence in \(H\) and let \(x \in H\). Then \(\langle v_n, x \rangle \to 0\) as \(n \to \infty\).

theorem tendsto_inner_atTop_zero {v : ℕ → H} (hv : Orthonormal 𝕜 v) (x : H) :
    Tendsto (fun n => ⟪v n, x⟫_𝕜) atTop (𝓝 0)
Uses 1
Proof usesFourier coefficients along an orthonormal family tend to 0

TheoremAn orthonormal sequence tends weakly to 0#✓fully proved

Let \(H\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((v_n)_{n \in \mathbb{N}}\) be an orthonormal sequence in \(H\). Then for every continuous linear functional \(f : H \to \mathbb{K}\), we have \(f(v_n) \to 0\) as \(n \to \infty\).

theorem tendsto_apply_atTop_zero [CompleteSpace H] {v : ℕ → H} (hv : Orthonormal 𝕜 v)
    (f : H →L[𝕜] 𝕜) :
    Tendsto (fun n => f (v n)) atTop (𝓝 0)
Uses 1
Proof usesAn orthonormal family tends weakly to 0

TheoremAn orthonormal sequence does not converge strongly to 0#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((v_n)_{n \in \mathbb{N}}\) be an orthonormal sequence in \(H\). Then \(v_n\) does not tend to \(0\) in norm as \(n \to \infty\).

Weak convergence does not upgrade to norm convergence here: every term of an orthonormal sequence has norm \(1\).

theorem not_tendsto_atTop_zero {v : ℕ → H} (hv : Orthonormal 𝕜 v) :
    ¬ Tendsto v atTop (𝓝 0)
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.