Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 22:42 c192937f

View on Github →

feat(analysis): derivative of a parametric interval integral (#10404)

Estimated changes

Created src/analysis/calculus/parametric_interval_integral.lean

added theorem interval_integral.has_deriv_at_integral_of_dominated_loc_of_deriv_le

added theorem interval_integral.has_deriv_at_integral_of_dominated_loc_of_lip

added theorem interval_integral.has_fderiv_at_integral_of_dominated_loc_of_lip

added theorem interval_integral.has_fderiv_at_integral_of_dominated_of_fderiv_le

Modified src/measure_theory/constructions/borel_space.lean

added theorem measurable_set_interval_oc