Two-variable associated R-relations

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_pair_contiguous (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) : u * (y - x) * regCarlsonRSlit t (pair (u + 1) v) (pair x y) = y * regCarlsonRSlit t (pair u v) (pair x y) - regCarlsonRSlit (t + 1) (pair u v) (pair x y)

The first two-node contiguous R-relation, without parameter denominators.

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_pair_contiguous_last (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) : v * (x - y) * regCarlsonRSlit t (pair u (v + 1)) (pair x y) = x * regCarlsonRSlit t (pair u v) (pair x y) - regCarlsonRSlit (t + 1) (pair u v) (pair x y)

The companion contiguous relation, raising the second parameter.

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_pair_correction_factor (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) : -regCarlsonRSlit (t + 1) (pair u v) (pair x y) + (x + y) * regCarlsonRSlit t (pair u v) (pair x y) - x * y * regCarlsonRSlit (t - 1) (pair u v) (pair x y) = u * v * (x - y) ^ 2 * regCarlsonRSlit (t - 1) (pair (u + 1) (v + 1)) (pair x y)

The R-correction in (3.10) has a squared node-difference factor.

theorem DirichletTransform.TwoVariable.carlsonPartialDeriv_regCarlsonRSlit_pair_mixed (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) : carlsonPartialDeriv 0 (carlsonPartialDeriv 1 (regCarlsonRSlit (t + 1) (pair u v))) (pair x y) = t * (t + 1) * u * v * regCarlsonRSlit (t - 1) (pair (u + 1) (v + 1)) (pair x y)

The two-node mixed derivative, valid even at the exceptional integral exponents.

theorem DirichletTransform.TwoVariable.regCarlsonRSlit_pair_three_term (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) : (u + v + t) * regCarlsonRSlit (t + 1) (pair u v) (pair x y) - ((u + t) * x + (v + t) * y) * regCarlsonRSlit t (pair u v) (pair x y) + t * x * y * regCarlsonRSlit (t - 1) (pair u v) (pair x y) = 0

The three-term R-recurrence, with division-free coefficients.