Theorem 2.1 — optimal redistribution: $\min_q D(J;q)=D_J$ , attained at $\bar q$ of (7)

Proved

ScenarioReduction.ForwardSelection.redistribution

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

optimal-transportp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1scenario-reduction

Let $\omega_1,\dots,\omega_N$ be scenarios in a finite-dimensional normed space with probabilities $p_i>0$ , $\sum_ip_i=1$ , and let $c$ be the cost (3) built from a growth function $h$ and a point $\omega_0$ . Let $J\subset\{1,\dots,N\}$ be a set of deleted scenarios with at least one scenario kept. For a reduced weight $q$ ( $q_j\ge 0$ , $\sum_{j\notin J}q_j=1$ ) let $D(J;q)$ be the optimal value of the linear transportation problem between $P=\sum_ip_i\delta_{\omega_i}$ and $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$ with cost $c$ . Then

D_J=\min\Bigl\{D(J;q):q_j\ge 0,\ \sum_{j\notin J}q_j=1\Bigr\}=\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j).

Moreover, for every choice $j(i)\in\arg\min_{j\notin J}c(\omega_i,\omega_j)$ ( $i\in J$ ), the minimum is attained at the redistributed weight

\bar q_j=p_j+\sum_{i\in J_j}p_i,\qquad J_j=\{i\in J:j(i)=j\},\qquad j\notin J,

which is itself a reduced weight, and $D(J;\bar q)=D_J$ .

The theorem turns the optimal reduction problem into the combinatorial problem (8) of choosing $J$ : once the deleted set is fixed, the best reduced measure moves the mass of each deleted scenario to a nearest kept one.

Formalization Note $D(J;q)$ is the paper's own finite transportation problem (p. 188), not the Kantorovich functional on measures. The first part is stated as: $D_J$ is the least value of the transportation cost over all pairs (reduced weight $q$ , feasible plan $\eta$ ). The second part states that $\bar q$ is a reduced weight and $D_J$ is the least transportation cost over plans with second marginal $\bar q$ . The hypothesis that $J$ has nonempty complement is necessary: for $J=\{1,\dots,N\}$ no reduced weight exists.

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_ForwardSelection_fmCost
import Definitions.Def_ScenarioReduction_ForwardSelection_reductionCost
import Definitions.Def_ScenarioReduction_ForwardSelection_IsTransportPlan

Formal statement

namespace ScenarioReduction.ForwardSelection

/-- Theorem 2.1 (redistribution), Heitsch–Römisch 2003, p. 190. For the cost (3) and a set `J` of
deleted scenarios with nonempty complement, `D_J` is the minimum of the transportation cost over all
reduced weights `q` and all plans `η` between `P` and `Q`, and the minimum is attained at the
redistributed weight `q̄` of (7), for every choice of nearest kept scenarios `j(i)`. -/
theorem redistribution {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)
    (J : Finset (Fin N)) (hJ : Jᶜ.Nonempty) :
    IsLeast {v : ℝ | ∃ q : Fin N → ℝ, ∃ η : Fin N → Fin N → ℝ, IsReducedWeight J q ∧
        IsTransportPlan J p q η ∧ v = transportCost (scenCost h ω₀ ω) J η}
      (reductionCost (scenCost h ω₀ ω) p J hJ) ∧
    ∀ jsel : Fin N → Fin N,
      (∀ i ∈ J, jsel i ∉ J ∧ ∀ j, j ∉ J → scenCost h ω₀ ω i (jsel i) ≤ scenCost h ω₀ ω i j) →
      IsReducedWeight J (redistWeight p J jsel) ∧
      IsLeast {v : ℝ | ∃ η : Fin N → Fin N → ℝ, IsTransportPlan J p (redistWeight p J jsel) η ∧
          v = transportCost (scenCost h ω₀ ω) J η}
        (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. 190, Theorem 2.1, eqs. (6)–(7)

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 (dimension $0$ allowed).
$h:\mathbb R\to\mathbb R$ is continuous and nondecreasing on $[0,\infty)$ , with $h(0)=0$ and $h\ge0$ on $[0,\infty)$ .
$\omega_0\in E$ is a reference point.
$N\in\mathbb N$ , and $\omega'_0,\dots,\omega'_{N-1}\in E$ are scenarios indexed by $[N]=\{0,\dots,N-1\}$ .
$p_i>0$ for every $i$ , and $\sum_i p_i=1$ .
$J\subseteq[N]$ is a set whose complement is nonempty.

Cost matrix.

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

Reduction cost.

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

Reduced weight and transport plan.

A reduced weight is a $q$ with $q_j\ge0$ for $j\notin J$ , $q_j=0$ for $j\in J$ , and $\sum_{j\notin J}q_j=1$ .
A transport plan between $p$ and $q$ is an array $\eta$ $η$ with:
- $\eta_{ij}\ge0$ for $j\notin J$ ;
- $\eta_{ij}=0$ for $j\in J$ ;
- $\sum_{i\in[N]}\eta_{ij}=q_j$ for each $j\notin J$ ;
- $\sum_{j\notin J}\eta_{ij}=p_i$ for every $i\in[N]$ .
Its cost is $T(\eta)=\sum_{i\in[N]}\sum_{j\notin J}C_{ij}\eta_{ij}$ .

Claim 1. $D_J$ is the least element of

\{\,T(\eta):\ q\text{ a reduced weight},\ \eta\text{ a transport plan between }p\text{ and }q\,\}.

That is, $D_J$ is attained by some pair $(q,\eta)$ , and $D_J\le T(\eta)$ for every such pair.

Claim 2. Take any $\sigma:[N]\to[N]$ such that, for every $i\in J$ :

$\sigma(i)\notin J$ , and
$C_{i\sigma(i)}\le C_{ij}$ for all $j\notin J$ .

Define $\bar q_j=0$ for $j\in J$ and $\bar q_j=p_j+\sum_{i\in J,\,\sigma(i)=j}p_i$ for $j\notin J$ . Then:

$\bar q$ is a reduced weight, and
$D_J$ is the least element of $\{T(\eta):\eta\text{ a transport plan between }p\text{ and }\bar q\}$ .

Values of $\sigma$ at indices outside $J$ are irrelevant.

Degenerate cases.

$\sum p_i=1$ forces $N\ge1$ , and the complement hypothesis excludes $J=[N]$ .
For $J=\varnothing$ : $D_J=0$ , $\bar q=p$ , and both claims assert that $0$ is the least attainable transport cost.
If $E$ has dimension $0$ , all scenarios equal $\omega_0$ , every $C_{ij}=0$ , and every set above is $\{0\}$ or contains only $0$ .
Values of $h$ on negative numbers never enter, since only norms are passed to $h$ .

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

Theorem 2.1 — optimal redistribution: min⁡qD(J;q)=DJ\min_q D(J;q)=D_Jminq​D(J;q)=DJ​, attained at qˉ\bar qqˉ​ of (7)

Theorem 2.1 — optimal redistribution: $\min_q D(J;q)=D_J$ , attained at $\bar q$ of (7)