Bounded Inverse-Limit Reconstruction

Abstract

Bounded compatible projection families reconstruct the cumulative Hilbert completion.

Theorem 1.1 (Bounded compatible families reconstruct the cumulative completion).

$$\begin{array}{c}\forall k,H:\mathrm{Type},\\ [\mathrm{RCLike}(k)],[\mathrm{NormedAddCommGroup}(H)],\\ [\mathrm{InnerProductSpace}(k,H)],[\mathrm{CompleteSpace}(H)],\\ S:\mathbb{N}\to \mathrm{Submodule}(k,H),\\ [\forall n:\mathbb{N},\mathrm{HasOrthogonalProjection}(S(n))],\\ hS:\mathrm{Monotone}(S),\\ \mathrm{Isometry}((\mathrm{canonicalReconstructionEquiv}(S,hS):\mathrm{cumulativeSpace}(S)\to \mathrm{boundedInverseLimit}(S)))\wedge \mathrm{Bijective}((\mathrm{canonicalReconstructionEquiv}(S,hS):\mathrm{cumulativeSpace}(S)\to \mathrm{boundedInverseLimit}(S)))\wedge (\forall x:\mathrm{cumulativeSpace}(S),\forall n:\mathbb{N},((\mathrm{canonicalReconstructionEquiv}(S,hS)(x):\mathrm{boundedInverseLimit}(S)):\mathrm{BoundedContinuousFunction}(\mathbb{N},H))(n)=\mathrm{starProjection}(S(n),(x:H)))\wedge \\ \mathrm{Isometry}((\mathrm{quotientReconstructionEquiv}(S,hS):\mathrm{Quotient}(H,\mathrm{residualSpace}(S))\to \mathrm{boundedInverseLimit}(S)))\wedge \mathrm{Bijective}((\mathrm{quotientReconstructionEquiv}(S,hS):\mathrm{Quotient}(H,\mathrm{residualSpace}(S))\to \mathrm{boundedInverseLimit}(S))).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let S be a monotone sequence of closed subspaces of a complete Hilbert space. Its bounded inverse limit is constructed as the subspace of bounded families x_n with x_n in S_n and with every earlier coordinate equal to the orthogonal projection of every later one.

The canonical map J sends x in the closure of the union of the stages to the family of its orthogonal projections. Increasing projection convergence proves that J preserves the norm. Conversely, projection compatibility gives a Pythagorean identity for coordinate differences; bounded squared norms therefore make every compatible family Cauchy.

The family limit lies in the cumulative closure and has exactly the given stage projections, proving bijectivity. The quotient conclusion is obtained by composing J with Mathlib’s canonical isometry from the quotient by the residual orthogonal complement to the cumulative space.

References

• Truth anchor: D5/S3/Quantum/Completion/BoundedInverseLimitReconstruction.bounded_inverse_limit_reconstruction