RegularPacketLocalization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Continuous frames from translated localizations

A finite-measure scalar cutoff has an exact Haar-averaged square norm. This gives the uniform bound needed when averaging local matrix compressions in the regular commutant proof.

theorem OAI.KadisonKastler.integrable_local_translates line 21

theorem OAI.KadisonKastler.integral_local_translates line 34

Source documentation

Integrating all translates of a local integral counts every point exactly by the measure of the localization set.

theorem integral_local_translates {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [CompleteSpace E]
    {g : ℝ → E} (hg : Integrable g volume)
    (s : Set ℝ) (hs : volume s ≠ ⊤) :
    (∫ r : ℝ, ∫ t in s, g (t + r)) = (volume s).toReal • ∫ t : ℝ, g t := by
…

theorem OAI.KadisonKastler.integrable_integral_local_translates line 44
theorem OAI.KadisonKastler.norm_local_translation_sq line 54
theorem OAI.KadisonKastler.integral_norm_local_translation_sq line 67
Source documentation
Translated cutoffs form a tight continuous frame.
```
theorem integral_norm_local_translation_sq
    (s : Set ℝ) (hs : MeasurableSet s) (hfinite : volume s ≠ ⊤)
    (f : RegularCoreHilbert H) :
    (∫ r : ℝ, ‖regularIndicatorProjection s hs
      ((regularRightTranslation (H := H) (Multiplicative.ofAdd r) :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularIndicatorProjection, OAI.KadisonKastler.regularRightTranslation

theorem OAI.KadisonKastler.integrable_norm_local_translation_sq line 80

Source documentation

The continuous frame's square norms are integrable.

theorem integrable_norm_local_translation_sq
    (s : Set ℝ) (hs : MeasurableSet s) (hfinite : volume s ≠ ⊤)
    (f : RegularCoreHilbert H) :
    Integrable (fun r : ℝ => ‖regularIndicatorProjection s hs
      ((regularRightTranslation (H := H) (Multiplicative.ofAdd r) :
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularIndicatorProjection, OAI.KadisonKastler.regularRightTranslation