OAI/Analysis/Nuclearity/CPMultiplicativeDefect.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A Cauchy--Schwarz bound for the multiplicative defect of a unital CP map

  1. lemma OAI.WeakPureInfiniteness.positiveMatrix_entry_norm_le line 20
  2. lemma OAI.WeakPureInfiniteness.completelyPositive_multiplicative_defect line 45
  3. lemma OAI.WeakPureInfiniteness.completelyPositive_defect_sqrt_le line 72
  4. lemma OAI.WeakPureInfiniteness.completelyPositive_mul_error_le line 85
  5. lemma OAI.WeakPureInfiniteness.completelyPositive_mul_tendsto line 101