Commit 2026-06-13 17:40 9e7b1c11

feat(Analysis/Complex/Exponential): add new bounds on exponential (#39690) We add new upper bounds on Real.exp in terms of 2x/(2+x), and use these to move some bounds on log higher in mathlib. We also add a lemma for the common bound (1+1/n)^n <= e, though this is a special-case of one_sub_div_pow_le_exp_neg (immediately before), but is added for convenience and discoverability, as this is a "well-known" bound.