Commit 2023-06-01 19:05 d4a3d044

View on Github →

feat: port Analysis.Calculus.MeanValue (#4249)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/MeanValue.lean

added theorem Antitone.concaveOn_univ_of_deriv

added theorem AntitoneOn.concaveOn_of_deriv

added theorem Convex.antitoneOn_of_deriv_nonpos

added theorem Convex.eqOn_of_fderivWithin_eq

added theorem Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt

added theorem Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt

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.is_const_of_fderivWithin_eq_zero

added theorem Convex.lipschitzOnWith_of_nnnorm_derivWithin_le

added theorem Convex.lipschitzOnWith_of_nnnorm_deriv_le

added theorem Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le

added theorem Convex.lipschitzOnWith_of_nnnorm_fderiv_le

added theorem Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le

added theorem Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le

added theorem Convex.monotoneOn_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.norm_image_sub_le_of_norm_derivWithin_le

added theorem Convex.norm_image_sub_le_of_norm_deriv_le

added theorem Convex.norm_image_sub_le_of_norm_fderivWithin_le'

added theorem Convex.norm_image_sub_le_of_norm_fderivWithin_le

added theorem Convex.norm_image_sub_le_of_norm_fderiv_le'

added theorem Convex.norm_image_sub_le_of_norm_fderiv_le

added theorem Convex.norm_image_sub_le_of_norm_hasDerivWithin_le

added theorem Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le'

added theorem Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le

added theorem Convex.strictAntiOn_of_deriv_neg

added theorem Convex.strictMonoOn_of_deriv_pos

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 antitone_of_deriv_nonpos

added theorem concaveOn_of_deriv2_nonpos'

added theorem concaveOn_of_deriv2_nonpos

added theorem concaveOn_univ_of_deriv2_nonpos

added theorem constant_of_derivWithin_zero

added theorem constant_of_has_deriv_right_zero

added theorem convexOn_of_deriv2_nonneg'

added theorem convexOn_of_deriv2_nonneg

added theorem convexOn_univ_of_deriv2_nonneg

added theorem domain_mvt

added theorem eq_of_derivWithin_eq

added theorem eq_of_fderiv_eq

added theorem eq_of_has_deriv_right_eq

added theorem exists_deriv_eq_slope

added theorem exists_hasDerivAt_eq_slope

added theorem exists_ratio_deriv_eq_ratio_slope'

added theorem exists_ratio_deriv_eq_ratio_slope

added theorem exists_ratio_hasDerivAt_eq_ratio_slope'

added theorem exists_ratio_hasDerivAt_eq_ratio_slope

added theorem hasStrictDerivAt_of_hasDerivAt_of_continuousAt

added theorem hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt

added theorem image_le_of_deriv_right_le_deriv_boundary

added theorem image_le_of_deriv_right_lt_deriv_boundary'

added theorem image_le_of_deriv_right_lt_deriv_boundary

added theorem image_le_of_liminf_slope_right_le_deriv_boundary

added theorem image_le_of_liminf_slope_right_lt_deriv_boundary'

added theorem image_le_of_liminf_slope_right_lt_deriv_boundary

added theorem image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary

added theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary'

added theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary

added theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary'

added theorem image_norm_le_of_norm_deriv_right_lt_deriv_boundary

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_deriv_eq_zero

added theorem is_const_of_fderiv_eq_zero

added theorem lipschitzWith_of_nnnorm_deriv_le

added theorem monotone_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 norm_image_sub_le_of_norm_deriv_le_segment'

added theorem norm_image_sub_le_of_norm_deriv_le_segment

added theorem norm_image_sub_le_of_norm_deriv_le_segment_01'

added theorem norm_image_sub_le_of_norm_deriv_le_segment_01

added theorem norm_image_sub_le_of_norm_deriv_right_le_segment

added theorem strictAnti_of_deriv_neg

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

added theorem strictMono_of_deriv_pos