Theorem 3.1 — box-robust sample average optimization is consistent

Proved

DistInterpRO.Consistency.theorem_3_1

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

consistencydistributionally-robust-optimizationkernel-density-estimationp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1robust-optimization

Let $V$ be a set of decisions, $\mathcal F\subseteq V$ a nonempty feasible set, and $f:V\times\mathbb R^m\to\mathbb R$ a utility with $f(v,\cdot)$ Borel measurable for every $v$ , satisfying

Boundedness: $|f(v,x)|\le C$ for all $v,x$ ;
Equicontinuity: $d(\epsilon)\to0$ as $\epsilon\downarrow0$ , where $d(\epsilon)=\sup_{v,x,\|\delta\|_\infty\le\epsilon}|f(v,x)-f(v,x+\delta)|$ .

Let $h^*$ be a probability density on $\mathbb R^m$ and $x_1,x_2,\dots$ i.i.d. samples from $h^*$ on a probability space. Let $\epsilon(n)>0$ satisfy

\epsilon(n)\downarrow0,\qquad n\,\epsilon(n)^m\uparrow\infty .

For each $n$ and each sample, let $v(n)$ be any maximiser over $\mathcal F$ of the box-robust objective

v\ \mapsto\ \frac1n\sum_{i=1}^n\ \inf_{\|\delta_i\|_\infty\le\epsilon(n)} f(v,x_i+\delta_i).

Then, with probability one,

\lim_{n\to\infty}\int_{\mathbb R^m}f(v(n),x)\,h^*(x)\,dx\ =\ \sup_{v\in\mathcal F}\int_{\mathbb R^m}f(v,x)\,h^*(x)\,dx;

that is, the robust optimization formulation is consistent.

The theorem says that robustifying a sampled stochastic program with $\ell_\infty$ boxes whose radius shrinks at the stated rate recovers the optimal expected utility, under boundedness and equicontinuity alone.

Formalization Note $\mathbb R^m$ is Fin m → ℝ with the sup norm. The samples $x_1,x_2,\dots$ are X 0, X 1, … (independent via iIndepFun, each with law volume.withDensity h*), and the $n$ -th problem uses the first $n$ . The maximisers form an arbitrary selection v n ω of the argmax — no measurability is assumed and the statement holds for every such selection; the paper's "arg max" presupposes that a maximiser exists, which is taken as a hypothesis. Implicit hypotheses made explicit: $\mathcal F\neq\emptyset$ , $\epsilon(n)>0$ (the kernel divides by $\epsilon(n)$ ), measurability of each $f(v,\cdot)$ , and that $h^*$ is a Lebesgue density (the paper integrates $h^*(x)\,dx$ ). " $\max_{v,x}|f|\le C$ " is read as the uniform bound $|f|\le C$ , the "max" in $d$ as a supremum, and " $d(\epsilon)\downarrow0$ " as $d(\epsilon)\to0$ as $\epsilon\downarrow0$ ( $d$ is automatically nondecreasing). The monotonicity in " $\epsilon(n)\downarrow0$ " and " $n\epsilon(n)^m\uparrow\infty$ " is kept as printed. The supremum on the right is a real supremum over the nonempty set $\mathcal F$ of values bounded by $C$ . Hypotheses range over all $v\in V$ ; instantiating $V=\mathcal F$ gives the version with hypotheses on $\mathcal F$ only.

Preamble

import Mathlib
import Definitions.Def_DistInterpRO_Consistency_Model

open MeasureTheory Filter Topology ProbabilityTheory

Formal statement

namespace DistInterpRO.Consistency

theorem theorem_3_1 {V : Type*} {m : ℕ} (F : Set V) (hF : F.Nonempty)
    (f : V → (Fin m → ℝ) → ℝ) (hfm : ∀ v, Measurable (f v))
    (C : ℝ) (hfC : ∀ v x, |f v x| ≤ C)
    (hd : Tendsto (modulus f) (𝓝[>] 0) (𝓝 0))
    (hstar : (Fin m → ℝ) → ℝ) (hstar_nonneg : ∀ x, 0 ≤ hstar x)
    (hstar_int : Integrable hstar) (hstar_one : ∫ x, hstar x = 1)
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (X : ℕ → Ω → Fin m → ℝ) (hXm : ∀ i, Measurable (X i)) (hind : iIndepFun X P)
    (hlaw : ∀ i, P.map (X i) = volume.withDensity (fun x => ENNReal.ofReal (hstar x)))
    (ε : ℕ → ℝ) (hε_pos : ∀ n, 0 < ε n)
    (hε_anti : Antitone ε) (hε_lim : Tendsto ε atTop (𝓝 0))
    (hnε_mono : Monotone (fun n : ℕ => (n : ℝ) * ε n ^ m))
    (hnε_lim : Tendsto (fun n : ℕ => (n : ℝ) * ε n ^ m) atTop atTop)
    (v : ℕ → Ω → V)
    (hv : ∀ n ω, v n ω ∈ F ∧ ∀ w ∈ F,
      roObjective f (ε n) (fun i : Fin n => X i ω) w ≤
        roObjective f (ε n) (fun i : Fin n => X i ω) (v n ω)) :
    ∀ᵐ ω ∂P, Tendsto (fun n : ℕ => ∫ x, f (v n ω) x * hstar x) atTop
      (𝓝 (⨆ w : F, ∫ x, f w x * hstar x)) := by sorry

end DistInterpRO.Consistency

Source

Xu, Caramanis and Mannor, A Distributional Interpretation of Robust Optimization, Math. Oper. Res. 37(1) (2012), p. 98, Theorem 3.1

Read-back

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

Let $V$ be an arbitrary type, $m \in \mathbb{N}$ , and $F \subseteq V$ a nonempty set. For each $v \in V$ , let $f_v : \mathbb{R}^m \to \mathbb{R}$ be a function, written $f(v, x)$ , that is Borel-measurable in $x$ . Assume $f$ is uniformly bounded by a real constant $C$ :

|f(v,x)| \le C \quad \text{for all } v \in V,\ x \in \mathbb{R}^m.

This forces $C \ge 0$ , because $V$ is nonempty. Assume also

\operatorname{modulus}(f)(t) \longrightarrow 0 \quad \text{as } t \to 0^{+}.

Here $\operatorname{modulus}(f)$ is a real-valued function of a real argument. It comes from the imported definitions file, whose code is not shown here, so what it measures cannot be stated. The only thing this hypothesis says is that its right-hand limit at $0$ is $0$ . The limit is taken over $t > 0$ only.

Let $h^\ast : \mathbb{R}^m \to \mathbb{R}$ satisfy these conditions:

$h^\ast(x) \ge 0$ for every $x$ ;
$h^\ast$ is Lebesgue-integrable;
$\int_{\mathbb{R}^m} h^\ast(x)\,dx = 1$ .

Let $(\Omega, P)$ be a probability space. Let $X_0, X_1, X_2, \dots : \Omega \to \mathbb{R}^m$ be measurable random vectors that are mutually independent under $P$ . Assume every $X_i$ has the law

P \circ X_i^{-1} = h^\ast(x)\,dx,

meaning Lebesgue measure with density $h^\ast$ .

Let $(\varepsilon_n)_{n \in \mathbb{N}}$ be a real sequence with these properties:

$\varepsilon_n > 0$ for every $n$ ;
it is non-increasing;
$\varepsilon_n \to 0$ ;
the sequence $n\,\varepsilon_n^{m}$ is non-decreasing in $n$ and tends to $+\infty$ .

Let $v_n : \Omega \to V$ be any maps, for $n \in \mathbb{N}$ . No measurability in $\omega$ is required. The hypothesis on them is: for every $n$ and every $\omega$ , $v_n(\omega) \in F$ , and for every $w \in F$ ,

\operatorname{roObjective}\big(f, \varepsilon_n, (X_0(\omega), \dots, X_{n-1}(\omega)), w\big) \;\le\; \operatorname{roObjective}\big(f, \varepsilon_n, (X_0(\omega), \dots, X_{n-1}(\omega)), v_n(\omega)\big).

In words, $v_n(\omega)$ maximizes $\operatorname{roObjective}$ over $F$ . That objective is built from $f$ , the radius $\varepsilon_n$ and the first $n$ samples. It is another imported definition whose code is not shown, so its formula cannot be described here. The hypothesis requires an exact maximizer to exist for every $n$ and every $\omega$ , not just almost surely. If for some $n$ and $\omega$ the maximum over $F$ is not attained, no such $v$ exists and the theorem holds vacuously.

Conclusion. For $P$ -almost every $\omega$ ,

\lim_{n \to \infty} \int_{\mathbb{R}^m} f\big(v_n(\omega), x\big)\, h^\ast(x)\,dx \;=\; \sup_{w \in F} \int_{\mathbb{R}^m} f(w, x)\, h^\ast(x)\,dx.

Both integrals are Lebesgue integrals. Each integrand is a measurable function bounded by $C$ multiplied by an integrable function, so it is integrable. Every integral in the family therefore lies in $[-C, C]$ , and the supremum is an ordinary finite real supremum over a nonempty, bounded-above set. It is not a default value.

Degenerate cases.

$n = 0$ : the sample tuple is empty, and $v_0(\omega)$ must maximize $\operatorname{roObjective}(f, \varepsilon_0, \text{empty sample}, \cdot)$ over $F$ . Also $0 \cdot \varepsilon_0^m = 0$ . This case affects nothing in the limit.
$m = 0$ : $\mathbb{R}^0$ is a single point, and Lebesgue measure on it is the unit point mass. Then $h^\ast$ must equal $1$ at that point, and every $X_i$ is constant. Since $\varepsilon_n^0 = 1$ , the conditions on $n\,\varepsilon_n^m$ reduce to " $n$ is non-decreasing and tends to $\infty$ ", which always holds. The conclusion becomes: almost surely, $f(v_n(\omega), \mathrm{pt}) \to \sup_{w \in F} f(w, \mathrm{pt})$ .
$F$ a single point $w_0$ : every $v_n(\omega) = w_0$ , and the conclusion holds trivially.
$V$ or $F$ empty: excluded by the nonemptiness of $F$ .
$\Omega$ : it cannot be empty, because it carries a probability measure.
Division, subtraction in $\mathbb{N}$ , or non-integrable integrals: none of these defaults appear in the statement itself. Whether any occur inside $\operatorname{modulus}$ or $\operatorname{roObjective}$ cannot be determined from the code shown.

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph