OAI/Analysis/ModularTheory/SpectralGaussian.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Strong Gaussian cutoffs in the modular spectral calculus. The compact spectral estimate is quantitative; no boundedness assumption on the modular generator is introduced.

  1. lemma OAI.WeakPureInfiniteness.modularGaussian_error line 17
  2. lemma OAI.WeakPureInfiniteness.modularGaussian_compact_error line 29
  3. lemma OAI.WeakPureInfiniteness.modularGaussian_compact_tendsto line 54
  4. def OAI.WeakPureInfiniteness.modularHalfGaussian line 64

    Source documentation

    A bounded regularization of the half-exponential.

    def modularHalfGaussian (n : ℕ) : BoundedContinuousFunction ℝ ℂ :=
…
  5. lemma OAI.WeakPureInfiniteness.modularHalfGaussian_apply line 76
  6. lemma OAI.WeakPureInfiniteness.modularHalfGaussian_resolvent line 79
  7. lemma OAI.WeakPureInfiniteness.modularGaussian_calculus_strong line 98
  8. lemma OAI.WeakPureInfiniteness.modularHalfGaussian_halfGraph line 105
  9. lemma OAI.WeakPureInfiniteness.modularHalfGaussian_calculus_strong line 111
  10. lemma OAI.WeakPureInfiniteness.modularHalfGaussian_tomita line 116
  11. lemma OAI.WeakPureInfiniteness.modularHalfGaussian_tomita_norm line 124