Dirichlet continuation on holomorphy domains

The domain-aware continuation predicate makes sense even on a nonconvex domain: native integral agreement is required only when the node convex hull is inside the domain. Values of the scalar function outside its domain are not used to characterize the continuation there.

We prove uniqueness on connected open domains and gluing along increasing open connected domains. Together these isolate the gluing step of the proposed simply connected planar version of Carlson (1969), Theorem 8. Existence of the local contour constructions on nonconvex Jordan domains, and existence of an appropriate Jordan-domain exhaustion, are still required. The theorems here do not assume or assert those missing existence results.

Extensions to multiply connected domains (where branches can acquire poles on collision diagonals) and to Riemann surfaces are left open.

def DirichletTransform.IsJointRegCarlsonContinuationOn {ι : Type u_1} [Fintype ι] (D : Set ℂ) (f : ℂ → ℂ) (G : (ι → ℂ) × (ι → ℂ) → ℂ) : Prop

A joint continuation on a possibly nonconvex holomorphy domain. Native agreement is required only for node tuples whose entire convex hull is in D.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.isOpen_carlsonNodeDomain {ι : Type u_1} [Finite ι] {D : Set ℂ} (hD : IsOpen D) : IsOpen {z : ι → ℂ | Set.range z ⊆ D}

A finite tuple of points in an open scalar domain varies in an open set.

theorem DirichletTransform.IsJointRegCarlsonContinuationOn.isRegCarlsonContinuation {ι : Type u_1} [Fintype ι] {D : Set ℂ} {f : ℂ → ℂ} {G : (ι → ℂ) × (ι → ℂ) → ℂ} (hG : IsJointRegCarlsonContinuationOn D f G) {z : ι → ℂ} (hz : (convexHull ℝ) (Set.range z) ⊆ D) : IsRegCarlsonContinuation f z fun (b : ι → ℂ) => G (b, z)

Native-compatible node tuples recover the previous fixed-node predicate.

theorem DirichletTransform.IsJointRegCarlsonContinuationOn.mono {ι : Type u_1} [Fintype ι] {D V : Set ℂ} {f : ℂ → ℂ} {G : (ι → ℂ) × (ι → ℂ) → ℂ} (hG : IsJointRegCarlsonContinuationOn D f G) (hVD : V ⊆ D) : IsJointRegCarlsonContinuationOn V f G

Restricting the scalar domain preserves a joint continuation.

theorem DirichletTransform.IsJointRegCarlsonContinuationOn.congr_fun {ι : Type u_1} [Fintype ι] {D : Set ℂ} {f g : ℂ → ℂ} {G : (ι → ℂ) × (ι → ℂ) → ℂ} (hG : IsJointRegCarlsonContinuationOn D f G) (hfg : Set.EqOn f g D) : IsJointRegCarlsonContinuationOn D g G

Changing the scalar function outside its holomorphy domain does not change the continuation predicate. In particular, a total Lean function does not impose spurious native-integral conditions outside D.

theorem DirichletTransform.IsJointRegCarlsonContinuationOn.eqOn {ι : Type u_1} [Fintype ι] {D : Set ℂ} (hDo : IsOpen D) (hDc : IsConnected D) {f : ℂ → ℂ} {G H : (ι → ℂ) × (ι → ℂ) → ℂ} (hG : IsJointRegCarlsonContinuationOn D f G) (hH : IsJointRegCarlsonContinuationOn D f H) : Set.EqOn G H {p : (ι → ℂ) × (ι → ℂ) | Set.range p.2 ⊆ D}

Uniqueness on a connected open scalar domain. Agreement is first obtained on a full neighborhood of a diagonal tuple, not just on the diagonal itself.

theorem DirichletTransform.exists_isJointRegCarlsonContinuationOn_of_convex {ι : Type u_1} [Fintype ι] {D : Set ℂ} (hDo : IsOpen D) (hDc : Convex ℝ D) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f D) : ∃ (G : (ι → ℂ) × (ι → ℂ) → ℂ), IsJointRegCarlsonContinuationOn D f G

The established convex-domain theorem supplies the domain-aware predicate.

theorem DirichletTransform.exists_isJointRegCarlsonContinuationOn_iUnion {ι : Type u_1} [Fintype ι] (U : ℕ → Set ℂ) (hUo : ∀ (n : ℕ), IsOpen (U n)) (hUc : ∀ (n : ℕ), IsConnected (U n)) (hUm : Monotone U) {f : ℂ → ℂ} (hF : ∀ (n : ℕ), ∃ (F : (ι → ℂ) × (ι → ℂ) → ℂ), IsJointRegCarlsonContinuationOn (U n) f F) : ∃ (G : (ι → ℂ) × (ι → ℂ) → ℂ), IsJointRegCarlsonContinuationOn (⋃ (n : ℕ), U n) f G

Local joint continuations on increasing connected open scalar domains glue to a joint continuation on their union. Compactness handles both the node set and, for native agreement, its entire convex hull. No nonempty-index assumption is needed. This theorem does not construct the local continuations or the cover.