OAI/Analysis/TracialSplitting/TraceConvexity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearTrace.clipScalar line 16
2. lemma OAI.NuclearTrace.clipScalar_continuous line 18
3. lemma OAI.NuclearTrace.clipScalar_nonneg line 23
4. lemma OAI.NuclearTrace.clipScalar_le_one line 26
5. lemma OAI.NuclearTrace.clipScalar_bounds line 32
6. def OAI.NuclearTrace.rowNormalizer line 64
7. lemma OAI.NuclearTrace.rowNormalizer_nonneg line 66
8. lemma OAI.NuclearTrace.rowNormalizer_le_one line 69
9. lemma OAI.NuclearTrace.abs_sub_one_cfc line 72
10. theorem OAI.NuclearTrace.rowNormalizer_bounds line 81