Two-variable Carlson R-polynomials

noncomputable def DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂ (n : ℕ) (b₀ b₁ x y : ℂ) : ℂ

The explicit Pochhammer numerator of a two-variable Carlson R-polynomial. This form is well-defined at all parameter values, including zeros of the usual normalizing Pochhammer symbol.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.TwoVariable.carlsonAffinePolynomial_pair (x y : ℂ) : carlsonAffinePolynomial (pair x y) = MvPolynomial.C x * MvPolynomial.X 0 + MvPolynomial.C y * MvPolynomial.X 1

The affine polynomial for a pair is the expected two-term linear polynomial.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator_pair (n : ℕ) (b₀ b₁ x y : ℂ) : carlsonRPolynomialNumerator n (pair b₀ b₁) (pair x y) = carlsonRPolynomialNumerator₂ n b₀ b₁ x y

The explicit two-variable Pochhammer numerator agrees with the specialization of the general multivariate numerator to Fin 2.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_swap (n : ℕ) (b₀ b₁ x y : ℂ) : carlsonRPolynomialNumerator₂ n b₁ b₀ y x = carlsonRPolynomialNumerator₂ n b₀ b₁ x y

Simultaneously exchanging the two parameters and variables leaves the two-variable Pochhammer numerator unchanged.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_neg (n : ℕ) (b₀ b₁ x y : ℂ) : carlsonRPolynomialNumerator₂ n b₀ b₁ (-x) (-y) = (-1) ^ n * carlsonRPolynomialNumerator₂ n b₀ b₁ x y

Negating both variables multiplies the two-variable numerator by its degree parity.

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_opposite (n : ℕ) (b₀ b₁ x : ℂ) : carlsonRPolynomialNumerator₂ n b₀ b₁ x (-x) = x ^ n * carlsonRPolynomialNumerator₂ n b₀ b₁ 1 (-1)

On a pair of opposite variables, homogeneity reduces the numerator to its value at (1, -1). This isolates the scalar coefficient evaluated in [Carl77, Theorem 6.9-1].

theorem DirichletTransform.TwoVariable.carlsonRPolynomialNumerator₂_eq_zero_of_odd (n : ℕ) (hn : Odd n) (b x : ℂ) : carlsonRPolynomialNumerator₂ n b b x (-x) = 0

The odd-degree equal-parameter Carlson numerator vanishes at opposite variables. This is the exceptional-parameter-free polynomial content of [Carl77, Theorem 6.9-1].

theorem DirichletTransform.TwoVariable.regRPolynomial_eq_numerator₂_mul_one_div_Gamma (n : ℕ) (b₀ b₁ x y : ℂ) : regRPolynomial n b₀ b₁ x y = carlsonRPolynomialNumerator₂ n b₀ b₁ x y * (Complex.Gamma (b₀ + b₁ + ↑n))⁻¹

The two-variable regularized Carlson polynomial in terms of its explicit Pochhammer numerator.

theorem DirichletTransform.TwoVariable.regRPolynomial_swap (n : ℕ) (b₀ b₁ x y : ℂ) : regRPolynomial n b₁ b₀ y x = regRPolynomial n b₀ b₁ x y

Simultaneously exchanging the two parameters and variables leaves the regularized two-variable R-polynomial unchanged.

theorem DirichletTransform.TwoVariable.regRPolynomial_eq_zero_of_odd (n : ℕ) (hn : Odd n) (b x : ℂ) : regRPolynomial n b b x (-x) = 0

The regularized equal-parameter Carlson polynomial of odd degree vanishes at opposite variables. This is the regularized form of [Carl77, Theorem 6.9-1].

theorem DirichletTransform.TwoVariable.carlsonPowerPolynomial_pair_smul (n : ℕ) (a x y : ℂ) : carlsonPowerPolynomial n (pair (a * x) (a * y)) = MvPolynomial.C (a ^ n) * carlsonPowerPolynomial n (pair x y)

The two-variable Carlson power kernel is homogeneous of degree n.