RegularCommutantDiagonal.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Generation of the bounded diagonal fields

The algebra generated by constant operators from P and scalar characters contains every bounded measurable P-valued field. Its commutant is recovered by the proved diagonal decomposition and countable commutant tests. This is a concrete generation statement, without any crossed-product input.

def OAI.KadisonKastler.regularDiagonalAlgebra line 26
Source documentation
Constants from P together with the complete scalar diagonal.
```
def regularDiagonalAlgebra (P : VonNeumannAlgebra H) :
    VonNeumannAlgebra (RegularCoreHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
theorem OAI.KadisonKastler.regularConstant_mem_diagonalAlgebra line 33
theorem OAI.KadisonKastler.regularCharacter_mem_constantDiagonalAlgebra line 39

theorem OAI.KadisonKastler.exists_field_of_mem_regularDiagonal_commutant line 46

Source documentation

Operators commuting with the diagonal algebra have P'-valued fields.

theorem exists_field_of_mem_regularDiagonal_commutant
    [TopologicalSpace.SeparableSpace H]
    (P : VonNeumannAlgebra H)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : T ∈ (regularDiagonalAlgebra P).commutant) :
    ∃ F : ℝ → H →L[ℂ] H,
      (∀ ξ, AEStronglyMeasurable (fun t => F t ξ) volume) ∧
      (∀ᵐ t ∂volume, ‖F t‖ ≤ ‖T‖) ∧ (∀ᵐ t ∂volume, F t ∈ P.commutant) ∧
      RepresentsOperatorField volume F T := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularDiagonalAlgebra, OAI.KadisonKastler.RepresentsOperatorField

theorem OAI.KadisonKastler.RepresentsOperatorField.mem_regularDiagonalAlgebra line 70
Source documentation
A represented field with almost-everywhere values in P belongs to the algebra generated by constants from P and scalar characters.
```
theorem RepresentsOperatorField.mem_regularDiagonalAlgebra
    [TopologicalSpace.SeparableSpace H]
    {F : ℝ → H →L[ℂ] H}
    {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) (P : VonNeumannAlgebra H)
    (hmem : ∀ᵐ t ∂volume, F t ∈ P) : T ∈ regularDiagonalAlgebra P := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.regularDiagonalAlgebra

theorem OAI.KadisonKastler.regularFieldOperator_mem_diagonalAlgebra line 94

Source documentation

An essentially bounded measurable field gives a concrete element of the constant-and-character algebra.

theorem regularFieldOperator_mem_diagonalAlgebra
    [TopologicalSpace.SeparableSpace H]
    (P : VonNeumannAlgebra H) (F : ℝ → H →L[ℂ] H)
    (hF : ∀ ξ, AEStronglyMeasurable (fun t => F t ξ) volume)
    (C : ℝ) (hC : ∀ᵐ t ∂volume, ‖F t‖ ≤ C)
    (hmem : ∀ᵐ t ∂volume, F t ∈ P) :
    regularFieldOperator volume F hF C hC ∈ regularDiagonalAlgebra P :=
…

Mentions: OAI.KadisonKastler.regularFieldOperator, OAI.KadisonKastler.regularDiagonalAlgebra