Joint continuation of general Carlson averages

The continuation assertion of Carlson's Theorem 6.3-6 (1977, p. 138): if f is holomorphic on a convex open set Ω, its Gamma-regularized Dirichlet average is jointly holomorphic in all Dirichlet parameters and all nodes in Ω. The same holds for averages of every derivative of f. No common disk containing the nodes is required.

The proof uses parametric tangential integration by parts, not Carlson's contour construction. The general rectifiable Jordan-curve representation in that theorem is a separate remaining assertion; this file does not prove that representation.

theorem DirichletTransform.exists_joint_isRegCarlsonContinuation {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) : ∃ (G : (ι → ℂ) × (ι → ℂ) → ℂ), AnalyticOnNhd ℂ G {p : (ι → ℂ) × (ι → ℂ) | Set.range p.2 ⊆ Ω} ∧ ∀ (z : ι → ℂ), Set.range z ⊆ Ω → IsRegCarlsonContinuation f z fun (b : ι → ℂ) => G (b, z)

Carlson 6.3-6, continuation assertion for n = 0. A regularized Dirichlet average has a continuation jointly holomorphic on ℂ^ι × Ω^ι, where Ω is any convex open set on which the averaged scalar function is holomorphic.

theorem DirichletTransform.analyticOnNhd_joint_of_isRegCarlsonContinuation {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {G : (ι → ℂ) × (ι → ℂ) → ℂ} (hG : ∀ (z : ι → ℂ), Set.range z ⊆ Ω → IsRegCarlsonContinuation f z fun (b : ι → ℂ) => G (b, z)) : AnalyticOnNhd ℂ G {p : (ι → ℂ) × (ι → ℂ) | Set.range p.2 ⊆ Ω}

Any family already characterized by the native integral and entire parameter dependence inherits joint holomorphy. No change of its definition is necessary.

theorem DirichletTransform.exists_joint_isRegCarlsonContinuation_iteratedDeriv {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) (n : ℕ) : ∃ (G : (ι → ℂ) × (ι → ℂ) → ℂ), AnalyticOnNhd ℂ G {p : (ι → ℂ) × (ι → ℂ) | Set.range p.2 ⊆ Ω} ∧ ∀ (z : ι → ℂ), Set.range z ⊆ Ω → IsRegCarlsonContinuation (iteratedDeriv n f) z fun (b : ι → ℂ) => G (b, z)

Carlson 6.3-6, continuation assertion for every derivative order. This is the joint holomorphic extension of F⁽ⁿ⁾(b,z) / Γ(∑ bᵢ) to all complex Dirichlet parameters.