Eq. (10) — keeping one scenario $u$ costs $\sum_{i=1}^N p_i c(\omega_i,\omega_u)$

Proved

ScenarioReduction.ForwardSelection.forward_first_step

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

p2o-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$ , and let $c$ be the cost (3). Deleting all scenarios but $u$ , i.e. $J=\{1,\dots,N\}\setminus\{u\}$ , has reduction cost

D_{\{1,\dots,N\}\setminus\{u\}}=\sum_{i=1}^Np_i\,c(\omega_i,\omega_u),

and consequently the values of problem (8) for $\#J=N-1$ are exactly the values of problem (10):

\bigl\{D_J:\#J=N-1\bigr\}=\Bigl\{\sum_{i=1}^Np_i\,c(\omega_i,\omega_u):u\in\{1,\dots,N\}\Bigr\},

so that (8) with $\#J=N-1$ takes the form $\min_{u\in\{1,\dots,N\}}\sum_{i=1}^Np_ic(\omega_i,\omega_u)$ .

This is the first step of forward selection: the first kept scenario minimizes the expected cost to all scenarios.

Formalization Note The sum runs over all $i$ , including $i=u$ , as printed; the term $i=u$ vanishes because $c(\omega,\omega)=0$ for the cost (3).

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_ForwardSelection_fmCost
import Definitions.Def_ScenarioReduction_ForwardSelection_reductionCost

Formal statement

namespace ScenarioReduction.ForwardSelection

/-- Eq. (10), Heitsch–Römisch 2003, p. 191. Keeping a single scenario `u` (deleting
`J = {1..N} ∖ {u}`) costs `D_J = ∑_{i=1}^N pᵢ c(ωᵢ, ω_u)`, and the values of problem (8) with
`#J = N − 1` are exactly the values `∑ᵢ pᵢ c(ωᵢ, ω_u)`, `u = 1..N`, of problem (10). -/
theorem forward_first_step {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, reductionCost (scenCost h ω₀ ω) p (Finset.univ.erase u)
        (compl_erase_nonempty _ _) = ∑ i, p i * scenCost h ω₀ ω i u) ∧
    {x : ℝ | ∃ J : Finset (Fin N), ∃ hJ : Jᶜ.Nonempty, J.card = N - 1 ∧
        x = reductionCost (scenCost h ω₀ ω) p J hJ} =
      Set.range (fun u : Fin N => ∑ i, p i * scenCost h ω₀ ω i u) := by sorry

end ScenarioReduction.ForwardSelection

Source

Heitsch, Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003), p. 191, eq. (10)

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$ are indexed by $[N]=\{0,\dots,N-1\}$ .
$p_i>0$ for all $i$ , and $\sum_ip_i=1$ .

Definitions.

C_{ij}=\max\{1,h(\|\omega'_i-\omega_0\|),h(\|\omega'_j-\omega_0\|)\}\,\|\omega'_i-\omega'_j\|,

and, for $J$ with nonempty complement,

D_J=\sum_{i\in J}p_i\min_{j\notin J}C_{ij}.

Claim (a). For every $u\in[N]$ ,

D_{[N]\setminus\{u\}}=\sum_{i\in[N]}p_i\,C_{iu}.

The right-hand sum includes the term $i=u$ , which is $p_uC_{uu}=0$ .

Claim (b). Two sets of reals are equal:

\{D_J:\ J\subseteq[N],\ [N]\setminus J\neq\varnothing,\ |J|=N-1\} =\Bigl\{\textstyle\sum_{i}p_iC_{iu}:\ u\in[N]\Bigr\}.

Degenerate cases.

The hypotheses force $N\ge1$ , so $N-1$ is ordinary subtraction.
For $N=1$ : the only admissible $J$ is $\varnothing$ with $D_\varnothing=0$ , and the right-hand set is $\{p_0C_{00}\}=\{0\}$ .
If all scenarios coincide, every value in both sets is $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

Eq. (10) — keeping one scenario uuu costs ∑i=1Npic(ωi,ωu)\sum_{i=1}^N p_i c(\omega_i,\omega_u)∑i=1N​pi​c(ωi​,ωu​)

Eq. (10) — keeping one scenario $u$ costs $\sum_{i=1}^N p_i c(\omega_i,\omega_u)$