Two-variable L-inversion

The full slit-domain correction is log x + log y; the log (x * y) version requires the branch-safe right-half-plane hypotheses.

theorem DirichletTransform.TwoVariable.regCarlsonLSlit_pair_inversion (t u v : ℂ) {x y : ℂ} (hz : pair x y ∈ carlsonRSlitDomain) : regCarlsonLSlit t (pair u v) (pair x y) = (Complex.log x + Complex.log y) * regCarlsonRSlit t (pair u v) (pair x y) - x ^ (t + v) * y ^ (t + u) * regCarlsonLSlit (-u - v - t) (pair v u) (pair x y)

Carlson (1987), (2.11), in branch-correct form on the entire product slit plane. No Gamma-regularity assumptions are needed for these regularized functions.

theorem DirichletTransform.TwoVariable.regCarlsonLSlit_pair_inversion_log_mul (t u v : ℂ) {x y : ℂ} (hx : 0 < x.re) (hy : 0 < y.re) : regCarlsonLSlit t (pair u v) (pair x y) = Complex.log (x * y) * regCarlsonRSlit t (pair u v) (pair x y) - x ^ (t + v) * y ^ (t + u) * regCarlsonLSlit (-u - v - t) (pair v u) (pair x y)

The paper's log (x * y) form of (2.11), on its branch-safe right half-plane.