OAI/Analysis/KadisonKastler/StripContourAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar modular strip averaging formula

This is the contour identity of Rieffel--Van Daele, Lemma 4.6, for the centered strip. The pole is removed before applying rectangle integration.

  1. theorem OAI.KadisonKastler.centered_strip_average line 19