OAI/Analysis/Nuclearity/UnitalCPContraction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Norm control for the unital return map in a nuclear approximation

  1. lemma OAI.WeakPureInfiniteness.completelyPositive_schwarz_of_unital line 15
  2. lemma OAI.WeakPureInfiniteness.completelyPositive_norm_apply_le_of_unital line 29
  3. lemma OAI.WeakPureInfiniteness.completelyPositive_norm_le_of_unital line 46