Carlson's continued Taylor representation

The R-polynomial expansion gives the entire regularized continuation in the Dirichlet parameters on the full scalar Taylor disk (Carlson, Theorem 6.3-1). The sharp estimate from Section 6.2 supplies locally uniform convergence.

theorem DirichletTransform.isRegCarlsonContinuation_taylor_of_geometric_bound {ι : Type u_1} [Fintype ι] (A : ℂ) (a : ℕ → ℂ) (z : ι → ℂ) (f : ℂ → ℂ) {C q : ℝ} (hC : 0 ≤ C) (hq : 0 ≤ q) (hqr : q * ‖fun (i : ι) => z i - A‖ < 1) (ha : ∀ (n : ℕ), ‖a n‖ ≤ C * q ^ n) (hsum : ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, HasSum (fun (n : ℕ) => a n * (carlsonAffineForm z u - A) ^ n) (f (carlsonAffineForm z u))) : IsRegCarlsonContinuation f z (regCarlsonTaylorSeries A a z)

A geometric coefficient bound yields a continued Taylor average. This internal criterion is discharged automatically by isRegCarlsonContinuation_taylor.

theorem DirichletTransform.isRegCarlsonContinuation_of_hasFPowerSeriesOnBall {ι : Type u_1} [Fintype ι] {A : ℂ} {a : ℕ → ℂ} {f : ℂ → ℂ} {R : NNReal} (hf : HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars ℂ a) A ↑R) {z : ι → ℂ} (hz : ‖fun (i : ι) => z i - A‖ < ↑R) : IsRegCarlsonContinuation f z (regCarlsonTaylorSeries A a z)

Scalar power-series data suffice for Carlson's continuation on the full disk; no separate domination hypothesis is needed.

theorem DirichletTransform.isRegCarlsonContinuation_taylor {ι : Type u_1} [Fintype ι] {A : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.ball A R)) {z : ι → ℂ} (hz : ‖fun (i : ι) => z i - A‖ < R) : IsRegCarlsonContinuation f z (regCarlsonTaylorSeries A (fun (n : ℕ) => iteratedDeriv n f A / ↑n.factorial) z)

Carlson's Theorem 6.3-1, entire in the parameters on the full holomorphy disk. The coefficients are the usual scalar Taylor coefficients f⁽ⁿ⁾(A) / n!.

theorem DirichletTransform.IsRegCarlsonContinuation.eq_taylor {ι : Type u_1} [Fintype ι] {A : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.ball A R)) {z : ι → ℂ} (hz : ‖fun (i : ι) => z i - A‖ < R) {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) : G = regCarlsonTaylorSeries A (fun (n : ℕ) => iteratedDeriv n f A / ↑n.factorial) z

Every entire continuation agrees with the Taylor construction wherever the nodes lie in a disk of holomorphy of the scalar function.

theorem DirichletTransform.summable_norm_regCarlsonTaylorSeries {ι : Type u_1} [Fintype ι] {A : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.ball A R)) {z : ι → ℂ} (hz : ‖fun (i : ι) => z i - A‖ < R) (b : ι → ℂ) : Summable fun (n : ℕ) => ‖iteratedDeriv n f A / ↑n.factorial * regCarlsonR n (fun (i : ι) => z i - A) b‖

Absolute convergence of the continued Taylor expansion at every complex parameter vector and throughout the full node disk.

theorem DirichletTransform.IsRegCarlsonContinuation.hasSum_taylor {ι : Type u_1} [Fintype ι] {A : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.ball A R)) {z : ι → ℂ} (hz : ‖fun (i : ι) => z i - A‖ < R) {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (b : ι → ℂ) : HasSum (fun (n : ℕ) => iteratedDeriv n f A / ↑n.factorial * regCarlsonR n (fun (i : ι) => z i - A) b) (G b)

The convergent R-polynomial Taylor series represents every continued average, including at exceptional total parameters.

theorem DirichletTransform.hasSumLocallyUniformlyOn_regCarlsonTaylorSeries_joint {ι : Type u_1} [Fintype ι] {A : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.ball A R)) : HasSumLocallyUniformlyOn (fun (n : ℕ) (p : ι ⊕ ι → ℂ) => iteratedDeriv n f A / ↑n.factorial * regCarlsonR n (fun (i : ι) => p (Sum.inr i) - A) fun (i : ι) => p (Sum.inl i)) (fun (p : ι ⊕ ι → ℂ) => regCarlsonTaylorSeries A (fun (n : ℕ) => iteratedDeriv n f A / ↑n.factorial) (fun (i : ι) => p (Sum.inr i)) fun (i : ι) => p (Sum.inl i)) {p : ι ⊕ ι → ℂ | ‖fun (i : ι) => p (Sum.inr i) - A‖ < R}

The Taylor series converges locally uniformly jointly in parameters and nodes on the full scalar holomorphy disk. The two coordinate blocks are encoded by Sum.

theorem DirichletTransform.analyticOnNhd_regCarlsonTaylorSeries_joint {ι : Type u_1} [Fintype ι] {A : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.ball A R)) : AnalyticOnNhd ℂ (fun (p : ι ⊕ ι → ℂ) => regCarlsonTaylorSeries A (fun (n : ℕ) => iteratedDeriv n f A / ↑n.factorial) (fun (i : ι) => p (Sum.inr i)) fun (i : ι) => p (Sum.inl i)) {p : ι ⊕ ι → ℂ | ‖fun (i : ι) => p (Sum.inr i) - A‖ < R}

The joint holomorphy conclusion of Carlson's Theorem 6.3-1. There are no Dirichlet-parameter exclusions, and the node domain is the full product of disks.