Mathlib.RingTheory.Polynomial.Pochhammer

ascPochhammer definition

: ℕ → S[X]

Full source

/-- `ascPochhammer S n` is the polynomial `X * (X + 1) * ... * (X + n - 1)`,
with coefficients in the semiring `S`.
-/
noncomputable def ascPochhammer : ℕ → S[X]
  | 0 => 1
  | n + 1 => X * (ascPochhammer n).comp (X + 1)

Rising factorial (Pochhammer) polynomial

Informal description

The rising factorial polynomial (also known as Pochhammer polynomial) $\text{ascPochhammer}_S(n) \in S[X]$ is defined recursively by: - $\text{ascPochhammer}_S(0) = 1$ - $\text{ascPochhammer}_S(n+1) = X \cdot \text{ascPochhammer}_S(n)(X + 1)$ This gives the polynomial $X(X+1)(X+2)\cdots(X+n-1)$ with coefficients in the semiring $S$.

ascPochhammer_zero theorem

: ascPochhammer S 0 = 1

Full source

@[simp]
theorem ascPochhammer_zero : ascPochhammer S 0 = 1 :=
  rfl

Base Case for Rising Factorial Polynomial: $\text{ascPochhammer}_S(0) = 1$

Informal description

The rising factorial polynomial (Pochhammer polynomial) of degree 0 is the constant polynomial 1, i.e., $\text{ascPochhammer}_S(0) = 1$.

ascPochhammer_one theorem

: ascPochhammer S 1 = X

Full source

@[simp]
theorem ascPochhammer_one : ascPochhammer S 1 = X := by simp [ascPochhammer]

First Degree Rising Factorial Polynomial: $\text{ascPochhammer}_S(1) = X$

Informal description

The rising factorial polynomial of degree 1 is equal to the indeterminate $X$, i.e., $\text{ascPochhammer}_S(1) = X$.

ascPochhammer_succ_left theorem

(n : ℕ) : ascPochhammer S (n + 1) = X * (ascPochhammer S n).comp (X + 1)

Full source

theorem ascPochhammer_succ_left (n : ℕ) :
    ascPochhammer S (n + 1) = X * (ascPochhammer S n).comp (X + 1) := by
  rw [ascPochhammer]

Recurrence Relation for Rising Factorial Polynomials

Informal description

For any natural number $n$, the $(n+1)$-th rising factorial polynomial satisfies the recurrence relation: $$ \text{ascPochhammer}_S(n+1) = X \cdot \text{ascPochhammer}_S(n)(X + 1) $$ where $\text{ascPochhammer}_S(n)(X + 1)$ denotes the composition of the $n$-th rising factorial polynomial with $X + 1$.

monic_ascPochhammer theorem

(n : ℕ) [Nontrivial S] [NoZeroDivisors S] : Monic <| ascPochhammer S n

Full source

theorem monic_ascPochhammer (n : ℕ) [Nontrivial S] [NoZeroDivisors S] :
    Monic <| ascPochhammer S n := by
  induction' n with n hn
  · simp
  · have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1
    rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegreenatDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]

Monic Property of Rising Factorial Polynomials

Informal description

For any natural number $n$ and any nontrivial semiring $S$ with no zero divisors, the rising factorial polynomial $\text{ascPochhammer}_S(n) = X(X+1)\cdots(X+n-1)$ is monic (i.e., its leading coefficient is 1).

ascPochhammer_map theorem

(f : S →+* T) (n : ℕ) : (ascPochhammer S n).map f = ascPochhammer T n

Full source

@[simp]
theorem ascPochhammer_map (f : S →+* T) (n : ℕ) :
    (ascPochhammer S n).map f = ascPochhammer T n := by
  induction n with
  | zero => simp
  | succ n ih => simp [ih, ascPochhammer_succ_left, map_comp]

Rising Factorial Polynomials are Preserved under Semiring Homomorphisms

Informal description

For any semiring homomorphism $f: S \to T$ and natural number $n$, the map of the rising factorial polynomial $\text{ascPochhammer}_S(n)$ under $f$ equals the rising factorial polynomial $\text{ascPochhammer}_T(n)$. That is, $$ f_*(\text{ascPochhammer}_S(n)) = \text{ascPochhammer}_T(n) $$ where $f_*$ denotes the polynomial map induced by $f$.

ascPochhammer_eval₂ theorem

(f : S →+* T) (n : ℕ) (t : T) : (ascPochhammer T n).eval t = (ascPochhammer S n).eval₂ f t

Full source

theorem ascPochhammer_eval₂ (f : S →+* T) (n : ℕ) (t : T) :
    (ascPochhammer T n).eval t = (ascPochhammer S n).eval₂ f t := by
  rw [← ascPochhammer_map f]
  exact eval_map f t

Evaluation of Rising Factorial Polynomials under Semiring Homomorphism

Informal description

For any semiring homomorphism $f: S \to T$, natural number $n$, and element $t \in T$, the evaluation of the rising factorial polynomial $\text{ascPochhammer}_T(n)$ at $t$ equals the evaluation of $\text{ascPochhammer}_S(n)$ at $t$ via the homomorphism $f$. That is, $$ \text{ascPochhammer}_T(n)(t) = \text{ascPochhammer}_S(n)(f(t)) $$ where $f(t)$ denotes the application of $f$ to the coefficients of the polynomial.

ascPochhammer_eval_comp theorem

 {R : Type*} [CommSemiring R] (n : ℕ) (p : R[X]) [Algebra R S] (x : S) :
  ((ascPochhammer S n).comp (p.map (algebraMap R S))).eval x = (ascPochhammer S n).eval (p.eval₂ (algebraMap R S) x)

Full source

theorem ascPochhammer_eval_comp {R : Type*} [CommSemiring R] (n : ℕ) (p : R[X]) [Algebra R S]
    (x : S) : ((ascPochhammer S n).comp (p.map (algebraMap R S))).eval x =
    (ascPochhammer S n).eval (p.eval₂ (algebraMap R S) x) := by
  rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]

Composition-Evaluation Commutation for Rising Factorial Polynomials

Informal description

Let $R$ be a commutative semiring and $S$ an $R$-algebra. For any natural number $n$, polynomial $p \in R[X]$, and element $x \in S$, the evaluation of the composition of the rising factorial polynomial $\text{ascPochhammer}_S(n)$ with $p$ (mapped to $S[X]$ via the algebra map) at $x$ equals the evaluation of $\text{ascPochhammer}_S(n)$ at $p(x)$. That is, $$ \left(\text{ascPochhammer}_S(n) \circ p_S\right)(x) = \text{ascPochhammer}_S(n)(p(x)) $$ where $p_S$ denotes the polynomial $p$ with coefficients mapped to $S$ via the algebra map $R \to S$.

ascPochhammer_eval_cast theorem

(n k : ℕ) : (((ascPochhammer ℕ n).eval k : ℕ) : S) = ((ascPochhammer S n).eval k : S)

Full source

@[simp, norm_cast]
theorem ascPochhammer_eval_cast (n k : ℕ) :
    (((ascPochhammer ℕ n).eval k : ℕ) : S) = ((ascPochhammer S n).eval k : S) := by
  rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast,Nat.cast_id]

Natural Number Coefficients Preserved Under Semiring Cast for Rising Factorial Evaluation

Informal description

For any natural numbers $n$ and $k$, the evaluation of the rising factorial polynomial $\text{ascPochhammer}_{\mathbb{N}}(n)$ at $k$, when cast to a semiring $S$, equals the evaluation of $\text{ascPochhammer}_S(n)$ at $k$. That is, $$ \left(\text{ascPochhammer}_{\mathbb{N}}(n)(k)\right)_S = \text{ascPochhammer}_S(n)(k) $$ where $(\cdot)_S$ denotes the canonical map from $\mathbb{N}$ to $S$.

ascPochhammer_eval_zero theorem

{n : ℕ} : (ascPochhammer S n).eval 0 = if n = 0 then 1 else 0

Full source

theorem ascPochhammer_eval_zero {n : ℕ} : (ascPochhammer S n).eval 0 = if n = 0 then 1 else 0 := by
  cases n
  · simp
  · simp [X_mul, Nat.succ_ne_zero, ascPochhammer_succ_left]

Evaluation of Rising Factorial at Zero: $\text{ascPochhammer}_S(n)(0) = \delta_{n0}$

Informal description

For any natural number $n$, the evaluation of the rising factorial polynomial $\text{ascPochhammer}_S(n)$ at $0$ is equal to $1$ if $n = 0$ and $0$ otherwise. That is, $$ \text{ascPochhammer}_S(n)(0) = \begin{cases} 1 & \text{if } n = 0, \\ 0 & \text{otherwise.} \end{cases} $$

ascPochhammer_zero_eval_zero theorem

: (ascPochhammer S 0).eval 0 = 1

Full source

theorem ascPochhammer_zero_eval_zero : (ascPochhammer S 0).eval 0 = 1 := by simp

Evaluation of Zero-th Rising Factorial at Zero is One

Informal description

The evaluation of the rising factorial polynomial $\text{ascPochhammer}_S(0)$ at $0$ equals $1$, i.e., $\text{ascPochhammer}_S(0)(0) = 1$.

ascPochhammer_ne_zero_eval_zero theorem

{n : ℕ} (h : n ≠ 0) : (ascPochhammer S n).eval 0 = 0

Full source

@[simp]
theorem ascPochhammer_ne_zero_eval_zero {n : ℕ} (h : n ≠ 0) : (ascPochhammer S n).eval 0 = 0 := by
  simp [ascPochhammer_eval_zero, h]

Vanishing of Rising Factorial at Zero for Nonzero $n$

Informal description

For any natural number $n \neq 0$, the evaluation of the rising factorial polynomial $\text{ascPochhammer}_S(n)$ at $0$ is equal to $0$, i.e., $\text{ascPochhammer}_S(n)(0) = 0$.

ascPochhammer_succ_right theorem

(n : ℕ) : ascPochhammer S (n + 1) = ascPochhammer S n * (X + (n : S[X]))

Full source

theorem ascPochhammer_succ_right (n : ℕ) :
    ascPochhammer S (n + 1) = ascPochhammer S n * (X + (n : S[X])) := by
  suffices h : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + (n : ℕℕ[X])) by
    apply_fun Polynomial.map (algebraMap ℕ S) at h
    simpa only [ascPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_natCast] using h
  induction n with
  | zero => simp
  | succ n ih =>
    conv_lhs =>
      rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕℕ[X]), ← Nat.cast_succ]

Recurrence relation for rising factorial polynomials: $\text{ascPochhammer}_S(n+1) = \text{ascPochhammer}_S(n)(X + n)$

Informal description

For any natural number $n$, the $(n+1)$-th rising factorial polynomial satisfies the recurrence relation: $$ \text{ascPochhammer}_S(n+1) = \text{ascPochhammer}_S(n) \cdot (X + n) $$ where $n$ is interpreted as a constant polynomial in $S[X]$.

ascPochhammer_succ_eval theorem

{S : Type*} [Semiring S] (n : ℕ) (k : S) : (ascPochhammer S (n + 1)).eval k = (ascPochhammer S n).eval k * (k + n)

Full source

theorem ascPochhammer_succ_eval {S : Type*} [Semiring S] (n : ℕ) (k : S) :
    (ascPochhammer S (n + 1)).eval k = (ascPochhammer S n).eval k * (k + n) := by
  rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]

Evaluation Recurrence for Rising Factorial Polynomials: $\text{ascPochhammer}_S(n+1)(k) = \text{ascPochhammer}_S(n)(k) \cdot (k + n)$

Informal description

For any semiring $S$, natural number $n$, and element $k \in S$, the evaluation of the $(n+1)$-th rising factorial polynomial at $k$ satisfies: $$ \text{ascPochhammer}_S(n+1)(k) = \text{ascPochhammer}_S(n)(k) \cdot (k + n) $$

ascPochhammer_succ_comp_X_add_one theorem

 (n : ℕ) : (ascPochhammer S (n + 1)).comp (X + 1) = ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (X + 1)

Full source

theorem ascPochhammer_succ_comp_X_add_one (n : ℕ) :
    (ascPochhammer S (n + 1)).comp (X + 1) =
      ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (X + 1) := by
  suffices (ascPochhammer ℕ (n + 1)).comp (X + 1) =
      ascPochhammer ℕ (n + 1) + (n + 1) * (ascPochhammer ℕ n).comp (X + 1)
    by simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
  nth_rw 2 [ascPochhammer_succ_left]
  rw [← add_mul, ascPochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, natCast_comp,
    add_comm, ← add_assoc]
  ring

Composition Identity for Rising Factorial Polynomials: $\text{ascPochhammer}_S(n+1)(X + 1) = \text{ascPochhammer}_S(n+1) + (n + 1) \cdot \text{ascPochhammer}_S(n)(X + 1)$

Informal description

For any natural number $n$, the composition of the $(n+1)$-th rising factorial polynomial $\text{ascPochhammer}_S(n+1)$ with the polynomial $X + 1$ satisfies: $$ \text{ascPochhammer}_S(n+1)(X + 1) = \text{ascPochhammer}_S(n+1) + (n + 1) \cdot \text{ascPochhammer}_S(n)(X + 1) $$ where $\text{ascPochhammer}_S(n)(X + 1)$ denotes the composition of the $n$-th rising factorial polynomial with $X + 1$, and $(n + 1) \cdot$ denotes the scalar multiplication by $n + 1$ in the polynomial ring $S[X]$.

ascPochhammer_mul theorem

(n m : ℕ) : ascPochhammer S n * (ascPochhammer S m).comp (X + (n : S[X])) = ascPochhammer S (n + m)

Full source

theorem ascPochhammer_mul (n m : ℕ) :
    ascPochhammer S n * (ascPochhammer S m).comp (X + (n : S[X])) = ascPochhammer S (n + m) := by
  induction' m with m ih
  · simp
  · rw [ascPochhammer_succ_right, Polynomial.mul_X_add_natCast_comp, ← mul_assoc, ih,
      ← add_assoc, ascPochhammer_succ_right, Nat.cast_add, add_assoc]

Product Formula for Rising Factorial Polynomials: $\text{ascPochhammer}_S(n) \cdot \text{ascPochhammer}_S(m)(X + n) = \text{ascPochhammer}_S(n + m)$

Informal description

For any natural numbers $n$ and $m$, the product of the rising factorial polynomial $\text{ascPochhammer}_S(n)$ and the composition of $\text{ascPochhammer}_S(m)$ with the polynomial $X + n$ equals the rising factorial polynomial $\text{ascPochhammer}_S(n + m)$. In other words: $$ \text{ascPochhammer}_S(n) \cdot \text{ascPochhammer}_S(m)(X + n) = \text{ascPochhammer}_S(n + m) $$ where $n$ is interpreted as a constant polynomial in $S[X]$.

ascPochhammer_nat_eq_ascFactorial theorem

(n : ℕ) : ∀ k, (ascPochhammer ℕ k).eval n = n.ascFactorial k

Full source

theorem ascPochhammer_nat_eq_ascFactorial (n : ℕ) :
    ∀ k, (ascPochhammer ℕ k).eval n = n.ascFactorial k
  | 0 => by rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]
  | t + 1 => by
    rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]

Evaluation of Rising Factorial Polynomial at Natural Number Equals Ascending Factorial: $\text{ascPochhammer}_{\mathbb{N}}(k)(n) = n^{\overline{k}}$

Informal description

For any natural numbers $n$ and $k$, evaluating the rising factorial polynomial $\text{ascPochhammer}_{\mathbb{N}}(k)$ at $n$ yields the ascending factorial $n^{\overline{k}}$, i.e., $$ \text{ascPochhammer}_{\mathbb{N}}(k)(n) = n^{\overline{k}} $$ where $n^{\overline{k}} = n(n+1)(n+2)\cdots(n+k-1)$ is the ascending factorial of $n$ with $k$ factors.

ascPochhammer_nat_eq_natCast_ascFactorial theorem

(S : Type*) [Semiring S] (n k : ℕ) : (ascPochhammer S k).eval (n : S) = n.ascFactorial k

Full source

theorem ascPochhammer_nat_eq_natCast_ascFactorial (S : Type*) [Semiring S] (n k : ℕ) :
    (ascPochhammer S k).eval (n : S) = n.ascFactorial k := by
  norm_cast
  rw [ascPochhammer_nat_eq_ascFactorial]

Evaluation of Rising Factorial Polynomial at Natural Number via Ascending Factorial: $\text{ascPochhammer}_S(k)(n) = n^{\overline{k}}$

Informal description

For any semiring $S$ and natural numbers $n$ and $k$, evaluating the rising factorial polynomial $\text{ascPochhammer}_S(k)$ at the natural number $n$ (viewed as an element of $S$ via the canonical map $\mathbb{N} \to S$) yields the ascending factorial $n^{\overline{k}}$. That is, $$ \text{ascPochhammer}_S(k)(n) = n^{\overline{k}} $$ where $n^{\overline{k}} = n(n+1)(n+2)\cdots(n+k-1)$ is the ascending factorial.

ascPochhammer_nat_eq_descFactorial theorem

(a b : ℕ) : (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b

Full source

theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) :
    (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b := by
  rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']

Evaluation of Rising Factorial Polynomial at Natural Number Equals Descending Factorial: $\text{ascPochhammer}_{\mathbb{N}}(b)(a) = (a + b - 1)^{\underline{b}}$

Informal description

For any natural numbers $a$ and $b$, evaluating the rising factorial polynomial $\text{ascPochhammer}_{\mathbb{N}}(b)$ at $a$ yields the descending factorial $(a + b - 1)^{\underline{b}}$, i.e., $$ \text{ascPochhammer}_{\mathbb{N}}(b)(a) = (a + b - 1)^{\underline{b}} $$ where $n^{\underline{k}} = n(n-1)(n-2)\cdots(n-k+1)$ is the descending factorial of $n$ with $k$ factors.

ascPochhammer_nat_eq_natCast_descFactorial theorem

(S : Type*) [Semiring S] (a b : ℕ) : (ascPochhammer S b).eval (a : S) = (a + b - 1).descFactorial b

Full source

theorem ascPochhammer_nat_eq_natCast_descFactorial (S : Type*) [Semiring S] (a b : ℕ) :
    (ascPochhammer S b).eval (a : S) = (a + b - 1).descFactorial b := by
  norm_cast
  rw [ascPochhammer_nat_eq_descFactorial]

Evaluation of Rising Factorial Polynomial via Descending Factorial: $\text{ascPochhammer}_S(b)(a) = (a + b - 1)^{\underline{b}}$

Informal description

For any semiring $S$ and natural numbers $a$ and $b$, evaluating the rising factorial polynomial $\text{ascPochhammer}_S(b)$ at the natural number $a$ (viewed as an element of $S$ via the canonical map $\mathbb{N} \to S$) yields the descending factorial $(a + b - 1)^{\underline{b}}$. That is, $$ \text{ascPochhammer}_S(b)(a) = (a + b - 1)^{\underline{b}} $$ where $n^{\underline{k}} = n(n-1)(n-2)\cdots(n-k+1)$ is the descending factorial of $n$ with $k$ factors.

ascPochhammer_natDegree theorem

(n : ℕ) [NoZeroDivisors S] [Nontrivial S] : (ascPochhammer S n).natDegree = n

Full source

@[simp]
theorem ascPochhammer_natDegree (n : ℕ) [NoZeroDivisors S] [Nontrivial S] :
    (ascPochhammer S n).natDegree = n := by
  induction' n with n hn
  · simp
  · have : natDegree (X + (n : S[X])) = 1 := natDegree_X_add_C (n : S)
    rw [ascPochhammer_succ_right,
        natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]
    cases n
    · simp
    · refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

Natural Degree of Rising Factorial Polynomial Equals Its Parameter

Informal description

For any natural number $n$ and any semiring $S$ with no zero divisors and at least two distinct elements, the natural degree of the rising factorial polynomial $\text{ascPochhammer}_S(n)$ is equal to $n$.

ascPochhammer_pos theorem

(n : ℕ) (s : S) (h : 0 < s) : 0 < (ascPochhammer S n).eval s

Full source

theorem ascPochhammer_pos (n : ℕ) (s : S) (h : 0 < s) : 0 < (ascPochhammer S n).eval s := by
  induction n with
  | zero =>
    simp only [ascPochhammer_zero, eval_one]
    exact zero_lt_one
  | succ n ih =>
    rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X,
      Nat.cast_comm, ← mul_add]
    exact mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))

Positivity of Rising Factorial Polynomial Evaluation at Positive Points

Informal description

For any natural number $n$ and any element $s$ in a semiring $S$ with $s > 0$, the evaluation of the rising factorial polynomial $\text{ascPochhammer}_S(n)$ at $s$ is positive, i.e., $\text{ascPochhammer}_S(n)(s) > 0$.

ascPochhammer_eval_one theorem

(S : Type*) [Semiring S] (n : ℕ) : (ascPochhammer S n).eval (1 : S) = (n ! : S)

Full source

@[simp]
theorem ascPochhammer_eval_one (S : Type*) [Semiring S] (n : ℕ) :
    (ascPochhammer S n).eval (1 : S) = (n ! : S) := by
  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.one_ascFactorial]

Evaluation of Rising Factorial at One Equals Factorial: $\text{ascPochhammer}_S(n)(1) = n!$

Informal description

For any semiring $S$ and natural number $n$, evaluating the rising factorial polynomial $\text{ascPochhammer}_S(n)$ at $1 \in S$ yields the factorial of $n$ in $S$, i.e., $$ \text{ascPochhammer}_S(n)(1) = n! $$ where $n!$ denotes the factorial of $n$ interpreted in $S$.

factorial_mul_ascPochhammer theorem

(S : Type*) [Semiring S] (r n : ℕ) : (r ! : S) * (ascPochhammer S n).eval (r + 1 : S) = (r + n)!

Full source

theorem factorial_mul_ascPochhammer (S : Type*) [Semiring S] (r n : ℕ) :
    (r ! : S) * (ascPochhammer S n).eval (r + 1 : S) = (r + n)! := by
  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]

Factorial-Rising Factorial Identity: $r! \cdot (r+1)^{\overline{n}} = (r+n)!$

Informal description

For any semiring $S$ and natural numbers $r$ and $n$, the product of the factorial $r!$ (viewed as an element of $S$) with the evaluation of the rising factorial polynomial $\text{ascPochhammer}_S(n)$ at $r+1$ equals the factorial $(r+n)!$ in $S$. That is, $$ r! \cdot \text{ascPochhammer}_S(n)(r+1) = (r+n)! $$ where $\text{ascPochhammer}_S(n)(X) = X(X+1)\cdots(X+n-1)$.

ascPochhammer_nat_eval_succ theorem

(r : ℕ) : ∀ n : ℕ, n * (ascPochhammer ℕ r).eval (n + 1) = (n + r) * (ascPochhammer ℕ r).eval n

Full source

theorem ascPochhammer_nat_eval_succ (r : ℕ) :
    ∀ n : ℕ, n * (ascPochhammer ℕ r).eval (n + 1) = (n + r) * (ascPochhammer ℕ r).eval n
  | 0 => by
    by_cases h : r = 0
    · simp only [h, zero_mul, zero_add]
    · simp only [ascPochhammer_eval_zero, zero_mul, if_neg h, mul_zero]
  | k + 1 => by simp only [ascPochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial, add_right_comm]

Recurrence Relation for Rising Factorial Evaluations: $n \cdot (n+1)^{\overline{r}} = (n + r) \cdot n^{\overline{r}}$

Informal description

For any natural numbers $r$ and $n$, the following identity holds for the rising factorial polynomial evaluated at $n+1$ and $n$: $$ n \cdot \text{ascPochhammer}_{\mathbb{N}}(r)(n+1) = (n + r) \cdot \text{ascPochhammer}_{\mathbb{N}}(r)(n) $$ where $\text{ascPochhammer}_{\mathbb{N}}(r)(x) = x(x+1)\cdots(x+r-1)$ is the rising factorial polynomial evaluated at $x$.

ascPochhammer_eval_succ theorem

(r n : ℕ) : (n : S) * (ascPochhammer S r).eval (n + 1 : S) = (n + r) * (ascPochhammer S r).eval (n : S)

Full source

theorem ascPochhammer_eval_succ (r n : ℕ) :
    (n : S) * (ascPochhammer S r).eval (n + 1 : S) =
    (n + r) * (ascPochhammer S r).eval (n : S) :=
  mod_cast congr_arg Nat.cast (ascPochhammer_nat_eval_succ r n)

Recurrence relation for rising factorial evaluations: $n \cdot (n+1)^{\overline{r}} = (n + r) \cdot n^{\overline{r}}$

Informal description

For any semiring $S$ and natural numbers $r$ and $n$, the following identity holds for the rising factorial polynomial evaluated at $n+1$ and $n$ (viewed as elements of $S$): $$ n \cdot \text{ascPochhammer}_S(r)(n+1) = (n + r) \cdot \text{ascPochhammer}_S(r)(n) $$ where $\text{ascPochhammer}_S(r)(X) = X(X+1)\cdots(X+r-1)$ is the rising factorial polynomial.

descPochhammer definition

: ℕ → R[X]

Full source

/-- `descPochhammer R n` is the polynomial `X * (X - 1) * ... * (X - n + 1)`,
with coefficients in the ring `R`.
-/
noncomputable def descPochhammer : ℕ → R[X]
  | 0 => 1
  | n + 1 => X * (descPochhammer n).comp (X - 1)

Falling factorial polynomial

Informal description

The falling factorial polynomial $\text{descPochhammer}_R(n)$ is defined as the product $X \cdot (X - 1) \cdots (X - n + 1)$ with coefficients in the ring $R$. Specifically: - $\text{descPochhammer}_R(0) = 1$ - $\text{descPochhammer}_R(1) = X$ - For $n \geq 1$, $\text{descPochhammer}_R(n+1) = X \cdot \text{descPochhammer}_R(n) \circ (X - 1)$ where $\circ$ denotes polynomial composition.

descPochhammer_zero theorem

: descPochhammer R 0 = 1

Full source

@[simp]
theorem descPochhammer_zero : descPochhammer R 0 = 1 :=
  rfl

Base case of falling factorial polynomial: $\text{descPochhammer}_R(0) = 1$

Informal description

The falling factorial polynomial $\text{descPochhammer}_R(0)$ of degree 0 is equal to the constant polynomial $1$.

descPochhammer_one theorem

: descPochhammer R 1 = X

Full source

@[simp]
theorem descPochhammer_one : descPochhammer R 1 = X := by simp [descPochhammer]

Falling factorial polynomial of degree 1: $\text{descPochhammer}_R(1) = X$

Informal description

The falling factorial polynomial $\text{descPochhammer}_R(1)$ of degree 1 is equal to the polynomial variable $X$, i.e., $\text{descPochhammer}_R(1) = X$.

descPochhammer_succ_left theorem

(n : ℕ) : descPochhammer R (n + 1) = X * (descPochhammer R n).comp (X - 1)

Full source

theorem descPochhammer_succ_left (n : ℕ) :
    descPochhammer R (n + 1) = X * (descPochhammer R n).comp (X - 1) := by
  rw [descPochhammer]

Recursive formula for falling factorial polynomial: $\text{descPochhammer}_R(n+1) = X \cdot \text{descPochhammer}_R(n)(X - 1)$

Informal description

For any natural number $n$, the falling factorial polynomial $\text{descPochhammer}_R(n+1)$ can be expressed as $X$ multiplied by the composition of $\text{descPochhammer}_R(n)$ with the polynomial $(X - 1)$. That is, \[ \text{descPochhammer}_R(n+1) = X \cdot \text{descPochhammer}_R(n)(X - 1). \]

monic_descPochhammer theorem

(n : ℕ) [Nontrivial R] [NoZeroDivisors R] : Monic <| descPochhammer R n

Full source

theorem monic_descPochhammer (n : ℕ) [Nontrivial R] [NoZeroDivisors R] :
    Monic <| descPochhammer R n := by
  induction' n with n hn
  · simp
  · have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1
    have : natDegreenatDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)
    rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]

Monicity of Falling Factorial Polynomial $\text{descPochhammer}_R(n)$

Informal description

For any natural number $n$ and any nontrivial ring $R$ with no zero divisors, the falling factorial polynomial $\text{descPochhammer}_R(n)$ is monic, meaning its leading coefficient is 1.

descPochhammer_map theorem

(f : R →+* T) (n : ℕ) : (descPochhammer R n).map f = descPochhammer T n

Full source

@[simp]
theorem descPochhammer_map (f : R →+* T) (n : ℕ) :
    (descPochhammer R n).map f = descPochhammer T n := by
  induction n with
  | zero => simp
  | succ n ih => simp [ih, descPochhammer_succ_left, map_comp]

Falling Factorial Polynomial Preserved Under Ring Homomorphism

Informal description

For any ring homomorphism $f \colon R \to T$ and any natural number $n$, the falling factorial polynomial $\text{descPochhammer}_R(n)$ maps under $f$ to the falling factorial polynomial $\text{descPochhammer}_T(n)$. That is, \[ f(\text{descPochhammer}_R(n)) = \text{descPochhammer}_T(n). \]

descPochhammer_eval_cast theorem

(n : ℕ) (k : ℤ) : (((descPochhammer ℤ n).eval k : ℤ) : R) = ((descPochhammer R n).eval k : R)

Full source

@[simp, norm_cast]
theorem descPochhammer_eval_cast (n : ℕ) (k : ℤ) :
    (((descPochhammer ℤ n).eval k : ℤ) : R) = ((descPochhammer R n).eval k : R) := by
  rw [← descPochhammer_map (algebraMap ℤ R), eval_map, ← eq_intCast (algebraMap ℤ R)]
  simp only [algebraMap_int_eq, eq_intCast, eval₂_at_intCast, Nat.cast_id, eq_natCast, Int.cast_id]

Evaluation of Falling Factorial Polynomials Commutes with Integer Coercion

Informal description

For any natural number $n$ and any integer $k$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_{\mathbb{Z}}(n)$ at $k$ (interpreted as an integer) and then coerced to a ring $R$ is equal to the evaluation of $\text{descPochhammer}_R(n)$ at $k$ (interpreted as an element of $R$). That is, \[ \text{descPochhammer}_{\mathbb{Z}}(n)(k) \text{ coerced to } R = \text{descPochhammer}_R(n)(k). \]

descPochhammer_eval_zero theorem

{n : ℕ} : (descPochhammer R n).eval 0 = if n = 0 then 1 else 0

Full source

theorem descPochhammer_eval_zero {n : ℕ} :
    (descPochhammer R n).eval 0 = if n = 0 then 1 else 0 := by
  cases n
  · simp
  · simp [X_mul, Nat.succ_ne_zero, descPochhammer_succ_left]

Evaluation of Falling Factorial at Zero: $\text{descPochhammer}_R(n)(0) = \delta_{n0}$

Informal description

For any natural number $n$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_R(n)$ at $0$ is equal to $1$ if $n = 0$ and $0$ otherwise. That is, \[ \text{descPochhammer}_R(n)(0) = \begin{cases} 1 & \text{if } n = 0, \\ 0 & \text{otherwise.} \end{cases} \]

descPochhammer_zero_eval_zero theorem

: (descPochhammer R 0).eval 0 = 1

Full source

theorem descPochhammer_zero_eval_zero : (descPochhammer R 0).eval 0 = 1 := by simp

Evaluation of Zero-th Falling Factorial at Zero: $\text{descPochhammer}_R(0)(0) = 1$

Informal description

For any ring $R$, evaluating the falling factorial polynomial $\text{descPochhammer}_R(0)$ at $0$ yields $1$, i.e., $\text{descPochhammer}_R(0)(0) = 1$.

descPochhammer_ne_zero_eval_zero theorem

{n : ℕ} (h : n ≠ 0) : (descPochhammer R n).eval 0 = 0

Full source

@[simp]
theorem descPochhammer_ne_zero_eval_zero {n : ℕ} (h : n ≠ 0) : (descPochhammer R n).eval 0 = 0 := by
  simp [descPochhammer_eval_zero, h]

Vanishing of Falling Factorial at Zero for $n \neq 0$: $\text{descPochhammer}_R(n)(0) = 0$

Informal description

For any natural number $n \neq 0$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_R(n)$ at $0$ is equal to $0$, i.e., $\text{descPochhammer}_R(n)(0) = 0$.

descPochhammer_succ_right theorem

(n : ℕ) : descPochhammer R (n + 1) = descPochhammer R n * (X - (n : R[X]))

Full source

theorem descPochhammer_succ_right (n : ℕ) :
    descPochhammer R (n + 1) = descPochhammer R n * (X - (n : R[X])) := by
  suffices h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - (n : ℤℤ[X])) by
    apply_fun Polynomial.map (algebraMap ℤ R) at h
    simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_intCast] using h
  induction n with
  | zero => simp [descPochhammer]
  | succ n ih =>
    conv_lhs =>
      rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]
    rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]

Recursive formula for falling factorial polynomial: $\text{descPochhammer}_R(n+1) = \text{descPochhammer}_R(n) \cdot (X - n)$

Informal description

For any natural number $n$, the falling factorial polynomial $\text{descPochhammer}_R(n+1)$ can be expressed as the product of $\text{descPochhammer}_R(n)$ and the polynomial $(X - n)$, i.e., \[ \text{descPochhammer}_R(n+1) = \text{descPochhammer}_R(n) \cdot (X - n). \]

descPochhammer_natDegree theorem

(n : ℕ) [NoZeroDivisors R] [Nontrivial R] : (descPochhammer R n).natDegree = n

Full source

@[simp]
theorem descPochhammer_natDegree (n : ℕ) [NoZeroDivisors R] [Nontrivial R] :
    (descPochhammer R n).natDegree = n := by
  induction' n with n hn
  · simp
  · have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)
    rw [descPochhammer_succ_right,
        natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]
    cases n
    · simp
    · refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

Natural Degree of Falling Factorial Polynomial: $\deg(\text{descPochhammer}_R(n)) = n$

Informal description

For any natural number $n$ and any ring $R$ with no zero divisors and at least two distinct elements, the natural degree of the falling factorial polynomial $\text{descPochhammer}_R(n)$ is equal to $n$.

descPochhammer_succ_eval theorem

{S : Type*} [Ring S] (n : ℕ) (k : S) : (descPochhammer S (n + 1)).eval k = (descPochhammer S n).eval k * (k - n)

Full source

theorem descPochhammer_succ_eval {S : Type*} [Ring S] (n : ℕ) (k : S) :
    (descPochhammer S (n + 1)).eval k = (descPochhammer S n).eval k * (k - n) := by
  rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]

Evaluation of Falling Factorial Polynomial: $\text{descPochhammer}_S(n+1)(k) = \text{descPochhammer}_S(n)(k) \cdot (k - n)$

Informal description

For any natural number $n$ and any element $k$ in a ring $S$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_S(n+1)$ at $k$ is equal to the evaluation of $\text{descPochhammer}_S(n)$ at $k$ multiplied by $(k - n)$, i.e., \[ \text{descPochhammer}_S(n+1)(k) = \text{descPochhammer}_S(n)(k) \cdot (k - n). \]

descPochhammer_succ_comp_X_sub_one theorem

 (n : ℕ) :
  (descPochhammer R (n + 1)).comp (X - 1) =
    descPochhammer R (n + 1) - (n + (1 : R[X])) • (descPochhammer R n).comp (X - 1)

Full source

theorem descPochhammer_succ_comp_X_sub_one (n : ℕ) :
    (descPochhammer R (n + 1)).comp (X - 1) =
      descPochhammer R (n + 1) - (n + (1 : R[X])) • (descPochhammer R n).comp (X - 1) := by
  suffices (descPochhammer ℤ (n + 1)).comp (X - 1) =
      descPochhammer ℤ (n + 1) - (n + 1) * (descPochhammer ℤ n).comp (X - 1)
    by simpa [map_comp] using congr_arg (Polynomial.map (Int.castRingHom R)) this
  nth_rw 2 [descPochhammer_succ_left]
  rw [← sub_mul, descPochhammer_succ_right ℤ n, mul_comp, mul_comm, sub_comp, X_comp, natCast_comp]
  ring

Composition Identity for Falling Factorial Polynomial: $\text{descPochhammer}_R(n+1)(X - 1) = \text{descPochhammer}_R(n+1) - (n + 1) \cdot \text{descPochhammer}_R(n)(X - 1)$

Informal description

For any natural number $n$, the composition of the falling factorial polynomial $\text{descPochhammer}_R(n+1)$ with $(X - 1)$ satisfies the relation: \[ \text{descPochhammer}_R(n+1)(X - 1) = \text{descPochhammer}_R(n+1) - (n + 1) \cdot \text{descPochhammer}_R(n)(X - 1). \]

descPochhammer_eq_ascPochhammer theorem

(n : ℕ) : descPochhammer ℤ n = (ascPochhammer ℤ n).comp ((X : ℤ[X]) - n + 1)

Full source

theorem descPochhammer_eq_ascPochhammer (n : ℕ) :
    descPochhammer ℤ n = (ascPochhammer ℤ n).comp ((X : ℤℤ[X]) - n + 1) := by
  induction n with
  | zero => rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]

Falling Factorial as Composition of Rising Factorial: $\text{descPochhammer}_{\mathbb{Z}}(n) = \text{ascPochhammer}_{\mathbb{Z}}(n)(X - n + 1)$

Informal description

For any natural number $n$, the falling factorial polynomial $\text{descPochhammer}_{\mathbb{Z}}(n)$ over the integers can be expressed as the composition of the rising factorial polynomial $\text{ascPochhammer}_{\mathbb{Z}}(n)$ with the polynomial $X - n + 1$, i.e., \[ \text{descPochhammer}_{\mathbb{Z}}(n) = \text{ascPochhammer}_{\mathbb{Z}}(n)(X - n + 1). \]

descPochhammer_eval_eq_ascPochhammer theorem

(r : R) (n : ℕ) : (descPochhammer R n).eval r = (ascPochhammer R n).eval (r - n + 1)

Full source

theorem descPochhammer_eval_eq_ascPochhammer (r : R) (n : ℕ) :
    (descPochhammer R n).eval r = (ascPochhammer R n).eval (r - n + 1) := by
  induction n with
  | zero => rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]

Evaluation of Falling Factorial in Terms of Rising Factorial: $\text{descPochhammer}_R(n)(r) = \text{ascPochhammer}_R(n)(r - n + 1)$

Informal description

For any element $r$ in a ring $R$ and any natural number $n$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_R(n)$ at $r$ is equal to the evaluation of the rising factorial polynomial $\text{ascPochhammer}_R(n)$ at $r - n + 1$. That is, \[ \text{descPochhammer}_R(n)(r) = \text{ascPochhammer}_R(n)(r - n + 1). \]

descPochhammer_mul theorem

(n m : ℕ) : descPochhammer R n * (descPochhammer R m).comp (X - (n : R[X])) = descPochhammer R (n + m)

Full source

theorem descPochhammer_mul (n m : ℕ) :
    descPochhammer R n * (descPochhammer R m).comp (X - (n : R[X])) = descPochhammer R (n + m) := by
  induction' m with m ih
  · simp
  · rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]

Product Formula for Falling Factorial Polynomials: $\text{descPochhammer}_R(n) \cdot \text{descPochhammer}_R(m)(X - n) = \text{descPochhammer}_R(n + m)$

Informal description

For any natural numbers $n$ and $m$, the product of the falling factorial polynomial $\text{descPochhammer}_R(n)$ and the composition of $\text{descPochhammer}_R(m)$ with the polynomial $(X - n)$ equals the falling factorial polynomial $\text{descPochhammer}_R(n + m)$. That is, \[ \text{descPochhammer}_R(n) \cdot \text{descPochhammer}_R(m)(X - n) = \text{descPochhammer}_R(n + m). \]

ascPochhammer_eval_neg_eq_descPochhammer theorem

(r : R) : ∀ (k : ℕ), (ascPochhammer R k).eval (-r) = (-1) ^ k * (descPochhammer R k).eval r

Full source

theorem ascPochhammer_eval_neg_eq_descPochhammer (r : R) : ∀ (k : ℕ),
    (ascPochhammer R k).eval (-r) = (-1)^k * (descPochhammer R k).eval r
  | 0 => by
    rw [ascPochhammer_zero, descPochhammer_zero]
    simp only [eval_one, pow_zero, mul_one]
  | (k+1) => by
    rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1)^k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]

Evaluation of Rising Factorial at Negative Argument in Terms of Falling Factorial: $\text{ascPochhammer}_R(k)(-r) = (-1)^k \text{descPochhammer}_R(k)(r)$

Informal description

For any element $r$ in a ring $R$ and any natural number $k$, evaluating the rising factorial polynomial $\text{ascPochhammer}_R(k)$ at $-r$ equals $(-1)^k$ times the evaluation of the falling factorial polynomial $\text{descPochhammer}_R(k)$ at $r$. That is, $$ \text{ascPochhammer}_R(k)(-r) = (-1)^k \cdot \text{descPochhammer}_R(k)(r). $$

descPochhammer_eval_eq_descFactorial theorem

(n k : ℕ) : (descPochhammer R k).eval (n : R) = n.descFactorial k

Full source

theorem descPochhammer_eval_eq_descFactorial (n k : ℕ) :
    (descPochhammer R k).eval (n : R) = n.descFactorial k := by
  induction k with
  | zero => rw [descPochhammer_zero, eval_one, Nat.descFactorial_zero, Nat.cast_one]
  | succ k ih =>
    rw [descPochhammer_succ_right, Nat.descFactorial_succ, mul_sub, eval_sub, eval_mul_X,
      ← Nat.cast_comm k, eval_natCast_mul, ← Nat.cast_comm n, ← sub_mul, ih]
    by_cases h : n < k
    · rw [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, mul_zero, mul_zero, Nat.cast_zero]
    · rw [Nat.cast_mul, Nat.cast_sub <| not_lt.mp h]

Evaluation of Falling Factorial Polynomial at Natural Number: $\text{descPochhammer}_R(k)(n) = n^{\underline{k}}$

Informal description

For any natural numbers $n$ and $k$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_R(k)$ at $n$ (interpreted as an element of $R$) equals the descending factorial $n^{\underline{k}}$, i.e., $$ \text{descPochhammer}_R(k)(n) = n^{\underline{k}}. $$

descPochhammer_int_eq_ascFactorial theorem

(a b : ℕ) : (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b

Full source

theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) :
    (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b := by
  rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b,
    Nat.add_descFactorial_eq_ascFactorial]

Evaluation of Falling Factorial Polynomial at Shifted Integer: $\text{descPochhammer}_{\mathbb{Z}}(b)(a + b) = (a + 1)^{\overline{b}}$

Informal description

For any natural numbers $a$ and $b$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_{\mathbb{Z}}(b)$ at the integer $a + b$ equals the ascending factorial $(a + 1)^{\overline{b}}$, i.e., $$ \text{descPochhammer}_{\mathbb{Z}}(b)(a + b) = (a + 1)^{\overline{b}}. $$

ascPochhammer_eval_neg_coe_nat_of_lt theorem

{n k : ℕ} (h : k < n) : (ascPochhammer R n).eval (-(k : R)) = 0

Full source

/-- The Pochhammer polynomial of degree `n` has roots at `0`, `-1`, ..., `-(n - 1)`. -/
theorem ascPochhammer_eval_neg_coe_nat_of_lt {n k : ℕ} (h : k < n) :
    (ascPochhammer R n).eval (-(k : R)) = 0 := by
  induction n with
  | zero => contradiction
  | succ n ih =>
    rw [ascPochhammer_succ_eval]
    rcases lt_trichotomy k n with hkn | rfl | hkn
    · simp [ih hkn]
    · simp
    · omega

Roots of Rising Factorial Polynomial at Negative Integers: $\text{ascPochhammer}_R(n)(-k) = 0$ for $k < n$

Informal description

For any natural numbers $n$ and $k$ with $k < n$, the evaluation of the rising factorial polynomial $\text{ascPochhammer}_R(n)$ at $-k$ (interpreted as an element of $R$) is zero, i.e., $$ \text{ascPochhammer}_R(n)(-k) = 0. $$

ascPochhammer_eval_eq_zero_iff theorem

[IsDomain R] (n : ℕ) (r : R) : (ascPochhammer R n).eval r = 0 ↔ ∃ k < n, k = -r

Full source

/-- Over an integral domain, the Pochhammer polynomial of degree `n` has roots *only* at
`0`, `-1`, ..., `-(n - 1)`. -/
@[simp]
theorem ascPochhammer_eval_eq_zero_iff [IsDomain R]
    (n : ℕ) (r : R) : (ascPochhammer R n).eval r = 0 ↔ ∃ k < n, k = -r := by
  refine ⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩
  · induction n with
    | zero => simp only [ascPochhammer_zero, Polynomial.eval_one, one_ne_zero] at zero'
    | succ n ih =>
      rw [ascPochhammer_succ_eval, mul_eq_zero] at zero'
      cases zero' with
      | inl h =>
        obtain ⟨rn, hrn, rrn⟩ := ih h
        exact ⟨rn, by omega, rrn⟩
      | inr h =>
        exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩
  · obtain ⟨rn, hrn, rnn⟩ := hrn
    convert ascPochhammer_eval_neg_coe_nat_of_lt hrn
    simp [rnn]

Characterization of Roots of Rising Factorial Polynomial: $\text{ascPochhammer}_R(n)(r) = 0 \iff r \in \{0, -1, \dots, -(n-1)\}$

Informal description

Let $R$ be an integral domain and $n$ a natural number. For any element $r \in R$, the rising factorial polynomial $\text{ascPochhammer}_R(n)$ evaluates to zero at $r$ if and only if there exists a natural number $k < n$ such that $k = -r$. In other words: $$ \text{ascPochhammer}_R(n)(r) = 0 \iff \exists k < n, r = -k. $$

descPochhammer_eval_coe_nat_of_lt theorem

{k n : ℕ} (h : k < n) : (descPochhammer R n).eval (k : R) = 0

Full source

/-- `descPochhammer R n` is `0` for `0, 1, …, n-1`. -/
theorem descPochhammer_eval_coe_nat_of_lt {k n : ℕ} (h : k < n) :
    (descPochhammer R n).eval (k : R) = 0 := by
  rw [descPochhammer_eval_eq_ascPochhammer, sub_add_eq_add_sub,
    ← Nat.cast_add_one, ← neg_sub, ← Nat.cast_sub h]
  exact ascPochhammer_eval_neg_coe_nat_of_lt (Nat.sub_lt_of_pos_le k.succ_pos h)

Roots of Falling Factorial Polynomial at Natural Numbers: $\text{descPochhammer}_R(n)(k) = 0$ for $k < n$

Informal description

For any natural numbers $k$ and $n$ with $k < n$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_R(n)$ at $k$ (interpreted as an element of $R$) is zero, i.e., $$ \text{descPochhammer}_R(n)(k) = 0. $$

descPochhammer_eval_eq_prod_range theorem

{R : Type*} [CommRing R] (n : ℕ) (r : R) : (descPochhammer R n).eval r = ∏ j ∈ Finset.range n, (r - j)

Full source

lemma descPochhammer_eval_eq_prod_range {R : Type*} [CommRing R] (n : ℕ) (r : R) :
    (descPochhammer R n).eval r = ∏ j ∈ Finset.range n, (r - j) := by
  induction n with
  | zero => simp
  | succ n ih => simp [descPochhammer_succ_right, ih, ← Finset.prod_range_succ]

Evaluation of Falling Factorial Polynomial as Product: $\text{descPochhammer}_R(n)(r) = \prod_{j=0}^{n-1} (r - j)$

Informal description

For any commutative ring $R$, natural number $n$, and element $r \in R$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_R(n)$ at $r$ equals the product $\prod_{j=0}^{n-1} (r - j)$. That is, \[ \text{descPochhammer}_R(n)(r) = \prod_{j=0}^{n-1} (r - j). \]

descPochhammer_pos theorem

{n : ℕ} {s : S} (h : n - 1 < s) : 0 < (descPochhammer S n).eval s

Full source

/-- `descPochhammer S n` is positive on `(n-1, ∞)`. -/
theorem descPochhammer_pos {n : ℕ} {s : S} (h : n - 1 < s) :
    0 < (descPochhammer S n).eval s := by
  rw [← sub_pos, ← sub_add] at h
  rw [descPochhammer_eval_eq_ascPochhammer]
  exact ascPochhammer_pos n (s - n + 1) h

Positivity of Falling Factorial Polynomial on $(n-1, \infty)$

Informal description

For any natural number $n$ and any element $s$ in a semiring $S$ such that $s > n-1$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_S(n)$ at $s$ is positive, i.e., $\text{descPochhammer}_S(n)(s) > 0$.

descPochhammer_nonneg theorem

{n : ℕ} {s : S} (h : n - 1 ≤ s) : 0 ≤ (descPochhammer S n).eval s

Full source

/-- `descPochhammer S n` is nonnegative on `[n-1, ∞)`. -/
theorem descPochhammer_nonneg {n : ℕ} {s : S} (h : n - 1 ≤ s) :
    0 ≤ (descPochhammer S n).eval s := by
  rcases eq_or_lt_of_le h with heq | h
  · rw [← heq, descPochhammer_eval_eq_ascPochhammer,
      sub_sub_cancel_left, neg_add_cancel, ascPochhammer_eval_zero]
    positivity
  · exact (descPochhammer_pos h).le

Nonnegativity of Falling Factorial Polynomial on $[n-1, \infty)$

Informal description

For any natural number $n$ and any element $s$ in a semiring $S$ such that $s \geq n - 1$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_S(n)$ at $s$ is nonnegative, i.e., $\text{descPochhammer}_S(n)(s) \geq 0$.

pow_le_descPochhammer_eval theorem

{n : ℕ} {s : S} (h : n - 1 ≤ s) : (s - n + 1) ^ n ≤ (descPochhammer S n).eval s

Full source

/-- `descPochhammer S n` is at least `(s-n+1)^n` on `[n-1, ∞)`. -/
theorem pow_le_descPochhammer_eval {n : ℕ} {s : S} (h : n - 1 ≤ s) :
    (s - n + 1)^n ≤ (descPochhammer S n).eval s := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Nat.cast_add_one, add_sub_cancel_right, ← sub_nonneg] at h
    have hsub1 : n - 1 ≤ s := (sub_le_self (n : S) zero_le_one).trans (le_of_sub_nonneg h)
    rw [pow_succ, descPochhammer_succ_eval, Nat.cast_add_one, sub_add, add_sub_cancel_right]
    apply mul_le_mul _ le_rfl h (descPochhammer_nonneg hsub1)
    exact (ih hsub1).trans' <| pow_le_pow_left₀ h (le_add_of_nonneg_right zero_le_one) n

Lower Bound for Falling Factorial Polynomial: $(s - n + 1)^n \leq \text{descPochhammer}_S(n)(s)$ on $[n-1, \infty)$

Informal description

For any natural number $n$ and any element $s$ in a semiring $S$ such that $s \geq n - 1$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_S(n)$ at $s$ satisfies the inequality $(s - n + 1)^n \leq \text{descPochhammer}_S(n)(s)$.

monotoneOn_descPochhammer_eval theorem

(n : ℕ) : MonotoneOn (descPochhammer S n).eval (Set.Ici (n - 1 : S))

Full source

/-- `descPochhammer S n` is monotone on `[n-1, ∞)`. -/
theorem monotoneOn_descPochhammer_eval (n : ℕ) :
    MonotoneOn (descPochhammer S n).eval (Set.Ici (n - 1 : S)) := by
  induction n with
  | zero => simp [monotoneOn_const]
  | succ n ih =>
    intro a ha b hb hab
    rw [Set.mem_Ici, Nat.cast_add_one, add_sub_cancel_right] at ha hb
    have ha_sub1 : n - 1 ≤ a := (sub_le_self (n : S) zero_le_one).trans ha
    have hb_sub1 : n - 1 ≤ b := (sub_le_self (n : S) zero_le_one).trans hb
    simp_rw [descPochhammer_succ_eval]
    exact mul_le_mul (ih ha_sub1 hb_sub1 hab) (sub_le_sub_right hab (n : S))
      (sub_nonneg_of_le ha) (descPochhammer_nonneg hb_sub1)

Monotonicity of Falling Factorial Polynomial Evaluations on $[n-1, \infty)$

Informal description

For any natural number $n$, the evaluation of the falling factorial polynomial $\text{descPochhammer}_S(n)$ is monotonically increasing on the interval $[n-1, \infty)$. That is, for any $x, y \in S$ with $x \geq n-1$ and $y \geq n-1$, if $x \leq y$ then $\text{descPochhammer}_S(n)(x) \leq \text{descPochhammer}_S(n)(y)$.

Mathlib.RingTheory.Polynomial.Pochhammer

Implementation

TODO