OAI/Analysis/TracialSplitting/Hypertraces.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NuclearTrace.nuclear_hypertrace_of_representations line 63
2. theorem OAI.NuclearTrace.nuclear_hypertrace line 92
3. lemma OAI.NuclearTrace.operator_le_of_unit_quadratic line 114
4. def OAI.NuclearTrace.vectorTest line 149
5. def OAI.NuclearTrace.stateTest line 152
6. lemma OAI.NuclearTrace.real_pi_linear_expansion line 155
7. lemma OAI.NuclearTrace.stateTest_mem_closure line 166
8. theorem OAI.NuclearTrace.finite_vector_state_approximation line 194
9. theorem OAI.NuclearTrace.nuclear_cyclic_extension line 233