OAI/Analysis/ModularTheory/TomitaTime.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Time-domain realizations of the regularized Tomita vectors, and the identification of their weighted transforms in the actual L² representation.

  1. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_continuous line 15
  2. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_bounded line 19
  3. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_memLp line 35
  4. def OAI.WeakPureInfiniteness.modularTomitaKernelVector line 46
  5. lemma OAI.WeakPureInfiniteness.modularTomitaKernelVector_ae line 49
  6. lemma OAI.WeakPureInfiniteness.modularTomitaTimeFunction_memLp line 54
  7. def OAI.WeakPureInfiniteness.modularTomitaTimeVector line 64
  8. lemma OAI.WeakPureInfiniteness.modularTomitaTimeVector_ae line 69
  9. lemma OAI.WeakPureInfiniteness.modularTomitaTimeVector_fourier line 73
  10. lemma OAI.WeakPureInfiniteness.modularCoefficient_kernelVector line 90