Quadratic Increment Characterisation of Semiconvexity

Let $n$ be a natural number with $1\le n$ and let $\mathbb{R}$ be the real numbers with the order $\le$ of their ordered field structure; write $2$ for $1+1$, which satisfies $0<2$ and therefore has a multiplicative inverse by claim 8 of Elementary Order Arithmetic in an Ordered Field, and write $\tfrac{s}{2}$ for the product of $s$ with that inverse. For a real number $s$ write $s^{2}$ for the power $s\cdot s$. Regard Euclidean space $\mathbb{R}^{n}$ as a real vector space, with the sum of points and the scalar multiple, write $x-y$ for the difference of points, and let $\lVert\,\cdot\,\rVert$ be the Euclidean norm.

Let $C\subseteq\mathbb{R}^{n}$ be convex, let $f:C\to\mathbb{R}$, and let $\mu\in\mathbb{R}$ satisfy $0\le\mu$.

Then $f$ is semiconvex on $C$ with constant $\mu$ if and only if for all $x,y\in C$ and every $t\in\mathbb{R}$ with $0\le t$ and $t\le 1$,

$$f\bigl(t\,x+(1-t)\,y\bigr)\le t\,f(x)+(1-t)\,f(y)+\frac{\mu}{2}\,t(1-t)\,\lVert x-y\rVert^{2},$$

the point $t\,x+(1-t)\,y$ lying in $C$ because $C$ is convex.