English
For every fixed k, n.descFactorial k and n^k have the same growth rate at infinity.
Русский
Для фиксированного k, n.descFactorial k и n^k имеют одинаковую асимптотическую скорость роста на бесконечности.
LaTeX
$$$ (\lambda n : \mathbb{N}) \mapsto (n.\mathrm{descFactorial}\ k : \mathbb{R}) \sim_{atTop} (n \mapsto n^{k}) $$$
Lean4
/-- Qary entropy is strictly increasing in the interval [0, 1 - q⁻¹]. -/
theorem qaryEntropy_strictMonoOn (qLe2 : 2 ≤ q) : StrictMonoOn (qaryEntropy q) (Icc 0 (1 - 1 / q)) :=
by
intro p1 hp1 p2 hp2 p1le2
apply strictMonoOn_of_deriv_pos (convex_Icc 0 (1 - 1 / (q : ℝ))) _ _ hp1 hp2 p1le2
· exact qaryEntropy_continuous.continuousOn
· intro p hp
have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qLe2
have zero_le_qinv : 0 < (q : ℝ)⁻¹ := by positivity
have : 0 < 1 - p := by
simp only [sub_pos]
have p_lt_1_minus_qinv : p < 1 - (q : ℝ)⁻¹ := by simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]
linarith
simp only [one_div, interior_Icc, mem_Ioo] at hp
rw [deriv_qaryEntropy (by linarith)]
· simp only [sub_pos, gt_iff_lt]
rw [← log_mul (by linarith) (by linarith)]
apply Real.strictMonoOn_log (mem_Ioi.mpr hp.1)
· simp_all only [mem_Ioi, mul_pos_iff_of_pos_left, show 0 < (q : ℝ) - 1 by linarith]
· have qpos : 0 < (q : ℝ) := by positivity
have : q * p < q - 1 := by
convert mul_lt_mul_of_pos_left hp.2 qpos using 1
simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
IsUnit.mul_inv_cancel]
linarith
exact (ne_of_gt (lt_add_neg_iff_lt.mp this : p < 1)).symm
