Commit 2025-03-11 01:14 35530f08

feat(Analysis/SpecialFunctions): prove special case of Jensen's inequality for binomial coefficients (#20738) Prove special case of Jensen's inequality for binomial coefficients using the descending Pochhammer polynomials. Also prove

• special case of Jensen's inequality for the descending factorial using the descending Pochhammer polynomials,
• the descending Pochhammer polynomials descPochhamer · n are monotone/convex on $$[n-1, \infty)$$,
• misc. analysis/ring theory lemmas for the descending Pochhammer polynomials.