Commit 2024-02-14 03:21 5bade013

View on Github →

feat: Variants of monotonicity from existence of a derivative (#10229) This PR provides variants of deriv lemmas stated in terms of HasDerivAt From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/Calculus/MeanValue.lean

deleted theorem Convex.antitoneOn_of_deriv_nonpos

deleted theorem Convex.monotoneOn_of_deriv_nonneg

deleted theorem Convex.strictAntiOn_of_deriv_neg

deleted theorem Convex.strictMonoOn_of_deriv_pos

added theorem StrictAntiOn_of_hasDerivWithinAt_pos

added theorem StrictMonoOn_of_hasDerivWithinAt_pos

added theorem antitoneOn_of_deriv_nonpos

added theorem antitoneOn_of_hasDerivWithinAt_nonpos

added theorem antitone_of_hasDerivAt_nonpos

added theorem concaveOn_of_hasDerivWithinAt2_nonpos

added theorem convexOn_of_hasDerivWithinAt2_nonneg

added theorem monotoneOn_of_deriv_nonneg

added theorem monotoneOn_of_hasDerivWithinAt_nonneg

added theorem monotone_of_hasDerivAt_nonneg

added theorem strictAntiOn_of_deriv_neg

added theorem strictAnti_of_hasDerivAt_pos

added theorem strictMonoOn_of_deriv_pos

added theorem strictMono_of_hasDerivAt_pos

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean