OAI/Analysis/KadisonKastler/HorizontalStripGluing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Holomorphic gluing across one horizontal line

This is the local analytic bridge for extending a bounded KMS strip whose two boundary values agree. Rectangular integrals split along the line; Morera's theorem then gives holomorphicity across it.

  1. theorem OAI.KadisonKastler.horizontal_rectangle_mem line 19
  2. theorem OAI.KadisonKastler.differentiableOn_horizontal_strip_glue line 27

    Source documentation

    Continuity and holomorphicity on both sides suffice across a horizontal seam.

    theorem differentiableOn_horizontal_strip_glue
    {f : ℂ → ℂ} {a b s : ℝ} (has : a < s) (hsb : s < b)
    (hc : ContinuousOn f {z | a < z.im ∧ z.im < b})
    (hd : ∀ z, a < z.im → z.im < b → z.im ≠ s → DifferentiableAt ℂ f z) :
    DifferentiableOn ℂ f {z | a < z.im ∧ z.im < b} := by
…