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