The iβ-periodic entire extension (strip Schwarz reflection)

Given a function F continuous on the closed strip 0 ≤ Im z ≤ β, holomorphic on the open strip, and with equal boundary values F(t) = F(t + iβ) on the real axis, this file constructs a bounded entire extension H agreeing with F on ℝ.

The extension is the iβ-periodic continuation: H z = F (z - ⌊Im z / β⌋ · iβ), which folds every point back into the fundamental strip. It is:

• continuous everywhere - across each gluing line Im z = kβ the boundary values match by periodicity (ContinuousOn.if);
• holomorphic off the lines - on each open strip it is F composed with a holomorphic shift into the open fundamental strip;
• holomorphic on the lines - by the horizontal-line removable singularity theorem differentiableOn_of_continuousOn_off_horizontal_line;
• bounded - its values are F-values on the fundamental strip.

The headline result exists_bounded_entire_extension_of_strip_periodic is exactly the construction that Physicslib4.AQFT.stripLiouville_of_entire_extension consumes, so it discharges the StripLiouville principle (and hence KMS invariance) for β > 0.

theorem Physicslib4.floor_div_eq_iff {β : ℝ} (hβ : 0 < β) (x : ℝ) (m : ℤ) : ⌊x / β⌋ = m ↔ ↑m * β ≤ x ∧ x < (↑m + 1) * β

Characterisation of ⌊x / β⌋ = m for β > 0: it is mβ ≤ x < (m+1)β.

theorem Physicslib4.sub_intMul_im (k : ℤ) (β : ℝ) (w : ℂ) : (w - ↑k * (↑β * Complex.I)).im = w.im - ↑k * β

The imaginary part of a vertical integer-multiple shift.

theorem Physicslib4.sub_intMul_re (k : ℤ) (β : ℝ) (w : ℂ) : (w - ↑k * (↑β * Complex.I)).re = w.re

The real part of a vertical integer-multiple shift is unchanged.

noncomputable def Physicslib4.pshift (β : ℝ) (z : ℂ) : ℂ

The vertical fold shift z ↦ z - ⌊Im z / β⌋ · iβ.

Equations

• Physicslib4.pshift β z = z - ↑⌊z.im / β⌋ * (↑β * Complex.I)

noncomputable def Physicslib4.pext (β : ℝ) (F : ℂ → ℂ) (z : ℂ) : ℂ

The iβ-periodic extension z ↦ F (pshift β z).

Equations

• Physicslib4.pext β F z = F (Physicslib4.pshift β z)

theorem Physicslib4.pshift_im (β : ℝ) (z : ℂ) : (pshift β z).im = z.im - ↑⌊z.im / β⌋ * β

theorem Physicslib4.pshift_im_mem {β : ℝ} (hβ : 0 < β) (z : ℂ) : 0 ≤ (pshift β z).im ∧ (pshift β z).im < β

The folded point lies in the fundamental strip 0 ≤ Im ≤ β (in fact < β).

theorem Physicslib4.pext_differentiableAt_offline {β : ℝ} {F : ℂ → ℂ} (hβ : 0 < β) (hdiff : DifferentiableOn ℂ F {z : ℂ | 0 < z.im ∧ z.im < β}) {z : ℂ} (hz : 0 < (pshift β z).im) : DifferentiableAt ℂ (pext β F) z

Off the gluing lines, the periodic extension is differentiable: near any point whose fold lands strictly inside the open strip, the floor is locally constant, so the extension is F composed with a holomorphic shift.

theorem Physicslib4.pext_differentiableAt_online {β : ℝ} {F : ℂ → ℂ} (hβ : 0 < β) (hcont : ContinuousOn F {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}) (hdiff : DifferentiableOn ℂ F {z : ℂ | 0 < z.im ∧ z.im < β}) (hper : ∀ (t : ℝ), F ↑t = F (↑t + ↑β * Complex.I)) {z₀ : ℂ} (hz₀ : (pshift β z₀).im = 0) : DifferentiableAt ℂ (pext β F) z₀

On a gluing line, the periodic extension is differentiable: on a ball around the point it equals a two-piece function glued across the line, which is continuous (boundary values match by periodicity) and holomorphic off the line, hence holomorphic by the removable-singularity theorem.

theorem Physicslib4.pext_differentiable {β : ℝ} {F : ℂ → ℂ} (hβ : 0 < β) (hcont : ContinuousOn F {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}) (hdiff : DifferentiableOn ℂ F {z : ℂ | 0 < z.im ∧ z.im < β}) (hper : ∀ (t : ℝ), F ↑t = F (↑t + ↑β * Complex.I)) : Differentiable ℂ (pext β F)

The periodic extension is entire.

theorem Physicslib4.exists_bounded_entire_extension_of_strip_periodic {β : ℝ} {F : ℂ → ℂ} (hβ : 0 < β) (hcont : ContinuousOn F {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}) (hdiff : DifferentiableOn ℂ F {z : ℂ | 0 < z.im ∧ z.im < β}) (hper : ∀ (t : ℝ), F ↑t = F (↑t + ↑β * Complex.I)) (hbdd : ∃ (C : ℝ), ∀ z ∈ {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}, ‖F z‖ ≤ C) : ∃ (H : ℂ → ℂ), Differentiable ℂ H ∧ Bornology.IsBounded (Set.range H) ∧ ∀ (t : ℝ), H ↑t = F ↑t

The iβ-periodic bounded entire extension. A function continuous on the closed strip 0 ≤ Im ≤ β, holomorphic on the open strip, bounded, and with equal boundary values F(t) = F(t + iβ), admits a bounded entire extension agreeing with it on the real axis.

theorem Physicslib4.pext_eq_of_mem_strip {β : ℝ} {F : ℂ → ℂ} (hβ : 0 < β) {z : ℂ} (h0 : 0 ≤ z.im) (hβz : z.im < β) : pext β F z = F z

The periodic extension agrees with F on the (half-open) fundamental strip 0 ≤ Im z < β, where the fold is the identity.

theorem Physicslib4.eq_zero_on_strip_of_zero_boundary {β : ℝ} {F : ℂ → ℂ} (hβ : 0 < β) (hcont : ContinuousOn F {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}) (hdiff : DifferentiableOn ℂ F {z : ℂ | 0 < z.im ∧ z.im < β}) (hbdd : ∃ (C : ℝ), ∀ z ∈ {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}, ‖F z‖ ≤ C) (hbot : ∀ (t : ℝ), F ↑t = 0) (htop : ∀ (t : ℝ), F (↑t + ↑β * Complex.I) = 0) {z : ℂ} (hz0 : 0 ≤ z.im) (hzβ : z.im ≤ β) : F z = 0

Vanishing from zero boundary values. A function continuous and bounded on the closed strip 0 ≤ Im z ≤ β, holomorphic on the open strip, whose boundary values on both lines vanish, is identically zero on the strip. The periodic extension is then a bounded entire function (its boundary values agree), hence constant by Liouville, and the constant is its value F(0) = 0.

theorem Physicslib4.eqOn_strip_of_eq_boundary {β : ℝ} (hβ : 0 < β) {F G : ℂ → ℂ} (hFc : ContinuousOn F {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}) (hFd : DifferentiableOn ℂ F {z : ℂ | 0 < z.im ∧ z.im < β}) (hFb : ∃ (C : ℝ), ∀ z ∈ {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}, ‖F z‖ ≤ C) (hGc : ContinuousOn G {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}) (hGd : DifferentiableOn ℂ G {z : ℂ | 0 < z.im ∧ z.im < β}) (hGb : ∃ (C : ℝ), ∀ z ∈ {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β}, ‖G z‖ ≤ C) (hbot : ∀ (t : ℝ), F ↑t = G ↑t) (htop : ∀ (t : ℝ), F (↑t + ↑β * Complex.I) = G (↑t + ↑β * Complex.I)) {z : ℂ} (hz0 : 0 ≤ z.im) (hzβ : z.im ≤ β) : F z = G z

Uniqueness from boundary values. Two functions continuous and bounded on the closed strip 0 ≤ Im z ≤ β, holomorphic on the open strip, that agree on both boundary lines, agree on the whole closed strip. (Their difference has zero boundary values, so vanishes by eq_zero_on_strip_of_zero_boundary.)