OAI/Analysis/KadisonKastler/CountableAmplificationNormal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Normality and separating vectors for countable amplification

Bounded weak operator limits pass through the countable diagonal action. A weighted dense sequence is a separating vector for that action. These are the concrete ingredients for a faithful cyclic representation.

  1. theorem OAI.KadisonKastler.l2Diagonal_tendsto_weak line 23
  2. instance OAI.KadisonKastler.countableHilbertSum_separable line 43
  3. def OAI.KadisonKastler.denseSequenceWeight line 63
  4. theorem OAI.KadisonKastler.denseSequenceWeight_pos line 67
  5. theorem OAI.KadisonKastler.norm_weighted_denseSeq_le line 71
  6. def OAI.KadisonKastler.weightedDenseVector line 80
  7. theorem OAI.KadisonKastler.weightedDenseVector_separating line 91
  8. theorem OAI.KadisonKastler.weightedDenseVector_ne_zero line 104
  9. def OAI.KadisonKastler.denseSeparatingUnitVector line 110
  10. theorem OAI.KadisonKastler.norm_denseSeparatingUnitVector line 113
  11. theorem OAI.KadisonKastler.denseSeparatingUnitVector_separating line 118