OperatorFieldValues.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Von Neumann algebra values of measurable operator fields

Commuting with constant operators in the commutant is a norm-closed condition. Countably many strong-operator tests identify this condition with pointwise membership outside one null set.

def OAI.KadisonKastler.operatorFieldAlgebra line 24
Source documentation
The closed field algebra commuting with the constant commutant.
```
def operatorFieldAlgebra (M : VonNeumannAlgebra H) :
    StarSubalgebra ℂ (WeakOperatorField (H := H) μ) :=
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.isClosed_operatorFieldAlgebra line 28
instance OAI.KadisonKastler.operatorFieldAlgebraCStar line 32
theorem OAI.KadisonKastler.mem_operatorFieldAlgebra_iff line 36
def OAI.KadisonKastler.HasOperatorValues line 49
Source documentation
Pointwise algebra membership of the canonical representative.
```
def HasOperatorValues (M : VonNeumannAlgebra H) (q : WeakOperatorField (H := H) μ) : Prop :=
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.hasOperatorValues_quotient_iff line 52
theorem OAI.KadisonKastler.mem_operatorFieldAlgebra_of_values line 66
theorem OAI.KadisonKastler.hasOperatorValues_of_mem line 85
Source documentation
Countably many constant commutant tests suffice to recover actual von Neumann algebra membership almost everywhere.
```
theorem hasOperatorValues_of_mem (M : VonNeumannAlgebra H)
    (q : WeakOperatorField (H := H) μ) (hq : q ∈ operatorFieldAlgebra (μ := μ) M) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField, OAI.KadisonKastler.operatorFieldAlgebra
theorem OAI.KadisonKastler.mem_operatorFieldAlgebra_iff_values line 123
theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorMean_mem line 132
Source documentation
The operator mean retains values in any specified von Neumann algebra.
```
theorem ScalarBoundaryMean.operatorMean_mem (m : ScalarBoundaryMean α)
    (hTom : PublishedFieldTomiyama (G := G) (H := H) (μ := μ))
…
```
Mentions: OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.PublishedFieldTomiyama