Infinite-Dimensional Projection Separation

Abstract

Dense finite-dimensional Hilbert projection towers converge on every vector while remaining a unit operator-norm distance from the identity.

Theorem 1.1 (Dense finite projection towers complete pointwise but not uniformly).

$$\begin{array}{c}\forall K,H,\mathrm{Hilbert}\left(K,H\right),\mathrm{InfiniteDimensional}\left(K,H\right),\\ S:\mathbb{N}\to \mathrm{ClosedSubspace}\left(H\right),\mathrm{Monotone}\left(S\right),\\ (\forall n,\mathrm{FiniteDimensional}\left(K,S(n)\right)),\mathrm{Cumulative}\left(S\right)=H,\\ (\forall n,S(n)\ne H)\wedge \\ (\forall x\in H,\lim \left(n,\infty ,P\left(S(n)\right)(x)\right)=x)\wedge \\ \neg (\lim \left(n,\infty ,\Vert I-P\left(S(n)\right)\Vert \right)=0)\wedge \\ (\forall n,\Vert I-P\left(S(n)\right)\Vert =1).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Completion/InfiniteDimensionalProjectionSeparation.infinite_dimensional_projection_separation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let S be an increasing sequence of finite-dimensional closed subspaces of an infinite-dimensional Hilbert space, with cumulative closed span equal to the whole ambient space.

No finite stage equals the ambient space. The canonical orthogonal projections nevertheless converge to the identity on every fixed vector, by the increasing-projection strong-limit theorem.

At every stage, the identity-minus-projection operator is the orthogonal projection onto the nonzero complementary subspace. Its operator norm is therefore exactly one, so the norm sequence cannot converge to zero.

References

• Truth anchor: D5/S3/Quantum/Completion/InfiniteDimensionalProjectionSeparation.infinite_dimensional_projection_separation
• Dependency: D5/S3/Quantum/Completion/IncreasingProjectionStrongLimit