Theorem Stirling.log_stirlingSeq_diff_le

Modification history

2026-03-24 16:10
Mathlib/Analysis/SpecialFunctions/Stirling.lean
feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq (#31366) …
Added Stirling.log_stirlingSeq_diff_leView on Github →