Quadratic transformations on the full Dirichlet parameter domain

The regularized transformations are entire identities in (t, β). The entire Gamma ratio below, rather than a quotient evaluated at Gamma poles, implements Legendre duplication. Node domains are unchanged from the native transformation theorems. EqualParameter supplies the canonical ordinary continuation, retaining the removable values at nonpositive integral β where the entire ratio here vanishes.

noncomputable def DirichletTransform.TwoVariable.quadraticGammaRatio (β : ℂ) : ℂ

Entire extension of Γ(β + 1/2) / Γ(2β). The formula remains meaningful at Gamma poles.

Equations

• DirichletTransform.TwoVariable.quadraticGammaRatio β = 2 ^ (1 - 2 * β) * ↑√Real.pi * (Complex.Gamma β)⁻¹

theorem DirichletTransform.TwoVariable.analyticOnNhd_quadraticGammaRatio : AnalyticOnNhd ℂ quadraticGammaRatio Set.univ

Legendre's duplication ratio is entire.

theorem DirichletTransform.TwoVariable.Gamma_mul_quadraticGammaRatio {β : ℂ} (hβ : 0 < β.re) : Complex.Gamma (β + β) * quadraticGammaRatio β = Complex.Gamma (β + 1 / 2)

Duplication converts the native normalization into the equal-parameter normalization.

theorem DirichletTransform.TwoVariable.regRContinued_firstQuadratic (t β x y : ℂ) (hz : FirstQuadraticDomain x y) : regCarlsonRContinued (2 * t) (pair x y) ⋯ (pair β β) = quadraticGammaRatio β * regCarlsonRContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (β + t) (1 / 2 - t))

First quadratic transformation, entire in both parameters, including exceptional Gamma parameters. There are no convergence or non-pole hypotheses.

theorem DirichletTransform.TwoVariable.regRContinued_secondQuadratic (t β x y : ℂ) (hz : SecondQuadraticDomain x y) : regCarlsonRContinued t (pair (x ^ 2) (y ^ 2)) ⋯ (pair β β) = quadraticGammaRatio β * regCarlsonRContinued t (pair (arithmeticMeanSq x y) (geometricMeanSq x y)) ⋯ (pair (2 * β + t) (1 / 2 - β - t))

Second quadratic transformation, entire in both parameters.