WeakFieldUnitary.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Unitary representatives of measurable operator classes

The AE-zero ideal has a useful lifting property: every unitary quotient class has an everywhere unitary, weakly measurable representative. Only a null set is changed, so no selection theorem is needed.

theorem OAI.KadisonKastler.WeakOperatorField.exists_unitary_lift line 24
Source documentation
A unitary operator class lifts to a unitary measurable representative.
```
theorem exists_unitary_lift (U : unitary (WeakOperatorField (H := H) μ)) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
def OAI.KadisonKastler.WeakOperatorRepresentative.unitaryEval line 76
Source documentation
Pointwise evaluation of a unitary representative is an actual unitary.
```
def unitaryEval (V : unitary (WeakOperatorRepresentative (H := H) μ)) (x : D) :
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative
theorem OAI.KadisonKastler.WeakOperatorRepresentative.unitaryEval_measurable line 85