OAI/Analysis/Nuclearity/UnitizedCompression.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite row compression stays in the original nonunital algebra. Its unitized matrix image is used only to apply the scalar sampling estimates.

  1. def OAI.WeakPureInfiniteness.unitizationOneByOne line 17
  2. lemma OAI.WeakPureInfiniteness.unitizationOneByOne_injective line 22
  3. lemma OAI.WeakPureInfiniteness.unitizationOneByOne_norm line 27
  4. def OAI.WeakPureInfiniteness.finiteRowCompression line 30
  5. lemma OAI.WeakPureInfiniteness.unitizationOneByOne_rowCompression line 33
  6. lemma OAI.WeakPureInfiniteness.finiteRowCompression_norm_le_one line 50
  7. lemma OAI.WeakPureInfiniteness.unitized_row_relative_offdiagonal line 64