Theorem Stirling.log_stirlingSeq_bounded_aux

Modification history

2026-03-24 16:10

Mathlib/Analysis/SpecialFunctions/Stirling.lean

feat(Analysis/SpecialFunctions/StirlingRobbins): Robbins' sharp stepwise bound for stirlingSeq (#31366) …

Modified Stirling.log_stirlingSeq_bounded_aux View on Github →

2023-06-09 10:15

Mathlib/Analysis/SpecialFunctions/Stirling.lean

feat: port Analysis.SpecialFunctions.Stirling (#4892)

Added Stirling.log_stirlingSeq_bounded_aux View on Github →