WeakFieldSpectralSupport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Spectral support inside measurable fields

The pointwise support of a continuous positive part is a measurable field. This connects the constructed kernel projection with the concrete spectral splittings already used in finite-factor arguments.

def OAI.KadisonKastler.WeakOperatorRepresentative.fullOperatorAlgebra line 25
Source documentation
The full concrete operator algebra.
```
def fullOperatorAlgebra : VonNeumannAlgebra H where
…
```
def OAI.KadisonKastler.WeakOperatorRepresentative.topElement line 42
Source documentation
The value of a field, viewed inside the full operator algebra.
```
def topElement (F : WeakOperatorRepresentative (H := H) μ) (x : D) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.topElement_val line 45
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_posPart line 48
theorem OAI.KadisonKastler.WeakOperatorRepresentative.topElement_posPart_val line 55
def OAI.KadisonKastler.WeakOperatorRepresentative.positiveSupport line 69
Source documentation
Support of the positive part, as an actual measurable field.
```
def positiveSupport (F : WeakOperatorRepresentative (H := H) μ) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.positiveSupport_isStarProjection line 73
theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_positiveSupport line 78
Source documentation
Evaluation agrees with the concrete range-projection construction.
```
theorem eval_positiveSupport (F : WeakOperatorRepresentative (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative