OAI/Analysis/TracialSplitting/VectorApproximation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NuclearTrace.stateTest_mem_closure_dense line 27
  2. theorem OAI.NuclearTrace.dense_vector_state_approximation line 46
  3. lemma OAI.NuclearTrace.domination_preGNS_norm line 87
  4. def OAI.NuclearTrace.dominationPreGNS line 93
  5. lemma OAI.NuclearTrace.dominationPreGNS_apply line 98
  6. def OAI.NuclearTrace.dominationGNS line 101
  7. lemma OAI.NuclearTrace.dominationGNS_coe line 104
  8. lemma OAI.NuclearTrace.dominationGNS_norm_bound line 108
  9. lemma OAI.NuclearTrace.dominationGNS_intertwines line 114
  10. lemma OAI.NuclearTrace.dominationGNS_adjoint_intertwines line 122
  11. def OAI.NuclearTrace.dominationDensity line 130
  12. lemma OAI.NuclearTrace.dominationDensity_nonneg line 133
  13. lemma OAI.NuclearTrace.dominationDensity_le line 137
  14. lemma OAI.NuclearTrace.dominationDensity_commutes line 157
  15. lemma OAI.NuclearTrace.dominationDensity_value line 166
  16. def OAI.NuclearTrace.selfAdjointComplexification line 180
  17. lemma OAI.NuclearTrace.selfAdjointComplexification_apply line 189
  18. lemma OAI.NuclearTrace.real_perturbation_nonneg line 198
  19. def OAI.NuclearTrace.realPerturbation line 213
  20. lemma OAI.NuclearTrace.realPerturbation_apply line 223
  21. lemma OAI.NuclearTrace.realPerturbation_le line 226
  22. theorem OAI.NuclearTrace.real_functional_in_commutant line 235