Structure of continuous coercive K-convex functions (Lemma 4.2.1(d))

Proved

BertsekasDP.kconvex_sS_structure

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

inventorycontrolk-convexitysspolicy

Lemma 4.2.1(d) (the $(s,S)$ structure). Let $K \ge 0$ and let $g$ be a continuous $K$ -convex function with $g(y) \to \infty$ as $|y| \to \infty$ . Then there exist scalars $s \le S$ such that:

$S$ is a global minimizer: $g(S) \le g(y)$ for every $y$ ;
$s$ is the reorder threshold, exactly $K$ above the minimum:

g(S) + K \;=\; g(s) \;<\; g(y) \qquad \text{for every } y < s ;

$g$ is non-increasing on $(-\infty, s)$ ;
no gain exceeds the fixed cost to the right of $s$ :

g(y) \;\le\; g(z) + K \qquad \text{for all } s \le y \le z .

These four properties are precisely what is needed to conclude that an $(s,S)$ policy is optimal: below $s$ the saving from moving to $S$ exceeds the fixed cost $K$ , so one orders up to $S$ ; at or above $s$ property 4 says no reachable point beats the current one by more than $K$ , so one does not order. This is the structural heart of Scarf's theorem on the optimality of $(s,S)$ inventory policies.

Formalization Note Existence is asserted, not uniqueness — several pairs $(s,S)$ may satisfy the conclusion. Property 2 is an exact equality $g(S) + K = g(s)$ , not an inequality, together with a strict inequality to the left of $s$ . Property 3 is stated on the open ray $(-\infty,s)$ and says nothing at $s$ itself. Coercivity is stated as divergence to $+\infty$ along both ends of the line.

Preamble

import Mathlib
import Definitions.Def_BertsekasKConvex

Formal statement

namespace BertsekasDP

theorem kconvex_sS_structure (K : ℝ) (g : ℝ → ℝ) (hK : 0 ≤ K)
    (hg : BertsekasKConvex K g) (hcont : Continuous g)
    (hcoer₁ : Filter.Tendsto g Filter.atTop Filter.atTop)
    (hcoer₂ : Filter.Tendsto g Filter.atBot Filter.atTop) :
    ∃ s S : ℝ, s ≤ S ∧
      (∀ y, g S ≤ g y) ∧
      (g S + K = g s) ∧
      (∀ y < s, g s < g y) ∧
      AntitoneOn g (Set.Iio s) ∧
      (∀ y z, s ≤ y → y ≤ z → g y ≤ g z + K) := by sorry

end BertsekasDP

Source

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

Read-back

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

Let $K$ be a real number with $0 \le K$ and $g : \mathbb{R} \to \mathbb{R}$ a function satisfying: the bundle's $K$ -convexity property (for all $z \ge 0$ , $b > 0$ , $y$ : $g(y) + \tfrac{z}{b}(g(y) - g(y-b)) \le K + g(z+y)$ ); continuity of $g$ on all of $\mathbb{R}$ ; $g(y) \to +\infty$ as $y \to +\infty$ ; and $g(y) \to +\infty$ as $y \to -\infty$ . The conclusion asserts the existence (plain $\exists$ , not unique existence) of two real numbers $s$ and $S$ such that all six of the following hold:

$s \le S$ ;
$S$ is a global minimizer of $g$ : for every $y \in \mathbb{R}$ , $g(S) \le g(y)$ ;
the exact equality $g(S) + K = g(s)$ (not an inequality: the value of $g$ at $s$ equals the minimum plus exactly $K$ );
for every $y < s$ , the strict inequality $g(s) < g(y)$ ;
$g$ is antitone (non-increasing) on the open ray $(-\infty, s)$ : for all $y, z$ with $y < s$ , $z < s$ , and $y \le z$ , one has $g(z) \le g(y)$ (this says nothing about the point $s$ itself or beyond it);
for all $y, z$ with $s \le y$ and $y \le z$ : $g(y) \le g(z) + K$ .

Edge case: $K = 0$ is allowed by the hypothesis $0 \le K$ ; in that case the third clause forces $g(s) = g(S)$ while the fourth still demands $g(s) < g(y)$ strictly for all $y < s$ .

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