Power-series representations using Carlson R-polynomials

This file provides the native integral representation and the Taylor-series definition. Carlson.RPolynomial.TaylorContinuation proves convergence on the full disk of holomorphy and joint analyticity in parameters and nodes.

def DirichletTransform.shiftCarlsonVariables {ι : Type u_1} (A : ℂ) (z : ι → ℂ) : ι → ℂ

Translation of Carlson's variables by the center of a power-series expansion.

Equations

• DirichletTransform.shiftCarlsonVariables A z i = z i - A

theorem DirichletTransform.hasSum_regCarlsonR_of_powerSeries {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (A : ℂ) (a : ℕ → ℂ) (z : ι → ℂ) (f : ℂ → ℂ) (M : ℕ → ℝ) (hM : Summable M) (hbound : ∀ (n : ℕ), ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, ‖a n * (carlsonAffineForm z u - A) ^ n‖ ≤ M n) (hsum : ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, HasSum (fun (n : ℕ) => a n * (carlsonAffineForm z u - A) ^ n) (f (carlsonAffineForm z u))) : HasSum (fun (n : ℕ) => a n * regCarlsonR n (shiftCarlsonVariables A z) b) (regCarlsonDirichletAverage b z f)

Carlson's Representation 5.7-2 in regularized form. The hypotheses state uniform summable domination and pointwise summation of the scalar power series on the convex hull of the supplied variables.

noncomputable def DirichletTransform.regCarlsonTaylorSeries {ι : Type u_1} [Fintype ι] (A : ℂ) (a : ℕ → ℂ) (z b : ι → ℂ) : ℂ

The R-polynomial Taylor series for Carlson's regularized Dirichlet average. Its convergence and continuation properties are proved in Carlson.RPolynomial.TaylorContinuation.

Equations

• DirichletTransform.regCarlsonTaylorSeries A a z b = ∑' (n : ℕ), a n * DirichletTransform.regCarlsonR n (fun (i : ι) => z i - A) b

theorem DirichletTransform.differentiable_regCarlsonTaylorTerm {ι : Type u_1} [Fintype ι] (A : ℂ) (a : ℕ → ℂ) (z : ι → ℂ) (n : ℕ) : Differentiable ℂ fun (b : ι → ℂ) => a n * regCarlsonR n (fun (i : ι) => z i - A) b

Each term of Carlson's Taylor-series construction is entire in the Dirichlet parameters.

theorem DirichletTransform.differentiable_regCarlsonTaylorPartialSum {ι : Type u_1} [Fintype ι] (A : ℂ) (a : ℕ → ℂ) (z : ι → ℂ) (N : ℕ) : Differentiable ℂ fun (b : ι → ℂ) => ∑ n ∈ Finset.range N, a n * regCarlsonR n (fun (i : ι) => z i - A) b

Every finite partial sum in Carlson's Taylor-series construction is entire in the Dirichlet parameters.