Commit 2021-07-17 17:47 7d754e06

View on Github →

chore(analysis/calculus/mean_value): use nnnorm in a few lemmas (#8348) Use nnnorm instead of norm and C : nnreal in lemmas about lipschitz_on_with. This way we can use them to prove any statement of the form lipschitz_on_with C f s, not only something of the form lipschitz_on_with (real.to_nnreal C) f s.

Estimated changes

Modified src/analysis/calculus/mean_value.lean

added theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_continuous_within_at

added theorem convex.lipschitz_on_with_of_nnnorm_deriv_le

added theorem convex.lipschitz_on_with_of_nnnorm_deriv_within_le

added theorem convex.lipschitz_on_with_of_nnnorm_fderiv_le

added theorem convex.lipschitz_on_with_of_nnnorm_fderiv_within_le

added theorem convex.lipschitz_on_with_of_nnnorm_has_deriv_within_le

added theorem convex.lipschitz_on_with_of_nnnorm_has_fderiv_within_le

deleted theorem convex.lipschitz_on_with_of_norm_deriv_le

deleted theorem convex.lipschitz_on_with_of_norm_deriv_within_le

deleted theorem convex.lipschitz_on_with_of_norm_fderiv_le

deleted theorem convex.lipschitz_on_with_of_norm_fderiv_within_le

deleted theorem convex.lipschitz_on_with_of_norm_has_deriv_within_le

deleted theorem convex.lipschitz_on_with_of_norm_has_fderiv_within_le

Modified src/analysis/calculus/parametric_integral.lean

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.nnnorm_smul_right_apply

Modified src/data/real/nnreal.lean