OAI/Analysis/OperatorAlgebra/DensitySpatialRepresentation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The left/right actions used by the finite-density argument are genuine spatial star representations on the Hilbert–Schmidt completion.

  1. instance OAI.WeakPureInfiniteness.densityHSNormed line 16
  2. instance OAI.WeakPureInfiniteness.densityHSInner line 17
  3. instance OAI.WeakPureInfiniteness.densityHSComplete line 18
  4. instance OAI.WeakPureInfiniteness.densityHSScalar line 19
  5. instance OAI.WeakPureInfiniteness.densityHSBounded line 20
  6. instance OAI.WeakPureInfiniteness.densityHSContinuous line 22
  7. def OAI.WeakPureInfiniteness.densityLeftRepresentation line 25
  8. def OAI.WeakPureInfiniteness.densityRightRepresentation line 29
  9. lemma OAI.WeakPureInfiniteness.densityLeftRight_commute line 33
  10. lemma OAI.WeakPureInfiniteness.densityLeft_coe line 39
  11. lemma OAI.WeakPureInfiniteness.densityLeft_unitary line 45
  12. lemma OAI.WeakPureInfiniteness.densityRight_unitary line 60