Averages of uniformly summable series #
This file supplies the dominated-convergence form of Carlson's Representation 5.7-2. A summable numerical majorant, uniform on the standard simplex, permits termwise application of the regularized Carlson Dirichlet average.
References #
- [Carl77] B. C. Carlson, Special Functions of Applied Mathematics, Section 5.7, Academic Press, 1977.
theorem
DirichletTransform.hasSum_regCarlsonDirichletAverage
{ι : Type u_1}
[Fintype ι]
{b : ι → ℂ}
(hb : b ∈ Complex.mvBetaConvergent)
(z : ι → ℂ)
(g : ℕ → ℂ → ℂ)
(f : ℂ → ℂ)
(M : ℕ → ℝ)
(hg : ∀ (n : ℕ), ContinuousOn (fun (u : ι → ℝ) => g n (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ ι))
(hM : Summable M)
(hbound : ∀ (n : ℕ), ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, ‖g n (carlsonAffineForm z u)‖ ≤ M n)
(hsum :
∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι,
HasSum (fun (n : ℕ) => g n (carlsonAffineForm z u)) (f (carlsonAffineForm z u)))
:
HasSum (fun (n : ℕ) => regCarlsonDirichletAverage b z (g n)) (regCarlsonDirichletAverage b z f)
A uniformly summably dominated series may be averaged term by term with respect to the regularized Dirichlet density. This is the general analytic core of Carlson's Representation 5.7-2.