OAI/Analysis/ModularTheory/WeightAdjointMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A norm-preserving conjugate-linear map on the actual core GNS Hilbert space. Gauge removal and Fourier transform turn a normal-ordered weight vector into its scalar frequency coefficient before modular conjugation.

  1. def OAI.WeakPureInfiniteness.modularConjugationLp line 18
  2. lemma OAI.WeakPureInfiniteness.modularConjugationLp_ae line 22
  3. lemma OAI.WeakPureInfiniteness.modularConjugationLp_norm line 26
  4. def OAI.WeakPureInfiniteness.modularWeightAdjointMap line 35
  5. lemma OAI.WeakPureInfiniteness.modularWeightAdjointMap_norm line 39
  6. lemma OAI.WeakPureInfiniteness.modularWeightAdjointMap_add line 46
  7. lemma OAI.WeakPureInfiniteness.modularWeightAdjointMap_continuous line 57