RegularFieldMembership.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Countable tests recover fiberwise algebra membership

A represented measurable field inherits commutation with a bounded set of constant operators on one common conull set. Countable strong tests justify the interchange of the almost-everywhere and operator quantifiers.

theorem OAI.KadisonKastler.RepresentsOperatorField.commute_constant_ae line 25

Source documentation

Constant commutation descends to a represented field almost everywhere.

theorem RepresentsOperatorField.commute_constant_ae
    {F : ℝ → H →L[ℂ] H} {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) (b : H →L[ℂ] H)
    (hcomm : Commute T (regularConstantHom volume b)) :
    ∀ᵐ t ∂volume, Commute (F t) b := by
…

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

theorem OAI.KadisonKastler.RepresentsOperatorField.commute_set_ae line 36

Source documentation

One common conull set works for a whole bounded collection of tests.

theorem RepresentsOperatorField.commute_set_ae
    {F : ℝ → H →L[ℂ] H} {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) (S : Set (H →L[ℂ] H))
    (hS : ∀ b ∈ S, ‖b‖ ≤ 1)
    (hcomm : ∀ b ∈ S, Commute T (regularConstantHom volume b)) :
    ∀ᵐ t ∂volume, ∀ b ∈ S, Commute (F t) b := by
…

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

theorem OAI.KadisonKastler.RepresentsOperatorField.mem_algebra_ae line 51
Source documentation
The field of an operator in the constant-commutant tensor algebra belongs to the original algebra almost everywhere.
```
theorem RepresentsOperatorField.mem_algebra_ae
    {F : ℝ → H →L[ℂ] H} {T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) (P : VonNeumannAlgebra H)
    (hT : T ∈ regularTensorAlgebra P) : ∀ᵐ t ∂volume, F t ∈ P := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.regularTensorAlgebra