RegularCommutantFourier.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete Fourier reductions for the regular commutant theorem

Translation commutation gives an actual bounded measurable Fourier field. Adjoining the character multipliers to the regular core generates the whole constant-commutant tensor algebra. These conclusions use the proved spectral and diagonal decomposition theorems, not a crossed-product commutant assumption.

theorem OAI.KadisonKastler.fourier_commute_characters_of_translations line 30
Source documentation
Fourier transformation sends translation commutation to character commutation.
```
theorem fourier_commute_characters_of_translations
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ s : Multiplicative ℝ, Commute T
      (regularRightTranslation (H := H) s :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularRightTranslation
theorem OAI.KadisonKastler.exists_fourierField_of_commute_translations line 46
Source documentation
Every translation-commuting operator has a bounded measurable Fourier field.
```
theorem exists_fourierField_of_commute_translations
    [TopologicalSpace.SeparableSpace H]
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ s : Multiplicative ℝ, Commute T
      (regularRightTranslation (H := H) s :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularRightTranslation
theorem OAI.KadisonKastler.exists_fourierField_mem_of_commute_translations line 66
Source documentation
A translation-commuting operator in the tensor algebra has Fourier fibers in that same algebra.
```
theorem exists_fourierField_mem_of_commute_translations
    [TopologicalSpace.SeparableSpace H]
    (P : VonNeumannAlgebra H)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ s : Multiplicative ℝ, Commute T
      (regularRightTranslation (H := H) s :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularRightTranslation
theorem OAI.KadisonKastler.exists_constant_of_commute_translations_characters line 88
Source documentation
Commutation with both the translations and the character multipliers forces an operator to be constant on the real variable.
```
theorem exists_constant_of_commute_translations_characters
    [TopologicalSpace.SeparableSpace H]
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (htrans : ∀ s : Multiplicative ℝ, Commute T
      (regularRightTranslation (H := H) s :
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularRightTranslation
def OAI.KadisonKastler.regularCoreDiagonalAlgebra line 110
Source documentation
Adjoin the full scalar diagonal to the actual regular core.
```
def regularCoreDiagonalAlgebra : VonNeumannAlgebra (RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularCore_le_diagonalAlgebra line 116
theorem OAI.KadisonKastler.regularCharacter_mem_diagonalAlgebra line 122
theorem OAI.KadisonKastler.exists_constant_of_mem_regularCoreDiagonal_commutant line 130
Source documentation
The commutant of the core together with the scalar diagonal consists only of constant operators from the original commutant.
```
theorem exists_constant_of_mem_regularCoreDiagonal_commutant
    [TopologicalSpace.SeparableSpace H]
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : T ∈ (regularCoreDiagonalAlgebra U hU P).commutant) :
    ∃ A ∈ P.commutant, T = regularConstantHom volume A := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreDiagonalAlgebra, OAI.KadisonKastler.regularConstantHom
theorem OAI.KadisonKastler.regularCoreDiagonalAlgebra_eq_tensor line 156
Source documentation
The scalar diagonal and the core generate the entire regular tensor algebra. This is the concrete dual-generation step, proved without the regular commutant input.
```
theorem regularCoreDiagonalAlgebra_eq_tensor [TopologicalSpace.SeparableSpace H]
    (hP : ∀ s x, x ∈ P → unitaryConj (U s) x ∈ P) :
    regularCoreDiagonalAlgebra U hU P = regularTensorAlgebra P := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreDiagonalAlgebra, OAI.KadisonKastler.regularTensorAlgebra