RegularConvolutionOperators.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Integrable convolution operators in the regular commutant

The common regular action is strongly continuous by its gauge equivalence to translations. Its integrable scalar averages belong to the generated commutant algebra. Products of two such averages with a constant commutant coefficient give the finite packet averages used in the reconstruction argument.

theorem OAI.KadisonKastler.continuous_regularCoreAction line 29
Source documentation
The common regular action inherits strong continuity from translations.
```
theorem continuous_regularCoreAction (f : RegularCoreHilbert H) :
    Continuous (fun t : ℝ => (regularCoreAction U (Multiplicative.ofAdd t) :
      RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) f) := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreAction
theorem OAI.KadisonKastler.regularCoreAction_norm_le_one line 46
def OAI.KadisonKastler.regularActionIntegral line 54
Source documentation
The convolution convention uses the action at -t.
```
def regularActionIntegral (w : ℝ → ℂ) (hw : Integrable w volume) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.norm_regularActionIntegral_le line 62
theorem OAI.KadisonKastler.regularActionIntegral_mem line 71
Source documentation
No normalizer hypothesis is needed for these explicit generators.
```
theorem regularActionIntegral_mem (P : VonNeumannAlgebra H)
    (w : ℝ → ℂ) (hw : Integrable w volume) :
    regularActionIntegral U hU w hw ∈ regularCommutantAlgebra U P := by
…
```
Mentions: OAI.KadisonKastler.regularActionIntegral, OAI.KadisonKastler.regularCommutantAlgebra

def OAI.KadisonKastler.regularPacketConvolution line 81

Source documentation

The finite packet average has a factored, algebra-valued realization.

def regularPacketConvolution
    (φ ψ : ℝ → ℂ) (hφ : Integrable φ volume) (hψ : Integrable ψ volume)
    (A : H →L[ℂ] H) : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert

theorem OAI.KadisonKastler.regularPacketConvolution_mem line 87