Commit 2023-06-09 10:15 f92a1528

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Stirling.lean

added theorem Stirling.log_stirlingSeq'_antitone

added theorem Stirling.log_stirlingSeq_bounded_aux

added theorem Stirling.log_stirlingSeq_bounded_by_constant

added theorem Stirling.log_stirlingSeq_diff_hasSum

added theorem Stirling.log_stirlingSeq_diff_le_geo_sum

added theorem Stirling.log_stirlingSeq_formula

added theorem Stirling.log_stirlingSeq_sub_log_stirlingSeq_succ

added theorem Stirling.second_wallis_limit

added theorem Stirling.stirlingSeq'_antitone

added theorem Stirling.stirlingSeq'_bounded_by_pos_constant

added theorem Stirling.stirlingSeq'_pos

added theorem Stirling.stirlingSeq_has_pos_limit_a

added theorem Stirling.stirlingSeq_one

added theorem Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq

added theorem Stirling.stirlingSeq_zero

added theorem Stirling.tendsto_self_div_two_mul_self_add_one

added theorem Stirling.tendsto_stirlingSeq_sqrt_pi