The native node domain of a holomorphic Dirichlet average

For any open scalar domain D, not necessarily convex, the node tuples whose convex hull lies in D form an open set. The regularized average continues jointly to all Dirichlet parameters on this node set. If D is star-convex, this node set is star-convex too, giving a useful uniqueness domain.

This does not extend the average to tuples whose convex hull leaves D. That is the additional content of Carlson (1969), Theorem 8, on simply connected domains; its general existence assertion remains open here.

def DirichletTransform.carlsonIntegralNodeDomain {ι : Type u_1} (D : Set ℂ) : Set (ι → ℂ)

The node tuples on which the scalar domain contains the whole simplex image.

Equations

• DirichletTransform.carlsonIntegralNodeDomain D = {z : ι → ℂ | (convexHull ℝ) (Set.range z) ⊆ D}

theorem DirichletTransform.mem_carlsonIntegralNodeDomain_iff {ι : Type u_1} [Fintype ι] {D : Set ℂ} {z : ι → ℂ} : z ∈ carlsonIntegralNodeDomain D ↔ ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, carlsonAffineForm z u ∈ D

Convex-hull containment can be tested on the simplex coordinates.

theorem DirichletTransform.range_subset_of_mem_carlsonIntegralNodeDomain {ι : Type u_1} {D : Set ℂ} {z : ι → ℂ} (hz : z ∈ carlsonIntegralNodeDomain D) : Set.range z ⊆ D

Each individual node lies in the scalar domain whenever the whole hull does.

theorem DirichletTransform.isOpen_carlsonIntegralNodeDomain {ι : Type u_1} [Finite ι] {D : Set ℂ} (hD : IsOpen D) : IsOpen (carlsonIntegralNodeDomain D)

Compactness of the simplex gives openness without requiring convexity of D.

theorem DirichletTransform.const_mem_carlsonIntegralNodeDomain {ι : Type u_1} [Finite ι] {D : Set ℂ} {c : ℂ} (hc : c ∈ D) : (fun (x : ι) => c) ∈ carlsonIntegralNodeDomain D

Constant node tuples belong whenever their common value belongs.

theorem DirichletTransform.starConvex_carlsonIntegralNodeDomain {ι : Type u_1} [Finite ι] {D : Set ℂ} {c : ℂ} (hD : StarConvex ℝ c D) : StarConvex ℝ (fun (x : ι) => c) (carlsonIntegralNodeDomain D)

Star-convexity passes from the scalar domain to the admissible node tuples.

theorem DirichletTransform.isConnected_carlsonIntegralNodeDomain {ι : Type u_1} [Finite ι] {D : Set ℂ} {c : ℂ} (hD : StarConvex ℝ c D) (hc : c ∈ D) : IsConnected (carlsonIntegralNodeDomain D)

The admissible node domain is connected for a nonempty star-convex scalar domain.

theorem DirichletTransform.exists_joint_isRegCarlsonContinuation_on_integralDomain {ι : Type u_1} [Fintype ι] {D : Set ℂ} (hDo : IsOpen D) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f D) : ∃ (G : (ι → ℂ) × (ι → ℂ) → ℂ), AnalyticOnNhd ℂ G (Set.univ ×ˢ carlsonIntegralNodeDomain D) ∧ ∀ z ∈ carlsonIntegralNodeDomain D, IsRegCarlsonContinuation f z fun (b : ι → ℂ) => G (b, z)

Joint entire-parameter continuation over the native node domain of any open holomorphy domain. Convexity of that scalar domain is not required.

theorem DirichletTransform.isJointRegCarlsonContinuationOn_of_convex_seed {ι : Type u_1} [Fintype ι] {D V : Set ℂ} {c : ℂ} (hDo : IsOpen D) (hDc : StarConvex ℝ c D) (hVo : IsOpen V) (hVc : Convex ℝ V) (hc : c ∈ V) (hVD : V ⊆ D) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f D) {F : (ι → ℂ) × (ι → ℂ) → ℂ} (hF : AnalyticOnNhd ℂ F {p : (ι → ℂ) × (ι → ℂ) | Set.range p.2 ⊆ D}) (hseed : ∀ (z : ι → ℂ), Set.range z ⊆ V → ∀ b ∈ Complex.mvBetaConvergent, F (b, z) = regCarlsonDirichletAverage b z f) : IsJointRegCarlsonContinuationOn D f F

Recognize native agreement throughout a star-convex scalar domain from agreement on a convex open seed containing its star center. Joint holomorphy on the full product domain is a hypothesis, not an existence conclusion.