OAI/Analysis/PureInfiniteness/NonunitalFiniteCompression.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite spectral compression estimates in the original nonunital algebra. Scalar sampling takes place only after the faithful unitization embedding.

  1. lemma OAI.WeakPureInfiniteness.nonunital_finite_compression_preservation line 17
  2. lemma OAI.WeakPureInfiniteness.nonunital_finite_compression_commutator line 53