Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-29 08:52 acf2038a

View on Github →

feat(analysis/calculus/mean_value): more corollaries of the MVT (#1819)

feat(analysis/calculus/mean_value): more corolaries of the MVT
Fix compile, add "strict inequalities" versions of some theorems, add docs
Update src/analysis/calculus/mean_value.lean
Add theorems for convex_on univ
Fix comments
@sgouezel adds missing articles Thanks a lot! We don't have them in Russian, so it's hard for me to put them right. Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Update src/analysis/calculus/mean_value.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Add more univ versions

Estimated changes

Modified src/analysis/calculus/mean_value.lean

added theorem antimono_of_deriv_nonpos

added theorem convex.antimono_of_deriv_nonpos

added theorem convex.image_sub_le_mul_sub_of_deriv_le

added theorem convex.image_sub_lt_mul_sub_of_deriv_lt

added theorem convex.mono_of_deriv_nonneg

added theorem convex.mul_sub_le_image_sub_of_le_deriv

added theorem convex.mul_sub_lt_image_sub_of_lt_deriv

added theorem convex.strict_antimono_of_deriv_neg

added theorem convex.strict_mono_of_deriv_pos

added theorem convex_on_of_deriv2_nonneg

added theorem convex_on_of_deriv_mono

added theorem convex_on_univ_of_deriv2_nonneg

added theorem convex_on_univ_of_deriv_mono

added theorem image_sub_le_mul_sub_of_deriv_le

added theorem image_sub_lt_mul_sub_of_deriv_lt

added theorem is_const_of_fderiv_eq_zero

added theorem mono_of_deriv_nonneg

added theorem mul_sub_le_image_sub_of_le_deriv

added theorem mul_sub_lt_image_sub_of_lt_deriv

added theorem strict_antimono_of_deriv_neg

added theorem strict_mono_of_deriv_pos

Modified src/analysis/convex.lean

deleted theorem convex_on_linorder

added theorem convex_on_real_of_slope_mono_adjacent

added theorem linear_order.convex_on_of_lt