Eq. (12) — the greedy single-deletion costs give a lower bound for problem (8)

Proved

ScenarioReduction.ForwardSelection.backward_lower_bound

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

p2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1scenario-reductionstochastic-programming

Let $N\ge 2$ , let $\omega_1,\dots,\omega_N$ be scenarios with probabilities $p_i>0$ , $\sum_ip_i=1$ , let $c$ be the cost (3), and let $n\in\mathbb N$ with $1\le n<N$ . Let $l_1,\dots,l_{N-n}$ be selected by rule (11),

l_i\in\arg\min_{l\in\{1,\dots,N\}\setminus\{l_1,\dots,l_{i-1}\}}p_l\min_{j\neq l}c(\omega_l,\omega_j),\qquad i=1,\dots,N-n .

Then for every $J\subset\{1,\dots,N\}$ with $\#J=N-n$ ,

lb:=\sum_{i=1}^{N-n}p_{l_i}\min_{j\neq l_i}c(\omega_{l_i},\omega_j)\;\le\;D_J ,

so $lb$ is a lower bound of the optimal value of (8).

The bound is computable by sorting the single-deletion costs and certifies the quality of any heuristic solution of the NP-hard problem (8).

Formalization Note The paper states the bound as "can be shown" with a reference to earlier work; the statement is taken as printed. $N\ge 2$ is needed for $\min_{j\ne l}$ to be defined and follows from $1\le n<N$ .

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_ForwardSelection_fmCost
import Definitions.Def_ScenarioReduction_ForwardSelection_reductionCost
import Definitions.Def_ScenarioReduction_ForwardSelection_IsBackwardGreedy

Formal statement

namespace ScenarioReduction.ForwardSelection

/-- Eq. (12), Heitsch–Römisch 2003, p. 191. If `l₁, …, l_{N-n}` are selected by rule (11), then
`lb = ∑_{i=1}^{N-n} p_{lᵢ} min_{j ≠ lᵢ} c(ω_{lᵢ}, ωⱼ)` is at most `D_J` for every `J` with
`#J = N − n`, i.e. a lower bound of the optimal value of (8). -/
theorem backward_lower_bound {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {N : ℕ} (h : ℝ → ℝ) (hh : IsGrowthFunction h) (ω₀ : E)
    (ω : Fin N → E) (p : Fin N → ℝ) (hp : ∀ i, 0 < p i) (hsum : ∑ i, p i = 1)
    (hN : 1 < N) (n : ℕ) (hn1 : 1 ≤ n) (hnN : n < N) (l : ℕ → Fin N)
    (hl : IsBackwardGreedy (scenCost h ω₀ ω) p hN (N - n) l)
    (J : Finset (Fin N)) (hJ : Jᶜ.Nonempty) (hcard : J.card = N - n) :
    ∑ i ∈ Finset.Icc 1 (N - n), singleCost (scenCost h ω₀ ω) p hN (l i) ≤
      reductionCost (scenCost h ω₀ ω) p J hJ := by sorry

end ScenarioReduction.ForwardSelection

Source

Heitsch, Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003), p. 191, eqs. (11)–(12)

Read-back

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

Setting and hypotheses.

$E$ is a finite-dimensional real normed vector space.
$h:\mathbb R\to\mathbb R$ is continuous and nondecreasing on $[0,\infty)$ , with $h(0)=0$ and $h\ge0$ there.
$\omega_0\in E$ , and $\omega'_0,\dots,\omega'_{N-1}\in E$ with $N\ge2$ .
$p_i>0$ for all $i$ , and $\sum_ip_i=1$ .
$n\in\mathbb N$ with $1\le n<N$ .

Definitions.

Cost matrix: $C_{ij}=\max\{1,h(\|\omega'_i-\omega_0\|),h(\|\omega'_j-\omega_0\|)\}\,\|\omega'_i-\omega'_j\|$ .
Single-deletion cost: $a_l=p_l\min_{j\ne l}C_{lj}$ .
Reduction cost: $D_J=\sum_{i\in J}p_i\min_{j\notin J}C_{ij}$ .

Hypothesis on the sequence. $l:\mathbb N\to[N]$ is a sequence ( $l_0$ never used) such that, for each $i=1,\dots,N-n$ :

$l_i\notin\{l_1,\dots,l_{i-1}\}$ , and
$a_{l_i}\le a_{l'}$ for every $l'\notin\{l_1,\dots,l_{i-1}\}$ .

Claim. For every $J\subseteq[N]$ with nonempty complement and $|J|=N-n$ ,

\sum_{i=1}^{N-n}a_{l_i}\ \le\ D_J.

Degenerate cases.

Since $1\le n<N$ , we have $1\le N-n\le N-1$ . The subtraction is ordinary, the sum is nonempty, and every $J$ of size $N-n$ automatically has a nonempty complement.
For $n=N-1$ the claim concerns single-element sets $J=\{j\}$ and reads $a_{l_1}\le p_j\min_{k\ne j}C_{jk}=a_j$ .
If all scenarios coincide, both sides are $0$ .

Human review

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

View graph