RegularIntervalAverages.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Normalized interval averages

The boundary strip has fixed width for fixed compact test vectors. Dividing the localization average by the interval length therefore recovers every translation-invariant operator weakly.

theorem OAI.KadisonKastler.norm_regularCut_translate_le line 24
theorem OAI.KadisonKastler.integrable_localized_coefficient line 34
theorem OAI.KadisonKastler.regularIntervalAverage_error_le line 55
Source documentation
The unnormalized error is confined to a fixed-width boundary strip.
```
theorem regularIntervalAverage_error_le
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ r : ℝ, Commute T (regularRightTranslation (H := H) (Multiplicative.ofAdd r) :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularRightTranslation
def OAI.KadisonKastler.regularNormalizedIntervalAverage line 93
Source documentation
The interval-length-normalized localization is a contraction on operators.
```
def regularNormalizedIntervalAverage (n : ℕ)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.norm_regularNormalizedIntervalAverage_le line 100