Thullen's lemma and the boundary distance of holomorphic hulls

Cauchy bounds on compact families of smaller balls control Taylor coefficients weighted by powers of a scalar holomorphic radius. These bounds transfer to the holomorphic hull, for Banach-valued functions by norming functionals, and give Taylor continuation on the indicated polydisc. Agreement is asserted near the center, not on unrelated components of the overlap. This proves radius preservation, exact hull boundary distance, and holomorphic convexity for domains of holomorphy.

References: [Scheidemann][Scheidemann2005] §6.2 and §7.3; [Hörmander][Hormander1973] §2.5; [Korevaar–Wiegerinck][KorevaarWiegerinck2017] §6.4.

Main results

taylor_continuation_on_holomorphicHull is Thullen's Taylor continuation lemma for Banach-valued functions. IsDomainOfHolomorphy.holomorphic_radius_bound is the weighted radius bound. IsDomainOfHolomorphy.hasHolomorphicHullRadiusProperty and hasHolomorphicHullDistanceProperty are the hull-radius and boundary-distance forms. IsDomainOfHolomorphy.isHolomorphicallyConvex is the forward Cartan–Thullen implication.

References

• [L. Hörmander, An Introduction to Complex Analysis in Several Variables][Hormander1973]
• [J. Korevaar and J. Wiegerinck, Several Complex Variables][KorevaarWiegerinck2017]
• [V. Scheidemann, Introduction to Complex Analysis in Several Variables][Scheidemann2005]

theorem SeveralComplexVariables.norm_multiIndexDeriv_le_on_holomorphicHull {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U K : Set (Fin n → ℂ)} (ho : IsOpen U) {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) (m : Fin n → ℕ) {M : ℝ} (hM : ∀ z ∈ K, ‖multiIndexDeriv m f z‖ ≤ M) (z : Fin n → ℂ) : z ∈ holomorphicHull U K → ‖multiIndexDeriv m f z‖ ≤ M

Mixed derivative bounds transfer to the holomorphic hull of the set on which they hold, for Banach-valued functions. This elementary step is independent of the Taylor continuation theorem.

noncomputable def SeveralComplexVariables.taylorSumAt {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : (Fin n → ℂ) → F) (a z : Fin n → ℂ) : F

The Taylor sum of a Banach-valued function centered at an arbitrary point, using the normalized multivariate Taylor coefficients.

Equations

• SeveralComplexVariables.taylorSumAt f a z = SeveralComplexVariables.powerSeriesSum (SeveralComplexVariables.holomorphicTaylorSeries f a) (z - a)

theorem SeveralComplexVariables.analyticAt_update_of_analyticOnNhd_closedPolydisc {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : (Fin n → ℂ) → F} {a : Fin n → ℂ} {r : ℝ} (hA : AnalyticOnNhd ℂ f (closedPolydisc a fun (x : Fin n) => r)) (z : Fin n → ℂ) : (z ∈ closedPolydisc a fun (x : Fin n) => r) → ∀ (i : Fin n), AnalyticAt ℂ (fun (v : ℂ) => f (Function.update z i v)) (z i)

Separate analyticity on a closed polydisc from joint analyticity.

theorem SeveralComplexVariables.norm_taylorCoeff_le {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (Fin n → ℂ)} {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) {a : Fin n → ℂ} {r M : ℝ} (hr : 0 < r) (hball : Metric.closedBall a r ⊆ U) (hM : ∀ z ∈ Metric.closedBall a r, ‖f z‖ ≤ M) (m : Fin n →₀ ℕ) : ‖holomorphicTaylorSeries f a m‖ ≤ M * ∏ i : Fin n, r⁻¹ ^ m i

A bound on a closed coordinate ball bounds each normalized Taylor coefficient.

theorem SeveralComplexVariables.taylorSumAt_eventuallyEq {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {f : (Fin n → ℂ) → F} {a : Fin n → ℂ} (hf : AnalyticAt ℂ f a) : taylorSumAt f a =ᶠ[nhds a] f

The normalized Taylor sum of an analytic germ agrees with its representative nearby.

theorem SeveralComplexVariables.taylor_continuation_on_holomorphicHull {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U K : Set (Fin n → ℂ)} (ho : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) {q : (Fin n → ℂ) → ℂ} {f : (Fin n → ℂ) → F} (hq : AnalyticOnNhd ℂ q U) (hf : AnalyticOnNhd ℂ f U) (hr : ∀ w ∈ K, Metric.ball w ‖q w‖ ⊆ U) {a : Fin n → ℂ} (ha : a ∈ holomorphicHull U K) : AnalyticOnNhd ℂ (taylorSumAt f a) (Metric.ball a ‖q a‖) ∧ taylorSumAt f a =ᶠ[nhds a] f ∧ HasSumLocallyUniformlyOn (fun (m : Fin n →₀ ℕ) (z : Fin n → ℂ) => (∏ i : Fin n, (z i - a i) ^ m i) • holomorphicTaylorSeries f a m) (taylorSumAt f a) (Metric.ball a ‖q a‖)

Thullen's lemma, with a holomorphic radius bound. For a Banach-valued function, the Taylor series centered at a hull point converges locally uniformly on the indicated polydisc and continues the original germ. The proof transfers uniform weighted Cauchy bounds from compact families of smaller balls to the hull, then compares with a product of geometric series.

theorem SeveralComplexVariables.exists_continuation_ball_of_mem_holomorphicHull {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U K : Set (Fin n → ℂ)} (ho : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) {r : ℝ} (hr : 0 < r) (hball : ∀ w ∈ K, Metric.ball w r ⊆ U) {a : Fin n → ℂ} (ha : a ∈ holomorphicHull U K) {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) : ∃ (g : (Fin n → ℂ) → F), AnalyticOnNhd ℂ g (Metric.ball a r) ∧ g =ᶠ[nhds a] f

The constant-radius form of Thullen's continuation lemma, for Banach-valued functions.

theorem SeveralComplexVariables.IsDomainOfHolomorphy.ball_subset_of_continuation {n : ℕ} {U : Set (Fin n → ℂ)} (hU : IsDomainOfHolomorphy U) (ho : IsOpen U) {a : Fin n → ℂ} (ha : a ∈ U) {r : ℝ} (hr : 0 < r) (he : ∀ (f : (Fin n → ℂ) → ℂ), AnalyticOnNhd ℂ f U → ∃ (g : (Fin n → ℂ) → ℂ), AnalyticOnNhd ℂ g (Metric.ball a r) ∧ g =ᶠ[nhds a] f) : Metric.ball a r ⊆ U

On a domain of holomorphy, a ball supporting continuation of every germ at its center must lie in the domain. The overlap is chosen uniformly, independently of the function.

theorem SeveralComplexVariables.IsDomainOfHolomorphy.holomorphic_radius_bound {n : ℕ} {U K : Set (Fin n → ℂ)} (hU : IsDomainOfHolomorphy U) (ho : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) {q : (Fin n → ℂ) → ℂ} (hq : AnalyticOnNhd ℂ q U) (hr : ∀ w ∈ K, Metric.ball w ‖q w‖ ⊆ U) (a : Fin n → ℂ) : a ∈ holomorphicHull U K → Metric.ball a ‖q a‖ ⊆ U

A domain of holomorphy preserves every radius bound supplied by a holomorphic function on a compact set, by Thullen's continuation lemma.

theorem SeveralComplexVariables.IsDomainOfHolomorphy.hasHolomorphicHullRadiusProperty {n : ℕ} {U : Set (Fin n → ℂ)} (hU : IsDomainOfHolomorphy U) (ho : IsOpen U) : HasHolomorphicHullRadiusProperty U

Domains of holomorphy preserve uniform polydisc radii on compact hulls.

theorem SeveralComplexVariables.IsDomainOfHolomorphy.hasHolomorphicHullDistanceProperty {n : ℕ} {U : Set (Fin n → ℂ)} (hU : IsDomainOfHolomorphy U) (ho : IsOpen U) : HasHolomorphicHullDistanceProperty U

The boundary distance of a compact holomorphic hull equals that of the original compact set in a domain of holomorphy.

theorem SeveralComplexVariables.IsDomainOfHolomorphy.isHolomorphicallyConvex {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} (hU : IsDomainOfHolomorphy U) (ho : IsOpen U) : IsHolomorphicallyConvex U

Cartan–Thullen, forward implication. An open domain of holomorphy in any finite-dimensional complex normed space is holomorphically convex. Linear transport of hull compactness is used here; no invariance of numerical boundary distance is asserted.