ConstructedModularData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Assembling the constructed bounded modular data

The modular group and spectral cuts yield bounded modular data when the group normalizes the algebra. Tomita conjugation gives the conjugation data when it identifies the algebra with its commutant.

def OAI.KadisonKastler.constructedModularSpectralResolution line 28
Source documentation
Spectral modular data for a modular group normalizing the algebra.
```
def constructedModularSpectralResolution
    (hnormal : ∀ t, Conjugates (modularStrongGroup J Ω hsep hcyc t) M M) :
    ModularSpectralResolution M Ω where
…
```
Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.modularStrongGroup, OAI.KadisonKastler.ModularSpectralResolution
def OAI.KadisonKastler.constructedModularConjugationData line 48
Source documentation
Modular conjugation data from the Tomita commutant identity.
```
def constructedModularConjugationData
    (hcomm : conjugateRightAlgebra (tomitaPolarConjugation J Ω hsep hcyc)
      (tomitaPolarConjugation_involutive J Ω hsep hcyc) M = M.commutant) :
    ModularConjugationData M Ω where
…
```
Mentions: OAI.KadisonKastler.conjugateRightAlgebra, OAI.KadisonKastler.tomitaPolarConjugation, OAI.KadisonKastler.tomitaPolarConjugation_involutive, OAI.KadisonKastler.ModularConjugationData