OAI/Analysis/KadisonKastler/StripContourBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Decay on the horizontal edges of the modular contour

  1. theorem OAI.KadisonKastler.norm_complex_sin_lower line 11
  2. theorem OAI.KadisonKastler.strip_sine_exponential_lower line 33
  3. theorem OAI.KadisonKastler.stripSineQuotient_decay line 46