Native integral quadratic transformations

theorem DirichletTransform.TwoVariable.rIntegral_firstQuadratic (t β x y : ℂ) (hbleft : pair β β ∈ Complex.mvBetaConvergent) (hbright : pair (β + t) (1 / 2 - t) ∈ Complex.mvBetaConvergent) (hz : FirstQuadraticDomain x y) : rIntegral (2 * t) β β x y = rIntegral t (β + t) (1 / 2 - t) (arithmeticMeanSq x y) (geometricMeanSq x y)

Carlson's first quadratic transformation 6.9-3 on a common native integral domain.

The extra convergence hypotheses make both sides genuine Dirichlet integrals. The larger parameter domain is treated separately in QuadraticContinuation and EqualParameter.

theorem DirichletTransform.TwoVariable.rIntegral_secondQuadratic (t β x y : ℂ) (hbleft : pair β β ∈ Complex.mvBetaConvergent) (hbright : pair (2 * β + t) (1 / 2 - β - t) ∈ Complex.mvBetaConvergent) (hz : SecondQuadraticDomain x y) : rIntegral t β β (x ^ 2) (y ^ 2) = rIntegral t (2 * β + t) (1 / 2 - β - t) (arithmeticMeanSq x y) (geometricMeanSq x y)

Carlson's second quadratic transformation 6.10-1 on a common native integral domain.