Differential and contiguous identities for two-variable Carlson polynomials

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_smul (n : ℕ) (p q c x y : ℂ) : carlsonRPolynomialNumerator₂ n p q (c * x) (c * y) = c ^ n * carlsonRPolynomialNumerator₂ n p q x y

Homogeneity of the two-variable Pochhammer numerator, including exceptional parameters.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_transform (n : ℕ) (p q x y : ℂ) : carlsonRPolynomialNumerator₂ n p q x y = (-1) ^ n * carlsonRPolynomialNumerator₂ n (1 - p - q - ↑n) q x (x - y)

Two-variable specialization of the division-free linear transformation.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_weighted_shift (n : ℕ) (p q x y : ℂ) : p * carlsonRPolynomialNumerator₂ n (p + 1) q x y + q * carlsonRPolynomialNumerator₂ n p (q + 1) x y = (p + q + ↑n) * carlsonRPolynomialNumerator₂ n p q x y

The weighted sum of the two parameter shifts only depends on the total parameter.

theorem DirichletTransform.TwoVariable.hasDerivAt_carlsonRPolynomialNumerator₂_left (n : ℕ) (p q x y : ℂ) : HasDerivAt (fun (w : ℂ) => carlsonRPolynomialNumerator₂ (n + 1) p q w y) ((↑n + 1) * p * carlsonRPolynomialNumerator₂ n (p + 1) q x y) x

Coordinate derivatives of the explicit two-variable numerator.

theorem DirichletTransform.TwoVariable.hasDerivAt_carlsonRPolynomialNumerator₂_right (n : ℕ) (p q x y : ℂ) : HasDerivAt (fun (w : ℂ) => carlsonRPolynomialNumerator₂ (n + 1) p q x w) ((↑n + 1) * q * carlsonRPolynomialNumerator₂ n p (q + 1) x y) y

theorem DirichletTransform.TwoVariable.hasDerivAt_carlsonRPolynomialNumerator₂_translate (n : ℕ) (p q x y w : ℂ) : HasDerivAt (fun (t : ℂ) => carlsonRPolynomialNumerator₂ (n + 1) p q (x + t) (y + t)) ((↑n + 1) * (p + q + ↑n) * carlsonRPolynomialNumerator₂ n p q (x + w) (y + w)) w

Simultaneously translating the nodes lowers the degree without shifting the parameters.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_contiguous (n : ℕ) (p q x y : ℂ) : (q - 1) * carlsonRPolynomialNumerator₂ (n + 1) p q x y + (↑n + 1) * (p + q + ↑n) * x * carlsonRPolynomialNumerator₂ n (p + 1) (q - 1) x y = (q + ↑n) * carlsonRPolynomialNumerator₂ (n + 1) (p + 1) (q - 1) x y

A division-free contiguous relation transferring one unit between the parameters.