OAI/Analysis/KadisonKastler/RegularIntervalAverageEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The boundary estimate for interval localization

An integrable coefficient which equals its invariant value on the interior interval and vanishes beyond the enlarged interval has an error controlled by the fixed-width boundary strip.

  1. theorem OAI.KadisonKastler.regular_interval_boundary_estimate line 19