Skip to content

Commit 35530f0

Browse files
mitchell-hornerRuben-VandeVelde
mitchell-horner
and
Ruben-VandeVelde
committed
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. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
1 parent 00d98b7 commit 35530f0

File tree

5 files changed

+305
-0
lines changed

5 files changed

+305
-0
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1425,6 +1425,7 @@ import Mathlib.Analysis.Convex.KreinMilman
14251425
import Mathlib.Analysis.Convex.Measure
14261426
import Mathlib.Analysis.Convex.Mul
14271427
import Mathlib.Analysis.Convex.PartitionOfUnity
1428+
import Mathlib.Analysis.Convex.Piecewise
14281429
import Mathlib.Analysis.Convex.Quasiconvex
14291430
import Mathlib.Analysis.Convex.Radon
14301431
import Mathlib.Analysis.Convex.Segment
@@ -1697,6 +1698,7 @@ import Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
16971698
import Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
16981699
import Mathlib.Analysis.SpecialFunctions.NonIntegrable
16991700
import Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
1701+
import Mathlib.Analysis.SpecialFunctions.Pochhammer
17001702
import Mathlib.Analysis.SpecialFunctions.PolarCoord
17011703
import Mathlib.Analysis.SpecialFunctions.PolynomialExp
17021704
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

‎Mathlib/Analysis/Convex/Piecewise.lean‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
/-
2+
Copyright (c) 2025 Mitchell Horner. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mitchell Horner
5+
-/
6+
import Mathlib.Analysis.Convex.Function
7+
8+
/-!
9+
# Convex and concave piecewise functions
10+
11+
This file proves convex and concave theorems for piecewise functions.
12+
13+
## Main statements
14+
15+
* `convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici` is the proof that the piecewise
16+
function `(Set.Iic e).piecewise f g` of a function `f` decreasing and convex on `Set.Iic e` and a
17+
function `g` increasing and convex on `Set.Ici e`, such that `f e = g e`, is convex on the
18+
universal set.
19+
20+
This version has the boundary point included in the left-hand function.
21+
22+
See `convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic` for the version with the
23+
boundary point included in the right-hand function.
24+
25+
See concave version(s) `concaveOn_univ_piecewise_Iic_of_monotoneOn_Iic_antitoneOn_Ici`
26+
and `concaveOn_univ_piecewise_Ici_of_antitoneOn_Ici_monotoneOn_Iic`.
27+
-/
28+
29+
30+
variable {𝕜 E β : Type*} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E]
31+
[OrderedSMul 𝕜 E] [OrderedAddCommGroup β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β}
32+
33+
/-- The piecewise function `(Set.Iic e).piecewise f g` of a function `f` decreasing and convex on
34+
`Set.Iic e` and a function `g` increasing and convex on `Set.Ici e`, such that `f e = g e`, is
35+
convex on the universal set. -/
36+
theorem convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici
37+
(hf : ConvexOn 𝕜 (Set.Iic e) f) (hg : ConvexOn 𝕜 (Set.Ici e) g)
38+
(h_anti : AntitoneOn f (Set.Iic e)) (h_mono : MonotoneOn g (Set.Ici e)) (h_eq : f e = g e) :
39+
ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise f g) := by
40+
refine ⟨convex_univ, fun x _ y _ a b ha hb hab ↦ ?_⟩
41+
by_cases hx : x ≤ e <;> by_cases hy : y ≤ e <;> push_neg at hx hy
42+
· have hc : a • x + b • y ≤ e := (Convex.combo_le_max x y ha hb hab).trans (max_le hx hy)
43+
rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hx, Set.piecewise_eq_of_mem (Set.Iic e) f g hy,
44+
Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
45+
exact hf.2 hx hy ha hb hab
46+
· rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hx,
47+
Set.piecewise_eq_of_not_mem (Set.Iic e) f g (Set.not_mem_Iic.mpr hy)]
48+
by_cases hc : a • x + b • y ≤ e <;> push_neg at hc
49+
· rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
50+
have hc' : a • x + b • e ≤ a • x + b • y :=
51+
add_le_add_left (smul_le_smul_of_nonneg_left hy.le hb) (a • x)
52+
trans a • f x + b • f e
53+
· exact (h_anti (hc'.trans hc) hc hc').trans (hf.2 hx Set.right_mem_Iic ha hb hab)
54+
· rw [add_le_add_iff_left, h_eq]
55+
exact smul_le_smul_of_nonneg_left (h_mono Set.left_mem_Ici hy.le hy.le) hb
56+
· rw [Set.piecewise_eq_of_not_mem (Set.Iic e) f g (Set.not_mem_Iic.mpr hc)]
57+
have hc' : a • x + b • y ≤ a • e + b • y :=
58+
add_le_add_right (smul_le_smul_of_nonneg_left hx ha) (b • y)
59+
trans a • g e + b • g y
60+
· exact (h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 Set.left_mem_Ici hy.le ha hb hab)
61+
· rw [add_le_add_iff_right, ← h_eq]
62+
exact smul_le_smul_of_nonneg_left (h_anti hx Set.right_mem_Iic hx) ha
63+
· rw [Set.piecewise_eq_of_not_mem (Set.Iic e) f g (Set.not_mem_Iic.mpr hx),
64+
Set.piecewise_eq_of_mem (Set.Iic e) f g hy]
65+
by_cases hc : a • x + b • y ≤ e <;> push_neg at hc
66+
· rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
67+
have hc' : a • e + b • y ≤ a • x + b • y :=
68+
add_le_add_right (smul_le_smul_of_nonneg_left hx.le ha) (b • y)
69+
trans a • f e + b • f y
70+
· exact (h_anti (hc'.trans hc) hc hc').trans (hf.2 Set.right_mem_Iic hy ha hb hab)
71+
· rw [add_le_add_iff_right, h_eq]
72+
exact smul_le_smul_of_nonneg_left (h_mono Set.left_mem_Ici hx.le hx.le) ha
73+
· rw [Set.piecewise_eq_of_not_mem (Set.Iic e) f g (Set.not_mem_Iic.mpr hc)]
74+
have hc' : a • x + b • y ≤ a • x + b • e :=
75+
add_le_add_left (smul_le_smul_of_nonneg_left hy hb) (a • x)
76+
trans a • g x + b • g e
77+
· exact (h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 hx.le Set.left_mem_Ici ha hb hab)
78+
· rw [add_le_add_iff_left, ← h_eq]
79+
exact smul_le_smul_of_nonneg_left (h_anti hy Set.right_mem_Iic hy) hb
80+
· have hc : e < a • x + b • y :=
81+
(lt_min hx hy).trans_le (Convex.min_le_combo x y ha hb hab)
82+
rw [(Set.Iic e).piecewise_eq_of_not_mem f g (Set.not_mem_Iic.mpr hx),
83+
(Set.Iic e).piecewise_eq_of_not_mem f g (Set.not_mem_Iic.mpr hy),
84+
(Set.Iic e).piecewise_eq_of_not_mem f g (Set.not_mem_Iic.mpr hc)]
85+
exact hg.2 hx.le hy.le ha hb hab
86+
87+
/-- The piecewise function `(Set.Ici e).piecewise f g` of a function `f` increasing and convex on
88+
`Set.Ici e` and a function `g` decreasing and convex on `Set.Iic e`, such that `f e = g e`, is
89+
convex on the universal set. -/
90+
theorem convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic
91+
(hf : ConvexOn 𝕜 (Set.Ici e) f) (hg : ConvexOn 𝕜 (Set.Iic e) g)
92+
(h_mono : MonotoneOn f (Set.Ici e)) (h_anti : AntitoneOn g (Set.Iic e)) (h_eq : f e = g e) :
93+
ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise f g) := by
94+
have h_piecewise_Ici_eq_piecewise_Iic :
95+
(Set.Ici e).piecewise f g = (Set.Iic e).piecewise g f := by
96+
ext x; by_cases hx : x = e
97+
<;> simp [Set.piecewise, @le_iff_lt_or_eq _ _ x e, ← @ite_not _ (e ≤ _), hx, h_eq]
98+
rw [h_piecewise_Ici_eq_piecewise_Iic]
99+
exact convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici hg hf h_anti h_mono h_eq.symm
100+
101+
/-- The piecewise function `(Set.Iic e).piecewise f g` of a function `f` increasing and concave on
102+
`Set.Iic e` and a function `g` decreasing and concave on `Set.Ici e`, such that `f e = g e`, is
103+
concave on the universal set. -/
104+
theorem concaveOn_univ_piecewise_Iic_of_monotoneOn_Iic_antitoneOn_Ici
105+
(hf : ConcaveOn 𝕜 (Set.Iic e) f) (hg : ConcaveOn 𝕜 (Set.Ici e) g)
106+
(h_mono : MonotoneOn f (Set.Iic e)) (h_anti : AntitoneOn g (Set.Ici e)) (h_eq : f e = g e) :
107+
ConcaveOn 𝕜 Set.univ ((Set.Iic e).piecewise f g) := by
108+
rw [← neg_convexOn_iff, ← Set.piecewise_neg]
109+
exact convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici
110+
hf.neg hg.neg h_mono.neg h_anti.neg (neg_inj.mpr h_eq)
111+
112+
/-- The piecewise function `(Set.Ici e).piecewise f g` of a function `f` decreasing and concave on
113+
`Set.Ici e` and a function `g` increasing and concave on `Set.Iic e`, such that `f e = g e`, is
114+
concave on the universal set. -/
115+
theorem concaveOn_univ_piecewise_Ici_of_antitoneOn_Ici_monotoneOn_Iic
116+
(hf : ConcaveOn 𝕜 (Set.Ici e) f) (hg : ConcaveOn 𝕜 (Set.Iic e) g)
117+
(h_anti : AntitoneOn f (Set.Ici e)) (h_mono : MonotoneOn g (Set.Iic e)) (h_eq : f e = g e) :
118+
ConcaveOn 𝕜 Set.univ ((Set.Ici e).piecewise f g) := by
119+
rw [← neg_convexOn_iff, ← Set.piecewise_neg]
120+
exact convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic
121+
hf.neg hg.neg h_anti.neg h_mono.neg (neg_inj.mpr h_eq)

‎Mathlib/Analysis/SpecialFunctions/Pochhammer.lean‎

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
/-
2+
Copyright (c) 2025 Mitchell Horner. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mitchell Horner
5+
-/
6+
import Mathlib.Algebra.BigOperators.Field
7+
import Mathlib.Analysis.Convex.Deriv
8+
import Mathlib.Analysis.Convex.Piecewise
9+
import Mathlib.Data.Nat.Choose.Cast
10+
11+
/-!
12+
# Pochhammer polynomials
13+
14+
This file proves analysis theorems for Pochhammer polynomials.
15+
16+
## Main statements
17+
18+
* `Differentiable.descPochhammer_eval` is the proof that the descending Pochhammer polynomial
19+
`descPochhammer ℝ n` is differentiable.
20+
21+
* `ConvexOn.descPochhammer_eval` is the proof that the descending Pochhammer polynomial
22+
`descPochhammer ℝ n` is convex on `[n-1, ∞)`.
23+
24+
* `descPochhammer_eval_le_sum_descFactorial` is a special case of **Jensen's inequality**
25+
for `Nat.descFactorial`.
26+
27+
* `descPochhammer_eval_div_factorial_le_sum_choose` is a special case of **Jensen's inequality**
28+
for `Nat.choose`.
29+
-/
30+
31+
32+
section DescPochhammer
33+
34+
variable {n : ℕ} {𝕜 : Type*} {k : 𝕜} [NontriviallyNormedField 𝕜]
35+
36+
/-- `descPochhammer 𝕜 n` is differentiable. -/
37+
theorem differentiable_descPochhammer_eval : Differentiable 𝕜 (descPochhammer 𝕜 n).eval := by
38+
simp [descPochhammer_eval_eq_prod_range, Differentiable.finset_prod]
39+
40+
/-- `descPochhammer 𝕜 n` is continuous. -/
41+
theorem continuous_descPochhammer_eval : Continuous (descPochhammer 𝕜 n).eval := by
42+
exact differentiable_descPochhammer_eval.continuous
43+
44+
lemma deriv_descPochhammer_eval_eq_sum_prod_range_erase (n : ℕ) (k : 𝕜) :
45+
deriv (descPochhammer 𝕜 n).eval k
46+
= ∑ i ∈ Finset.range n, ∏ j ∈ (Finset.range n).erase i, (k - j) := by
47+
simp [descPochhammer_eval_eq_prod_range, deriv_finset_prod]
48+
49+
/-- `deriv (descPochhammer ℝ n)` is monotone on `(n-1, ∞)`. -/
50+
lemma monotoneOn_deriv_descPochhammer_eval (n : ℕ) :
51+
MonotoneOn (deriv (descPochhammer ℝ n).eval) (Set.Ioi (n - 1 : ℝ)) := by
52+
induction n with
53+
| zero => simp [monotoneOn_const]
54+
| succ n ih =>
55+
intro a ha b hb hab
56+
rw [Set.mem_Ioi, Nat.cast_add_one, add_sub_cancel_right] at ha hb
57+
simp_rw [deriv_descPochhammer_eval_eq_sum_prod_range_erase]
58+
apply Finset.sum_le_sum; intro i hi
59+
apply Finset.prod_le_prod
60+
· intro j hj
61+
rw [Finset.mem_erase, Finset.mem_range] at hj
62+
apply sub_nonneg_of_le
63+
exact ha.le.trans' (mod_cast Nat.le_pred_of_lt hj.2)
64+
· intro j hj
65+
rwa [← sub_le_sub_iff_right (j : ℝ)] at hab
66+
67+
/-- `descPochhammer ℝ n` is convex on `[n-1, ∞)`. -/
68+
theorem convexOn_descPochhammer_eval (n : ℕ) :
69+
ConvexOn ℝ (Set.Ici (n - 1 : ℝ)) (descPochhammer ℝ n).eval := by
70+
rcases n.eq_zero_or_pos with h_eq | _
71+
· simp [h_eq, convexOn_const, convex_Ici]
72+
· apply MonotoneOn.convexOn_of_deriv (convex_Ici (n - 1 : ℝ))
73+
continuous_descPochhammer_eval.continuousOn
74+
differentiable_descPochhammer_eval.differentiableOn
75+
rw [interior_Ici]
76+
exact monotoneOn_deriv_descPochhammer_eval n
77+
78+
private lemma piecewise_Ici_descPochhammer_eval_zero_eq_descFactorial (k n : ℕ) :
79+
(Set.Ici (n - 1 : ℝ)).piecewise (descPochhammer ℝ n).eval 0 k
80+
= k.descFactorial n := by
81+
rw [Set.piecewise, descPochhammer_eval_eq_descFactorial, ite_eq_left_iff, Set.mem_Ici, not_le,
82+
eq_comm, Pi.zero_apply, Nat.cast_eq_zero, Nat.descFactorial_eq_zero_iff_lt, ← @Nat.cast_lt ℝ]
83+
exact (sub_lt_self (n : ℝ) zero_lt_one).trans'
84+
85+
private lemma convexOn_piecewise_Ici_descPochhammer_eval_zero (hn : n ≠ 0) :
86+
ConvexOn ℝ Set.univ ((Set.Ici (n - 1 : ℝ)).piecewise (descPochhammer ℝ n).eval 0) := by
87+
rw [← Nat.pos_iff_ne_zero] at hn
88+
apply convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic
89+
(convexOn_descPochhammer_eval n) (convexOn_const 0 (convex_Iic (n - 1 : ℝ)))
90+
(monotoneOn_descPochhammer_eval n) antitoneOn_const
91+
simpa [← Nat.cast_pred hn] using descPochhammer_eval_coe_nat_of_lt (Nat.sub_one_lt_of_lt hn)
92+
93+
/-- Special case of **Jensen's inequality** for `Nat.descFactorial`. -/
94+
theorem descPochhammer_eval_le_sum_descFactorial
95+
(hn : n ≠ 0) {ι : Type*} {t : Finset ι} (p : ι → ℕ) (w : ι → ℝ)
96+
(h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (h_avg : n - 1 ≤ ∑ i ∈ t, w i * p i) :
97+
(descPochhammer ℝ n).eval (∑ i ∈ t, w i * p i)
98+
≤ ∑ i ∈ t, w i * (p i).descFactorial n := by
99+
let f : ℝ → ℝ := (Set.Ici (n - 1 : ℝ)).piecewise (descPochhammer ℝ n).eval 0
100+
suffices h_jensen : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i) by
101+
simpa only [smul_eq_mul, f, Set.piecewise_eq_of_mem (Set.Ici (n - 1 : ℝ)) _ _ h_avg,
102+
piecewise_Ici_descPochhammer_eval_zero_eq_descFactorial] using h_jensen
103+
exact ConvexOn.map_sum_le (convexOn_piecewise_Ici_descPochhammer_eval_zero hn) h₀ h₁ (by simp)
104+
105+
/-- Special case of **Jensen's inequality** for `Nat.choose`. -/
106+
theorem descPochhammer_eval_div_factorial_le_sum_choose
107+
(hn : n ≠ 0) {ι : Type*} {t : Finset ι} (p : ι → ℕ) (w : ι → ℝ)
108+
(h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (h_avg : n - 1 ≤ ∑ i ∈ t, w i * p i) :
109+
(descPochhammer ℝ n).eval (∑ i ∈ t, w i * p i) / n.factorial
110+
≤ ∑ i ∈ t, w i * (p i).choose n := by
111+
simp_rw [Nat.cast_choose_eq_descPochhammer_div,
112+
mul_div, ← Finset.sum_div, descPochhammer_eval_eq_descFactorial]
113+
apply div_le_div_of_nonneg_right _ (Nat.cast_nonneg n.factorial)
114+
exact descPochhammer_eval_le_sum_descFactorial hn p w h₀ h₁ h_avg
115+
116+
end DescPochhammer

‎Mathlib/Data/Nat/Choose/Cast.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,11 @@ end DivisionSemiring
4040
section DivisionRing
4141
variable [DivisionRing K] [CharZero K]
4242

43+
theorem cast_choose_eq_descPochhammer_div (a b : ℕ) :
44+
(a.choose b : K) = (descPochhammer K b).eval ↑a / b ! := by
45+
rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
46+
mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]
47+
4348
theorem cast_choose_two (a : ℕ) : (a.choose 2 : K) = a * (a - 1) / 2 := by
4449
rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm,
4550
cast_mul, cast_two, eq_div_iff_mul_eq (two_ne_zero : (2 : K) ≠ 0)]

‎Mathlib/RingTheory/Polynomial/Pochhammer.lean‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -416,4 +416,65 @@ theorem ascPochhammer_eval_eq_zero_iff [IsDomain R]
416416
convert ascPochhammer_eval_neg_coe_nat_of_lt hrn
417417
simp [rnn]
418418

419+
/-- `descPochhammer R n` is `0` for `0, 1, …, n-1`. -/
420+
theorem descPochhammer_eval_coe_nat_of_lt {k n : ℕ} (h : k < n) :
421+
(descPochhammer R n).eval (k : R) = 0 := by
422+
rw [descPochhammer_eval_eq_ascPochhammer, sub_add_eq_add_sub,
423+
← Nat.cast_add_one, ← neg_sub, ← Nat.cast_sub h]
424+
exact ascPochhammer_eval_neg_coe_nat_of_lt (Nat.sub_lt_of_pos_le k.succ_pos h)
425+
426+
lemma descPochhammer_eval_eq_prod_range {R : Type*} [CommRing R] (n : ℕ) (r : R) :
427+
(descPochhammer R n).eval r = ∏ j ∈ Finset.range n, (r - j) := by
428+
induction n with
429+
| zero => simp
430+
| succ n ih => simp [descPochhammer_succ_right, ih, ← Finset.prod_range_succ]
431+
419432
end Ring
433+
434+
section StrictOrderedRing
435+
436+
variable {S : Type*} [StrictOrderedRing S]
437+
438+
/-- `descPochhammer S n` is positive on `(n-1, ∞)`. -/
439+
theorem descPochhammer_pos {n : ℕ} {s : S} (h : n - 1 < s) :
440+
0 < (descPochhammer S n).eval s := by
441+
rw [← sub_pos, ← sub_add] at h
442+
rw [descPochhammer_eval_eq_ascPochhammer]
443+
exact ascPochhammer_pos n (s - n + 1) h
444+
445+
/-- `descPochhammer S n` is nonnegative on `[n-1, ∞)`. -/
446+
theorem descPochhammer_nonneg {n : ℕ} {s : S} (h : n - 1 ≤ s) :
447+
0 ≤ (descPochhammer S n).eval s := by
448+
rcases eq_or_lt_of_le h with heq | h
449+
· rw [← heq, descPochhammer_eval_eq_ascPochhammer,
450+
sub_sub_cancel_left, neg_add_cancel, ascPochhammer_eval_zero]
451+
positivity
452+
· exact (descPochhammer_pos h).le
453+
454+
/-- `descPochhammer S n` is at least `(s-n+1)^n` on `[n-1, ∞)`. -/
455+
theorem pow_le_descPochhammer_eval {n : ℕ} {s : S} (h : n - 1 ≤ s) :
456+
(s - n + 1)^n ≤ (descPochhammer S n).eval s := by
457+
induction n with
458+
| zero => simp
459+
| succ n ih =>
460+
rw [Nat.cast_add_one, add_sub_cancel_right, ← sub_nonneg] at h
461+
have hsub1 : n - 1 ≤ s := (sub_le_self (n : S) zero_le_one).trans (le_of_sub_nonneg h)
462+
rw [pow_succ, descPochhammer_succ_eval, Nat.cast_add_one, sub_add, add_sub_cancel_right]
463+
apply mul_le_mul _ le_rfl h (descPochhammer_nonneg hsub1)
464+
exact (ih hsub1).trans' <| pow_le_pow_left₀ h (le_add_of_nonneg_right zero_le_one) n
465+
466+
/-- `descPochhammer S n` is monotone on `[n-1, ∞)`. -/
467+
theorem monotoneOn_descPochhammer_eval (n : ℕ) :
468+
MonotoneOn (descPochhammer S n).eval (Set.Ici (n - 1 : S)) := by
469+
induction n with
470+
| zero => simp [monotoneOn_const]
471+
| succ n ih =>
472+
intro a ha b hb hab
473+
rw [Set.mem_Ici, Nat.cast_add_one, add_sub_cancel_right] at ha hb
474+
have ha_sub1 : n - 1 ≤ a := (sub_le_self (n : S) zero_le_one).trans ha
475+
have hb_sub1 : n - 1 ≤ b := (sub_le_self (n : S) zero_le_one).trans hb
476+
simp_rw [descPochhammer_succ_eval]
477+
exact mul_le_mul (ih ha_sub1 hb_sub1 hab) (sub_le_sub_right hab (n : S))
478+
(sub_nonneg_of_le ha) (descPochhammer_nonneg hb_sub1)
479+
480+
end StrictOrderedRing

0 commit comments

Comments
 (0)