OAI/Analysis/TracialCohomology/HilbertNormalParts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Hilbert normal parts for bounded Hochschild cohomology.

  1. def OAI.HochschildNormalPart.hilbertNormalFunctional line 24
  2. lemma OAI.HochschildNormalPart.hilbertNormalFunctional_apply line 55
  3. def OAI.HochschildNormalPart.hilbertNormalValue line 59
  4. lemma OAI.HochschildNormalPart.hilbertNormalValue_inner line 62
  5. lemma OAI.HochschildNormalPart.hilbertNormalValue_add line 72
  6. lemma OAI.HochschildNormalPart.hilbertNormalValue_smul line 78
  7. lemma OAI.HochschildNormalPart.hilbertNormalValue_norm line 84
  8. def OAI.HochschildNormalPart.hilbertNormalPart line 89
  9. lemma OAI.HochschildNormalPart.hilbertNormalPart_inner line 96
  10. lemma OAI.HochschildNormalPart.hilbertNormalPart_pairing line 100
  11. lemma OAI.HochschildNormalPart.hilbertNormalPart_norm line 108
  12. lemma OAI.HochschildNormalPart.hilbertNormalPart_mem line 111
  13. lemma OAI.HochschildNormalPart.factored_normal_part_mem line 123
  14. lemma OAI.HochschildNormalPart.factored_normal_part_apply line 130
  15. lemma OAI.HochschildNormalPart.factored_bilinear_normalization line 136
  16. lemma OAI.HochschildNormalPart.hasPreadjoint_iff_scalar line 167
  17. lemma OAI.HochschildNormalPart.operator_bilinear_normalization line 176