Commit 2026-03-24 16:10 45d2beed
View on Github →feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq (#31366)
This PR refactors Stirling.lean to use Robbin's bound log (stirlingSeq n) - log (stirlingSeq (n+1)) ≤ 1 / (12 n (n + 1)).
The original PR was by @FaffyWaffles but the PR has now been adopted by @tb65536.