OAI/Analysis/KadisonKastler/PeriodicStripExtension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A bounded holomorphic strip with matching boundary values is constant

The matching edges give a periodic extension. The preceding rectangular Morera argument removes the seams, and Liouville applies to the extension.

  1. def OAI.KadisonKastler.periodicStripExtension line 20
  2. theorem OAI.KadisonKastler.periodicStripExtension_eq line 23
  3. theorem OAI.KadisonKastler.periodicStripExtension_continuousOn_cell line 37
  4. theorem OAI.KadisonKastler.periodicStripExtension_continuous line 53
  5. theorem OAI.KadisonKastler.periodicStripExtension_differentiableAt_cell line 79
  6. theorem OAI.KadisonKastler.periodicStripExtension_differentiable line 94
  7. theorem OAI.KadisonKastler.bounded_matching_strip_constant line 121

    Source documentation

    The exact scalar uniqueness statement needed after normalizing a KMS strip.

    theorem bounded_matching_strip_constant {f : ℂ → ℂ}
    (he : ∀ t : ℝ, f ((t : ℂ) + I) = f t)
    (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) :
    ∀ z : ℂ, 0 ≤ z.im → z.im ≤ 1 → f z = f 0 := by
…