OAI/Analysis/KadisonKastler/ModularStripKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A bounded analytic kernel for modular matrix coefficients

The factor s absorbs the possible growth of the logarithmic modular phase on the closed KMS strip. No modular algebra invariance is used.

  1. def OAI.KadisonKastler.modularStripKernel line 16
  2. theorem OAI.KadisonKastler.modularStripKernel_differentiable line 19
  3. theorem OAI.KadisonKastler.modularStripKernel_hasDerivAt line 24
  4. theorem OAI.KadisonKastler.modularStripKernel_norm line 34
  5. theorem OAI.KadisonKastler.modularStripKernel_norm_le_one line 51