Eq. (17), conclusion — $z^{[i]}_u=D_{J^{[i-1]}\setminus\{u\}}$ for every $u\in J^{[i-1]}$

Proved

ScenarioReduction.ForwardSelection.zStep_eq_reductionCost

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

greedy-algorithmp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1scenario-reductionstochastic-programming

Let $\omega_1,\dots,\omega_N$ be scenarios with probabilities $p_i>0$ , $\sum_ip_i=1$ , $c$ the cost (3), and $u_1,u_2,\dots$ any sequence of indices, with $J^{[i]}$ , $c^{[i]}$ and $z^{[i]}$ as in Algorithm 2.4. For every step $i\ge 1$ and every $u\in J^{[i-1]}$ ,

z^{[i]}_u=\sum_{k\in J^{[i-1]}\setminus\{u\}}p_k\min_{j\notin J^{[i-1]}\setminus\{u\}}c(\omega_k,\omega_j)=D_{J^{[i-1]}\setminus\{u\}} .

Hence the objective minimized in each step of Algorithm 2.4 coincides with the objective of the forward selection principle (16), which is the content of the chain (17).

Formalization Note No run hypothesis is assumed: the identity holds for every sequence $u$ .

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_ForwardSelection_fmCost
import Definitions.Def_ScenarioReduction_ForwardSelection_reductionCost
import Definitions.Def_ScenarioReduction_ForwardSelection_IsFastForwardRun

Formal statement

namespace ScenarioReduction.ForwardSelection

/-- Eq. (17), Heitsch–Römisch 2003, p. 194 (last two lines). For any sequence `u`, any step
`i ≥ 1` and any `v ∈ J^{[i-1]}`, the quantity of Algorithm 2.4 is the reduction cost (8) of
deleting `J^{[i-1]} ∖ {v}`: `z^{[i]}_v = D_{J^{[i-1]} ∖ {v}}`. -/
theorem zStep_eq_reductionCost {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)
    (u : ℕ → Fin N) (i : ℕ) (hi : 1 ≤ i) (v : Fin N) (hv : v ∈ Jstep u (i - 1)) :
    zStep (scenCost h ω₀ ω) p u i v =
      reductionCost (scenCost h ω₀ ω) p ((Jstep u (i - 1)).erase v)
        (compl_erase_nonempty _ _) := by sorry

end ScenarioReduction.ForwardSelection

Source

Heitsch, Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003), p. 194, proof of Theorem 2.5, eq. (17)

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$ , $N\in\mathbb N$ , and $\omega'_0,\dots,\omega'_{N-1}\in E$ indexed by $[N]=\{0,\dots,N-1\}$ .
$p_i>0$ for all $i$ , and $\sum_ip_i=1$ .
$u:\mathbb N\to[N]$ is an arbitrary sequence $u_1,u_2,\dots$ (repeats allowed, no selection rule required).
$i\ge1$ , and $v\in J^{[i-1]}=[N]\setminus\{u_1,\dots,u_{i-1}\}$ .

Definitions.

Cost matrix: $C_{kj}=\max\{1,h(\|\omega'_k-\omega_0\|),h(\|\omega'_j-\omega_0\|)\}\,\|\omega'_k-\omega'_j\|$ .
Recursive costs: $c^{[1]}=C$ , and $c^{[i]}_{kv}=\min\{c^{[i-1]}_{kv},c^{[i-1]}_{k\,u_{i-1}}\}$ for $i\ge2$ .
Step quantity: $z^{[i]}_v=\sum_{k\in J^{[i-1]}\setminus\{v\}}p_k\,c^{[i]}_{kv}$ .
Reduction cost: for $K$ with nonempty complement, $D_K=\sum_{k\in K}p_k\min_{j\notin K}C_{kj}$ .

Claim.

z^{[i]}_v=D_{J^{[i-1]}\setminus\{v\}}=\sum_{k\in J^{[i-1]}\setminus\{v\}}p_k\min_{j\notin J^{[i-1]}\setminus\{v\}}C_{kj}.

Degenerate cases.

For $i=1$ : $J^{[0]}=[N]$ and the claim reads $\sum_{k\ne v}p_kC_{kv}=D_{[N]\setminus\{v\}}$ .
If $J^{[i-1]}=\{v\}$ , both sides are the empty sum $0$ .
The hypotheses force $N\ge1$ .

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

Eq. (17), conclusion — zu[i]=DJ[i−1]∖{u}z^{[i]}_u=D_{J^{[i-1]}\setminus\{u\}}zu[i]​=DJ[i−1]∖{u}​ for every u∈J[i−1]u\in J^{[i-1]}u∈J[i−1]

Eq. (17), conclusion — $z^{[i]}_u=D_{J^{[i-1]}\setminus\{u\}}$ for every $u\in J^{[i-1]}$