Polynomial quadratic transformations

The squared-node regression theorem is retained alongside the correct involutive identity.

theorem DirichletTransform.TwoVariable.numerator₂_zero_right (n : ℕ) (p q x : ℂ) : carlsonRPolynomialNumerator₂ n p q x 0 = Polynomial.eval p (ascPochhammer ℂ n) * x ^ n

theorem DirichletTransform.TwoVariable.numerator₂_even_opposite (n : ℕ) (β w : ℂ) : carlsonRPolynomialNumerator₂ (2 * n) β β w (-w) = 4 ^ n * Polynomial.eval β (ascPochhammer ℂ n) * Polynomial.eval (1 / 2) (ascPochhammer ℂ n) * w ^ (2 * n)

The even moments on opposite nodes, in division-free form.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_firstQuadratic_even (n : ℕ) (β x y : ℂ) : Polynomial.eval (β + 1 / 2) (ascPochhammer ℂ n) * carlsonRPolynomialNumerator₂ (2 * n) β β x y = Polynomial.eval (2 * β) (ascPochhammer ℂ (2 * n)) * carlsonRPolynomialNumerator₂ n (β + ↑n) (1 / 2 - ↑n) (arithmeticMeanSq x y) (geometricMeanSq x y)

Division-free polynomial form of the even-degree first quadratic transformation 6.9-8. It is valid at exceptional parameters because no Pochhammer symbol is divided out.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_firstQuadratic_odd (n : ℕ) (β x y : ℂ) : Polynomial.eval (β + 1 / 2) (ascPochhammer ℂ n) * carlsonRPolynomialNumerator₂ (2 * n + 1) β β x y = (x + y) / 2 * Polynomial.eval (2 * β) (ascPochhammer ℂ (2 * n + 1)) * carlsonRPolynomialNumerator₂ n (1 + β + ↑n) (-1 / 2 - ↑n) (arithmeticMeanSq x y) (geometricMeanSq x y)

Division-free polynomial form of the odd-degree first quadratic transformation 6.9-9.

theorem DirichletTransform.TwoVariable.secondQuadratic_unsquared_counterexample : Polynomial.eval (1 - 2 * 1 - 2 * 1) (ascPochhammer ℂ 1) * carlsonRPolynomialNumerator₂ 1 1 1 (2 ^ 2) (0 ^ 2) ≠ Polynomial.eval 1 (ascPochhammer ℂ 1) * carlsonRPolynomialNumerator₂ 1 (1 / 2 - 1 - 1) (1 / 2 - 1 - 1) (2 + 0) (2 - 0)

Regression check: the version of the second quadratic identity with unsquared right-hand nodes is false, already for n = β = 1, x = 2, y = 0.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_secondQuadratic (n : ℕ) (β x y : ℂ) : Polynomial.eval (1 - 2 * β - 2 * ↑n) (ascPochhammer ℂ n) * carlsonRPolynomialNumerator₂ n β β (x ^ 2) (y ^ 2) = Polynomial.eval β (ascPochhammer ℂ n) * carlsonRPolynomialNumerator₂ n (1 / 2 - β - ↑n) (1 / 2 - β - ↑n) ((x + y) ^ 2) ((x - y) ^ 2)

Division-free polynomial form of Carlson's involutive transformation 6.10-3. Both transformed nodes must be squared: both sides are homogeneous of degree 2 * n in x,y. Omitting the squares gives the false identity refuted above.