OAI/Analysis/KadisonKastler/ComplementaryContractionLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A contractive lift perpendicular to a prescribed isometry

This is the geometric completion step: the unused norm in one coordinate supports a new column perpendicular to the already prescribed column.

  1. theorem OAI.KadisonKastler.exists_complementary_contraction_lift line 21