OAI/Analysis/BoundedHochschild/NormalVectors.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Normal vectors and projections for Hilbert-space representations.

  1. def OAI.HochschildNormalPart.predualEmbedding line 35
  2. lemma OAI.HochschildNormalPart.predualEmbedding_apply line 57
  3. def OAI.HochschildNormalPart.normalDual line 61
  4. lemma OAI.HochschildNormalPart.mem_normalDual line 63
  5. lemma OAI.HochschildNormalPart.normalDual_closed line 71
  6. lemma OAI.HochschildNormalPart.normalDual_comp line 75
  7. def OAI.HochschildNormalPart.coefficient line 86
  8. lemma OAI.HochschildNormalPart.coefficient_apply line 103
  9. lemma OAI.HochschildNormalPart.coefficient_norm line 106
  10. def OAI.HochschildNormalPart.normalVectors line 116
  11. lemma OAI.HochschildNormalPart.mem_normalVectors line 119
  12. lemma OAI.HochschildNormalPart.normalVectors_closed line 123
  13. instance OAI.HochschildNormalPart.normalVectors_complete line 129
  14. lemma OAI.HochschildNormalPart.normalVectors_mul line 132
  15. lemma OAI.HochschildNormalPart.normalVectors_commutant line 143
  16. lemma OAI.HochschildNormalPart.projection_commutes line 158
  17. def OAI.HochschildNormalPart.normalProjection line 172
  18. lemma OAI.HochschildNormalPart.normalProjection_mul line 174
  19. lemma OAI.HochschildNormalPart.normalProjection_commutant line 182
  20. def OAI.HochschildNormalPart.coefficientLeft line 194
  21. lemma OAI.HochschildNormalPart.coefficientLeft_apply line 203
  22. def OAI.HochschildNormalPart.cyclicSpace line 207
  23. lemma OAI.HochschildNormalPart.cyclicSpace_closed line 210
  24. instance OAI.HochschildNormalPart.cyclicSpace_complete line 213
  25. lemma OAI.HochschildNormalPart.cyclicSpace_mem line 216
  26. lemma OAI.HochschildNormalPart.cyclicSpace_mul line 221
  27. lemma OAI.HochschildNormalPart.cyclicProjection_mul line 237
  28. lemma OAI.HochschildNormalPart.cyclic_coefficients_normal line 247
  29. lemma OAI.HochschildNormalPart.normalProjection_fixes_normal line 269
  30. def OAI.HochschildNormalPart.sumOperator line 316
  31. lemma OAI.HochschildNormalPart.sumOperator_apply line 322
  32. def OAI.HochschildNormalPart.sumRepresentation line 326
  33. lemma OAI.HochschildNormalPart.sumRepresentation_apply line 342
  34. lemma OAI.HochschildNormalPart.coefficient_sum line 346
  35. lemma OAI.HochschildNormalPart.mem_normalVectors_sum line 357
  36. lemma OAI.HochschildNormalPart.normalProjection_sum line 378
  37. lemma OAI.HochschildNormalPart.coefficient_normal_eq_of_eq line 397