OAI/Analysis/KadisonKastler/WeightedStripKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An endpoint-continuous modular strip kernel

The extra factor s (1-s)^2 makes both boundary functions continuous on the closed resolvent spectrum. It will cancel on a dense operator range.

  1. def OAI.KadisonKastler.weightedStripKernel line 18
  2. theorem OAI.KadisonKastler.weighted_exponents_pos line 21
  3. theorem OAI.KadisonKastler.weightedStripKernel_continuousAt line 26
  4. theorem OAI.KadisonKastler.weightedStripKernel_differentiableAt line 37
  5. theorem OAI.KadisonKastler.weightedStripKernel_norm_le_one line 48