OAI/Analysis/BoundedHochschild/UltrapowerMoments.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Centered sequences and unitary moments in tracial ultrapowers.

  1. def OAI.HochschildUltrapower.traceScalarSequence line 39
  2. lemma OAI.HochschildUltrapower.traceScalarSequence_apply line 42
  3. lemma OAI.HochschildUltrapower.quotient_traceScalarSequence line 45
  4. def OAI.HochschildUltrapower.centeredSequence line 62
  5. lemma OAI.HochschildUltrapower.centeredSequence_apply line 63
  6. lemma OAI.HochschildUltrapower.quotient_centeredSequence line 65
  7. lemma OAI.HochschildUltrapower.norm_centered_half line 71
  8. lemma OAI.HochschildUltrapower.trace_centered_half line 84
  9. def OAI.HochschildUltrapower.unitarySequence line 87
  10. lemma OAI.HochschildUltrapower.unitarySequence_apply line 91
  11. def OAI.HochschildUltrapower.quotientUnitary line 94
  12. lemma OAI.HochschildUltrapower.quotientUnitary_coe line 96
  13. def OAI.HochschildPatching.mapUnitary line 111
  14. lemma OAI.HochschildPatching.mapUnitary_coe line 113
  15. lemma OAI.HochschildPatching.mapUnitary_zpow line 115
  16. lemma OAI.HochschildPatching.unitary_power_eq line 120
  17. lemma OAI.HochschildPatching.mixedEval_unitary_product line 130
  18. lemma OAI.HochschildPatching.wordCoeff_hom line 143
  19. lemma OAI.HochschildPatching.mixedEval_hom line 145
  20. def OAI.HochschildPatching.evalSequence line 156
  21. lemma OAI.HochschildPatching.evalSequence_apply line 164
  22. lemma OAI.HochschildPatching.eval_unitarySequence line 165
  23. lemma OAI.HochschildPatching.mixedEval_sequence line 170
  24. theorem OAI.HochschildUltrapower.exists_quotient_unitary_moments line 194
  25. lemma OAI.HochschildPatching.exists_finite_reindex line 244
  26. lemma OAI.HochschildPatching.all_finite_words line 275
  27. theorem OAI.HochschildUltrapower.exists_quotient_unitary_all_moments line 302