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.
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)
Instances For
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)
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)
Instances For
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).