OAI/Analysis/KadisonKastler/KMSScalarStrip.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.kms_strip_exponential line 16

   Source documentation

   A positive modular frequency is uniquely determined by the ratio of the boundary values of its bounded KMS strip.

   theorem kms_strip_exponential {f : ℂ → ℂ} {L : ℝ} (hL : 0 ≤ L)
       (hc : ContinuousOn f {z | 0 ≤ z.im ∧ z.im ≤ 1})
       (hd : DifferentiableOn ℂ f {z | 0 < z.im ∧ z.im < 1})
       (hb : ∃ C : ℝ, ∀ z : ℂ, 0 ≤ z.im → z.im ≤ 1 → ‖f z‖ ≤ C)
       (he : ∀ t : ℝ, f ((t : ℂ) + I) = (Real.exp (-L) : ℂ) * f t) :
       ∀ t : ℝ, f t = Complex.exp (I * (L : ℂ) * t) * f 0 := by
   …