Convex ⟹ K-convex (Lemma 4.2.1(a))

Proved

BertsekasDP.kconvex_of_convex

by Shuze Chen · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

k-convexity

Lemma 4.2.1(a). Every real-valued convex function $g$ on the line is $0$ -convex, and hence $K$ -convex for every $K \ge 0$ :

g(y) + \frac{z}{b}\bigl(g(y) - g(y-b)\bigr) \;\le\; K + g(z+y) \qquad \text{for all } z \ge 0, \; b > 0, \; y \in \mathbb{R}, \; K \ge 0.

The content is that $K$ -convexity genuinely generalizes convexity, so the machinery developed for fixed ordering costs applies verbatim to the zero-fixed-cost case treated earlier in §4.2. Concretely, the chord slope of a convex function over $[y-b,y]$ never exceeds its average rate of increase to the right of $y$ , which is the inequality above with $K = 0$ ; enlarging $K$ only weakens it.

Formalization Note Convexity is assumed on all of $\mathbb{R}$ in Mathlib's sense, with no continuity hypothesis added. The conclusion is stated as a conjunction — the $K=0$ case and the case of arbitrary $K \ge 0$ — even though the first is the instance $K = 0$ of the second.

Preamble

import Mathlib
import Definitions.Def_BertsekasKConvex

Formal statement

namespace BertsekasDP

theorem kconvex_of_convex (g : ℝ → ℝ) (hg : ConvexOn ℝ Set.univ g) :
    BertsekasKConvex 0 g ∧ ∀ K : ℝ, 0 ≤ K → BertsekasKConvex K g := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Lemma 4.2.1(a)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let $g : \mathbb{R} \to \mathbb{R}$ and assume $g$ is convex on all of $\mathbb{R}$ in the standard sense: for all $x, y \in \mathbb{R}$ and all reals $a, b \ge 0$ with $a + b = 1$ ,

g(a x + b y) \;\le\; a\, g(x) + b\, g(y).

(No continuity is assumed; convexity on the whole line is the only hypothesis.) The conclusion is a conjunction of two claims: (1) $g$ satisfies the bundle's $K$ -convexity property with $K = 0$ , i.e. for all $z \ge 0$ , $b > 0$ , $y$ : $g(y) + \tfrac{z}{b}(g(y) - g(y-b)) \le g(z+y)$ ; and (2) for every real $K$ with $0 \le K$ , $g$ satisfies the bundle's property with that constant $K$ , i.e. $g(y) + \tfrac{z}{b}(g(y) - g(y-b)) \le K + g(z+y)$ for all $z \ge 0$ , $b > 0$ , $y$ . Note that the first conjunct is exactly the instance $K = 0$ of the second, so the two conjuncts are not independent.

Human review

Endorsed by Community (Bot) · Sep 8, 2026
Endorsed by Shuze Chen · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph