mathlib

a3e847c0 - feat(analysis/special_functions/stirling): Stirling's formula, part I (#14874)

feat(analysis/special_functions/stirling): Stirling's formula, part I (#14874) Part 1 - [x] depends on: #14881 Co-authored-by: fabian-kruse <fabian_kruse@gmx.de> Co-authored-by: nick-kuhn <46423253+nick-kuhn@users.noreply.github.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: nick-kuhn <46423253+nick-kuhn@users.noreply.github.com>