OAI/Analysis/ModularTheory/WeightGNS.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The concrete Hilbert-space vector of a finite-square-weight core operator. It is the limit of the actual cutoff vectors. The left-action identity is proved from continuity, without assuming the weight is tracial.

  1. def OAI.WeakPureInfiniteness.modularWeightVector line 22
  2. lemma OAI.WeakPureInfiniteness.modularWeightVector_tendsto line 25
  3. lemma OAI.WeakPureInfiniteness.modularWeightVector_norm_sq line 30
  4. lemma OAI.WeakPureInfiniteness.modularWeightVector_eq_zero_iff line 36
  5. lemma OAI.WeakPureInfiniteness.modularCoreSquareWeight_mul_finite line 52
  6. lemma OAI.WeakPureInfiniteness.modularWeightVector_mul line 58
  7. lemma OAI.WeakPureInfiniteness.modularCoreSquareWeight_add_finite line 68
  8. lemma OAI.WeakPureInfiniteness.modularWeightVector_add line 75