ModularStateAction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A semantic certificate for the modular action of a vector state

The bounded KMS strip condition is Blackadar, Operator Algebras, III.4.7.1--2 (printed pp.325--326). For a faithful normal vector state it characterizes its modular automorphism group. Retaining the condition prevents the core classification from being applied to an arbitrary strongly continuous action.

def OAI.KadisonKastler.VectorStateKMS line 24
Source documentation
The scalar strip condition at inverse temperature minus one, with the sign convention σ_t(x) = U_t x U_t*.
```
def VectorStateKMS (M : VonNeumannAlgebra H) (Ω : H)
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H)) : Prop :=
…
```
structure OAI.KadisonKastler.IsModularStateGroup line 37
Source documentation
The canonical implementation fixes the vector; together with the strip condition this identifies the represented modular state action.
```
structure IsModularStateGroup (M : VonNeumannAlgebra H) (Ω : H)
    (U : Multiplicative ℝ →* unitary (H →L[ℂ] H)) : Prop where
…
```
theorem OAI.KadisonKastler.productVectorState_unitaryConj_of_fixes line 42
theorem OAI.KadisonKastler.IsModularStateGroup.state_invariant line 58