Chapter 8, Theorem 2 — Edmundson-Madansky upper bound

Proved

StochasticProg.Bounds.thm2_edmundson_madansky_upper_bound

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

convex-optimizationextreme-pointsprobabilitystochastic-programming

Chapter 8, Theorem 2 (Birge & Louveaux, pp. 347-348): the Edmundson-Madansky upper bound.

Fix a probability space $(\Omega,\mu)$ , a complete normed real vector space $E$ , a compact set $\Xi\subseteq E$ , and a random vector $\xi:\Omega\to E$ with $\xi(\omega)\in\Xi$ almost surely and $\xi$ Bochner-integrable. Fix $\alpha$ , $D\subseteq\alpha$ , $x\in D$ , and $g:\alpha\to E\to\mathbb R$ with $g(x,\cdot)$ convex and continuous on $\Xi$ and $\omega\mapsto g(x,\xi(\omega))$ integrable. Let Ext be a type standing for the extreme points $\mathrm{ext}\,\Xi$ of $\mathrm{co}\,\Xi$ , carrying the discrete measurable-space structure (every subset measurable, matching the book's "Borel field ... the collection of all subsets"), and toE : Ext → E an embedding whose range is exactly $\mathrm{ext}\,\Xi$ (formally (convexHull ℝ Ξ).extremePoints ℝ). Let φ : E → Measure Ext assign to every $e\in\Xi$ a probability measure φ e on Ext with barycenter $e$ ,

\int_{\mathrm{Ext}} \mathrm{toE}(y)\,\varphi(e)(dy) = e \qquad (e\in\Xi),

such that $\omega\mapsto\varphi(\xi(\omega))(A)$ is measurable for every $A\subseteq\mathrm{Ext}$ (the disintegration hypothesis). Let μExt be a probability measure on Ext satisfying the book's defining equation (2.6),

\mu\mathrm{Ext}(A) = \int_\Omega \varphi(\xi(\omega))(A)\,d\mu(\omega) \qquad (A\subseteq\mathrm{Ext}),

and suppose $y\mapsto g(x,\mathrm{toE}(y))$ is $\mu\mathrm{Ext}$ -integrable. Then

\int_\Omega g(x,\xi(\omega))\,d\mu(\omega) \;\le\; \int_{\mathrm{Ext}} g(x,\mathrm{toE}(y))\,d\mu\mathrm{Ext}(y) ,

i.e. $\mathbb E(g(x)) \le \int_{\mathrm{ext}\Xi} g(x,e)\,\lambda(de)$ , the book's (2.5).

Formalization Note μExt (the book's $\lambda$ , renamed since λ is a reserved Lean keyword) is taken as a hypothesis satisfying its defining equation rather than constructed from φ, since the book's own proof does not construct it either — constructing a measure from a set function via eq. (2.6) is a separate, book-external piece of measure theory. The barycenter condition on φ and the measurability of $\omega\mapsto\varphi(\xi(\omega))(A)$ are both load-bearing hypotheses the book's proof genuinely uses, not boilerplate.

Preamble

import Mathlib

open MeasureTheory

Formal statement

namespace StochasticProg.Bounds

variable {Ω E α : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]

/-- Chapter 8, Theorem 2 (Birge & Louveaux, pp. 347-348): the Edmundson-Madansky upper bound.
`Ext` stands for the extreme points `extΞ` of `co Ξ`, carrying the Borel field of *all* its
subsets (`hExtσ`) that the book specifies; `toE` embeds `Ext` into `E` with range exactly
`extΞ`. For every `e ∈ Ξ`, `φ e` is a probability measure on `Ext` with barycenter `e`
(eq. 2.4) and `ω ↦ φ (ξ ω) A` measurable for every `A` (the disintegration hypothesis); `μExt`
is the probability measure on `Ext` defined from `φ` and `ξ` by eq. (2.6). Then
`E(g(x)) ≤ ∫_{extΞ} g(x, e) μExt(de)` (eq. 2.5). -/
theorem thm2_edmundson_madansky_upper_bound
    {Ξ : Set E} (hΞcompact : IsCompact Ξ)
    {Ext : Type*} [MeasurableSpace Ext] (hExtσ : ∀ A : Set Ext, MeasurableSet A)
    (toE : Ext → E) (hExt : Set.range toE = (convexHull ℝ Ξ).extremePoints ℝ)
    {ξ : Ω → E} (hξrange : ∀ᵐ ω ∂μ, ξ ω ∈ Ξ) (hξint : Integrable ξ μ)
    {D : Set α} {x : α} (hx : x ∈ D) {g : α → E → ℝ}
    (hgconv : ConvexOn ℝ Ξ (g x)) (hgcont : ContinuousOn (g x) Ξ)
    (hgint : Integrable (fun ω => g x (ξ ω)) μ)
    (φ : E → Measure Ext) [∀ e, IsProbabilityMeasure (φ e)]
    (hbary : ∀ e ∈ Ξ, ∫ y : Ext, toE y ∂(φ e) = e)
    (hφmeas : ∀ A : Set Ext, Measurable fun ω => (φ (ξ ω)) A)
    (μExt : Measure Ext) [IsProbabilityMeasure μExt]
    (hμExtdef : ∀ A : Set Ext, μExt A = ∫⁻ ω, (φ (ξ ω)) A ∂μ)
    (hgeint : Integrable (fun y : Ext => g x (toE y)) μExt) :
    ∫ ω, g x (ξ ω) ∂μ ≤ ∫ y : Ext, g x (toE y) ∂μExt := by sorry

end StochasticProg.Bounds

Source

Birge & Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer 2011, p. 347-348, Chapter 8, Theorem 2 (eq. 2.4-2.6)

Read-back

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

Let $\Omega$ be a type equipped with a $\sigma$ -algebra and a probability measure $\mu$ (total mass $1$ ); let $E$ be a complete normed real vector space (a Banach space); and let $\alpha$ be an arbitrary type with no structure. The declaration is a universally quantified statement over the following data and hypotheses, all of which are assumptions.

Data and hypotheses.

$\Xi \subseteq E$ is a compact set. (No non-emptiness or convexity is assumed; $\Xi = \varnothing$ is permitted by this hypothesis alone.)
$\mathrm{Ext}$ is a type carrying a $\sigma$ -algebra, and it is assumed that every subset $A \subseteq \mathrm{Ext}$ is measurable for that $\sigma$ -algebra.
$\iota : \mathrm{Ext} \to E$ is a function (no measurability or injectivity is assumed) whose image is exactly the set of extreme points of the convex hull $\operatorname{co}\Xi$ of $\Xi$ :

\iota(\mathrm{Ext}) = \operatorname{ext}\big(\operatorname{co}\Xi\big).

(If $\operatorname{co}\Xi$ has no extreme points, this forces $\mathrm{Ext}$ to be empty, which is then incompatible with the existence of the probability measures below; in that case the hypotheses are unsatisfiable.)

$\xi : \Omega \to E$ is a function such that $\xi(\omega) \in \Xi$ for $\mu$ -almost every $\omega$ , and $\xi$ is Bochner integrable with respect to $\mu$ (in particular, $\xi$ is $\mu$ -a.e. strongly measurable and $\int \|\xi\| \, d\mu < \infty$ ).
$D \subseteq \alpha$ is a set and $x \in D$ is a point of it. Beyond the membership $x \in D$ , neither $D$ nor $x$ is used anywhere else in the statement.
$g : \alpha \to E \to \mathbb{R}$ is a function such that, for the fixed $x$ , the map $e \mapsto g(x, e)$ is convex on $\Xi$ (i.e. $\Xi$ is a convex set and $g(x,\cdot)$ satisfies the convexity inequality for points of $\Xi$ — the convexity-on-a-set predicate here includes the requirement that $\Xi$ itself be convex), continuous on $\Xi$ (continuity in the relative topology of $\Xi$ ), and such that $\omega \mapsto g(x, \xi(\omega))$ is $\mu$ -integrable. Nothing is assumed about $g(x,\cdot)$ outside $\Xi$ , nor about $g(x', \cdot)$ for $x' \ne x$ .
$\varphi : E \to \mathrm{Measure}(\mathrm{Ext})$ assigns to every point $e \in E$ (not only to $e \in \Xi$ ) a measure on $\mathrm{Ext}$ that is a probability measure.
Barycenter condition: for every $e \in \Xi$ ,

\int_{\mathrm{Ext}} \iota(y)\, \varphi_e(dy) = e,

where the left side is the Bochner integral of $\iota$ against $\varphi_e$ . (Note: if $\iota$ is not $\varphi_e$ -a.e. strongly measurable or not integrable, this Bochner integral is by convention the zero vector, so the condition then reads $e = 0$ .)

Measurability of the disintegration: for every subset $A \subseteq \mathrm{Ext}$ , the function $\omega \mapsto \varphi_{\xi(\omega)}(A)$ (with values in $[0,\infty]$ ) is measurable on $\Omega$ .
$\mu_{\mathrm{Ext}}$ is a probability measure on $\mathrm{Ext}$ satisfying, for every subset $A \subseteq \mathrm{Ext}$ ,

\mu_{\mathrm{Ext}}(A) = \int_\Omega \varphi_{\xi(\omega)}(A)\, \mu(d\omega),

the right side being the Lebesgue integral of a $[0,\infty]$ -valued function.

The function $y \mapsto g(x, \iota(y))$ on $\mathrm{Ext}$ is $\mu_{\mathrm{Ext}}$ -integrable.

Conclusion. Under all of the above,

\int_\Omega g\big(x, \xi(\omega)\big)\, \mu(d\omega) \;\le\; \int_{\mathrm{Ext}} g\big(x, \iota(y)\big)\, \mu_{\mathrm{Ext}}(dy),

a non-strict inequality between two real numbers, each a Bochner integral of a real-valued function (both integrands are assumed integrable, so neither integral takes the junk value $0$ for non-integrability).

Edge cases made explicit. The inequality is stated only for the single fixed $x$ ; no quantification over $D$ occurs. The integrals are with respect to the given $\mu$ and $\mu_{\mathrm{Ext}}$ only; nothing asserts that $\mu_{\mathrm{Ext}}$ is determined by $\varphi$ and $\xi$ beyond the stated identity on all subsets, and nothing asserts existence of such a $\varphi$ or $\mu_{\mathrm{Ext}}$ — they are inputs. If $\Xi$ is empty, then $\xi(\omega)\in\Xi$ a.e. is impossible for a probability measure $\mu$ , so the hypotheses are unsatisfiable and the statement holds vacuously. If $\operatorname{co}\Xi$ has no extreme points (which cannot happen for nonempty compact $\Xi$ in a Banach space but is not excluded syntactically), $\mathrm{Ext}$ is empty and the probability-measure assumptions on $\varphi_e$ and $\mu_{\mathrm{Ext}}$ cannot hold, again making the statement vacuous.

Human review

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

View graph