Expectation preserves K-convexity (Lemma 4.2.1(c))

Proved

BertsekasDP.kconvex_expectation

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

expectationk-convexity

Lemma 4.2.1(c). Let $g$ be $K$ -convex and let $w$ be a random variable taking finitely many values, with probabilities $p_\omega \ge 0$ summing to $1$ . Then the expectation

y \;\longmapsto\; \mathbb{E}_w\bigl[g(y - w)\bigr] \;=\; \sum_{\omega} p_\omega \, g\bigl(y - w_\omega\bigr)

is again $K$ -convex, with the same constant $K$ .

This is the step that carries $K$ -convexity across a stage of the inventory recursion: after the ordering decision, the stock is reduced by a random demand, and the resulting expected cost-to-go must remain $K$ -convex for the argument to continue by induction. That the constant does not grow is what keeps the eventual $(s,S)$ structure tied to the single fixed ordering cost.

Formalization Note The disturbance is finitely supported, so the expectation is a finite weighted sum and the source's integrability proviso $\mathbb{E}|g(y-w)| < \infty$ is automatic. Individual weights may be zero; the hypothesis that they sum to $1$ makes the statement vacuous over an empty outcome type.

Preamble

import Mathlib
import Definitions.Def_BertsekasKConvex

Formal statement

namespace BertsekasDP

theorem kconvex_expectation {Ω : Type} [Fintype Ω] (K : ℝ) (g : ℝ → ℝ)
    (p : Ω → ℝ) (hp : ∀ ω, 0 ≤ p ω) (hsum : ∑ ω, p ω = 1) (w : Ω → ℝ)
    (hg : BertsekasKConvex K g) :
    BertsekasKConvex K (fun y => ∑ ω, p ω * g (y - w ω)) := by sorry

end BertsekasDP

Source

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

Read-back

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

Let $\Omega$ be a finite type (an implicit argument; $\Omega$ may be empty), $K$ a real number, $g : \mathbb{R} \to \mathbb{R}$ , $p : \Omega \to \mathbb{R}$ , and $w : \Omega \to \mathbb{R}$ . Assume: $p(\omega) \ge 0$ for every $\omega \in \Omega$ ; $\sum_{\omega \in \Omega} p(\omega) = 1$ ; and $g$ satisfies 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)$ ). The conclusion is that the function

y \;\longmapsto\; \sum_{\omega \in \Omega} p(\omega)\, g\bigl(y - w(\omega)\bigr)

satisfies the bundle's property with the same constant $K$ . There is no hypothesis $K \ge 0$ stated here (though, as noted in the definition's read-back, $K$ -convexity of $g$ itself forces $0 \le K$ whenever $\Omega$ -independent instantiation $z=0$ is applied to $hg$ ). Edge case: if $\Omega$ is empty, the hypothesis $\sum_\omega p(\omega) = 1$ reads $0 = 1$ and is unsatisfiable, so the theorem is vacuously true for empty $\Omega$ . The "expectation" is a finite weighted sum with weights $p$ ; no probability-theoretic structure beyond nonnegativity and summing to $1$ is involved, and the weights are not required to be positive (individual $p(\omega)$ may be $0$ ).

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