Two-variable associated L-relations

Carlson (1987), (3.10), including the factored and mixed-derivative forms.

theorem DirichletTransform.TwoVariable.regCarlsonLSlit_pair_three_term (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) : (u + v + t) * regCarlsonLSlit (t + 1) (pair u v) (pair x y) - ((u + t) * x + (v + t) * y) * regCarlsonLSlit t (pair u v) (pair x y) + t * x * y * regCarlsonLSlit (t - 1) (pair u v) (pair x y) = -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)

The first equality of Carlson (1987), (3.10), including its R-correction. The further factored and mixed-node-derivative forms are separate statements.

theorem DirichletTransform.TwoVariable.regCarlsonLSlit_pair_three_term_factored (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) : (u + v + t) * regCarlsonLSlit (t + 1) (pair u v) (pair x y) - ((u + t) * x + (v + t) * y) * regCarlsonLSlit t (pair u v) (pair x y) + t * x * y * regCarlsonLSlit (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 factored equality in Carlson (1987), (3.10), with all Gamma factors cleared.

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

The mixed-derivative equality in (3.10), without dividing by t * (t + 1). This formulation includes t = 0, t = -1, and coincident nodes.

theorem DirichletTransform.TwoVariable.regCarlsonLSlit_pair_three_term_mixed_div (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) (ht : t ≠ 0) (ht₁ : t + 1 ≠ 0) : (u + v + t) * regCarlsonLSlit (t + 1) (pair u v) (pair x y) - ((u + t) * x + (v + t) * y) * regCarlsonLSlit t (pair u v) (pair x y) + t * x * y * regCarlsonLSlit (t - 1) (pair u v) (pair x y) = (x - y) ^ 2 / (t * (t + 1)) * carlsonPartialDeriv 0 (carlsonPartialDeriv 1 (regCarlsonRSlit (t + 1) (pair u v))) (pair x y)

The quotient form printed in (3.10), with its necessary exponent exclusions.