WeakFieldProjectionDensity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Spectral step approximation of measurable fields

A common dyadic mesh is used for every point of the measure space. Measurability of its finitely many projection fields follows inductively from the constructed spectral support. The existing concrete spectral interval estimate gives a uniform operator-norm error.

def OAI.KadisonKastler.WeakOperatorRepresentative.projectionField line 42
theorem OAI.KadisonKastler.WeakOperatorRepresentative.projectionField_isStarProjection line 48
theorem OAI.KadisonKastler.WeakOperatorRepresentative.topElement_isSelfAdjoint line 60
theorem OAI.KadisonKastler.WeakOperatorRepresentative.spectral_level_measurable line 66
def OAI.KadisonKastler.WeakOperatorRepresentative.uniformInterval line 128
theorem OAI.KadisonKastler.WeakOperatorRepresentative.selfAdjoint_mem_closed_projection_span line 153
Source documentation
Every self-adjoint measurable field is uniformly approximated by finite linear combinations of measurable projection fields.
```
theorem selfAdjoint_mem_closed_projection_span (F : WeakOperatorRepresentative (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.closed_projection_span_eq_top line 218
Source documentation
The measurable representative algebra has norm-dense projection span.
```
theorem closed_projection_span_eq_top :
    (Submodule.span ℂ {p : WeakOperatorRepresentative (H := H) μ |
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative