Commit 2024-03-22 16:42 ab37dcaf

View on Github →

refactor(Analysis/Calculus/MeanValue): move convexity material elsewhere (#11588) This PR carves off lemmas about convex functions from Analysis/Calculus/MeanValue.lean and relocates them to a new file. (This is a preparatory step for adding some more lemmas on this topic, since MeanValue.lean is already over-long.)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/MeanValue.lean

deleted theorem Antitone.concaveOn_univ_of_deriv

deleted theorem AntitoneOn.concaveOn_of_deriv

deleted theorem Monotone.convexOn_univ_of_deriv

deleted theorem MonotoneOn.convexOn_of_deriv

deleted theorem StrictAnti.strictConcaveOn_univ_of_deriv

deleted theorem StrictAntiOn.strictConcaveOn_of_deriv

deleted theorem StrictMono.strictConvexOn_univ_of_deriv

deleted theorem StrictMonoOn.exists_deriv_lt_slope

deleted theorem StrictMonoOn.exists_deriv_lt_slope_aux

deleted theorem StrictMonoOn.exists_slope_lt_deriv

deleted theorem StrictMonoOn.exists_slope_lt_deriv_aux

deleted theorem StrictMonoOn.strictConvexOn_of_deriv

deleted theorem concaveOn_of_deriv2_nonpos'

deleted theorem concaveOn_of_deriv2_nonpos

deleted theorem concaveOn_of_hasDerivWithinAt2_nonpos

deleted theorem concaveOn_univ_of_deriv2_nonpos

deleted theorem convexOn_of_deriv2_nonneg'

deleted theorem convexOn_of_deriv2_nonneg

deleted theorem convexOn_of_hasDerivWithinAt2_nonneg

deleted theorem convexOn_univ_of_deriv2_nonneg

deleted theorem strictConcaveOn_of_deriv2_neg'

deleted theorem strictConcaveOn_of_deriv2_neg

deleted theorem strictConcaveOn_univ_of_deriv2_neg

deleted theorem strictConvexOn_of_deriv2_pos'

deleted theorem strictConvexOn_of_deriv2_pos

deleted theorem strictConvexOn_univ_of_deriv2_pos

Created Mathlib/Analysis/Convex/Deriv.lean

added theorem Antitone.concaveOn_univ_of_deriv

added theorem AntitoneOn.concaveOn_of_deriv

added theorem Monotone.convexOn_univ_of_deriv

added theorem MonotoneOn.convexOn_of_deriv

added theorem StrictAnti.strictConcaveOn_univ_of_deriv

added theorem StrictAntiOn.strictConcaveOn_of_deriv

added theorem StrictMono.strictConvexOn_univ_of_deriv

added theorem StrictMonoOn.exists_deriv_lt_slope

added theorem StrictMonoOn.exists_deriv_lt_slope_aux

added theorem StrictMonoOn.exists_slope_lt_deriv

added theorem StrictMonoOn.exists_slope_lt_deriv_aux

added theorem StrictMonoOn.strictConvexOn_of_deriv

added theorem concaveOn_of_deriv2_nonpos'

added theorem concaveOn_of_deriv2_nonpos

added theorem concaveOn_of_hasDerivWithinAt2_nonpos

added theorem concaveOn_univ_of_deriv2_nonpos

added theorem convexOn_of_deriv2_nonneg'

added theorem convexOn_of_deriv2_nonneg

added theorem convexOn_of_hasDerivWithinAt2_nonneg

added theorem convexOn_univ_of_deriv2_nonneg

added theorem strictConcaveOn_of_deriv2_neg'

added theorem strictConcaveOn_of_deriv2_neg

added theorem strictConcaveOn_univ_of_deriv2_neg

added theorem strictConvexOn_of_deriv2_pos'

added theorem strictConvexOn_of_deriv2_pos

added theorem strictConvexOn_univ_of_deriv2_pos

Modified Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean

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

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean