OAI/Analysis/TracialSplitting/NuclearApproximation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NuclearTrace.scalarMix_trace_sq_le line 22
2. lemma OAI.NuclearTrace.matrixSynthesis_eq_mix line 36
3. lemma OAI.NuclearTrace.scalarMix_sub line 42
4. lemma OAI.NuclearTrace.trace_pairing_sum_bound line 49
5. lemma OAI.NuclearTrace.matrixSynthesis_difference_pairing line 72
6. lemma OAI.NuclearTrace.row_mass_nonneg line 106
7. lemma OAI.NuclearTrace.rowNormalizer_mass line 110
8. lemma OAI.NuclearTrace.rowNormalizer_error_mass line 119
9. theorem OAI.NuclearTrace.rowNormalizer_pairing_bound line 130