ModularSiteEigen.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Modular eigenoperators from the site-state balance identity

theorem OAI.KadisonKastler.state_balance_unitary line 16

theorem OAI.KadisonKastler.modular_eigen_of_state_balance line 45

Source documentation

The KMS condition turns a weighted trace identity into an operator eigenvalue.

theorem modular_eigen_of_state_balance
    (m : ModularSpectralResolution M Ω)
    (hsep : Function.Injective (algebraVectorMap M Ω))
    (x : H →L[ℂ] H) (hx : x ∈ M) (L : ℝ) (hL : 0 ≤ L)
    (hbal : ∀ y ∈ M, productVectorState Ω (y * x) =
      (Real.exp (-L) : ℂ) * productVectorState Ω (x * y)) (t : ℝ) :
    unitaryConj (m.group (Multiplicative.ofAdd t)) x =
      Complex.exp (Complex.I * (L : ℂ) * t) • x := by
…

Mentions: OAI.KadisonKastler.ModularSpectralResolution, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.productVectorState, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.PointedMatrixSites.twoRatio_site_modular_eigen line 97
Source documentation
The off-diagonal matrix unit at every site has its prescribed modular frequency.
```
theorem twoRatio_site_modular_eigen
    (S : PointedMatrixSites M Ω twoRatioSiteParameter)
    (m : ModularSpectralResolution M Ω) (i : TwoRatioSite) (t : ℝ) :
    unitaryConj (m.group (Multiplicative.ofAdd t)) ((S.site i).entry 0 1) =
      Complex.exp (Complex.I * ((-Real.log (twoRatioSiteParameter i) : ℝ) : ℂ) * t) •
        (S.site i).entry 0 1 := by
…
```
Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.twoRatioSiteParameter, OAI.KadisonKastler.ModularSpectralResolution, OAI.KadisonKastler.TwoRatioSite, OAI.KadisonKastler.unitaryConj
theorem OAI.KadisonKastler.PointedMatrixSites.twoRatio_site_modular_star_eigen line 128
theorem OAI.KadisonKastler.PointedMatrixSites.twoRatio_site_algebra_le line 143