OAI/Analysis/TracialCohomology/RandomSigns.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Random signs for bounded Hochschild cohomology.

  1. def OAI.PopaQuantization.sign line 18
  2. lemma OAI.PopaQuantization.sign_sq line 19
  3. lemma OAI.PopaQuantization.sign_sum line 20
  4. def OAI.PopaQuantization.character line 23
  5. lemma OAI.PopaQuantization.character_empty line 26
  6. lemma OAI.PopaQuantization.character_singleton line 27
  7. lemma OAI.PopaQuantization.character_eq_prod line 29
  8. lemma OAI.PopaQuantization.character_pair line 38
  9. lemma OAI.PopaQuantization.character_orthogonal line 43
  10. lemma OAI.PopaQuantization.signed_norm_sq line 67
  11. lemma OAI.PopaQuantization.character_mean_square line 79
  12. abbrev OAI.PopaQuantization.UpperPair line 93
  13. def OAI.PopaQuantization.pairLabel line 95
  14. lemma OAI.PopaQuantization.pairLabel_injective line 100
  15. lemma OAI.PopaQuantization.sum_diagonal_upper line 122
  16. def OAI.PopaQuantization.pairCoefficients line 152
  17. lemma OAI.PopaQuantization.quadratic_expansion line 157
  18. theorem OAI.PopaQuantization.quadratic_mean_square_bound line 169