RegularizedModularGroup.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Bounded logarithmic approximations to the modular group

The logarithmic generator of the graph resolvent is regularized at both endpoints. Each approximation is an actual norm-continuous unitary group. The strong limit and its modular properties are subsequent constructions.

def OAI.KadisonKastler.scaleSelfAdjoint line 21
Source documentation
Real scaling written through the complex scalar action.
```
def scaleSelfAdjoint (a : selfAdjoint (H →L[ℂ] H)) (t : ℝ) : selfAdjoint (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.scaleSelfAdjoint_add line 27

def OAI.KadisonKastler.boundedSelfAdjointGroup line 34

Source documentation

Exponentiation of a bounded self-adjoint generator.

def boundedSelfAdjointGroup (a : selfAdjoint (H →L[ℂ] H)) :
    Multiplicative ℝ →* unitary (H →L[ℂ] H) where
…

theorem OAI.KadisonKastler.boundedSelfAdjointGroup_continuous line 49
theorem OAI.KadisonKastler.boundedSelfAdjointGroup_stronglyContinuous line 55

def OAI.KadisonKastler.regularizedModularLog line 61

Source documentation

The bounded approximation to log ((1-R)/R).

def regularizedModularLog (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (ε : ℝ) : selfAdjoint (H →L[ℂ] H) :=
…

def OAI.KadisonKastler.regularizedModularGroup line 68

Source documentation

The regularized unitary groups used to approach the modular group.

def regularizedModularGroup (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (ε : ℝ) : Multiplicative ℝ →* unitary (H →L[ℂ] H) :=
…

theorem OAI.KadisonKastler.regularizedModularGroup_stronglyContinuous line 72