OAI/Analysis/ModularTheory/TranslationWeight.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The regular translation calculus acts on the scalar weight vectors by ordinary frequency multiplication. Integrable frequency envelopes therefore give actual finite-weight elements of the core.

  1. lemma OAI.WeakPureInfiniteness.vectorLpRepresentation_compLp line 21
  2. lemma OAI.WeakPureInfiniteness.vectorLpRepresentation_complex line 34
  3. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_fourierInclusion line 46
  4. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_weightNorm line 57
  5. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_weight_le line 64