OAI/Analysis/BoundedHochschild/OperatorPrimitives.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Primitives on operator algebras and polar partial isometries.

  1. def OAI.BoundedHochschild.rankOneColumn line 29
  2. lemma OAI.BoundedHochschild.rankOneColumn_apply line 32
  3. lemma OAI.BoundedHochschild.mul_rankOneColumn line 35
  4. def OAI.BoundedHochschild.columnEvaluate line 42
  5. lemma OAI.BoundedHochschild.columnEvaluate_apply line 47
  6. def OAI.BoundedHochschild.operatorHomotopy line 52
  7. lemma OAI.BoundedHochschild.operatorHomotopy_apply line 56
  8. lemma OAI.BoundedHochschild.operatorHomotopy_cocycle line 60
  9. lemma OAI.BoundedHochschild.operatorHomotopy_norm line 79
  10. theorem OAI.BoundedHochschild.primitive_on_operators_of_dual_pair line 98
  11. theorem OAI.BoundedHochschild.primitive_on_operators line 115
  12. theorem OAI.HochschildPolar.exists_polar_contraction line 144
  13. lemma OAI.HochschildPolar.support_right_annihilate line 174
  14. theorem OAI.HochschildPolar.exists_polar_partial_isometry line 184