Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-18 08:44 c158ce85

View on Github →

feat(analysis/calculus): converse mean value inequality (#4173) Also restate mean value inequality in terms of lipschitz_on_with. From the sphere eversion project.

Estimated changes

Modified src/analysis/calculus/fderiv.lean

added theorem fderiv_at.le_of_lip

added theorem has_fderiv_at.le_of_lip

Modified src/analysis/calculus/mean_value.lean

added theorem convex.lipschitz_on_with_of_norm_deriv_le

added theorem convex.lipschitz_on_with_of_norm_deriv_within_le

added theorem convex.lipschitz_on_with_of_norm_fderiv_le

added theorem convex.lipschitz_on_with_of_norm_fderiv_within_le

added theorem convex.lipschitz_on_with_of_norm_has_deriv_within_le

added theorem convex.lipschitz_on_with_of_norm_has_fderiv_within_le

Modified src/topology/metric_space/lipschitz.lean

added theorem lipschitz_on_with_empty