Documentation

TauCeti.Analysis.Complex.Conformal.Removability.Basic

Painlevé removability across a line #

A line is a removable set for continuous holomorphic functions: if F is continuous on an open set Ω ⊆ ℂ and holomorphic on Ω off a line, then F is holomorphic on all of Ω. This is the straight-line base case toward the L4 analytic-arc removability result in the conformal-mapping roadmap (ConformalMapping/README.md); curved analytic arcs remain outside this module's scope. It is the analytic content that makes the Schwarz reflection principle work, and it is what lets two functions holomorphic on the two open sides of a line be glued along it as soon as the glued function is continuous.

The proof is the classical Morera argument. By Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn, holomorphy on an open set is equivalent to continuity together with the vanishing of every rectangle-boundary integral (Complex.IsConservativeOn). Continuity is a hypothesis; for the rectangle integrals we work with the real axis and split each rectangle there into its part above and its part below. Each half is bounded by the axis, so its open interior misses the axis entirely, where F is holomorphic; Mathlib's continuous-on-closed Cauchy–Goursat lemma Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn then makes each half's boundary integral vanish, and the shared axis edge cancels when the two halves are recombined. An arbitrary line is reduced to the real axis by the affine chart w ↦ p + (q - p) * w, which is a biholomorphism of ℂ carrying ℝ onto the line through p and q.

In accordance with the conformal-mapping roadmap's generality bar, the results are stated for scalar-valued functions F : ℂ → ℂ, even though the Morera argument and its Mathlib inputs also support Banach-valued functions. The roadmap deliberately requires every theorem added in layers L0–L6 to remain scalar; the Banach-valued generalization is therefore outside this module's scope.

Main results #

The Cauchy foundations consumed here are Mathlib's: the rectangle Cauchy–Goursat theorem (Analysis/Complex/CauchyIntegral.lean) and the disc Morera theorem (Analysis/Complex/HasPrimitives.lean). Layer L4 of the roadmap is absent from the upstream Mathlib Riemann-mapping effort leanprover-community/mathlib4#33505, so this is new Lean formalization rather than a shim; any shared foundational API should still be refactored onto Mathlib's once that human-curated work lands.

References #

source
theorem TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_im_ne_zero {Ω : Set ℂ} {F : ℂ → ℂ} (hΩ : IsOpen Ω) (hcont : ContinuousOn F Ω) (hdiff : DifferentiableOn ℂ F (Ω ∩ {z : ℂ | z.im ≠ 0})) :
DifferentiableOn ℂ F Ω

Painlevé removability of the real axis. A function continuous on an open set Ω ⊆ ℂ and holomorphic on the part of Ω off the real axis is holomorphic on all of Ω.

This is the base case of removability across a line: an arbitrary line is reduced to it by an affine change of variable in TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_of_subset_range_lineMap.

source
theorem TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_im_pos_of_differentiableOn_im_neg {Ω : Set ℂ} {F : ℂ → ℂ} (hΩ : IsOpen Ω) (hcont : ContinuousOn F Ω) (hpos : DifferentiableOn ℂ F (Ω ∩ {z : ℂ | 0 < z.im})) (hneg : DifferentiableOn ℂ F (Ω ∩ {z : ℂ | z.im < 0})) :
DifferentiableOn ℂ F Ω

Gluing across the real axis. A function on an open set Ω ⊆ ℂ that is holomorphic on the open upper part and on the open lower part of Ω, and merely continuous on Ω, is holomorphic on all of Ω. This is the form in which removability is used to glue two separately defined holomorphic branches along the axis, as in the Schwarz reflection principle.

source
theorem TauCeti.mem_range_lineMap_iff {p q z : ℂ} :
z ∈ Set.range ⇑(AffineMap.lineMap p q) ↔ ∃ (t : ℝ), z = p + ↑t * (q - p)

Membership in the line through two points, in the "base point plus real multiple of the direction" form used by the affine chart below.

source
theorem TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_of_subset_range_lineMap {Ω : Set ℂ} {F : ℂ → ℂ} {p q : ℂ} {S : Set ℂ} (hS : S ⊆ Set.range ⇑(AffineMap.lineMap p q)) (hΩ : IsOpen Ω) (hcont : ContinuousOn F Ω) (hdiff : DifferentiableOn ℂ F (Ω \ S)) :
DifferentiableOn ℂ F Ω

Painlevé removability across a line. Let S be any subset of the line through points p and q, such as the whole line or a segment. A function continuous on an open set Ω ⊆ ℂ and holomorphic on Ω \ S is holomorphic on all of Ω.

For distinct p and q, the line is straightened to the real axis by the affine chart w ↦ p + (q - p) * w; when p = q, S is a singleton and is contained in any nondegenerate line through p.

source
theorem TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_im_eq {Ω : Set ℂ} {F : ℂ → ℂ} {c : ℝ} (hΩ : IsOpen Ω) (hcont : ContinuousOn F Ω) (hdiff : DifferentiableOn ℂ F (Ω \ {z : ℂ | z.im = c})) :
DifferentiableOn ℂ F Ω

Painlevé removability across a horizontal line. A function continuous on an open set Ω ⊆ ℂ and holomorphic off the horizontal line {z | z.im = c} is holomorphic on all of Ω.

source
theorem TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_re_eq {Ω : Set ℂ} {F : ℂ → ℂ} {c : ℝ} (hΩ : IsOpen Ω) (hcont : ContinuousOn F Ω) (hdiff : DifferentiableOn ℂ F (Ω \ {z : ℂ | z.re = c})) :
DifferentiableOn ℂ F Ω

Painlevé removability across a vertical line. A function continuous on an open set Ω ⊆ ℂ and holomorphic off the vertical line {z | z.re = c} is holomorphic on all of Ω.