OAI/Analysis/KadisonKastler/WeightedStripAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Applying the scalar strip formula to bounded operators

Extra resolvent powers make the spectral strip norm continuous up to both edges. Consequently the scalar contour theorem applies to every ambient operator, with no algebra normalization premise.

  1. def OAI.KadisonKastler.weightedStripCoefficient line 22
  2. theorem OAI.KadisonKastler.weightedStripCoefficient_differentiableOn line 27
  3. theorem OAI.KadisonKastler.weightedStripCoefficient_bound line 42
  4. theorem OAI.KadisonKastler.weightedStripCoefficient_average line 66