Quadratic transformations with slit-plane transformed nodes

Both regularized transformations hold for all complex parameters whenever the unsquared variables x,y have positive real parts. Their squares, product, and squared arithmetic mean need only lie in the slit plane; they need not have positive real parts. This extends the earlier Lean formulations that required right-half-plane transformed nodes. The node domain agrees with Carlson 1977, §§6.9–6.10; it is not an enlargement of the published domain.

The proof uses joint node holomorphy and agreement near (1,1). It does not claim every component of the algebraic preimage of the slit plane: branches on larger domains still require separate analysis. The finer equal-parameter normalization and its L-function transformations are not extended by this file.

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

A product of two right-half-plane numbers avoids the principal branch cut.

theorem DirichletTransform.TwoVariable.sq_mem_slitPlane_of_re_pos {x : ℂ} (hx : 0 < x.re) : x ^ 2 ∈ Complex.slitPlane

Squaring a right-half-plane number can leave that half-plane but not the slit plane.

theorem DirichletTransform.TwoVariable.meanSquares_mem_slitDomain {x y : ℂ} (hx : 0 < x.re) (hy : 0 < y.re) : pair (arithmeticMeanSq x y) (geometricMeanSq x y) ∈ carlsonRSlitDomain

The two transformed mean squares stay on the principal slit branch.

theorem DirichletTransform.TwoVariable.regRSlit_firstQuadratic (t β x y : ℂ) (hx : 0 < x.re) (hy : 0 < y.re) : regCarlsonRSlit (2 * t) (pair β β) (pair x y) = quadraticGammaRatio β * regCarlsonRSlit t (pair (β + t) (1 / 2 - t)) (pair (arithmeticMeanSq x y) (geometricMeanSq x y))

First quadratic transformation, with no restriction on the real parts of the transformed mean squares and no Dirichlet-parameter exclusions.

theorem DirichletTransform.TwoVariable.regRSlit_secondQuadratic (t β x y : ℂ) (hx : 0 < x.re) (hy : 0 < y.re) : regCarlsonRSlit t (pair β β) (pair (x ^ 2) (y ^ 2)) = quadraticGammaRatio β * regCarlsonRSlit t (pair (2 * β + t) (1 / 2 - β - t)) (pair (arithmeticMeanSq x y) (geometricMeanSq x y))

Second quadratic transformation on the whole positive-real-part square-root domain. The squared input nodes and both transformed nodes may have negative real parts.