Towards horizontal-line removability (Morera-based)

This file proves the horizontal-line removable singularity theorem: a function continuous on an open set U and holomorphic on U minus a horizontal line is holomorphic on all of U (differentiableOn_of_continuousOn_off_horizontal_line). That theorem is the missing prerequisite for the strip Schwarz reflection used in the KMS invariance proof (StripLiouville).

Foundation (rectangle contour integrals)

• Physicslib4.rectIntegralReal: the contour integral of f over the boundary of the axis-parallel rectangle [a,b] × [c,d] (Cauchy-Goursat normal form, matching Complex.integral_boundary_rect_eq_zero_*), parameterized by real bounds.
• Physicslib4.rectIntegralReal_horizontal_split: additivity across a horizontal split - the rectangle integral over [a,b] × [c,d] is the sum of those over [a,b] × [c,ℓ] and [a,b] × [ℓ,d]. The shared horizontal edge at im = ℓ cancels; the vertical edges combine via interval-integral additivity.
• Physicslib4.rectIntegralReal_eq_zero_of_continuousOn_of_differentiableOn: the Cauchy-Goursat theorem in rectIntegralReal form.
• Physicslib4.rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line: straddling-rectangle vanishing - if f is continuous on the closed rectangle and holomorphic off the line im = ℓ (with c ≤ ℓ ≤ d), then rectIntegralReal = 0, by splitting at ℓ (_horizontal_split) and applying Cauchy-Goursat to each sub-rectangle (continuous on closure, holomorphic on interior, which avoids the line).

Morera glue and removability

• Physicslib4.wedgeIntegral_add_wedgeIntegral_eq_rectIntegralReal: the bridge to Mathlib's Morera API - the sum of the two opposite wedge integrals (Complex.wedgeIntegral) equals our rectIntegralReal.
• Physicslib4.rectIntegralReal_eq_zero_of_subset: every closed rectangle in U has vanishing boundary integral (any corner ordering, any line position), reducing to ordered bounds via rectIntegralReal_swap_re/_swap_im.
• Physicslib4.differentiableOn_of_continuousOn_off_horizontal_line: the removable-singularity theorem, via Morera (Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn).

Holomorphic gluing across a horizontal line

• Half-plane topology helpers isOpen_setOf_im_lt, closure_setOf_im_lt, closure_setOf_not_im_lt, frontier_setOf_im_lt.
• Physicslib4.differentiableOn_if_of_eqOn_horizontal_line: the general Schwarz-reflection gluing lemma - two functions holomorphic on the open half-planes below/above a horizontal line, continuous up to it, and agreeing on it, glue to a function holomorphic across it. This is the reusable, spacetime- and strip-agnostic mechanism specialized by the iβ-periodic strip reflection (Physicslib4.pext_differentiableAt_online) that discharges StripLiouville (and hence KMS invariance) via Physicslib4.AQFT.stripLiouville_of_entire_extension.

noncomputable def Physicslib4.rectIntegralReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (a b c d : ℝ) : E

The contour integral of f over the boundary of the axis-parallel rectangle [a, b] × [c, d] (with real bounds), in the Cauchy-Goursat normal form: bottom edge minus top edge, plus I · (right edge minus left edge).

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.rectIntegralReal_horizontal_split {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (a b c d ℓ : ℝ) (hrL : IntervalIntegrable (fun (y : ℝ) => f (↑b + ↑y * Complex.I)) MeasureTheory.volume c ℓ) (hrU : IntervalIntegrable (fun (y : ℝ) => f (↑b + ↑y * Complex.I)) MeasureTheory.volume ℓ d) (hlL : IntervalIntegrable (fun (y : ℝ) => f (↑a + ↑y * Complex.I)) MeasureTheory.volume c ℓ) (hlU : IntervalIntegrable (fun (y : ℝ) => f (↑a + ↑y * Complex.I)) MeasureTheory.volume ℓ d) : rectIntegralReal f a b c d = rectIntegralReal f a b c ℓ + rectIntegralReal f a b ℓ d

Additivity of the rectangle contour integral across a horizontal split. Splitting [a,b] × [c,d] along the horizontal line im = ℓ into a lower rectangle [a,b] × [c,ℓ] and an upper rectangle [a,b] × [ℓ,d], the boundary integrals add: the contributions of the shared edge im = ℓ cancel (it is traversed in opposite directions), and the left/right edges combine by interval-integral additivity. The hypotheses are interval-integrability of the two vertical-edge integrands on each piece.

theorem Physicslib4.rectIntegralReal_eq_zero_of_continuousOn_of_differentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (a b c d : ℝ) (Hc : ContinuousOn f (Set.uIcc a b ×ℂ Set.uIcc c d)) (Hd : DifferentiableOn ℂ f (Set.Ioo (min a b) (max a b) ×ℂ Set.Ioo (min c d) (max c d))) : rectIntegralReal f a b c d = 0

Cauchy-Goursat theorem in rectIntegralReal form. If f is continuous on the closed rectangle [a,b] × [c,d] and holomorphic on its interior, the boundary contour integral vanishes.

theorem Physicslib4.rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (a b c d ℓ : ℝ) (hab : a ≤ b) (hcℓ : c ≤ ℓ) (hℓd : ℓ ≤ d) (Hc : ContinuousOn f (Set.uIcc a b ×ℂ Set.uIcc c d)) (Hd : DifferentiableOn ℂ f (Set.Icc a b ×ℂ Set.Icc c d \ {z : ℂ | z.im = ℓ})) : rectIntegralReal f a b c d = 0

Straddling-rectangle vanishing. If f is continuous on the closed rectangle [a,b] × [c,d] and holomorphic everywhere on it except possibly on the horizontal line im = ℓ (with c ≤ ℓ ≤ d), then its boundary contour integral still vanishes. The proof splits the rectangle at ℓ into a lower and an upper piece (rectIntegralReal_horizontal_split); each piece is continuous on its closure and holomorphic on its interior (whose imaginary parts are strictly on one side of ℓ, hence avoid the line), so Cauchy-Goursat applies to each.

theorem Physicslib4.rectIntegralReal_swap_re {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (a b c d : ℝ) : rectIntegralReal f b a c d = -rectIntegralReal f a b c d

Swapping the real bounds negates the rectangle contour integral.

theorem Physicslib4.rectIntegralReal_swap_im {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (a b c d : ℝ) : rectIntegralReal f a b d c = -rectIntegralReal f a b c d

Swapping the imaginary bounds negates the rectangle contour integral.

theorem Physicslib4.wedgeIntegral_add_wedgeIntegral_eq_rectIntegralReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) : z.wedgeIntegral w f + w.wedgeIntegral z f = rectIntegralReal f z.re w.re z.im w.im

The sum of the two opposite wedge integrals equals the rectangle contour integral. This is the bridge between Mathlib's Complex.IsConservativeOn (phrased via wedgeIntegral) and our rectIntegralReal: the two wedges trace the four edges of the rectangle, with the shared diagonal-free edges combining into the full boundary.

theorem Physicslib4.rectIntegralReal_eq_zero_of_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} (ℓ : ℝ) (f : ℂ → E) (hc : ContinuousOn f U) (hd : DifferentiableOn ℂ f (U \ {z : ℂ | z.im = ℓ})) (a b c d : ℝ) (hsub : Set.uIcc a b ×ℂ Set.uIcc c d ⊆ U) : rectIntegralReal f a b c d = 0

Rectangle integrals vanish on a set, off a horizontal line. If f is continuous on a set U and holomorphic on U minus the horizontal line im = ℓ, then the boundary integral of f over any closed rectangle contained in U vanishes - regardless of corner ordering and of where the line sits relative to the rectangle. The proof reduces to ordered bounds via the swap lemmas, then splits into three positions of ℓ: inside [c,d] (straddling vanishing) or outside on either side (plain Cauchy-Goursat, the interior avoiding the line).

theorem Physicslib4.differentiableOn_of_continuousOn_off_horizontal_line {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} (hU : IsOpen U) (ℓ : ℝ) (f : ℂ → E) (hc : ContinuousOn f U) (hd : DifferentiableOn ℂ f (U \ {z : ℂ | z.im = ℓ})) : DifferentiableOn ℂ f U

Horizontal-line removable singularity (Morera). If f is continuous on an open set U and holomorphic on U minus the horizontal line im = ℓ, then f is holomorphic on all of U. The line is removed: continuity across it plus holomorphy on either side forces differentiability on it.

The proof is Morera's theorem in the form Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn: it suffices that f is conservative on U, i.e. every rectangle boundary integral vanishes, which is rectIntegralReal_eq_zero_of_subset.

Half-plane topology and holomorphic gluing across a horizontal line

theorem Physicslib4.isOpen_setOf_im_lt (c : ℝ) : IsOpen {z : ℂ | z.im < c}

The open lower half-plane {Im z < c} is open.

theorem Physicslib4.closure_setOf_im_lt (c : ℝ) : closure {z : ℂ | z.im < c} = {z : ℂ | z.im ≤ c}

Closure of the open lower half-plane {Im z < c} is {Im z ≤ c}.

theorem Physicslib4.closure_setOf_not_im_lt (c : ℝ) : closure {z : ℂ | ¬z.im < c} = {z : ℂ | c ≤ z.im}

Closure of {¬ (Im z < c)} is {c ≤ Im z}.

theorem Physicslib4.frontier_setOf_im_lt (c : ℝ) : frontier {z : ℂ | z.im < c} = {z : ℂ | z.im = c}

Frontier of {Im z < c} is the line {Im z = c}.

theorem Physicslib4.differentiableOn_if_of_eqOn_horizontal_line {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} (hU : IsOpen U) (ℓ : ℝ) {g h : ℂ → E} (hgc : ContinuousOn g (U ∩ {z : ℂ | z.im ≤ ℓ})) (hhc : ContinuousOn h (U ∩ {z : ℂ | ℓ ≤ z.im})) (hgd : DifferentiableOn ℂ g (U ∩ {z : ℂ | z.im < ℓ})) (hhd : DifferentiableOn ℂ h (U ∩ {z : ℂ | ℓ < z.im})) (hglue : ∀ z ∈ U, z.im = ℓ → g z = h z) : DifferentiableOn ℂ (fun (z : ℂ) => if z.im < ℓ then g z else h z) U

Holomorphic gluing across a horizontal line (Schwarz-reflection form). Suppose g is continuous on the closed lower part U ∩ {Im ≤ ℓ} and holomorphic on the open lower part U ∩ {Im < ℓ}; h is continuous on the closed upper part U ∩ {ℓ ≤ Im} and holomorphic on the open upper part U ∩ {ℓ < Im}; and the two agree on the line Im = ℓ inside U. Then the piecewise function z ↦ if Im z < ℓ then g z else h z is holomorphic on the open set U.

The pieces glue to a function continuous on U (ContinuousOn.if, using that the closures of the two open half-planes are the closed half-planes and their common frontier is the line), holomorphic off the line, hence holomorphic across it by differentiableOn_of_continuousOn_off_horizontal_line. This is the reusable mechanism underlying the strip Schwarz reflection.