OAI/Analysis/KadisonKastler/StripSineQuotient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing the pole in the modular strip contour

The scalar contour step in Rieffel--Van Daele, Lemma 4.6, uses (exp (i φ z) f z - f 0) / sin (π z). Divided differences remove its singularity at zero without assuming a residue theorem.

  1. def OAI.KadisonKastler.stripSineSlope line 21
  2. theorem OAI.KadisonKastler.stripSineSlope_ne_zero line 24
  3. theorem OAI.KadisonKastler.stripSineSlope_differentiable line 52
  4. def OAI.KadisonKastler.stripSineQuotient line 57
  5. theorem OAI.KadisonKastler.stripSineQuotient_eq line 60
  6. theorem OAI.KadisonKastler.stripSineQuotient_differentiableOn line 69
  7. theorem OAI.KadisonKastler.stripSineQuotient_continuousOn line 80