Theorems · Theorem · real analysis

Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} {f' : E → E →L[𝕜] G},
  Convex ℝ s →
    ∀ {f : E → G},
      (∀ᶠ (y : E) in nhdsWithin x s, HasFDerivWithinAt f (f' y) s y) →
        ContinuousWithinAt f' s x → ∀ (K : NNReal), ‖f' x‖₊ < K → ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t

Let s be a convex set in a real normed vector space E, let f : E → G be a function differentiable within s in a neighborhood of x : E with derivative f'. Suppose that f' is continuous within s at x. Then for any number K : ℝ≥0 larger than ‖f' x‖₊, f is K-Lipschitz on some neighborhood of x within s. See also Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt for a version that claims existence of K instead of an explicit estimate.

Defined in

Mathlib.Analysis.Calculus.MeanValue

Cited by

2 results in Mathlib

Foundations

Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNontriviallyNormedFieldIsRCLikeNormedFieldNormedSpaceNormedAddCommGroupNormedSpace