RegularFourierTransport.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Fourier transport of constant operators and real translations

theorem OAI.KadisonKastler.postcomp_toLp line 16
Distinct definitions of this name: OAI/Analysis/KadisonKastler/L2FourierNaturality.lean:19 (different declaration text). Qualify references as OAI.KadisonKastler.postcomp_toLp@path.
theorem OAI.KadisonKastler.fourier_postcomp line 24
Distinct definitions of this name: OAI/Analysis/KadisonKastler/L2FourierNaturality.lean:27 (different declaration text). Qualify references as OAI.KadisonKastler.fourier_postcomp@path.
theorem OAI.KadisonKastler.fourier_constant_schwartz line 33
Distinct definitions of this name: OAI/Analysis/KadisonKastler/FourierConstant.lean:27 (different declaration text). Qualify references as OAI.KadisonKastler.fourier_constant_schwartz@path.
theorem OAI.KadisonKastler.fourier_regularConstantHom line 45
Source documentation
Fourier transformation commutes with every constant operator.
```
theorem fourier_regularConstantHom (b : H →L[ℂ] H) (f : RegularCoreHilbert H) :
    (𝓕 (regularConstantHom volume b f) : RegularCoreHilbert H) =
      regularConstantHom volume b (𝓕 f) := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularConstantHom
theorem OAI.KadisonKastler.translate_toLp line 60
theorem OAI.KadisonKastler.fourier_translate_schwartz line 71
Distinct definitions of this name: OAI/Analysis/KadisonKastler/FourierTranslation.lean:46 (same statement text; different proof or body). Qualify references as OAI.KadisonKastler.fourier_translate_schwartz@path.
theorem OAI.KadisonKastler.fourier_regularTranslateApply line 94
Source documentation
Right translation becomes multiplication by the positive Fourier character.
Distinct definitions of this name: OAI/Analysis/KadisonKastler/FourierTranslation.lean:62 (same statement text; different proof or body). Qualify references as OAI.KadisonKastler.fourier_regularTranslateApply@path.
```
theorem fourier_regularTranslateApply (s : ℝ) (f : RegularCoreHilbert H) :
    (𝓕 (regularTranslateApply s f) : RegularCoreHilbert H) =
      (regularCharacterUnitary (H := H) (2 * Real.pi * s) :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularTranslateApply, OAI.KadisonKastler.regularCharacterUnitary

theorem OAI.KadisonKastler.fourierConj_regularConstantHom line 113

Source documentation

Constant operators are unchanged by Fourier conjugation.

theorem fourierConj_regularConstantHom (b : H →L[ℂ] H) :
    (Lp.fourierTransformₗᵢ ℝ H).conjStarAlgEquiv (regularConstantHom volume b) =
      regularConstantHom volume b := by
…

Mentions: OAI.KadisonKastler.regularConstantHom

theorem OAI.KadisonKastler.fourierConj_regularTranslation line 125
Source documentation
Translation generators become the complete scalar-character family.
```
theorem fourierConj_regularTranslation (s : ℝ) :
    (Lp.fourierTransformₗᵢ ℝ H).conjStarAlgEquiv
      (regularRightTranslation (H := H) (Multiplicative.ofAdd s) :
…
```
Mentions: OAI.KadisonKastler.regularRightTranslation