Commit 2021-12-23 16:33 1a57c79e

View on Github →

feat(analysis/calculus): assorted simple lemmas (#10975) Various lemmas from the formalization of the Cauchy integral formula (#10000 and some later developments on top of it). Also add @[measurability] attrs to theorems like measurable_fderiv.

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem has_deriv_within_at.scomp_has_deriv_at

Modified src/analysis/calculus/fderiv.lean

added theorem differentiable_on.differentiable_at

added theorem differentiable_on.eventually_differentiable_at

Modified src/analysis/calculus/fderiv_measurable.lean

modified theorem measurable_deriv

modified theorem measurable_fderiv

modified theorem measurable_fderiv_apply_const

Modified src/analysis/calculus/mean_value.lean

added theorem is_const_of_deriv_eq_zero

added theorem lipschitz_with_of_nnnorm_deriv_le