Inverse Blaschke History Deletion

Abstract

The adjoint of an inner isometry is a coisometry that deletes exactly its finite model-space histories, with index equal to their dimension.

Theorem 1.1 (Inverse inner factors delete the model-space history).

$$\begin{gathered} T:=V^{\ast },K:=(\mathrm{ran}\left(V\right){)}^{\perp },P_K:=I-V{V}^{\ast }, \\ \mathrm{Isometry}(V)\wedge \dim (K)=m⟶T{T}^{\ast }=I\wedge T^{\ast }T=I-P_K, \\ \mathrm{ran}(P_K)=\ker (T)=K\wedge \mathrm{Surjective}(T)\wedge \mathrm{Fredholm}(T)\wedge \mathrm{ind}(T)=m, \\ H/\mathrm{ran}\left(V\right)\equiv K. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ShiftOperators/InverseBlaschkeHistoryDeletion.inverse_blaschke_history_deletion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let V be an isometry on a complete real or complex Hilbert space. Set T equal to its adjoint, let K be the orthogonal complement of the range of V, and suppose K has finite dimension m. Then T is a coisometry, its initial projection is the identity minus the orthogonal projection onto K, and its kernel is exactly K.

The defect I minus VV-star is proved to be a star projection whose range is K. Surjectivity follows from T composed with V being the identity. Consequently T is Fredholm with index m, while Mathlib’s quotientEquivOrthogonal explicitly identifies the cokernel of V with the same model space K.

The source statement referred directly to finite Blaschke products, Hardy-space Toeplitz operators, and their model spaces, for which the repository has no construction. The formal theorem therefore states the exact operator data supplied by that analytic setting: isometry of V and finite model-space dimension. No Toeplitz or Blaschke result is assumed under an opaque name.

References

• Truth anchor: D5/S3/Zeros/ShiftOperators/InverseBlaschkeHistoryDeletion.inverse_blaschke_history_deletion