WeakOperatorCoefficients.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Scalar coefficients determine weak operator fields

def OAI.KadisonKastler.WeakOperatorRepresentative.asUniformFamily line 21
Source documentation
A representative is the one-element case of a uniformly bounded family.
```
def asUniformFamily (F : WeakOperatorRepresentative (H := H) μ) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
def OAI.KadisonKastler.WeakOperatorRepresentative.coefficient line 30
Source documentation
Scalar matrix coefficients as L-infinity classes.
```
def coefficient (F : WeakOperatorRepresentative (H := H) μ) (ξ η : H) : ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative, OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.WeakOperatorRepresentative.coefficient_ae line 34
def OAI.KadisonKastler.WeakOperatorRepresentative.scalarKernel line 39
Source documentation
The bounded sesquilinear kernel of a representative.
```
def scalarKernel (F : WeakOperatorRepresentative (H := H) μ) : ScalarOperatorKernel H μ where
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative, OAI.KadisonKastler.ScalarOperatorKernel
theorem OAI.KadisonKastler.WeakOperatorRepresentative.coefficient_eq_of_ae line 51
Source documentation
Almost-everywhere equal representatives have identical scalar coefficients.
```
theorem coefficient_eq_of_ae (F G : WeakOperatorRepresentative (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.ae_eq_of_coefficient_eq line 59
Source documentation
Conversely, a countable dense set of coefficients detects AE equality.
```
theorem ae_eq_of_coefficient_eq [TopologicalSpace.SeparableSpace H]
    (F G : WeakOperatorRepresentative (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.quotient_eq_iff_coefficient_eq line 82
Source documentation
Scalar coefficients exactly detect equality in the actual C-star quotient.
```
theorem quotient_eq_iff_coefficient_eq [TopologicalSpace.SeparableSpace H]
    (F G : WeakOperatorRepresentative (H := H) μ) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative