OAI/Analysis/ModularTheory/TomitaLp.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Weighted L² convergence for the full Tomita orbit. This turns the frequencywise Gaussian identity into convergence of actual Hilbert-space vectors, with the square norm required for the core weight calculation.

  1. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_weighted_integral_limit_all line 19
  2. def OAI.WeakPureInfiniteness.modularTomitaFourierFunction line 71
  3. lemma OAI.WeakPureInfiniteness.modularTomitaFourierFunction_memLp line 75
  4. def OAI.WeakPureInfiniteness.modularTomitaFourierVector line 90
  5. lemma OAI.WeakPureInfiniteness.modularTomitaFourierVector_ae line 98
  6. lemma OAI.WeakPureInfiniteness.modularTomitaLimitFunction_memLp line 106
  7. def OAI.WeakPureInfiniteness.modularTomitaLimitVector line 113
  8. lemma OAI.WeakPureInfiniteness.modularTomitaLimitVector_ae line 120
  9. lemma OAI.WeakPureInfiniteness.modularTomitaLimitVector_norm_sq line 126
  10. lemma OAI.WeakPureInfiniteness.modularTomitaFourierVector_tendsto line 136