mathlib3 documentation

ring_theory.polynomial.pochhammer

The Pochhammer polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define and prove some basic relations about pochhammer S n : S[X] := X * (X + 1) * ... * (X + n - 1) which is also known as the rising factorial. A version of this definition that is focused on nat can be found in data.nat.factorial as nat.asc_factorial.

Implementation #

As with many other families of polynomials, even though the coefficients are always in ℕ, we define the polynomial with coefficients in any [semiring S].

TODO #

There is lots more in this direction:

source
noncomputable def pochhammer (S : Type u) [semiring S] :
ℕ → polynomial S

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

Equations
source
@[simp]
theorem pochhammer_zero (S : Type u) [semiring S] :
pochhammer S 0 = 1
source
@[simp]
theorem pochhammer_one (S : Type u) [semiring S] :
pochhammer S 1 = polynomial.X
source
theorem pochhammer_succ_left (S : Type u) [semiring S] (n : ℕ) :
pochhammer S (n + 1) = polynomial.X * (pochhammer S n).comp (polynomial.X + 1)
source
@[simp]
theorem pochhammer_map {S : Type u} [semiring S] {T : Type v} [semiring T] (f : S →+* T) (n : ℕ) :
polynomial.map f (pochhammer S n) = pochhammer T n
source
@[simp, norm_cast]
theorem pochhammer_eval_cast (S : Type u) [semiring S] (n k : ℕ) :
↑(polynomial.eval k (pochhammer ℕ n)) = polynomial.eval ↑k (pochhammer S n)
source
theorem pochhammer_eval_zero (S : Type u) [semiring S] {n : ℕ} :
polynomial.eval 0 (pochhammer S n) = ite (n = 0) 1 0
source
theorem pochhammer_zero_eval_zero (S : Type u) [semiring S] :
polynomial.eval 0 (pochhammer S 0) = 1
source
@[simp]
theorem pochhammer_ne_zero_eval_zero (S : Type u) [semiring S] {n : ℕ} (h : n ≠ 0) :
polynomial.eval 0 (pochhammer S n) = 0
source
theorem pochhammer_succ_right (S : Type u) [semiring S] (n : ℕ) :
pochhammer S (n + 1) = pochhammer S n * (polynomial.X + ↑n)
source
theorem pochhammer_succ_eval {S : Type u_1} [semiring S] (n : ℕ) (k : S) :
polynomial.eval k (pochhammer S (n + 1)) = polynomial.eval k (pochhammer S n) * (k + ↑n)
source
theorem pochhammer_succ_comp_X_add_one (S : Type u) [semiring S] (n : ℕ) :
(pochhammer S (n + 1)).comp (polynomial.X + 1) = pochhammer S (n + 1) + (n + 1) • (pochhammer S n).comp (polynomial.X + 1)
source
theorem polynomial.mul_X_add_nat_cast_comp (S : Type u) [semiring S] {p q : polynomial S} {n : ℕ} :
(p * (polynomial.X + ↑n)).comp q = p.comp q * (q + ↑n)
source
theorem pochhammer_mul (S : Type u) [semiring S] (n m : ℕ) :
pochhammer S n * (pochhammer S m).comp (polynomial.X + ↑n) = pochhammer S (n + m)
source
theorem pochhammer_nat_eq_asc_factorial (n k : ℕ) :
polynomial.eval (n + 1) (pochhammer ℕ k) = n.asc_factorial k
source
theorem pochhammer_nat_eq_desc_factorial (a b : ℕ) :
polynomial.eval a (pochhammer ℕ b) = (a + b - 1).desc_factorial b
source
theorem pochhammer_pos {S : Type u_1} [strict_ordered_semiring S] (n : ℕ) (s : S) (h : 0 < s) :
0 < polynomial.eval s (pochhammer S n)
source
@[simp]
theorem pochhammer_eval_one (S : Type u_1) [semiring S] (n : ℕ) :
polynomial.eval 1 (pochhammer S n) = ↑(n.factorial)
source
theorem factorial_mul_pochhammer (S : Type u_1) [semiring S] (r n : ℕ) :
↑(r.factorial) * polynomial.eval (↑r + 1) (pochhammer S n) = ↑((r + n).factorial)
source
theorem pochhammer_nat_eval_succ (r n : ℕ) :
n * polynomial.eval (n + 1) (pochhammer ℕ r) = (n + r) * polynomial.eval n (pochhammer ℕ r)
source
theorem pochhammer_eval_succ (S : Type u_1) [semiring S] (r n : ℕ) :
↑n * polynomial.eval (↑n + 1) (pochhammer S r) = (↑n + ↑r) * polynomial.eval ↑n (pochhammer S r)