Commit 2023-12-17 15:16 d84bf685

View on Github →

feat: x ^ n / n ! ≤ exp x (#9099) Also make private/delete the intermediate lemmas of the form x + 1 ≤ Real.exp x so that people use the more general final results instead.

Estimated changes

Modified Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

Modified Mathlib/Combinatorics/Additive/Behrend.lean

Modified Mathlib/Data/Complex/Exponential.lean

deleted theorem Real.add_one_le_exp_of_nonneg

added theorem Real.add_one_lt_exp

deleted theorem Real.add_one_lt_exp_of_neg

deleted theorem Real.add_one_lt_exp_of_nonzero

deleted theorem Real.add_one_lt_exp_of_pos

added theorem Real.exp_abs_le

added theorem Real.exp_nonneg

deleted theorem Real.one_sub_le_exp_minus_of_nonneg

added theorem Real.one_sub_le_exp_neg

deleted theorem Real.one_sub_lt_exp_minus_of_pos

added theorem Real.one_sub_lt_exp_neg

added theorem Real.pow_div_factorial_le_exp