Continued Cauchy representations of Dirichlet averages

The circle version of Carlson (1969), §5, Theorem 3, for every derivative order and all complex Dirichlet parameters. This extends the native-parameter circle formula in Dirichlet.Average.Cauchy. The continued contour expression is jointly holomorphic in parameters and interior nodes, even when the boundary function is only continuous. For a function holomorphic in the disk it is the unique regularized continuation of the corresponding derivative average.

General Jordan contours and their contour-adapted resolvent branches remain necessary for Carlson's Theorems 5 and 8 on nonconvex simply connected domains. The multiply connected and Riemann-surface extensions are left open.

theorem DirichletTransform.mem_carlsonResolventDomain_of_mem_sphere {ι : Type u_1} [Fintype ι] {c s : ℂ} {R : ℝ} {z : ι → ℂ} (hz : Set.range z ⊆ Metric.ball c R) (hs : s ∈ Metric.sphere c R) : (s, z) ∈ carlsonResolventDomain

A circle surrounding all nodes avoids all their simplex affine combinations.

noncomputable def DirichletTransform.continuedRegCarlsonCauchyRepresentation {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) (c : ℂ) (R : ℝ) (f : ℂ → ℂ) : ℂ

The continued circle-Cauchy expression for the average of the nth derivative.

Equations

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

theorem DirichletTransform.analyticOnNhd_continuedRegCarlsonCauchyRepresentation {ι : Type u_1} [Fintype ι] (n : ℕ) {c : ℂ} {R : ℝ} (hR : 0 ≤ R) {f : ℂ → ℂ} (hf : ContinuousOn f (Metric.sphere c R)) : AnalyticOnNhd ℂ (fun (p : (ι → ℂ) × (ι → ℂ)) => continuedRegCarlsonCauchyRepresentation n p.1 p.2 c R f) {p : (ι → ℂ) × (ι → ℂ) | Set.range p.2 ⊆ Metric.ball c R}

The continued contour expression is jointly holomorphic in all complex Dirichlet parameters and interior nodes. Boundary continuity of f suffices.

theorem DirichletTransform.continuedRegCarlsonCauchyRepresentation_eq_native {ι : Type u_1} [Fintype ι] (n : ℕ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) {c : ℂ} {R : ℝ} (hR : 0 < R) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hz : Set.range z ⊆ Metric.ball c R) : continuedRegCarlsonCauchyRepresentation n b z c R f = regCarlsonDirichletAverage b z (iteratedDeriv n f)

The circle expression recovers the native average on its convergence region.

theorem DirichletTransform.isRegCarlsonContinuation_continuedRegCarlsonCauchyRepresentation {ι : Type u_1} [Fintype ι] (n : ℕ) {z : ι → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hz : Set.range z ⊆ Metric.ball c R) : IsRegCarlsonContinuation (iteratedDeriv n f) z fun (b : ι → ℂ) => continuedRegCarlsonCauchyRepresentation n b z c R f

Carlson's circle-Cauchy expression is an entire regularized continuation, for every derivative order; no boundary derivatives are required.

theorem DirichletTransform.isJointRegCarlsonContinuationOn_circle {ι : Type u_1} [Fintype ι] (n : ℕ) {c : ℂ} {R : ℝ} (hR : 0 < R) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) : IsJointRegCarlsonContinuationOn (Metric.ball c R) (iteratedDeriv n f) fun (p : (ι → ℂ) × (ι → ℂ)) => continuedRegCarlsonCauchyRepresentation n p.1 p.2 c R f

The circle construction supplies a domain-aware joint continuation on its interior disk, ready for comparison and gluing with other local constructions.

theorem DirichletTransform.IsRegCarlsonContinuation.eq_circleIntegral {ι : Type u_1} [Fintype ι] {n : ℕ} {f : ℂ → ℂ} {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation (iteratedDeriv n f) z G) {c : ℂ} {R : ℝ} (hR : 0 < R) (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hz : Set.range z ⊆ Metric.ball c R) (b : ι → ℂ) : G b = ↑n.factorial * (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (s : ℂ) in C(c, R), continuedRegCarlsonResolvent n b z s * f s

Any established entire continuation has the circle-Cauchy representation at every complex Dirichlet parameter, including poles of the unregularized average.

theorem DirichletTransform.continuedRegCarlsonCauchyRepresentation_eq_of_disks {ι : Type u_1} [Fintype ι] (n : ℕ) {f : ℂ → ℂ} {z : ι → ℂ} {c d : ℂ} {R S : ℝ} (hR : 0 < R) (hS : 0 < S) (hfR : DiffContOnCl ℂ f (Metric.ball c R)) (hfS : DiffContOnCl ℂ f (Metric.ball d S)) (hzR : Set.range z ⊆ Metric.ball c R) (hzS : Set.range z ⊆ Metric.ball d S) (b : ι → ℂ) : continuedRegCarlsonCauchyRepresentation n b z c R f = continuedRegCarlsonCauchyRepresentation n b z d S f

Independence of the enclosing circle for all complex parameters. Both circles must bound disks on which the same scalar function is holomorphic.