OAI/Analysis/Nuclearity/MinimalCornerNorm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Faithful corner inclusions preserve the minimal norm. Cutting both tensor factors is a compression by one contractive elementary projection.

  1. lemma OAI.WeakPureInfiniteness.norm_minimalSum_flip line 19
  2. lemma OAI.WeakPureInfiniteness.norm_minimalSum_mapLeft line 27
  3. lemma OAI.WeakPureInfiniteness.norm_minimalSum_mapBoth line 35
  4. def OAI.WeakPureInfiniteness.isometricCornerOppositeLift line 51
  5. lemma OAI.WeakPureInfiniteness.isometricCornerOppositeLift_injective line 73
  6. lemma OAI.WeakPureInfiniteness.norm_minimalSum_cornerLift line 80
  7. lemma OAI.WeakPureInfiniteness.norm_minimalSum_projection_cut line 89