Entire-parameter continuation of the Cauchy resolvent

This is the convex-hull-complement part of Carlson (1969), §5, Lemma 1. The regularized integer resolvent is jointly holomorphic in the Dirichlet parameters, the nodes, and the exterior evaluation point. All complex Dirichlet parameters are allowed, without Gamma-pole exclusions. The proof uses the parametric simplex integration-by-parts construction rather than a logarithmic branch.

This is not yet the contour-adapted branch on a nonconvex Jordan domain in Carlson's Theorems 4–5. That construction and the simply connected extension of Theorem 8 remain further work. Extensions to multiply connected domains and to Riemann surfaces are deliberately left open.

def DirichletTransform.carlsonResolventDomain {ι : Type u_1} [Fintype ι] : Set (ℂ × (ι → ℂ))

Evaluation points which avoid every affine combination of the nodes on the real simplex. This form of the domain makes its openness follow from compactness.

Equations

• DirichletTransform.carlsonResolventDomain = {p : ℂ × (ι → ℂ) | ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, p.1 - DirichletTransform.carlsonAffineForm p.2 u ≠ 0}

theorem DirichletTransform.isOpen_carlsonResolventDomain {ι : Type u_1} [Fintype ι] : IsOpen carlsonResolventDomain

The resolvent domain is open jointly in its evaluation point and nodes.

theorem DirichletTransform.mem_carlsonResolventDomain_of_not_mem_convexHull {ι : Type u_1} [Fintype ι] {s : ℂ} {z : ι → ℂ} (hs : s ∉ (convexHull ℝ) (Set.range z)) : (s, z) ∈ carlsonResolventDomain

In particular, every point outside the convex hull is in the resolvent domain.

def DirichletTransform.resolventCoordinates {ι : Type u_1} (q : Option ι → ℂ) : ℂ × (ι → ℂ)

Separate the evaluation coordinate from the node coordinates.

Equations

• DirichletTransform.resolventCoordinates q = (q none, fun (i : ι) => q (some i))

theorem DirichletTransform.exists_joint_regCarlsonResolvent {ι : Type u_1} [Fintype ι] (n : ℕ) : ∃ (H : (ι → ℂ) × (Option ι → ℂ) → ℂ), AnalyticOnNhd ℂ H (Set.univ ×ˢ (resolventCoordinates ⁻¹' carlsonResolventDomain)) ∧ ∀ (q : Option ι → ℂ), resolventCoordinates q ∈ carlsonResolventDomain → Set.EqOn (fun (b : ι → ℂ) => H (b, q)) (fun (b : ι → ℂ) => regCarlsonResolvent n b (fun (i : ι) => q (some i)) (q none)) Complex.mvBetaConvergent

Coordinate form of the joint entire-parameter resolvent construction.

noncomputable def DirichletTransform.continuedRegCarlsonResolvent {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) (s : ℂ) : ℂ

The entire-parameter regularized integer resolvent. Values outside carlsonResolventDomain are unspecified; theorems only use it on that domain.

Equations

• DirichletTransform.continuedRegCarlsonResolvent n b z s = ⋯.choose (b, fun (i : Option ι) => i.elim s z)

theorem DirichletTransform.analyticOnNhd_continuedRegCarlsonResolvent {ι : Type u_1} [Fintype ι] (n : ℕ) : AnalyticOnNhd ℂ (fun (p : (ι → ℂ) × ℂ × (ι → ℂ)) => continuedRegCarlsonResolvent n p.1 p.2.2 p.2.1) (Set.univ ×ˢ carlsonResolventDomain)

Joint analyticity in all parameters, evaluation point, and nodes.

theorem DirichletTransform.continuedRegCarlsonResolvent_eq_native {ι : Type u_1} [Fintype ι] (n : ℕ) {b z : ι → ℂ} {s : ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hs : (s, z) ∈ carlsonResolventDomain) : continuedRegCarlsonResolvent n b z s = regCarlsonResolvent n b z s

The continued kernel agrees with the native resolvent on the convergence region.

theorem DirichletTransform.isRegCarlsonContinuation_continuedRegCarlsonResolvent {ι : Type u_1} [Fintype ι] (n : ℕ) {z : ι → ℂ} {s : ℂ} (hs : (s, z) ∈ carlsonResolventDomain) : IsRegCarlsonContinuation (fun (w : ℂ) => (s - w) ^ (-(↑n + 1))) z fun (b : ι → ℂ) => continuedRegCarlsonResolvent n b z s

At a fixed exterior point the resolvent is the unique entire continuation of the corresponding native Carlson average.