log_stirlingSeq'_antitone — Mathlib

English

The function n ↦ log(stirlingSeq(n+1)) is nonincreasing in n (i.e., antitone).

Русский

Функция n ↦ log(stirlingSeq(n+1)) монотонно не возрастает по n (антитонна).

LaTeX

$$$\\text{Antitone}( \\;\\log(\\operatorname{stirlingSeq}(n+1))\\; )$$$

Lean4

/-- The sequence `log ∘ stirlingSeq ∘ succ` is monotone decreasing -/
theorem log_stirlingSeq'_antitone : Antitone (Real.log ∘ stirlingSeq ∘ succ) :=
  antitone_nat_of_succ_le fun n => sub_nonneg.mp <| (log_stirlingSeq_diff_hasSum n).nonneg fun m => by positivity

Похожие утверждения