OAI/Analysis/Nuclearity/QuotientCPMap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded completely positive maps annihilating a quotient kernel descend with their norm bound. The matrix positivity step lifts a square root. This does not assert that nuclear approximations already annihilate the kernel.

  1. theorem OAI.WeakPureInfiniteness.continuousLinear_descends line 18
  2. theorem OAI.WeakPureInfiniteness.matrixMap_surjective line 49
  3. theorem OAI.WeakPureInfiniteness.matrixMap_positive_lift line 61
  4. theorem OAI.WeakPureInfiniteness.completelyPositive_descends line 71
  5. theorem OAI.WeakPureInfiniteness.cpMap_descends line 84