Theorems · Theorem · convex and discrete geometry

ConvexOn.lipschitzOnWith_of_abs_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {ε r M : ℝ},
  ConvexOn ℝ (Metric.ball x₀ r) f →
    0 < ε → (∀ (a : E), dist a x₀ < r → |f a| ≤ M) → LipschitzOnWith (2 * M / ε).toNNReal f (Metric.ball x₀ (r - ε))

Defined in

Mathlib.Analysis.Convex.Continuous

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace