Dependence of Carlson's R-function on a small variable

This file develops [Carl77, Section 8.3]. Its core result identifies the sectorial limit as one variable tends to zero with deletion of that variable and a beta-factor correction.

tendsto_regCarlsonRContinued_update_zero_of_pos allows arbitrary individual Dirichlet parameters and any approach through the right half-plane. It still assumes positive real parts for both endpoint exponents. The double-shift recurrence 8.3(5) is available for removing those restrictions; the corresponding induction on the limit, and continuation to larger slit-plane sectors, remain to be proved.

def DirichletTransform.carlsonSmallVariableSector (δ r : ℝ) : Set ℂ

A closed right-half-plane subsector used when a native R-integral variable approaches zero. Carlson's wider slit-plane sector is recovered only after continuation in the variables.

Equations

• DirichletTransform.carlsonSmallVariableSector δ r = {w : ℂ | ‖w‖ ≤ r ∧ (w = 0 ∨ |w.arg| ≤ Real.pi / 2 - δ)}

theorem DirichletTransform.norm_le_of_mem_carlsonSmallVariableSector {δ r : ℝ} {w : ℂ} (hw : w ∈ carlsonSmallVariableSector δ r) : ‖w‖ ≤ r

Every point of Carlson's small-variable sector has norm at most its radius.

def DirichletTransform.eraseCarlsonParameter {ι : Type u_1} (i : ι) (b : ι → ℂ) : { j : ι // j ≠ i } → ℂ

The parameter vector obtained by deleting a distinguished coordinate.

Equations

• DirichletTransform.eraseCarlsonParameter i b j = b ↑j

def DirichletTransform.eraseCarlsonVariable {ι : Type u_1} (i : ι) (z : ι → ℂ) : { j : ι // j ≠ i } → ℂ

The variable vector obtained by deleting a distinguished coordinate.

Equations

• DirichletTransform.eraseCarlsonVariable i z j = z ↑j

theorem DirichletTransform.tendsto_regCarlsonRIntegral_update_zero {ι : Type u_1} [Fintype ι] (i : ι) {a a' : ℂ} {b z : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (ha'i : 0 < (a' - b i).re) (hsum : a + a' = ∑ j : ι, b j) (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : Filter.Tendsto (fun (w : ℂ) => regCarlsonRIntegral (-a) b (Function.update z i w)) (nhdsWithin 0 {0}ᶜ ⊓ Filter.principal (carlsonSmallVariableSector 1 1)) (nhds (Complex.Gamma (a' - b i) / Complex.Gamma a' * regCarlsonRIntegral (-a) (eraseCarlsonParameter i b) (eraseCarlsonVariable i z)))

Carlson's sectorial small-variable limit, Theorem 8.3-1, in regularized form.

The beta factors in Carlson's unregularized statement are absorbed by Gamma regularization; the remaining shifted Gamma factor is displayed explicitly.

theorem DirichletTransform.carlsonRVariableDomain_update {ι : Type u_1} {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (i : ι) {w : ℂ} (hw : 0 < w.re) : Function.update z i w ∈ carlsonRVariableDomain

Updating one node preserves the domain when the replacement has positive real part.

theorem DirichletTransform.regCarlsonRContinued_eq_sum_double_shift {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (i : ι) : regCarlsonRContinued t z hz b = ∑ j : ι, addDirichletUnit b i j * ((∑ k : ι, b k + t) * z j - t * z i) * regCarlsonRContinued (t - 1) z hz (addDirichletUnit (addDirichletUnit b i) j)

Carlson's recurrence 8.3(5), used to move both endpoint exponents into their convergence half-planes. This regularized form has no denominators.

theorem DirichletTransform.tendsto_regCarlsonRContinued_update_zero_of_pos {ι : Type u_1} [Fintype ι] (i : ι) {a a' : ℂ} {b z : ι → ℂ} (ha : 0 < a.re) (ha' : 0 < a'.re) (ha'i : 0 < (a' - b i).re) (hsum : a + a' = ∑ j : ι, b j) (hz : z ∈ carlsonRVariableDomain) {E : Type u_2} {l : Filter E} {w : E → ℂ} (hw : ∀ (x : E), 0 < (w x).re) (hlim : Filter.Tendsto w l (nhds 0)) : Filter.Tendsto (fun (x : E) => regCarlsonRContinued (-a) (Function.update z i (w x)) ⋯ b) l (nhds (Complex.Gamma (a' - b i) / Complex.Gamma a' * regCarlsonRContinued (-a) (eraseCarlsonVariable i z) ⋯ (eraseCarlsonParameter i b)))

The small-variable limit for the continued R-function with unrestricted individual Dirichlet parameters. The approach can be any filter in the right half-plane; no narrower angular sector is needed. The positive endpoint-exponent hypotheses are still required here.