OAI/Analysis/TracialSplitting/StateExtension.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentMain.selfAdjointFunctionalComplex line 21
  2. lemma OAI.CurrentMain.selfAdjointFunctionalComplex_apply line 30
  3. lemma OAI.CurrentMain.selfAdjointFunctional_nonneg line 35
  4. def OAI.CurrentMain.selfAdjointEmbedding line 63
  5. lemma OAI.CurrentMain.state_realPart_bound line 73
  6. def OAI.CurrentMain.stateRealLinear line 89
  7. def OAI.CurrentMain.stateRealContinuous line 94
  8. theorem OAI.CurrentMain.state_extension line 99
  9. lemma OAI.NuclearTrace.null_right_mul line 175
  10. lemma OAI.NuclearTrace.null_left_mul line 184
  11. lemma OAI.NuclearTrace.diagonal_left line 206
  12. lemma OAI.NuclearTrace.diagonal_right line 211
  13. lemma OAI.NuclearTrace.diagonal_null line 216
  14. lemma OAI.NuclearTrace.diagonal_centralizes line 230
  15. theorem OAI.NuclearTrace.nuclear_diagonal_extension line 258
  16. theorem OAI.NuclearTrace.nuclear_commuting_hypertrace line 284