OAI/Analysis/TracialCohomology/DominatedFactorization.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Dominated factorization for bounded Hochschild cohomology.

  1. def OAI.HochschildDomination.PreHilbert line 24
  2. instance OAI.HochschildDomination.PreHilbert.(instance at line 28) line 28
  3. instance OAI.HochschildDomination.PreHilbert.(instance at line 29) line 29
  4. def OAI.HochschildDomination.PreHilbert.of line 31
  5. def OAI.HochschildDomination.PreHilbert.val line 32
  6. lemma OAI.HochschildDomination.PreHilbert.of_val line 35
  7. lemma OAI.HochschildDomination.PreHilbert.val_of line 37
  8. abbrev OAI.HochschildDomination.PreHilbert.core line 39
  9. instance OAI.HochschildDomination.PreHilbert.(instance at line 57) line 57
  10. instance OAI.HochschildDomination.PreHilbert.(instance at line 59) line 59
  11. lemma OAI.HochschildDomination.PreHilbert.norm_def line 62
  12. lemma OAI.HochschildDomination.PreHilbert.norm_of_le line 66
  13. def OAI.HochschildDomination.PreHilbert.ofCLM line 82
  14. lemma OAI.HochschildDomination.PreHilbert.ofCLM_apply line 85
  15. abbrev OAI.HochschildDomination.Hilbert line 89
  16. def OAI.HochschildDomination.beta line 91
  17. def OAI.HochschildDomination.alphaPre line 98
  18. def OAI.HochschildDomination.alpha line 109
  19. lemma OAI.HochschildDomination.factorization line 112
  20. lemma OAI.HochschildDomination.beta_norm_sq line 126
  21. theorem OAI.HochschildDomination.exists_quartic_hilbert_modulus line 136