Proof of Theorem 2, upper bound: q̄ is feasible and D(J; q̄) ≤ Σ_{i∈J} p_i min_{j∉J} c(ω_i, ω_j)

Proved

ScenarioReduction.Redistribution.qbar_upper_bound

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

optimal-transportp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1scenario-reductionstochastic-programming

Under the standing assumptions of Section 3, let $J\subsetneq\{1,\dots,N\}$ and choose for every deleted index $i\in J$ a kept index $j(i)\notin J$ with $j(i)\in\arg\min_{j\notin J}c(\omega_i,\omega_j)$ . Put $J_j=\{i\in J: j(i)=j\}$ and define the optimal redistribution

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

Then $\bar q$ is a feasible reduced weight ( $\bar q_j\ge0$ and $\sum_{j\notin J}\bar q_j=1$ ), and

D(J;\bar q)\le\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j).

Together with the lower bound this shows that $\bar q$ is an optimal reweighting of the kept scenarios: every deleted scenario hands its probability to a nearest kept scenario.

Formalization Note The statement holds for every arg-min selector $j(\cdot)$ , not a particular one. The selector's values must be kept indices, because $c(\omega_i,\omega_i)=0$ would make $i$ itself an arg-min over all indices. The complement of $J$ is assumed nonempty (implicit on p. 501).

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_Redistribution_transportValue

open Finset

Formal statement

namespace ScenarioReduction.Redistribution

theorem qbar_upper_bound {Ω : Type*} {N : ℕ} (c : Ω → Ω → ℝ) (ω : Fin N → Ω) (p : Fin N → ℝ)
    (hc : ∀ a b : Ω, 0 ≤ c a b) (hc1 : ∀ a b : Ω, c a b = 0 ↔ a = b)
    (hc2 : ∀ a b : Ω, c a b = c b a)
    (hp : ∀ i, 0 < p i) (hp1 : ∑ i, p i = 1)
    (J : Finset (Fin N)) (hJ : Jᶜ.Nonempty) (jsel : Fin N → Fin N)
    (hsel : IsArgminSelector c ω J jsel) :
    IsReducedWeight J (qbar p J jsel) ∧
      transportValue c ω p J (qbar p J jsel) ≤ ∑ i ∈ J, p i * minOver Jᶜ (fun j => c (ω i) (ω j)) := by sorry

end ScenarioReduction.Redistribution

Source

Dupačová, Gröwe-Kuska, Römisch, Scenario reduction in stochastic programming, Math. Program. Ser. A 95 (2003), p. 501, §3, proof of Theorem 2, upper bound (definition of η̄ and q̄, and the display D(J; q̄) ≤ …)

Read-back

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

The data are:

an arbitrary type $\Omega$ and $N \in \mathbb{N}$ ;
$c : \Omega \times \Omega \to \mathbb{R}$ ;
$\omega : [N] \to \Omega$ and $p : [N] \to \mathbb{R}$ ;
$J \subseteq [N]$ ;
a map $\sigma : [N] \to [N]$ .

The hypotheses are:

$c \ge 0$ ;
$c(a, b) = 0 \iff a = b$ ;
$c$ is symmetric;
$p_i > 0$ for all $i$ , and $\sum_i p_i = 1$ ;
$J^c \neq \emptyset$ ;
$\sigma$ is an arg-min selector for $J$ : for every $i \in J$ , $\sigma(i) \notin J$ and $c(\omega_i, \omega_{\sigma(i)}) \le c(\omega_i, \omega_j)$ for all $j \notin J$ . Nothing is required of $\sigma$ outside $J$ .

Define

\bar q_j = p_j + \sum_{i \in J,\ \sigma(i) = j} p_i \qquad (j \in [N]).

The theorem asserts both of the following:

$\bar q$ is a reduced weight for $J$ : $\bar q_j \ge 0$ for $j \notin J$ and $\sum_{j \notin J} \bar q_j = 1$ .
The transport value is bounded above:

D(J; \bar q) \;\le\; \sum_{i \in J} p_i \,\min_{j \notin J} c(\omega_i, \omega_j).

Here $D(J; \bar q)$ is the infimum of $\sum_{i \in [N]} \sum_{j \notin J} c(\omega_i, \omega_j)\, \eta_{ij}$ over matrices $\eta$ with:

$\eta_{ij} \ge 0$ for $j \notin J$ ;
$\sum_{j \notin J} \eta_{ij} = p_i$ for every $i$ ;
$\sum_i \eta_{ij} = \bar q_j$ for every $j \notin J$ .

It is $0$ if no such $\eta$ exists.

Degenerate cases:

$N = 0$ . The statement is vacuous.
$J = \emptyset$ . Then $\sigma$ is unconstrained and $\bar q = p$ . The claims become " $p$ is a reduced weight for $\emptyset$ " and $D(\emptyset; p) \le 0$ .
$J = [N]$ . This is excluded by $J^c \neq \emptyset$ .

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