RegularCoreEigenoperator.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Site eigenoperators become coefficient-weighted frequency shifts

theorem OAI.KadisonKastler.fourierConj_regularCharacter line 17
Source documentation
A scalar character becomes a frequency translation.
```
theorem fourierConj_regularCharacter (s : ℝ) :
    (Lp.fourierTransformₗᵢ ℝ H).conjStarAlgEquiv
      (regularCharacterUnitary (H := H) (2 * Real.pi * s) :
…
```
Mentions: OAI.KadisonKastler.regularCharacterUnitary
theorem OAI.KadisonKastler.regularCoreEmbedding_of_eigenoperator line 39
Source documentation
The regular representation of an eigenoperator is a constant coefficient followed by the associated character multiplier.
```
theorem regularCoreEmbedding_of_eigenoperator (b : H →L[ℂ] H) (s : ℝ)
    (heigen : ∀ t : ℝ, unitaryConj (star (U (Multiplicative.ofAdd t))) b =
      regularCharacterScalar (2 * Real.pi * s) t • b) :
    regularCoreEmbedding U hU b = regularConstantHom volume b *
      (regularCharacterUnitary (H := H) (2 * Real.pi * s) :
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCharacterScalar, OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularConstantHom, OAI.KadisonKastler.regularCharacterUnitary
theorem OAI.KadisonKastler.fourierConj_regularCoreEigenoperator line 64
Source documentation
After Fourier transform, the eigenoperator is a coefficient-weighted translation. This is the shift used in the factorial-core argument.
```
theorem fourierConj_regularCoreEigenoperator (b : H →L[ℂ] H) (s : ℝ)
    (heigen : ∀ t : ℝ, unitaryConj (star (U (Multiplicative.ofAdd t))) b =
      regularCharacterScalar (2 * Real.pi * s) t • b) :
    (Lp.fourierTransformₗᵢ ℝ H).conjStarAlgEquiv (regularCoreEmbedding U hU b) =
      regularConstantHom volume b *
        (regularRightTranslation (H := H) (Multiplicative.ofAdd (-s)) :
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCharacterScalar, OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularConstantHom, OAI.KadisonKastler.regularRightTranslation