OAI/Analysis/TracialSplitting/MatrixCoefficients.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NuclearTrace.coefficientMap_change_vectors line 26
  2. lemma OAI.NuclearTrace.coefficientMap_orthonormal line 73
  3. def OAI.NuclearTrace.operatorMatrix line 100
  4. lemma OAI.NuclearTrace.operatorMatrix_apply line 104
  5. def OAI.NuclearTrace.orthonormalLinear line 111
  6. lemma OAI.NuclearTrace.orthonormalLinear_basis line 115
  7. lemma OAI.NuclearTrace.orthonormalLinear_orthonormal line 120
  8. def OAI.NuclearTrace.orthonormalInclusion line 126
  9. lemma OAI.NuclearTrace.orthonormalInclusion_basis line 132
  10. def OAI.NuclearTrace.compressionMatrix line 136
  11. lemma OAI.NuclearTrace.compressionMatrix_apply line 143
  12. lemma OAI.NuclearTrace.compressionMatrix_one line 151
  13. lemma OAI.NuclearTrace.compressionMatrix_norm line 157
  14. lemma OAI.NuclearTrace.coefficientMap_factorization line 173
  15. lemma OAI.NuclearTrace.coefficientMap_one line 179
  16. lemma OAI.NuclearTrace.coefficient_choi_nonneg line 193
  17. structure OAI.NuclearTrace.FiniteCoefficientSystem line 218
  18. def OAI.NuclearTrace.blockDiagHom line 233
  19. def OAI.NuclearTrace.matrixSynthesis line 259
  20. lemma OAI.NuclearTrace.matrixSynthesis_one line 264
  21. lemma OAI.NuclearTrace.matrixSynthesis_smul line 269
  22. def OAI.NuclearTrace.FiniteCoefficientSystem.output line 282
  23. def OAI.NuclearTrace.FiniteCoefficientSystem.zero line 285
  24. lemma OAI.NuclearTrace.FiniteCoefficientSystem.zero_output line 294
  25. def OAI.NuclearTrace.FiniteCoefficientSystem.scale line 297
  26. lemma OAI.NuclearTrace.FiniteCoefficientSystem.scale_output line 300
  27. def OAI.NuclearTrace.FiniteCoefficientSystem.add line 305
  28. lemma OAI.NuclearTrace.FiniteCoefficientSystem.add_output line 321
  29. def OAI.NuclearTrace.finiteSystemCone line 340
  30. theorem OAI.NuclearTrace.coefficientCone_finite_system line 356