OAI/Analysis/ModularTheory/NormalAdjointMap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Identification of the conjugate-linear norm isometry on normal-ordered weight vectors. This gives a common linear formula for the limits of regularized adjoints, so finite sums can be treated without a false termwise norm argument.

  1. lemma OAI.WeakPureInfiniteness.modularGauge_coefficient_scalar line 19
  2. lemma OAI.WeakPureInfiniteness.modularNormalOrdered_mem line 35
  3. lemma OAI.WeakPureInfiniteness.modularNormalOrdered_finite line 41
  4. lemma OAI.WeakPureInfiniteness.modularNormalWeightVector_gauge line 48
  5. lemma OAI.WeakPureInfiniteness.modularConjugationLp_weightedCoefficient line 63
  6. lemma OAI.WeakPureInfiniteness.modularWeightAdjointMap_normal line 88