OAI/Analysis/Nuclearity/CPNormFromPositive.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A completely positive map is contractive when it is contractive on positive elements. The argument normalizes by the operator norm and applies Schwarz once; no quantitative limit is needed.

  1. theorem OAI.WeakPureInfiniteness.cp_norm_le_one_of_positive_bound line 18
  2. theorem OAI.WeakPureInfiniteness.cp_norm_le_one_of_positive_bound_nonunital line 66