OAI/Analysis/ModularTheory/WeightMonomials.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-weight vectors for translation multipliers. Their frequency function is the multiplier times exp(πt), with the normalization fixed by the actual regular representation. These are the starting vectors for the Tomita symmetry calculation on normal-ordered core elements.

  1. def OAI.WeakPureInfiniteness.modularWeightedFunction line 18
  2. lemma OAI.WeakPureInfiniteness.modularWeightedFunction_norm_sq line 21
  3. lemma OAI.WeakPureInfiniteness.modularWeightedFunction_memLp line 30
  4. def OAI.WeakPureInfiniteness.modularWeightedVector line 38
  5. lemma OAI.WeakPureInfiniteness.modularWeightedVector_ae line 43
  6. lemma OAI.WeakPureInfiniteness.modularWeightedVector_cutoff line 47
  7. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_finite line 68
  8. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_weightVector line 74
  9. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_weight_exact line 86
  10. lemma OAI.WeakPureInfiniteness.modularCoefficient_scalar_norm_sq line 99
  11. lemma OAI.WeakPureInfiniteness.modularNormalOrdered_weight_exact line 112