OAI/Analysis/PureInfiniteness/TwoMatrixNuclear.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The two-by-two nuclearity specialization used by the doubled-corner application. Matrix errors are controlled by continuity on finitely many entries; the completely positive approximations remain contractions.

  1. lemma OAI.WeakPureInfiniteness.completelyPositive_comp line 18
  2. lemma OAI.WeakPureInfiniteness.starHomContinuousLinear_norm_le_one line 25
  3. def OAI.WeakPureInfiniteness.twoMatrixReindex line 32
  4. def OAI.WeakPureInfiniteness.twoMatrixPack line 37
  5. def OAI.WeakPureInfiniteness.twoMatrixUnpack line 41
  6. lemma OAI.WeakPureInfiniteness.twoMatrixUnpack_pack line 45
  7. def OAI.WeakPureInfiniteness.twoMatrixEntries line 57
  8. theorem OAI.WeakPureInfiniteness.nuclear_twoMatrix line 65