OAI/Analysis/JiangSu/CentralSequences/OrderZeroContractiveCut.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompletelyPositiveOperations.norm_le_of_order_zero_relation line 17
2. def OAI.CompletelyPositiveOperations.cutoffMultiplier line 31
3. lemma OAI.CompletelyPositiveOperations.cutoffMultiplier_continuous line 33
4. lemma OAI.CompletelyPositiveOperations.cutoffMultiplier_nonneg line 36
5. lemma OAI.CompletelyPositiveOperations.cutoffMultiplier_mul_le_one line 39
6. theorem OAI.CompletelyPositiveOperations.order_zero_contractive_cut line 45