Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-16 12:10 fc35e1e9

View on Github →

feat(archive/100-theorems-list): Stirling, part 2 (#14875) feat(archive/100-theorems-list): Stirling Part 2

depends on: #14874 [part 1]

Estimated changes

Modified docs/100.yaml

Modified src/analysis/special_functions/stirling.lean

deleted theorem log_stirling_seq'_antitone

deleted theorem log_stirling_seq_bounded_aux

deleted theorem log_stirling_seq_bounded_by_constant

deleted theorem log_stirling_seq_diff_has_sum

deleted theorem log_stirling_seq_diff_le_geo_sum

deleted theorem log_stirling_seq_formula

deleted theorem log_stirling_seq_sub_log_stirling_seq_succ

added theorem stirling.log_stirling_seq'_antitone

added theorem stirling.log_stirling_seq_bounded_aux

added theorem stirling.log_stirling_seq_bounded_by_constant

added theorem stirling.log_stirling_seq_diff_has_sum

added theorem stirling.log_stirling_seq_diff_le_geo_sum

added theorem stirling.log_stirling_seq_formula

added theorem stirling.log_stirling_seq_sub_log_stirling_seq_succ

added theorem stirling.second_wallis_limit

added theorem stirling.stirling_seq'_antitone

added theorem stirling.stirling_seq'_bounded_by_pos_constant

added theorem stirling.stirling_seq'_pos

added theorem stirling.stirling_seq_has_pos_limit_a

added theorem stirling.stirling_seq_one

added theorem stirling.stirling_seq_pow_four_div_stirling_seq_pow_two_eq

added theorem stirling.stirling_seq_zero

added theorem stirling.tendsto_self_div_two_mul_self_add_one

added theorem stirling.tendsto_stirling_seq_sqrt_pi

added theorem stirling.tendsto_w_at_top:

deleted theorem stirling_seq'_antitone

deleted theorem stirling_seq'_bounded_by_pos_constant

deleted theorem stirling_seq'_pos

deleted theorem stirling_seq_has_pos_limit_a

deleted theorem stirling_seq_one

deleted theorem stirling_seq_zero