Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-14 12:02 cc1690e3

View on Github →

feat(analysis/calculus/parametric_integral): derivative of parametric integrals (#7437) from the sphere eversion project

Estimated changes

Created src/analysis/calculus/parametric_integral.lean

added theorem has_deriv_at_of_dominated_loc_of_deriv_le

added theorem has_deriv_at_of_dominated_loc_of_lip

added theorem has_fderiv_at_of_dominated_loc_of_lip'

added theorem has_fderiv_at_of_dominated_loc_of_lip

added theorem has_fderiv_at_of_dominated_of_fderiv_le

Modified src/data/real/nnreal.lean

added theorem nnreal.coe_of_real_le

added theorem real.nnabs_of_nonneg