English
A function is m-strongly convex on s if and only if it is uniformly convex on s with modulus φ(r) = m/2 · r^2.
Русский
Функция на множестве s является m‑сильно выпуклой тогда и только тогда, когда она униформно выпукла на s с модулем φ(r) = (m/2) r^2.
LaTeX
$$$$ \text{StrongConvexOn}(s,m,f) \iff \text{UniformConvexOn}(s,\lambda r. \tfrac{m}{2} r^2)(f). $$$$
Lean4
/-- A function `f` from a real normed space is `m`-strongly convex if it is uniformly convex with
modulus `φ(r) = m / 2 * r ^ 2`.
In an inner product space, this is equivalent to `x ↦ f x - m / 2 * ‖x‖ ^ 2` being convex. -/
def StrongConvexOn (s : Set E) (m : ℝ) : (E → ℝ) → Prop :=
UniformConvexOn s fun r ↦ m / (2 : ℝ) * r ^ 2
