Commit 2023-05-24 15:17 009b0477

View on Github →

chore: forward-port #19026 (#4129) Fiddly, not done yet ... help welcome. Cross-reference: https://github.com/leanprover-community/mathlib/pull/19026.

Estimated changes

Modified Mathlib/Analysis/Convex/Slope.lean

added theorem ConvexOn.secant_mono

added theorem ConvexOn.secant_mono_aux1

added theorem ConvexOn.secant_mono_aux2

added theorem ConvexOn.secant_mono_aux3

added theorem StrictConcaveOn.secant_strict_mono

added theorem StrictConvexOn.secant_strict_mono

added theorem StrictConvexOn.secant_strict_mono_aux1

added theorem StrictConvexOn.secant_strict_mono_aux2

added theorem StrictConvexOn.secant_strict_mono_aux3

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

added theorem Real.log_lt_sub_one_of_pos

Modified Mathlib/Data/Complex/Exponential.lean

modified theorem Real.add_one_le_exp_of_nonneg

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