Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-23 09:02 ced1f120

View on Github →

feat(analysis/calculus): strictly differentiable (or C^1) map is locally Lipschitz (#8362)

Estimated changes

Modified src/analysis/calculus/fderiv.lean

added theorem has_strict_fderiv_at.exists_lipschitz_on_with

added theorem has_strict_fderiv_at.exists_lipschitz_on_with_of_nnnorm_lt

Modified src/analysis/calculus/mean_value.lean

added theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at

deleted theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_continuous_within_at

added theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt

Modified src/analysis/calculus/times_cont_diff.lean

added theorem has_ftaylor_series_up_to_on.exists_lipschitz_on_with

added theorem has_ftaylor_series_up_to_on.exists_lipschitz_on_with_of_nnnorm_lt

added theorem times_cont_diff_at.exists_lipschitz_on_with

added theorem times_cont_diff_at.exists_lipschitz_on_with_of_nnnorm_lt

added theorem times_cont_diff_within_at.exists_lipschitz_on_with

Modified src/analysis/normed_space/basic.lean

modified theorem add_monoid_hom.lipschitz_of_bound

added theorem add_monoid_hom.lipschitz_of_bound_nnnorm

added theorem lipschitz_with_iff_norm_sub_le

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.is_O_with_comp

added theorem continuous_linear_map.is_O_with_id

added theorem continuous_linear_map.is_O_with_sub

added theorem continuous_linear_map.le_op_nnnorm

modified theorem continuous_linear_map.lipschitz

added theorem linear_map.lipschitz_of_bound_nnnorm