Elementary bounds for ascending Pochhammer symbols

theorem Complex.norm_ascPochhammer_eval_le_ascPochhammer (a : ℂ) (n : ℕ) {B : ℝ} (ha : ‖a‖ ≤ B) : ‖Polynomial.eval a (ascPochhammer ℂ n)‖ ≤ Polynomial.eval B (ascPochhammer ℝ n)

The sharp elementary Pochhammer bound, retaining the rising factorial rather than replacing every factor by the largest one.

theorem Complex.norm_ascPochhammer_eval_le (a : ℂ) (k : ℕ) {B : ℝ} (hB : 0 ≤ B) (ha : ‖a‖ ≤ B) : ‖Polynomial.eval a (ascPochhammer ℂ k)‖ ≤ (B + ↑k) ^ k

An ascending Pochhammer symbol is bounded by a power of a uniform bound on the argument.