WeakFieldNorm.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The quotient norm is the essential operator norm

The general Banach quotient supplies arbitrarily close representatives. A countable intersection gives the exact essential bound, and cutting off its exceptional set produces a norm-minimizing representative.

theorem OAI.KadisonKastler.operatorField_ae_norm_le line 23
Source documentation
Every representative satisfies its quotient norm bound almost everywhere.
```
theorem operatorField_ae_norm_le (F : WeakOperatorRepresentative (H := H) μ) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.exists_operatorFieldRepresentative line 41
Source documentation
The actual weak-operator quotient admits representatives attaining its norm.
```
theorem exists_operatorFieldRepresentative (T : WeakOperatorField (H := H) μ) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField