OAI/Analysis/PureInfiniteness/NonunitalCrossCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal spectral return columns give small mixed compressions in the original nonunital algebra.

  1. lemma OAI.WeakPureInfiniteness.disjoint_columns_cross_diagonal_zero line 16
  2. lemma OAI.WeakPureInfiniteness.unitizationOneByOne_cross_norm line 32
  3. lemma OAI.WeakPureInfiniteness.nonunital_cross_compression_norm_le line 38