Removable singularities along a coordinate hyperplane

Let V be a finite-dimensional complex normed space, U ⊆ V and s ⊆ ℂ open sets, and c a point of ℂ. This file proves the Riemann extension theorem across the coordinate hyperplane V × {c}: a function f analytic on U × (s \ {c}) whose slices z ↦ f (w, z) are bounded near c extends to a function analytic on all of U × s, and the extension is unique.

Only the slices of f are assumed bounded, not f itself near U × {c}. Each slice extends across c by the one-variable removable singularity theorem (Complex.differentiableOn_update_limUnder_of_bddAbove), and the slice extensions together form the extension of f. They do not give its joint analyticity: near a point (w₀, c) the extension is written as the Cauchy integral (w, z) ↦ (2πi)⁻¹ ∮ ζ in C(c, ρ), (ζ - z)⁻¹ • f (w, ζ) over a circle on which f is jointly analytic, and this integral depends analytically on the parameter (w, z) by TauCeti.analyticAt_circleIntegral.

This extension theorem is the step of Puiseux-type arguments with parameters in which the roots of a polynomial with analytic coefficients, known to be analytic off a hyperplane and bounded near it, are shown to be analytic across it.

Main results

• TauCeti.exists_analyticOnNhd_prod_eqOn: the Riemann extension theorem across a coordinate hyperplane.
• TauCeti.eqOn_prod_of_eqOn_prod_diff_singleton: uniqueness of the extension, for continuous functions.

References

• R. C. Gunning, H. Rossi, Analytic Functions of Several Complex Variables, Chapter I (the Riemann extension theorem).
• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, J. Symbolic Comput. 92 (2019), §4, for its use in Puiseux-type arguments with parameters.

theorem TauCeti.eqOn_prod_of_eqOn_prod_diff_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {g₁ g₂ : X × ℂ → Y} {U : Set X} {s : Set ℂ} {c : ℂ} (hs : IsOpen s) (h₁ : ContinuousOn g₁ (U ×ˢ s)) (h₂ : ContinuousOn g₂ (U ×ˢ s)) (h : Set.EqOn g₁ g₂ (U ×ˢ (s \ {c}))) : Set.EqOn g₁ g₂ (U ×ˢ s)

Uniqueness of extensions across a coordinate hyperplane. Two functions continuous on U × s, for s ⊆ ℂ open, which agree off the hyperplane z = c agree on all of U × s.

theorem TauCeti.exists_analyticOnNhd_prod_eqOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V × ℂ → E} {U : Set V} {s : Set ℂ} {c : ℂ} [FiniteDimensional ℂ V] (hU : IsOpen U) (hs : IsOpen s) (hf : AnalyticOnNhd ℂ f (U ×ˢ (s \ {c}))) (hb : c ∈ s → ∀ w ∈ U, ∃ t ∈ nhds c, BddAbove ((norm ∘ fun (z : ℂ) => f (w, z)) '' (t \ {c}))) : ∃ (g : V × ℂ → E), AnalyticOnNhd ℂ g (U ×ˢ s) ∧ Set.EqOn g f (U ×ˢ (s \ {c}))

The Riemann extension theorem across a coordinate hyperplane. Let U ⊆ V and s ⊆ ℂ be open. If f is analytic on U × (s \ {c}) and, when c ∈ s, each slice z ↦ f (w, z), for w ∈ U, is bounded on a punctured neighbourhood of c, then some g analytic on U × s agrees with f on U × (s \ {c}). Such a g is unique on U × s by eqOn_prod_of_eqOn_prod_diff_singleton.