RegularCoreCentralField.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Fourier fields of central elements in the actual regular core

theorem OAI.KadisonKastler.regularCore_central_fourier_field line 29

Source documentation

Centrality supplies diagonal decomposition after Fourier transform; countable commutant tests put its fibers in the original algebra. The only inputs are the separate published spectral and diagonal theorems.

theorem regularCore_central_fourier_field
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (hP : ∀ s x, x ∈ P → unitaryConj (U s) x ∈ P)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : T ∈ regularCoreAlgebra U hU P)
    (hcentral : ∀ S ∈ regularCoreAlgebra U hU P, S * T = T * S) :
    ∃ F : ℝ → H →L[ℂ] H,
      (∀ ξ, AEStronglyMeasurable (fun t => F t ξ) volume) ∧
      (∀ᵐ t ∂volume, ‖F t‖ ≤ ‖T‖) ∧ (∀ᵐ t ∂volume, F t ∈ P) ∧
      RepresentsOperatorField volume F ((Lp.fourierTransformₗᵢ ℝ H).conjStarAlgEquiv T) := by
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreAlgebra, OAI.KadisonKastler.RepresentsOperatorField

theorem OAI.KadisonKastler.regularCoreEmbedding_eq_constant_of_fixed line 63
Source documentation
Fixed operators have constant regular embeddings.
```
theorem regularCoreEmbedding_eq_constant_of_fixed (b : H →L[ℂ] H)
    (hfixed : ∀ s, unitaryConj (U s) b = b) :
    regularCoreEmbedding U hU b = regularConstantHom volume b := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularConstantHom

theorem OAI.KadisonKastler.regularCore_central_fourier_commutes_fixed line 81

Source documentation

A fixed base element commutes with the Fourier transform of a central core element, in its constant representation.

theorem regularCore_central_fourier_commutes_fixed
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hcentral : ∀ S ∈ regularCoreAlgebra U hU P, S * T = T * S)
    (b : H →L[ℂ] H) (hb : b ∈ P) (hfixed : ∀ s, unitaryConj (U s) b = b) :
    Commute ((Lp.fourierTransformₗᵢ ℝ H).conjStarAlgEquiv T)
      (regularConstantHom volume b) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreAlgebra, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularConstantHom

theorem OAI.KadisonKastler.constant_commutes_regularEmbedding line 95
Source documentation
Commutation with a constant operator in the regular representation recovers commutation at time zero by continuity of the modular action.
```
theorem constant_commutes_regularEmbedding
    (A x : H →L[ℂ] H)
    (hc : Commute (regularConstantHom volume A) (regularCoreEmbedding U hU x)) :
    Commute A x := by
…
```
Mentions: OAI.KadisonKastler.regularConstantHom, OAI.KadisonKastler.regularCoreEmbedding

theorem OAI.KadisonKastler.regularCore_constant_central_scalar line 121

Source documentation

A constant central operator in the core of a factor is scalar.

theorem regularCore_constant_central_scalar
    (hP : ∀ s x, x ∈ P → unitaryConj (U s) x ∈ P) (hfactor : ScalarCenter P)
    (A : H →L[ℂ] H)
    (hA : regularConstantHom volume A ∈ regularCoreAlgebra U hU P)
    (hcentral : ∀ S ∈ regularCoreAlgebra U hU P,
      S * regularConstantHom volume A = regularConstantHom volume A * S) :
    ∃ c : ℂ, regularConstantHom volume A = c •
      (1 : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) := by
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.regularConstantHom, OAI.KadisonKastler.regularCoreAlgebra, OAI.KadisonKastler.RegularCoreHilbert