Confluence of Carlson's R-function to the S-function

This file formalizes the confluence limit of [Carl77, Section 5.10]. Natural exponents are used first: this is the branch-independent form of Carlson's limit and is directly supported by Mathlib's theorem Complex.tendsto_one_add_div_pow_exp.

References

• [Carl77] B. C. Carlson, Special Functions of Applied Mathematics, Section 5.10, Academic Press, 1977.

noncomputable def DirichletTransform.carlsonConfluentVariables {ι : Type u_1} (n : ℕ) (z : ι → ℂ) : ι → ℂ

The Carlson variables which coalesce at 1 in the confluence limit R → S.

Equations

• DirichletTransform.carlsonConfluentVariables n z i = 1 + z i / ↑n

theorem DirichletTransform.carlsonAffineForm_confluentVariables {ι : Type u_1} [Fintype ι] {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) (n : ℕ) (z : ι → ℂ) : carlsonAffineForm (carlsonConfluentVariables n z) u = 1 + carlsonAffineForm z u / ↑n

Carlson's affine form turns confluent variables into the corresponding scalar confluent variable.

theorem DirichletTransform.tendsto_carlsonAffineForm_confluentVariables_pow {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : Filter.Tendsto (fun (n : ℕ) => carlsonAffineForm (carlsonConfluentVariables n z) u ^ n) Filter.atTop (nhds (Complex.exp (carlsonAffineForm z u)))

Pointwise confluence of the natural-power Carlson kernel to the exponential kernel.

theorem DirichletTransform.norm_carlsonAffineForm_confluentVariables_pow_le {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : ‖carlsonAffineForm (carlsonConfluentVariables n z) u ^ n‖ ≤ Real.exp (∑ i : ι, ‖z i‖)

A uniform bound for the natural-power kernels occurring in Carlson's confluence limit.

theorem DirichletTransform.tendsto_regCarlsonRIntegral_confluent {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (hb : b ∈ Complex.mvBetaConvergent) : Filter.Tendsto (fun (n : ℕ) => regCarlsonRIntegral (↑n) b (carlsonConfluentVariables n z)) Filter.atTop (nhds (regCarlsonSIntegral b z))

Carlson's confluence theorem 5.10-1 for the native regularized integrals: natural-power R functions with variables coalescing at 1 converge to the S function.

theorem DirichletTransform.tendsto_carlsonRIntegral_confluent {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (hb : b ∈ Complex.mvBetaConvergent) : Filter.Tendsto (fun (n : ℕ) => carlsonRIntegral (↑n) b (carlsonConfluentVariables n z)) Filter.atTop (nhds (carlsonSIntegral b z))

Carlson's confluence theorem 5.10-1 for the native unregularized integrals.