OAI/Analysis/KadisonKastler/NearlyFullCornerWitness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform projection witness in every nearly full corner

The constant is independent of the corner. The hypotheses are the actual positive reference and the all-vector remote coisometries already constructed in the spatial two-ratio product.

  1. theorem OAI.KadisonKastler.nearly_full_corner_projection_witness line 25