Pochhammer polynomials

This file proves analysis theorems for Pochhammer polynomials.

Main statements

• Differentiable.descPochhammer_eval is the proof that the descending Pochhammer polynomial descPochhammer ℝ n is differentiable.

• ConvexOn.descPochhammer_eval is the proof that the descending Pochhammer polynomial descPochhammer ℝ n is convex on [n-1, ∞).

• descPochhammer_eval_le_sum_descFactorial is a special case of Jensen's inequality for Nat.descFactorial.

• descPochhammer_eval_div_factorial_le_sum_choose is a special case of Jensen's inequality for Nat.choose.

theorem differentiable_descPochhammer_eval {n : ℕ} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : Differentiable 𝕜 fun (a : 𝕜) => Polynomial.eval a (descPochhammer 𝕜 n)

descPochhammer 𝕜 n is differentiable.

theorem continuous_descPochhammer_eval {n : ℕ} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : Continuous fun (a : 𝕜) => Polynomial.eval a (descPochhammer 𝕜 n)

descPochhammer 𝕜 n is continuous.

theorem deriv_descPochhammer_eval_eq_sum_prod_range_erase {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (n : ℕ) (k : 𝕜) : deriv (fun (a : 𝕜) => Polynomial.eval a (descPochhammer 𝕜 n)) k = ∑ i ∈ Finset.range n, ∏ j ∈ (Finset.range n).erase i, (k - ↑j)

theorem monotoneOn_deriv_descPochhammer_eval (n : ℕ) : MonotoneOn (deriv fun (a : ℝ) => Polynomial.eval a (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))

deriv (descPochhammer ℝ n) is monotone on (n-1, ∞).

theorem convexOn_descPochhammer_eval (n : ℕ) : ConvexOn ℝ (Set.Ici (↑n - 1)) fun (a : ℝ) => Polynomial.eval a (descPochhammer ℝ n)

descPochhammer ℝ n is convex on [n-1, ∞).

theorem descPochhammer_eval_le_sum_descFactorial {n : ℕ} (hn : n ≠ 0) {ι : Type u_2} {t : Finset ι} (p : ι → ℕ) (w : ι → ℝ) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)) : Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * ↑((p i).descFactorial n)

Special case of Jensen's inequality for Nat.descFactorial.

theorem descPochhammer_eval_div_factorial_le_sum_choose {n : ℕ} (hn : n ≠ 0) {ι : Type u_2} {t : Finset ι} (p : ι → ℕ) (w : ι → ℝ) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)) : Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) / ↑n.factorial ≤ ∑ i ∈ t, w i * ↑((p i).choose n)

Special case of Jensen's inequality for Nat.choose.