PublishedRegularDiagonal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Published spectral and diagonal decomposition inputs

The two inputs are kept separate. Blackadar, Operator Algebras (2006), I.7.4.5--7 and I.7.4.10 (printed pp.35--37), gives the spectral-commutant consequence of Stone's theorem: the commutant of multiplication by exp(i a t), for all real a, commutes with every bounded Borel multiplier. Here the generator is multiplication by the coordinate t.

III.1.6.2--3 (printed pp.253--254) gives the diagonal-commutant decomposition on the standard trivial field over the real line. Its conclusion is only the existence of a measurable bounded operator field representing an operator. Neither input asserts a core or fixed-point identification.

def OAI.KadisonKastler.regularScalarMultiplier line 32
Source documentation
The actual multiplication operator associated to a bounded Borel scalar function on the real line.
```
def regularScalarMultiplier (φ : ℝ → ℂ) (hφ : Measurable φ)
    (C : ℝ) (hC : ∀ t, ‖φ t‖ ≤ C) :
    RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert
def OAI.KadisonKastler.PublishedRealSpectralCommutant line 46
Source documentation
Stone's spectral-commutant theorem, restricted to the concrete character multiplication group on the real line.
```
def PublishedRealSpectralCommutant : Prop :=
…
```
def OAI.KadisonKastler.PublishedRealDiagonalDecomposition line 56
Source documentation
The diagonal-commutant decomposition theorem on a separable constant Hilbert field over Lebesgue measure.
```
def PublishedRealDiagonalDecomposition : Prop :=
…
```