Commit 2025-12-23 12:27 987f1b48

View on Github →

feat: add ContDiff.lipschitzOnWith (#30612) A C¹ function is Lipschitz on each convex compact set. From sphere-eversion. Re-done version of https://github.com/leanprover-community/mathlib4/pull/12673.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/RCLike.lean

added theorem ContDiffOn.exists_lipschitzOnWith

added theorem ContDiffOn.locallyLipschitzOn

modified theorem ContDiffWithinAt.exists_lipschitzOnWith

modified theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith

modified theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt

Modified Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean

added theorem LocallyLipschitzOn.exists_lipschitzOnWith_of_compact

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

added theorem lipschitzOnWith_closure_iff