Interchanging an exponent and a Dirichlet parameter

The two numerator parameters in the Gauss series are symmetric. We establish this symmetry first near the all-one node vector, then continue in the parameters and in the slit-plane node. This is the R-identity underlying Carlson (1987), (2.12).

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_zero_left (n : ℕ) (u v y : ℂ) : carlsonRPolynomialNumerator₂ n u v 0 y = Polynomial.eval v (ascPochhammer ℂ n) * y ^ n

Only one monomial survives when the first polynomial node vanishes.

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_parameterSymmetry (a u v : ℂ) {w : ℂ} (hw : w ∈ Complex.slitPlane) : regCarlsonRSlit (-a) (pair u v) (pair 1 w) = regCarlsonRSlit (-v) (pair (u + v - a) a) (pair 1 w)

Gauss numerator-parameter symmetry on the entire slit plane, with all complex parameters allowed by reciprocal-Gamma regularization.

theorem DirichletTransform.TwoVariable.div_mem_slitPlane_of_re_pos {x y : ℂ} (hx : 0 < x.re) (hy : 0 < y.re) : x / y ∈ Complex.slitPlane

A ratio of two right-half-plane numbers cannot lie on the nonpositive real axis.

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_normalize_first (t : ℂ) (b : Fin 2 → ℂ) {x y : ℂ} (hx : 0 < x.re) (hy : 0 < y.re) : regCarlsonRSlit t b (pair x y) = x ^ t * regCarlsonRSlit t b (pair 1 (y / x))

Normalize the first node, with branch control for arbitrary right-half-plane nodes. The normalized second node need only belong to the slit plane.

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_parameterInterchange (t u v : ℂ) {x y : ℂ} (hx : 0 < x.re) (hy : 0 < y.re) : regCarlsonRSlit t (pair u v) (pair x y) = x ^ t * regCarlsonRSlit (-v) (pair (u + v + t) (-t)) (pair 1 (y / x))

Exponent-parameter interchange at two right-half-plane nodes, with no parameter restrictions and a slit-plane ratio on the transformed side.

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_pair_swap (t u v : ℂ) {x y : ℂ} (hx : x ∈ Complex.slitPlane) (hy : y ∈ Complex.slitPlane) : regCarlsonRSlit t (pair v u) (pair y x) = regCarlsonRSlit t (pair u v) (pair x y)

Simultaneously swapping the two parameters and nodes on the slit domain.

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_parameterInterchange_last (t u v : ℂ) {x y : ℂ} (hx : 0 < x.re) (hy : 0 < y.re) : regCarlsonRSlit t (pair u v) (pair x y) = y ^ t * regCarlsonRSlit (-u) (pair (-t) (u + v + t)) (pair (x / y) 1)

The second form of the exponent-parameter interchange, normalized at the last node.