OAI/Analysis/BoundedHochschild/RelativeQuantization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Relative small corners, root phases and weak powers of unitaries.

  1. lemma OAI.HochschildQuantization.corner_norm_sq line 41
  2. lemma OAI.HochschildQuantization.corner_trace_re line 46
  3. theorem OAI.HochschildQuantization.exists_relative_small_corner line 55
  4. def OAI.HochschildRootPhase.character line 119
  5. lemma OAI.HochschildRootPhase.character_apply line 125
  6. lemma OAI.HochschildRootPhase.character_zero line 128
  7. lemma OAI.HochschildRootPhase.character_add line 129
  8. lemma OAI.HochschildRootPhase.character_norm line 132
  9. lemma OAI.HochschildRootPhase.character_star line 134
  10. lemma OAI.HochschildRootPhase.character_eq_one_iff line 139
  11. lemma OAI.HochschildRootPhase.sum_character line 156
  12. lemma OAI.HochschildRootPhase.orthogonality line 165
  13. lemma OAI.HochschildRootPhase.character_parseval line 173
  14. def OAI.HochschildMatrixSystems.MatrixSystem.diagonalRoot line 215
  15. lemma OAI.HochschildMatrixSystems.MatrixSystem.diagonalRoot_zero line 218
  16. lemma OAI.HochschildMatrixSystems.MatrixSystem.diagonalRoot_mul line 221
  17. lemma OAI.HochschildMatrixSystems.MatrixSystem.diagonalRoot_star line 227
  18. lemma OAI.HochschildMatrixSystems.MatrixSystem.diagonalRoot_unitary line 231
  19. def OAI.HochschildMatrixSystems.MatrixSystem.rootUnitary line 236
  20. def OAI.HochschildMatrixSystems.MatrixSystem.integerRootHom line 238
  21. lemma OAI.HochschildMatrixSystems.MatrixSystem.rootUnitary_zpow line 245
  22. lemma OAI.HochschildMatrixSystems.MatrixSystem.single_frequency_injective line 258
  23. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_root_parseval line 268
  24. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_root_energy_bound line 291
  25. lemma OAI.HochschildMatrixSystems.MatrixSystem.exists_root_trace_energy line 314
  26. theorem OAI.HochschildMatrixSystems.exists_unitary_weak_powers line 341