OAI/Analysis/JiangSu/Comparison/ProjectionDefect.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentMain.positive_contraction_defect_nonneg line 12
2. lemma OAI.CurrentMain.limitTrace_detects_positive_zero line 24
3. theorem OAI.CurrentMain.projection_of_vanishing_tracial_defect line 33
4. lemma OAI.CurrentMain.limitTrace_eq_of_coordinate_errors line 61
5. lemma OAI.DirectComparison.cfc_clamp_of_positive_contractive line 85
6. lemma OAI.DirectComparison.positive_contraction_lift line 98
7. lemma OAI.DirectComparison.directPositiveCut_norm_le line 126
8. lemma OAI.DirectComparison.boundedFamilyEval_continuous line 135
9. theorem OAI.DirectComparison.projection_supply line 152