OAI/Analysis/TracialSplitting/CoefficientApproximation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearTrace.coefficientSelfAdjMap line 90
2. def OAI.NuclearTrace.coefficientCone line 97
3. lemma OAI.NuclearTrace.coefficientCone_zero line 103
4. def OAI.NuclearTrace.evalTuple line 110
5. def OAI.NuclearTrace.tracialTupleSeminorm line 116
6. lemma OAI.NuclearTrace.tracialTupleSeminorm_apply line 120
7. lemma OAI.NuclearTrace.tracialTupleSeminorm_continuous line 125
8. lemma OAI.NuclearTrace.tracialTupleSeminorm_single line 132
9. theorem OAI.NuclearTrace.nuclear_tracial_coefficient_approximation line 137
10. theorem OAI.NuclearTrace.compact_convex_uniform_cost line 201