Commit 2023-05-17 22:36 a8b2226c

View on Github →

feat(analysis/convex/specific_functions): elementary convexity proofs (#19026) Give elementary proofs for the convexity of pow, zpow, exp, log and rpow, avoiding the second derivative test. See Zulip

Estimated changes

Modified src/analysis/convex/slope.lean

added theorem convex_on.secant_mono

added theorem convex_on.secant_mono_aux1

added theorem convex_on.secant_mono_aux2

added theorem convex_on.secant_mono_aux3

added theorem strict_concave_on.secant_strict_mono

added theorem strict_convex_on.secant_strict_mono

added theorem strict_convex_on.secant_strict_mono_aux1

added theorem strict_convex_on.secant_strict_mono_aux2

added theorem strict_convex_on.secant_strict_mono_aux3

Modified src/analysis/convex/specific_functions.lean

modified theorem convex_on_zpow

added theorem one_add_mul_self_le_rpow_one_add

added theorem one_add_mul_self_lt_rpow_one_add

Modified src/analysis/special_functions/log/basic.lean

added theorem real.log_lt_sub_one_of_pos

Modified src/data/complex/exponential.lean

deleted theorem real.add_one_le_exp_of_nonpos

added theorem real.add_one_lt_exp_of_neg

added theorem real.add_one_lt_exp_of_nonzero

added theorem real.add_one_lt_exp_of_pos

added theorem real.exp_bound_div_one_sub_of_interval'

deleted theorem real.exp_bound_div_one_sub_of_interval_approx

added theorem real.one_sub_le_exp_minus_of_nonneg

deleted theorem real.one_sub_le_exp_minus_of_pos

added theorem real.one_sub_lt_exp_minus_of_pos

added theorem real.quadratic_le_exp_of_nonneg

added theorem real.sum_le_exp_of_nonneg