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] : Nat → Polynomial S

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

Equations

• Eq (ascPochhammer S 0) 1
• Eq (ascPochhammer S n.succ) (HMul.hMul Polynomial.X ((ascPochhammer S n).comp (HAdd.hAdd Polynomial.X 1)))

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

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

theorem ascPochhammer_succ_left (S : Type u) [Semiring S] (n : Nat) : Eq (ascPochhammer S (HAdd.hAdd n 1)) (HMul.hMul Polynomial.X ((ascPochhammer S n).comp (HAdd.hAdd Polynomial.X 1)))

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

theorem ascPochhammer_map {S : Type u} [Semiring S] {T : Type v} [Semiring T] (f : RingHom S T) (n : Nat) : Eq (Polynomial.map f (ascPochhammer S n)) (ascPochhammer T n)

theorem ascPochhammer_eval₂ {S : Type u} [Semiring S] {T : Type v} [Semiring T] (f : RingHom S T) (n : Nat) (t : T) : Eq (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 : Nat) (p : Polynomial R) [Algebra R S] (x : S) : Eq (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))

theorem ascPochhammer_eval_cast (S : Type u) [Semiring S] (n k : Nat) : Eq (Polynomial.eval k (ascPochhammer Nat n)).cast (Polynomial.eval k.cast (ascPochhammer S n))

theorem ascPochhammer_eval_zero (S : Type u) [Semiring S] {n : Nat} : Eq (Polynomial.eval 0 (ascPochhammer S n)) (ite (Eq n 0) 1 0)

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

theorem ascPochhammer_ne_zero_eval_zero (S : Type u) [Semiring S] {n : Nat} (h : Ne n 0) : Eq (Polynomial.eval 0 (ascPochhammer S n)) 0

theorem ascPochhammer_succ_right (S : Type u) [Semiring S] (n : Nat) : Eq (ascPochhammer S (HAdd.hAdd n 1)) (HMul.hMul (ascPochhammer S n) (HAdd.hAdd Polynomial.X n.cast))

theorem ascPochhammer_succ_eval {S : Type u_1} [Semiring S] (n : Nat) (k : S) : Eq (Polynomial.eval k (ascPochhammer S (HAdd.hAdd n 1))) (HMul.hMul (Polynomial.eval k (ascPochhammer S n)) (HAdd.hAdd k n.cast))

theorem ascPochhammer_succ_comp_X_add_one (S : Type u) [Semiring S] (n : Nat) : Eq ((ascPochhammer S (HAdd.hAdd n 1)).comp (HAdd.hAdd Polynomial.X 1)) (HAdd.hAdd (ascPochhammer S (HAdd.hAdd n 1)) (HSMul.hSMul (HAdd.hAdd n 1) ((ascPochhammer S n).comp (HAdd.hAdd Polynomial.X 1))))

theorem ascPochhammer_mul (S : Type u) [Semiring S] (n m : Nat) : Eq (HMul.hMul (ascPochhammer S n) ((ascPochhammer S m).comp (HAdd.hAdd Polynomial.X n.cast))) (ascPochhammer S (HAdd.hAdd n m))

theorem ascPochhammer_nat_eq_ascFactorial (n k : Nat) : Eq (Polynomial.eval n (ascPochhammer Nat k)) (n.ascFactorial k)

theorem ascPochhammer_nat_eq_natCast_ascFactorial (S : Type u_1) [Semiring S] (n k : Nat) : Eq (Polynomial.eval n.cast (ascPochhammer S k)) (n.ascFactorial k).cast

theorem ascPochhammer_nat_eq_descFactorial (a b : Nat) : Eq (Polynomial.eval a (ascPochhammer Nat b)) ((HSub.hSub (HAdd.hAdd a b) 1).descFactorial b)

theorem ascPochhammer_nat_eq_natCast_descFactorial (S : Type u_1) [Semiring S] (a b : Nat) : Eq (Polynomial.eval a.cast (ascPochhammer S b)) ((HSub.hSub (HAdd.hAdd a b) 1).descFactorial b).cast

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

theorem ascPochhammer_pos {S : Type u_1} [StrictOrderedSemiring S] (n : Nat) (s : S) (h : LT.lt 0 s) : LT.lt 0 (Polynomial.eval s (ascPochhammer S n))

theorem ascPochhammer_eval_one (S : Type u_2) [Semiring S] (n : Nat) : Eq (Polynomial.eval 1 (ascPochhammer S n)) n.factorial.cast

theorem factorial_mul_ascPochhammer (S : Type u_2) [Semiring S] (r n : Nat) : Eq (HMul.hMul r.factorial.cast (Polynomial.eval (HAdd.hAdd r.cast 1) (ascPochhammer S n))) (HAdd.hAdd r n).factorial.cast

theorem ascPochhammer_nat_eval_succ (r n : Nat) : Eq (HMul.hMul n (Polynomial.eval (HAdd.hAdd n 1) (ascPochhammer Nat r))) (HMul.hMul (HAdd.hAdd n r) (Polynomial.eval n (ascPochhammer Nat r)))

theorem ascPochhammer_eval_succ (S : Type u_1) [Semiring S] (r n : Nat) : Eq (HMul.hMul n.cast (Polynomial.eval (HAdd.hAdd n.cast 1) (ascPochhammer S r))) (HMul.hMul (HAdd.hAdd n.cast r.cast) (Polynomial.eval n.cast (ascPochhammer S r)))

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

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

Equations

• Eq (descPochhammer R 0) 1
• Eq (descPochhammer R n.succ) (HMul.hMul Polynomial.X ((descPochhammer R n).comp (HSub.hSub Polynomial.X 1)))

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

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

theorem descPochhammer_succ_left (R : Type u) [Ring R] (n : Nat) : Eq (descPochhammer R (HAdd.hAdd n 1)) (HMul.hMul Polynomial.X ((descPochhammer R n).comp (HSub.hSub Polynomial.X 1)))

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

theorem descPochhammer_map {R : Type u} [Ring R] {T : Type v} [Ring T] (f : RingHom R T) (n : Nat) : Eq (Polynomial.map f (descPochhammer R n)) (descPochhammer T n)

theorem descPochhammer_eval_cast (R : Type u) [Ring R] (n : Nat) (k : Int) : Eq (Polynomial.eval k (descPochhammer Int n)).cast (Polynomial.eval k.cast (descPochhammer R n))

theorem descPochhammer_eval_zero (R : Type u) [Ring R] {n : Nat} : Eq (Polynomial.eval 0 (descPochhammer R n)) (ite (Eq n 0) 1 0)

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

theorem descPochhammer_ne_zero_eval_zero (R : Type u) [Ring R] {n : Nat} (h : Ne n 0) : Eq (Polynomial.eval 0 (descPochhammer R n)) 0

theorem descPochhammer_succ_right (R : Type u) [Ring R] (n : Nat) : Eq (descPochhammer R (HAdd.hAdd n 1)) (HMul.hMul (descPochhammer R n) (HSub.hSub Polynomial.X n.cast))

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

theorem descPochhammer_succ_eval {S : Type u_1} [Ring S] (n : Nat) (k : S) : Eq (Polynomial.eval k (descPochhammer S (HAdd.hAdd n 1))) (HMul.hMul (Polynomial.eval k (descPochhammer S n)) (HSub.hSub k n.cast))

theorem descPochhammer_succ_comp_X_sub_one (R : Type u) [Ring R] (n : Nat) : Eq ((descPochhammer R (HAdd.hAdd n 1)).comp (HSub.hSub Polynomial.X 1)) (HSub.hSub (descPochhammer R (HAdd.hAdd n 1)) (HSMul.hSMul (HAdd.hAdd n.cast 1) ((descPochhammer R n).comp (HSub.hSub Polynomial.X 1))))

theorem descPochhammer_eq_ascPochhammer (n : Nat) : Eq (descPochhammer Int n) ((ascPochhammer Int n).comp (HAdd.hAdd (HSub.hSub Polynomial.X n.cast) 1))

theorem descPochhammer_eval_eq_ascPochhammer (R : Type u) [Ring R] (r : R) (n : Nat) : Eq (Polynomial.eval r (descPochhammer R n)) (Polynomial.eval (HAdd.hAdd (HSub.hSub r n.cast) 1) (ascPochhammer R n))

theorem descPochhammer_mul (R : Type u) [Ring R] (n m : Nat) : Eq (HMul.hMul (descPochhammer R n) ((descPochhammer R m).comp (HSub.hSub Polynomial.X n.cast))) (descPochhammer R (HAdd.hAdd n m))

theorem ascPochhammer_eval_neg_eq_descPochhammer (R : Type u) [Ring R] (r : R) (k : Nat) : Eq (Polynomial.eval (Neg.neg r) (ascPochhammer R k)) (HMul.hMul (HPow.hPow (-1) k) (Polynomial.eval r (descPochhammer R k)))

theorem descPochhammer_eval_eq_descFactorial (R : Type u) [Ring R] (n k : Nat) : Eq (Polynomial.eval n.cast (descPochhammer R k)) (n.descFactorial k).cast

theorem descPochhammer_int_eq_ascFactorial (a b : Nat) : Eq (Polynomial.eval (HAdd.hAdd a.cast b.cast) (descPochhammer Int b)) ((HAdd.hAdd a 1).ascFactorial b).cast

theorem ascPochhammer_eval_neg_coe_nat_of_lt {R : Type u} [Ring R] {n k : Nat} (h : LT.lt k n) : Eq (Polynomial.eval (Neg.neg k.cast) (ascPochhammer R n)) 0

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

theorem ascPochhammer_eval_eq_zero_iff {R : Type u} [Ring R] [IsDomain R] (n : Nat) (r : R) : Iff (Eq (Polynomial.eval r (ascPochhammer R n)) 0) (Exists fun (k : Nat) => And (LT.lt k n) (Eq k.cast (Neg.neg 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 : Nat} (h : LT.lt k n) : Eq (Polynomial.eval k.cast (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 : Nat) (r : R) : Eq (Polynomial.eval r (descPochhammer R n)) ((Finset.range n).prod fun (j : Nat) => HSub.hSub r j.cast)

theorem descPochhammer_pos {S : Type u_1} [StrictOrderedRing S] {n : Nat} {s : S} (h : LT.lt (HSub.hSub n.cast 1) s) : LT.lt 0 (Polynomial.eval s (descPochhammer S n))

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

theorem descPochhammer_nonneg {S : Type u_1} [StrictOrderedRing S] {n : Nat} {s : S} (h : LE.le (HSub.hSub n.cast 1) s) : LE.le 0 (Polynomial.eval s (descPochhammer S n))

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

theorem pow_le_descPochhammer_eval {S : Type u_1} [StrictOrderedRing S] {n : Nat} {s : S} (h : LE.le (HSub.hSub n.cast 1) s) : LE.le (HPow.hPow (HAdd.hAdd (HSub.hSub s n.cast) 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} [StrictOrderedRing S] (n : Nat) : MonotoneOn (fun (a : S) => Polynomial.eval a (descPochhammer S n)) (Set.Ici (HSub.hSub n.cast 1))

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