OAI/Analysis/KadisonKastler/WeightedStripContinuous.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The weighted strip as a holomorphic continuous spectral function

  1. theorem OAI.KadisonKastler.weightedStripKernel_continuous_s line 17
  2. def OAI.KadisonKastler.weightedStripContinuous line 24
  3. theorem OAI.KadisonKastler.weightedStripContinuous_apply line 30
  4. theorem OAI.KadisonKastler.weightedStripContinuous_continuousOn line 35
  5. theorem OAI.KadisonKastler.weightedStripContinuous_differentiableOn line 51
  6. theorem OAI.KadisonKastler.weightedStripContinuous_norm_le line 64