OAI/Analysis/JiangSu/Excision/ExcisionFullnessError.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectComparison.norm_two_sided_contractions line 17
2. lemma OAI.DirectComparison.norm_sqrt_upperCut_le line 27
3. lemma OAI.DirectComparison.norm_star_commutator line 36
4. lemma OAI.DirectComparison.fullness_error_le line 41
5. lemma OAI.DirectComparison.hereditaryUpperCut_trace_lower_simple line 67
6. theorem OAI.DirectComparison.central_fullness_error_tendsto line 78
7. theorem OAI.DirectComparison.eventual_hereditary_upperCut_trace_lower line 89