OAI/Analysis/ModularTheory/TomitaRegularizer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A finite-weight approximate identity whose GNS vector is the explicit time-domain Gaussian used in the Tomita calculation. The factor 2π is fixed by the Fourier convention, rather than absorbed into an informal notation.

  1. def OAI.WeakPureInfiniteness.modularFrequencyGaussian line 16
  2. lemma OAI.WeakPureInfiniteness.modularFrequencyGaussian_norm line 19
  3. lemma OAI.WeakPureInfiniteness.modularFrequencyGaussian_tendsto line 22
  4. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_fourier_scalar line 26
  5. lemma OAI.WeakPureInfiniteness.modularFrequencyGaussian_integrable line 54
  6. lemma OAI.WeakPureInfiniteness.modularFrequencyGaussian_weightedVector line 69
  7. lemma OAI.WeakPureInfiniteness.modularFrequencyGaussian_weightVector line 82
  8. lemma OAI.WeakPureInfiniteness.modularFrequencyGaussian_strong line 92