The Pochhammer polynomials

We define and prove some basic relations about ascPochhammer S n : S[X] := X * (X + 1) * ... * (X + n - 1) which is also known as the rising factorial and about descPochhammer R n : R[X] := X * (X - 1) * ... * (X - n + 1) which is also known as the falling factorial. Versions of this definition that are focused on Nat can be found in Data.Nat.Factorial as Nat.ascFactorial and Nat.descFactorial.

Implementation

As with many other families of polynomials, even though the coefficients are always in ℕ or ℤ , we define the polynomial with coefficients in any [Semiring S] or [Ring R]. In an integral domain S, we show that ascPochhammer S n is zero iff n is a sufficiently large non-positive integer.

TODO

There is lots more in this direction:

• q-factorials, q-binomials, q-Pochhammer.

noncomputable def ascPochhammer (S : Type u) [Semiring S] : ℕ → Polynomial S

ascPochhammer S n is the polynomial X * (X + 1) * ... * (X + n - 1), with coefficients in the semiring S.

@[simp]

theorem ascPochhammer_zero (S : Type u) [Semiring S] : ascPochhammer S 0 = 1

@[simp]

theorem ascPochhammer_one (S : Type u) [Semiring S] : ascPochhammer S 1 = Polynomial.X

theorem ascPochhammer_succ_left (S : Type u) [Semiring S] (n : ℕ) : ascPochhammer S (n + 1) = Polynomial.X * (ascPochhammer S n).comp (Polynomial.X + 1)

theorem monic_ascPochhammer (S : Type u) [Semiring S] (n : ℕ) [Nontrivial S] [NoZeroDivisors S] : (ascPochhammer S n).Monic

@[simp]

theorem ascPochhammer_map {S : Type u} [Semiring S] {T : Type v} [Semiring T] (f : S →+* T) (n : ℕ) : Polynomial.map f (ascPochhammer S n) = ascPochhammer T n

theorem ascPochhammer_eval₂ {S : Type u} [Semiring S] {T : Type v} [Semiring T] (f : S →+* T) (n : ℕ) (t : T) : Polynomial.eval t (ascPochhammer T n) = Polynomial.eval₂ f t (ascPochhammer S n)

theorem ascPochhammer_eval_comp {S : Type u} [Semiring S] {R : Type u_1} [CommSemiring R] (n : ℕ) (p : Polynomial R) [Algebra R S] (x : S) : Polynomial.eval x ((ascPochhammer S n).comp (Polynomial.map (algebraMap R S) p)) = Polynomial.eval (Polynomial.eval₂ (algebraMap R S) x p) (ascPochhammer S n)

@[simp]

theorem ascPochhammer_eval_cast (S : Type u) [Semiring S] (n k : ℕ) : ↑(Polynomial.eval k (ascPochhammer ℕ n)) = Polynomial.eval (↑k) (ascPochhammer S n)

theorem ascPochhammer_eval_zero (S : Type u) [Semiring S] {n : ℕ} : Polynomial.eval 0 (ascPochhammer S n) = if n = 0 then 1 else 0

theorem ascPochhammer_zero_eval_zero (S : Type u) [Semiring S] : Polynomial.eval 0 (ascPochhammer S 0) = 1

@[simp]

theorem ascPochhammer_ne_zero_eval_zero (S : Type u) [Semiring S] {n : ℕ} (h : n ≠ 0) : Polynomial.eval 0 (ascPochhammer S n) = 0

theorem ascPochhammer_succ_right (S : Type u) [Semiring S] (n : ℕ) : ascPochhammer S (n + 1) = ascPochhammer S n * (Polynomial.X + ↑n)

theorem ascPochhammer_succ_eval {S : Type u_1} [Semiring S] (n : ℕ) (k : S) : Polynomial.eval k (ascPochhammer S (n + 1)) = Polynomial.eval k (ascPochhammer S n) * (k + ↑n)

theorem ascPochhammer_succ_comp_X_add_one (S : Type u) [Semiring S] (n : ℕ) : (ascPochhammer S (n + 1)).comp (Polynomial.X + 1) = ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (Polynomial.X + 1)

theorem ascPochhammer_mul (S : Type u) [Semiring S] (n m : ℕ) : ascPochhammer S n * (ascPochhammer S m).comp (Polynomial.X + ↑n) = ascPochhammer S (n + m)

theorem ascPochhammer_nat_eq_ascFactorial (n k : ℕ) : Polynomial.eval n (ascPochhammer ℕ k) = n.ascFactorial k

theorem ascPochhammer_nat_eq_natCast_ascFactorial (S : Type u_1) [Semiring S] (n k : ℕ) : Polynomial.eval (↑n) (ascPochhammer S k) = ↑(n.ascFactorial k)

theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) : Polynomial.eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b

theorem ascPochhammer_nat_eq_natCast_descFactorial (S : Type u_1) [Semiring S] (a b : ℕ) : Polynomial.eval (↑a) (ascPochhammer S b) = ↑((a + b - 1).descFactorial b)

@[simp]

theorem ascPochhammer_natDegree (S : Type u) [Semiring S] (n : ℕ) [NoZeroDivisors S] [Nontrivial S] : (ascPochhammer S n).natDegree = n

theorem ascPochhammer_pos {S : Type u_1} [Semiring S] [PartialOrder S] [IsStrictOrderedRing S] (n : ℕ) (s : S) (h : 0 < s) : 0 < Polynomial.eval s (ascPochhammer S n)

@[simp]

theorem ascPochhammer_eval_one (S : Type u_2) [Semiring S] (n : ℕ) : Polynomial.eval 1 (ascPochhammer S n) = ↑n.factorial

theorem factorial_mul_ascPochhammer (S : Type u_2) [Semiring S] (r n : ℕ) : ↑r.factorial * Polynomial.eval (↑r + 1) (ascPochhammer S n) = ↑(r + n).factorial

theorem ascPochhammer_nat_eval_succ (r n : ℕ) : n * Polynomial.eval (n + 1) (ascPochhammer ℕ r) = (n + r) * Polynomial.eval n (ascPochhammer ℕ r)

theorem ascPochhammer_eval_succ (S : Type u_1) [Semiring S] (r n : ℕ) : ↑n * Polynomial.eval (↑n + 1) (ascPochhammer S r) = (↑n + ↑r) * Polynomial.eval (↑n) (ascPochhammer S r)

noncomputable def descPochhammer (R : Type u) [Ring R] : ℕ → Polynomial R

descPochhammer R n is the polynomial X * (X - 1) * ... * (X - n + 1), with coefficients in the ring R.

@[simp]

theorem descPochhammer_zero (R : Type u) [Ring R] : descPochhammer R 0 = 1

@[simp]

theorem descPochhammer_one (R : Type u) [Ring R] : descPochhammer R 1 = Polynomial.X

theorem descPochhammer_succ_left (R : Type u) [Ring R] (n : ℕ) : descPochhammer R (n + 1) = Polynomial.X * (descPochhammer R n).comp (Polynomial.X - 1)

theorem monic_descPochhammer (R : Type u) [Ring R] (n : ℕ) [Nontrivial R] [NoZeroDivisors R] : (descPochhammer R n).Monic

@[simp]

theorem descPochhammer_map {R : Type u} [Ring R] {T : Type v} [Ring T] (f : R →+* T) (n : ℕ) : Polynomial.map f (descPochhammer R n) = descPochhammer T n

@[simp]

theorem descPochhammer_eval_cast (R : Type u) [Ring R] (n : ℕ) (k : ℤ) : ↑(Polynomial.eval k (descPochhammer ℤ n)) = Polynomial.eval (↑k) (descPochhammer R n)

theorem descPochhammer_eval_zero (R : Type u) [Ring R] {n : ℕ} : Polynomial.eval 0 (descPochhammer R n) = if n = 0 then 1 else 0

theorem descPochhammer_zero_eval_zero (R : Type u) [Ring R] : Polynomial.eval 0 (descPochhammer R 0) = 1

@[simp]

theorem descPochhammer_ne_zero_eval_zero (R : Type u) [Ring R] {n : ℕ} (h : n ≠ 0) : Polynomial.eval 0 (descPochhammer R n) = 0

theorem descPochhammer_succ_right (R : Type u) [Ring R] (n : ℕ) : descPochhammer R (n + 1) = descPochhammer R n * (Polynomial.X - ↑n)

@[simp]

theorem descPochhammer_natDegree (R : Type u) [Ring R] (n : ℕ) [NoZeroDivisors R] [Nontrivial R] : (descPochhammer R n).natDegree = n

theorem descPochhammer_succ_eval {S : Type u_1} [Ring S] (n : ℕ) (k : S) : Polynomial.eval k (descPochhammer S (n + 1)) = Polynomial.eval k (descPochhammer S n) * (k - ↑n)

theorem descPochhammer_succ_comp_X_sub_one (R : Type u) [Ring R] (n : ℕ) : (descPochhammer R (n + 1)).comp (Polynomial.X - 1) = descPochhammer R (n + 1) - (↑n + 1) • (descPochhammer R n).comp (Polynomial.X - 1)

theorem descPochhammer_eq_ascPochhammer (n : ℕ) : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (Polynomial.X - ↑n + 1)

theorem descPochhammer_eval_eq_ascPochhammer (R : Type u) [Ring R] (r : R) (n : ℕ) : Polynomial.eval r (descPochhammer R n) = Polynomial.eval (r - ↑n + 1) (ascPochhammer R n)

theorem descPochhammer_mul (R : Type u) [Ring R] (n m : ℕ) : descPochhammer R n * (descPochhammer R m).comp (Polynomial.X - ↑n) = descPochhammer R (n + m)

theorem ascPochhammer_eval_neg_eq_descPochhammer (R : Type u) [Ring R] (r : R) (k : ℕ) : Polynomial.eval (-r) (ascPochhammer R k) = (-1) ^ k * Polynomial.eval r (descPochhammer R k)

theorem descPochhammer_eval_eq_descFactorial (R : Type u) [Ring R] (n k : ℕ) : Polynomial.eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)

theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) : Polynomial.eval (↑a + ↑b) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)

theorem ascPochhammer_eval_neg_coe_nat_of_lt {R : Type u} [Ring R] {n k : ℕ} (h : k < n) : Polynomial.eval (-↑k) (ascPochhammer R n) = 0

The Pochhammer polynomial of degree n has roots at 0, -1, ..., -(n - 1).

@[simp]

theorem ascPochhammer_eval_eq_zero_iff {R : Type u} [Ring R] [IsDomain R] (n : ℕ) (r : R) : Polynomial.eval r (ascPochhammer R n) = 0 ↔ ∃ k < n, ↑k = -r

Over an integral domain, the Pochhammer polynomial of degree n has roots only at 0, -1, ..., -(n - 1).

theorem descPochhammer_eval_coe_nat_of_lt {R : Type u} [Ring R] {k n : ℕ} (h : k < n) : Polynomial.eval (↑k) (descPochhammer R n) = 0

descPochhammer R n is 0 for 0, 1, …, n-1.

theorem descPochhammer_eval_eq_prod_range {R : Type u_1} [CommRing R] (n : ℕ) (r : R) : Polynomial.eval r (descPochhammer R n) = ∏ j ∈ Finset.range n, (r - ↑j)

theorem descPochhammer_pos {S : Type u_1} [Ring S] [PartialOrder S] [IsStrictOrderedRing S] {n : ℕ} {s : S} (h : ↑n - 1 < s) : 0 < Polynomial.eval s (descPochhammer S n)

descPochhammer S n is positive on (n-1, ∞).

theorem descPochhammer_nonneg {S : Type u_1} [Ring S] [PartialOrder S] [IsStrictOrderedRing S] {n : ℕ} {s : S} (h : ↑n - 1 ≤ s) : 0 ≤ Polynomial.eval s (descPochhammer S n)

descPochhammer S n is nonnegative on [n-1, ∞).

theorem pow_le_descPochhammer_eval {S : Type u_1} [Ring S] [PartialOrder S] [IsStrictOrderedRing S] {n : ℕ} {s : S} (h : ↑n - 1 ≤ s) : (s - ↑n + 1) ^ n ≤ Polynomial.eval s (descPochhammer S n)

descPochhammer S n is at least (s-n+1)^n on [n-1, ∞).

theorem monotoneOn_descPochhammer_eval {S : Type u_1} [Ring S] [PartialOrder S] [IsStrictOrderedRing S] (n : ℕ) : MonotoneOn (fun (a : S) => Polynomial.eval a (descPochhammer S n)) (Set.Ici (↑n - 1))

descPochhammer S n is monotone on [n-1, ∞).