Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 15:47 8f000ca2

View on Github →

feat(analysis/special_functions/exp): add lemmas about is_o/is_O/is_Theta (#15506) Add lemmas about asymptotic comparison of exp (f x) and exp (g x).

Estimated changes

Modified src/analysis/special_functions/exp.lean

added theorem real.is_O_exp_comp_exp_comp

added theorem real.is_O_exp_comp_one

modified theorem real.is_O_one_exp_comp

added theorem real.is_Theta_exp_comp_exp_comp

added theorem real.is_Theta_exp_comp_one

modified theorem real.is_bounded_under_ge_exp_comp

modified theorem real.is_bounded_under_le_exp_comp

added theorem real.is_o_exp_comp_exp_comp

added theorem real.is_o_one_exp_comp

modified theorem real.tendsto_comp_exp_at_bot

modified theorem real.tendsto_comp_exp_at_top

modified theorem real.tendsto_exp_comp_at_top

added theorem real.tendsto_exp_comp_nhds_zero