Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

BalancedHankelSchmidt

Abstract

Balanced actual Gramians yield the complete Schmidt decomposition of the true infinite Hankel operator.

Definition 1.1 (The inverse square-root diagonal).

Formalization. D5/S3/Observer/Hankel/BalancedHankelSchmidt.invRootDiagonal (✓ std3).

Source. Repository-derived.

Commentary.

The diagonal consists of the reciprocals of the nonnegative real square roots of the weights.

Definition 1.2 (normalized Future).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.normalizedFuture

Formalization. D5/S3/Observer/Hankel/BalancedHankelSchmidt.normalizedFuture (✓ std3).

Source. Repository-derived.

Commentary.

Constructs an isometry by normalizing actual future trajectories with the diagonal Gramian; norm preservation is proved.

Definition 1.3 (left Isometry).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.leftIsometry

Formalization. D5/S3/Observer/Hankel/BalancedHankelSchmidt.leftIsometry (✓ std3).

Source. Repository-derived.

Commentary.

Actual original-system future trajectories span the finite left Schmidt subspace.

Definition 1.4 (right Isometry).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.rightIsometry

Formalization. D5/S3/Observer/Hankel/BalancedHankelSchmidt.rightIsometry (✓ std3).

Source. Repository-derived.

Commentary.

Actual dual-system trajectories span the finite right Schmidt subspace.

Theorem 1.5 (hankel isometric factorization).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.hankel_isometric_factorization

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/BalancedHankelSchmidt.hankel_isometric_factorization (✓ std3). ∎

Source. Repository-derived.

Commentary.

Proves the full l2 operator equals the left isometry composed with the balancing diagonal and the right isometry adjoint.

Definition 1.6 (left Mode).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.leftMode

Formalization. D5/S3/Observer/Hankel/BalancedHankelSchmidt.leftMode (✓ std3).

Source. Repository-derived.

Commentary.

Constructs the left singular output trajectory associated with a standard state coordinate.

Definition 1.7 (right Mode).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.rightMode

Formalization. D5/S3/Observer/Hankel/BalancedHankelSchmidt.rightMode (✓ std3).

Source. Repository-derived.

Commentary.

Constructs the right singular input trajectory associated with a standard state coordinate.

Theorem 1.8 (modes orthonormal).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.modes_orthonormal

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/BalancedHankelSchmidt.modes_orthonormal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both trajectory families are orthonormal in their genuine infinite l2 spaces.

Theorem 1.9 (hankel mode equations).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.hankel_mode_equations

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/BalancedHankelSchmidt.hankel_mode_equations (✓ std3). ∎

Source. Repository-derived.

Commentary.

Proves both forward and adjoint singular-vector equations for every positive balancing weight.

Theorem 1.10 (hankel schmidt expansion).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.hankel_schmidt_expansion

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/BalancedHankelSchmidt.hankel_schmidt_expansion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Proves the complete finite Schmidt expansion for every l2 input, not only finite-support test inputs.

Theorem 1.11 (hankel kernel iff).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.hankel_kernel_iff

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/BalancedHankelSchmidt.hankel_kernel_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Proves the nullspace is precisely the orthogonal complement of the constructed right singular modes.

Theorem 1.12 (nonzero squared singular value).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.nonzero_squared_singular_value

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/BalancedHankelSchmidt.nonzero_squared_singular_value (✓ std3). ∎

Source. Repository-derived.

Commentary.

Proves every nonzero eigenvalue of the actual Hankel adjoint-composition is a squared balancing weight. Repeated weights retain orthogonal modes.

Theorem 1.13 (constructed core singular values).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.constructed_core_singular_values

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/BalancedHankelSchmidt.constructed_core_singular_values (✓ std3). ∎

Source. Repository-derived.

Commentary.

Instantiates the existing finite Gramian singular-value theorem with actual positive square roots. It is supplementary to the separately proved infinite decomposition.

Theorem 1.14 (constructed hankel schmidt).

Lean statement: D5/S3/Observer/Hankel/BalancedHankelSchmidt.constructed_hankel_schmidt

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/BalancedHankelSchmidt.constructed_hankel_schmidt (✓ std3). ∎

Source. Repository-derived.

Commentary.

End-to-end identification from the original system: constructs actual Gramians and coordinates, proves orthonormal modes, full expansion, kernel characterization and Gramian-product characteristic polynomial. The finite singular multiset is not assumed sorted.

References