RegularLocalizationAverage.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Bounded Haar averages of localized operators

The translated-cutoff analysis map takes values in an actual Hilbert space of square-integrable vectors. Sandwiching a constant amplification by this map constructs the Haar average without requiring operator-norm measurability.

theorem OAI.KadisonKastler.localFrame_memLp line 25
def OAI.KadisonKastler.regularLocalFrameValue line 34
Source documentation
The continuous analysis map of the translated scalar cutoff.
```
def regularLocalFrameValue (f : RegularCoreHilbert H) :
    Lp (RegularCoreHilbert H) 2 (volume : Measure ℝ) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularLocalFrameValue_apply_ae line 38
theorem OAI.KadisonKastler.norm_regularLocalFrameValue_sq line 43
theorem OAI.KadisonKastler.norm_regularLocalFrameValue line 55
def OAI.KadisonKastler.regularLocalFrame line 65
Source documentation
The translated-cutoff analysis map is bounded with its exact frame constant.
```
def regularLocalFrame : RegularCoreHilbert H →L[ℂ]
    Lp (RegularCoreHilbert H) 2 (volume : Measure ℝ) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.norm_regularLocalFrame_le line 100
def OAI.KadisonKastler.regularLocalizationAverage line 107
Source documentation
The unnormalized Haar average of localized copies of an operator.
```
def regularLocalizationAverage
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.norm_frame_sandwich_le line 113
theorem OAI.KadisonKastler.norm_regularLocalizationAverage_le line 131

theorem OAI.KadisonKastler.inner_regularLocalizationAverage line 142

Source documentation

Matrix coefficients of the Haar average are the actual scalar integrals.

theorem inner_regularLocalizationAverage
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (f g : RegularCoreHilbert H) :
    inner ℂ f (regularLocalizationAverage s hs hfinite T g) =
      ∫ r : ℝ, inner ℂ (regularIndicatorProjection s hs (regularTranslateApply r f))
        (T (regularIndicatorProjection s hs (regularTranslateApply r g))) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularLocalizationAverage, OAI.KadisonKastler.regularIndicatorProjection, OAI.KadisonKastler.regularTranslateApply