Descending Pochhammer polynomials

This module provides basic lemmas for descending Pochhammer polynomials descPochhammer R n over general rings, together with their sums over integer intervals.

The monicity result holds over any ring, and the degree results require only a nontrivial ring. The summation identity also holds over arbitrary rings; no division by m + 1 is needed.

Main declarations

• TauCeti.monic_descPochhammer: descPochhammer R n is monic over any ring R.
• TauCeti.descPochhammer_natDegree: (descPochhammer R n).natDegree = n for nontrivial R.
• TauCeti.descPochhammer_degree: (descPochhammer R n).degree = n for nontrivial R.
• TauCeti.descPochhammer_succ_eval_add_one: the falling factorial of degree m + 1 at x + 1 is x + 1 times the one of degree m at x.
• TauCeti.sum_Ico_descPochhammer_eval: its sum over a half-open integer interval is the endpoint difference of the next falling factorial, after clearing the denominator.
• TauCeti.mul_prod_sq_sub_sq_eq_descPochhammer_eval: the odd polynomial x (x² - 1²) ⋯ (x² - k²) is the falling factorial of degree 2k + 1 at x + k.
• TauCeti.factorial_dvd_mul_prod_sq_sub_sq: its values at the integers are divisible by (2k + 1)!.
• TauCeti.two_mul_prod_sq_sub_sq_eq: twice the even polynomial (x² - 0²) ⋯ (x² - k²) is the sum of the falling factorials of degree 2k + 2 at x + k + 1 and at x + k.
• TauCeti.mul_factorial_dvd_prod_sq_sub_sq: its values at the integers are divisible by (k + 1) (2k + 1)! = (2k + 2)! / 2, which is its value at k + 1 (TauCeti.prod_sq_sub_sq_eq_mul_factorial).
• TauCeti.prod_sub_mul_add_add_one_eq_descPochhammer_eval: the polynomial ∏_{m < k} (x - m) (x + m + 1) in x (x + 1) is the falling factorial of degree 2k at x + k.
• TauCeti.two_mul_add_one_mul_prod_sub_mul_add_add_one_eq: weighted by 2x + 1, it is the sum of the falling factorials of degree 2k + 1 at x + k + 1 and at x + k.
• TauCeti.factorial_dvd_two_mul_add_one_mul_prod_sub_mul_add_add_one: the values of the weighted polynomial at the integers are divisible by (2k + 1)!.

theorem TauCeti.monic_descPochhammer {R : Type u_1} [Ring R] (n : ℕ) : (descPochhammer R n).Monic

Unlike monic_descPochhammer, this drops [Nontrivial R] and [NoZeroDivisors R] and holds over any ring.

@[simp]

theorem TauCeti.descPochhammer_natDegree {R : Type u_1} [Ring R] [Nontrivial R] (n : ℕ) : (descPochhammer R n).natDegree = n

Unlike descPochhammer_natDegree, this drops [NoZeroDivisors R] and holds over any nontrivial ring.

@[simp]

theorem TauCeti.descPochhammer_degree {R : Type u_1} [Ring R] [Nontrivial R] (n : ℕ) : (descPochhammer R n).degree = ↑n

The degree of the descending Pochhammer polynomial over any nontrivial ring is n.

theorem TauCeti.descPochhammer_succ_eval_add_one {R : Type u_1} [Ring R] (m : ℕ) (x : R) : Polynomial.eval (x + 1) (descPochhammer R (m + 1)) = (x + 1) * Polynomial.eval x (descPochhammer R m)

Shifting the argument of a falling factorial by one strips off its leading linear factor: the degree m + 1 falling factorial at x + 1 is (x + 1) times the degree m one at x.

Sums over integer intervals

theorem TauCeti.sum_Ico_descPochhammer_eval {R : Type u_1} [Ring R] (m : ℕ) {p q : ℤ} (h : p ≤ q) : (↑m + 1) * ∑ t ∈ Finset.Ico p q, Polynomial.eval (↑t) (descPochhammer R m) = Polynomial.eval (↑q) (descPochhammer R (m + 1)) - Polynomial.eval (↑p) (descPochhammer R (m + 1))

The discrete antiderivative of a falling factorial. Summing the degree m falling factorial over the integer range p ≤ t < q gives the difference of the degree m + 1 falling factorial at the endpoints, after multiplying the sum by m + 1. The identity holds in any coefficient ring; it does not require m + 1 to be invertible.

For q < p the interval is empty while the endpoint difference need not vanish.

An odd polynomial as a falling factorial

theorem TauCeti.mul_prod_sq_sub_sq_eq_descPochhammer_eval {R : Type u_1} [CommRing R] (k : ℕ) (x : R) : x * ∏ m ∈ Finset.range k, (x ^ 2 - (↑m + 1) ^ 2) = Polynomial.eval (x + ↑k) (descPochhammer R (2 * k + 1))

An odd polynomial as a falling factorial. The product x · (x² - 1²) (x² - 2²) ⋯ (x² - k²) is the product (x + k) (x + k - 1) ⋯ (x - k) of the 2k + 1 consecutive values centred at x, that is, the falling factorial of degree 2k + 1 evaluated at x + k.

theorem TauCeti.factorial_dvd_mul_prod_sq_sub_sq (k : ℕ) (x : ℤ) : ↑(2 * k + 1).factorial ∣ x * ∏ m ∈ Finset.range k, (x ^ 2 - (↑m + 1) ^ 2)

The product x · (x² - 1²) ⋯ (x² - k²) is divisible by (2k + 1)! at every integer x, being the product (x - k) (x - k + 1) ⋯ (x + k) of 2k + 1 consecutive integers (Nat.factorial_coe_dvd_prod).

An even polynomial as two falling factorials

theorem TauCeti.two_mul_prod_sq_sub_sq_eq {R : Type u_1} [CommRing R] (k : ℕ) (x : R) : 2 * ∏ m ∈ Finset.range (k + 1), (x ^ 2 - ↑m ^ 2) = Polynomial.eval (x + ↑k + 1) (descPochhammer R (2 * k + 2)) + Polynomial.eval (x + ↑k) (descPochhammer R (2 * k + 2))

An even polynomial as two falling factorials. The product (x² - 0²) (x² - 1²) ⋯ (x² - k²) is x times the falling factorial of degree 2k + 1 at x + k, so doubling it, as 2x = (x + k + 1) + (x - k - 1), splits it into the falling factorials of degree 2k + 2 at x + k + 1 and at x + k.

theorem TauCeti.mul_factorial_dvd_prod_sq_sub_sq (k : ℕ) (x : ℤ) : (↑k + 1) * ↑(2 * k + 1).factorial ∣ ∏ m ∈ Finset.range (k + 1), (x ^ 2 - ↑m ^ 2)

The product (x² - 0²) (x² - 1²) ⋯ (x² - k²) is divisible by (k + 1) (2k + 1)! = (2k + 2)! / 2 at every integer x: twice it is a sum of two falling factorials of degree 2k + 2 (TauCeti.two_mul_prod_sq_sub_sq_eq), each a multiple of (2k + 2)! (Ring.descPochhammer_eq_factorial_smul_choose).

theorem TauCeti.prod_sq_sub_sq_eq_mul_factorial {R : Type u_1} [CommRing R] (k : ℕ) : ∏ m ∈ Finset.range (k + 1), (↑(k + 1) ^ 2 - ↑m ^ 2) = ↑((k + 1) * (2 * k + 1).factorial)

The value of (x² - 0²) (x² - 1²) ⋯ (x² - k²) at x = k + 1 is (k + 1) (2k + 1)!, which is (2k + 2)! / 2.

A polynomial in x (x + 1) as a falling factorial

theorem TauCeti.prod_sub_mul_add_add_one_eq_descPochhammer_eval {R : Type u_1} [CommRing R] (k : ℕ) (x : R) : ∏ m ∈ Finset.range k, (x - ↑m) * (x + ↑m + 1) = Polynomial.eval (x + ↑k) (descPochhammer R (2 * k))

A polynomial in x (x + 1) as a falling factorial. The product ∏_{m < k} (x - m) (x + m + 1), whose factors are x (x + 1) - m (m + 1), is the product (x + k) (x + k - 1) ⋯ (x - k + 1) of the 2k consecutive values centred at x + 1/2, that is, the falling factorial of degree 2k evaluated at x + k.

theorem TauCeti.two_mul_add_one_mul_prod_sub_mul_add_add_one_eq {R : Type u_1} [CommRing R] (k : ℕ) (x : R) : (2 * x + 1) * ∏ m ∈ Finset.range k, (x - ↑m) * (x + ↑m + 1) = Polynomial.eval (x + ↑k + 1) (descPochhammer R (2 * k + 1)) + Polynomial.eval (x + ↑k) (descPochhammer R (2 * k + 1))

The weighted polynomial in x (x + 1) as two falling factorials. Weighting ∏_{m < k} (x - m) (x + m + 1) by 2x + 1 = (x + k + 1) + (x - k) splits it into the falling factorials of degree 2k + 1 at x + k + 1 and at x + k.

theorem TauCeti.factorial_dvd_two_mul_add_one_mul_prod_sub_mul_add_add_one (k : ℕ) (x : ℤ) : ↑(2 * k + 1).factorial ∣ (2 * x + 1) * ∏ m ∈ Finset.range k, (x - ↑m) * (x + ↑m + 1)

The weighted product (2x + 1) ∏_{m < k} (x - m) (x + m + 1) is divisible by (2k + 1)! at every integer x, being a sum of two falling factorials of degree 2k + 1 (Ring.descPochhammer_eq_factorial_smul_choose).