Documentation

Mathlib.RingTheory.Polynomial.Pochhammer

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:

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

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

Equations
Instances For
    @[simp]
    theorem ascPochhammer_zero (S : Type u) [Semiring S] :
    @[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 : ) :
    theorem ascPochhammer_eval₂ {S : Type u} [Semiring S] {T : Type v} [Semiring T] (f : S →+* T) (n : ) (t : T) :
    @[simp]
    theorem ascPochhammer_eval_zero (S : Type u) [Semiring S] {n : } :
    Polynomial.eval 0 (ascPochhammer S n) = if n = 0 then 1 else 0
    @[simp]
    theorem ascPochhammer_ne_zero_eval_zero (S : Type u) [Semiring S] {n : } (h : 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) :
    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_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) :
    @[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_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] :

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

    Equations
    Instances For
      @[simp]
      theorem descPochhammer_zero (R : Type u) [Ring R] :
      @[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 : ) :
      @[simp]
      theorem descPochhammer_eval_cast (R : Type u) [Ring R] (n : ) (k : ) :
      theorem descPochhammer_eval_zero (R : Type u) [Ring R] {n : } :
      Polynomial.eval 0 (descPochhammer R n) = if n = 0 then 1 else 0
      @[simp]
      theorem descPochhammer_ne_zero_eval_zero (R : Type u) [Ring R] {n : } (h : 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) :
      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_mul (R : Type u) [Ring R] (n : ) (m : ) :
      descPochhammer R n * (descPochhammer R m).comp (Polynomial.X - n) = descPochhammer R (n + m)
      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)