OAI/Analysis/BoundedHochschild/RankOneQuantization.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Rank-one projections, phase coefficients and small corners.

  1. def OAI.HochschildMatrixSystems.MatrixSystem.scalarMatrix line 38
  2. lemma OAI.HochschildMatrixSystems.MatrixSystem.scalarMatrix_mul line 40
  3. lemma OAI.HochschildMatrixSystems.MatrixSystem.scalarMatrix_star line 54
  4. lemma OAI.HochschildMatrixSystems.MatrixSystem.scalarMatrix_smul line 59
  5. lemma OAI.HochschildMatrixSystems.MatrixSystem.phase_star_self' line 63
  6. def OAI.HochschildMatrixSystems.MatrixSystem.rankOne line 66
  7. lemma OAI.HochschildMatrixSystems.MatrixSystem.rankOne_star line 69
  8. lemma OAI.HochschildMatrixSystems.MatrixSystem.rankOne_mul line 76
  9. lemma OAI.HochschildMatrixSystems.MatrixSystem.rankOne_projection line 90
  10. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_scalarMatrix_commutant line 96
  11. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_rankOne_commutant line 106
  12. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_rankOne line 116
  13. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_ext line 123
  14. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_entry line 127
  15. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_smul line 139
  16. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_sum line 143
  17. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_scalarMatrix line 148
  18. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_mul_mem line 155
  19. def OAI.HochschildMatrixSystems.MatrixSystem.phaseCoefficient line 164
  20. lemma OAI.HochschildMatrixSystems.MatrixSystem.phaseCoefficient_mem line 167
  21. lemma OAI.HochschildMatrixSystems.MatrixSystem.rankOne_compression line 175
  22. lemma OAI.HochschildMatrixSystems.MatrixSystem.rankOne_compression_norm line 194
  23. lemma OAI.HochschildMatrixSystems.MatrixSystem.phaseCoefficient_energy_bound line 236
  24. lemma OAI.HochschildMatrixSystems.MatrixSystem.exists_phase_energy_bound line 271
  25. lemma OAI.HochschildQuantization.exists_large_small_expectations line 309
  26. theorem OAI.HochschildQuantization.exists_small_corner_of_trace_limit line 336
  27. theorem OAI.HochschildQuantization.exists_small_corner line 403