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].

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.

Equations

• ascPochhammer S 0 = 1
• ascPochhammer S n.succ = Polynomial.X * (ascPochhammer S n).comp (Polynomial.X + 1)

@[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_descFactorial (a : ℕ) (b : ℕ) : Polynomial.eval a (ascPochhammer ℕ 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} [StrictOrderedSemiring 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.

Equations

• descPochhammer R 0 = 1
• descPochhammer R n.succ = Polynomial.X * (descPochhammer R n).comp (Polynomial.X - 1)

@[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)