DiagonalDecomposition.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The real-line diagonal-commutant decomposition

The local representatives determine a bounded operator on the rational core at almost every point. The pointwise difference bound then proves that the resulting field represents the original operator on every L2 vector, without choosing an uncountable common conull set.

theorem OAI.KadisonKastler.exists_diagonalField_of_commute_indicators line 25
theorem OAI.KadisonKastler.publishedRealDiagonalDecomposition line 75
Source documentation
Blackadar III.1.6.2--3, for the exact constant Hilbert field over Lebesgue measure required by the regular-core argument.
```
theorem publishedRealDiagonalDecomposition : PublishedRealDiagonalDecomposition.{u} := by
…
```