OAI/Analysis/KadisonKastler/PositiveCompressionFullness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform algebraic fullness from a positive compression

The type III spectral-projection argument produces an isometry v for which v* x* x v is bounded below. Inverting a normalized compression gives explicit left and right factors with controlled norms.

  1. theorem OAI.KadisonKastler.exists_fullness_factors_of_positive_compression line 20