Positive combinations (Lemma 4.2.1(b))

Proved

BertsekasDP.kconvex_combination

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

k-convexity

Lemma 4.2.1(b). Let $g_1$ be $K$ -convex and $g_2$ be $L$ -convex, with $K \ge 0$ and $L \ge 0$ . Then for all scalars $\alpha > 0$ and $\rho > 0$ the positive combination is $(\alpha K + \rho L)$ -convex:

\alpha g_1 + \rho g_2 \quad \text{is} \quad (\alpha K + \rho L)\text{-convex}.

So the class of $K$ -convex functions is closed under positive linear combinations, with the constants combining by the very same combination. This is what makes $K$ -convexity usable inside a dynamic programming recursion, where each stage forms sums of a current cost and a discounted or weighted cost-to-go: the fixed-cost parameter propagates linearly rather than degrading uncontrollably.

Formalization Note The coefficients are only required to be strictly positive; they need not sum to $1$ , so the statement covers arbitrary positive combinations, not merely convex ones.

Preamble

import Mathlib
import Definitions.Def_BertsekasKConvex

Formal statement

namespace BertsekasDP

theorem kconvex_combination (K L α ρ : ℝ) (g₁ g₂ : ℝ → ℝ)
    (hK : 0 ≤ K) (hL : 0 ≤ L) (hα : 0 < α) (hρ : 0 < ρ)
    (h₁ : BertsekasKConvex K g₁) (h₂ : BertsekasKConvex L g₂) :
    BertsekasKConvex (α * K + ρ * L) (fun y => α * g₁ y + ρ * g₂ y) := by sorry

end BertsekasDP

Source

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

Read-back

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

Let $K, L, \alpha, \rho$ be real numbers and $g_1, g_2 : \mathbb{R} \to \mathbb{R}$ functions. Assume: $0 \le K$ ; $0 \le L$ ; $0 < \alpha$ ; $0 < \rho$ ; $g_1$ satisfies the bundle's $K$ -convexity property (for all $z \ge 0$ , $b > 0$ , $y \in \mathbb{R}$ : $g_1(y) + \tfrac{z}{b}(g_1(y) - g_1(y-b)) \le K + g_1(z+y)$ ); and $g_2$ satisfies the same property with constant $L$ . The conclusion is that the function $y \mapsto \alpha\, g_1(y) + \rho\, g_2(y)$ satisfies the bundle's property with constant $\alpha K + \rho L$ , i.e. for all $z \ge 0$ , $b > 0$ , $y \in \mathbb{R}$ :

\bigl(\alpha g_1 + \rho g_2\bigr)(y) + \frac{z}{b}\Bigl(\bigl(\alpha g_1 + \rho g_2\bigr)(y) - \bigl(\alpha g_1 + \rho g_2\bigr)(y-b)\Bigr) \;\le\; \alpha K + \rho L + \bigl(\alpha g_1 + \rho g_2\bigr)(z+y).

The coefficients $\alpha, \rho$ are only required to be strictly positive; they are not required to sum to $1$ , so this covers arbitrary positive linear combinations, not only convex combinations.

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