Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-04 18:07 a3e847c0

View on Github →

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

depends on: #14881

Estimated changes

Created src/analysis/special_functions/stirling.lean

added theorem log_stirling_seq'_antitone

added theorem log_stirling_seq_bounded_aux

added theorem log_stirling_seq_bounded_by_constant

added theorem log_stirling_seq_diff_has_sum

added theorem log_stirling_seq_diff_le_geo_sum

added theorem log_stirling_seq_formula

added theorem log_stirling_seq_sub_log_stirling_seq_succ

added theorem stirling_seq'_antitone

added theorem stirling_seq'_bounded_by_pos_constant

added theorem stirling_seq'_pos

added theorem stirling_seq_has_pos_limit_a

added theorem stirling_seq_one

added theorem stirling_seq_zero