OAI/Analysis/ModularTheory/WeightCutoffs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual finite vector functionals for the modular-core weight construction. The frequency cutoff is exp(πt) on [-n,n], with the sign fixed by the Fourier convention in ModularFourierTranslation. These are positive functionals, not yet an assertion of a tracial or semifinite limit.

  1. def OAI.WeakPureInfiniteness.modularWeightCutoffFunction line 16
  2. lemma OAI.WeakPureInfiniteness.modularWeightCutoff_memLp line 19
  3. def OAI.WeakPureInfiniteness.modularWeightCutoffVector line 28
  4. lemma OAI.WeakPureInfiniteness.modularWeightCutoffVector_ae line 31
  5. def OAI.WeakPureInfiniteness.modularCoreWeightVector line 38
  6. def OAI.WeakPureInfiniteness.modularCoreCutoffFunctional line 41
  7. lemma OAI.WeakPureInfiniteness.modularCoreCutoffFunctional_compression line 53
  8. lemma OAI.WeakPureInfiniteness.modularCoreCutoffFunctional_one line 67
  9. lemma OAI.WeakPureInfiniteness.modularCoreCutoffFunctional_monomial line 73
  10. lemma OAI.WeakPureInfiniteness.modularCoreCutoffFunctional_bound line 85