PublishedModularSpectral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The published modular spectral resolution, in bounded coordinates

Blackadar, Operator Algebras (2006), III.4.3.2 and III.4.4.7--9 and III.4.6.1--2 (printed pp.313, 316--317, 320), gives the modular group, centralizer characterization and the polar decomposition of the closed Tomita operator. III.4.7.1--2 (pp.325--326) identifies its action by the KMS strip condition. I.7.4.5--7 and I.7.4.10 (pp.34--37) give its logarithmic spectral resolution and functional calculus.

We retain only the upper cuts of log Δ, their Fourier gauge identity, and the bounded functional-calculus identities at distance 1/2 from a cut. The first entry of the graph projection is (1 + c² Δ)⁻¹. The identification of the second graph coordinate may be any antiunitary. There is no comparison between two algebras in this published input.

structure OAI.KadisonKastler.ModularSpectralResolution line 36
Source documentation
The part of modular spectral theory used by the application. All operators retained here are bounded, including the restricted inverse.
```
structure ModularSpectralResolution (M : VonNeumannAlgebra H) (Ω : H) where
…
```
def OAI.KadisonKastler.PublishedModularSpectralResolution line 69
Source documentation
Tomita--Takesaki and the spectral theorem at a cyclic separating vector, restricted to the bounded data above.
```
def PublishedModularSpectralResolution : Prop :=
…
```