Proof of Theorem 2, lower bound: Σ_{i∈J} p_i min_{k∉J} c(ω_i, ω_k) ≤ D(J; q) for every feasible q

Proved

ScenarioReduction.Redistribution.dual_lower_bound

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

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

Under the standing assumptions of Section 3 ( $p_i>0$ , $\sum_ip_i=1$ ; $c\ge0$ , $c(\omega,\tilde\omega)=0$ iff $\omega=\tilde\omega$ , $c$ symmetric), let $J\subsetneq\{1,\dots,N\}$ be a set of deleted scenarios, so that at least one scenario is kept. For every choice of reduced weights $q$ ( $q_j\ge0$ for $j\notin J$ , $\sum_{j\notin J}q_j=1$ ),

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

Here $D(J;q)$ is the Kantorovich distance between $P=\sum_ip_i\delta_{\omega_i}$ and the reduced measure $\sum_{j\notin J}q_j\delta_{\omega_j}$ . The left-hand side does not depend on $q$ , so it bounds from below the best distance that any reweighting of the kept scenarios can achieve; it is the lower half of Theorem 2.

Formalization Note The hypothesis that the complement of $J$ is nonempty is implicit on p. 501 (the minimum over $k\notin J$ must range over a nonempty set) and is stated explicitly. The paper's lead-in sentence writes the expression as $\sum_{j\in J}p_j\min_{i\notin J}c_{ij}$ , swapping the letters $i$ and $j$ ; the formalization follows the display that ends the step, which matches (11).

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_Redistribution_transportValue

open Finset

Formal statement

namespace ScenarioReduction.Redistribution

theorem dual_lower_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) (q : Fin N → ℝ) (hq : IsReducedWeight J q) :
    ∑ i ∈ J, p i * minOver Jᶜ (fun k => c (ω i) (ω k)) ≤ transportValue c ω p J q := 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, lower bound (second paragraph and display)

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}$ ;
points $\omega : [N] \to \Omega$ , where $[N] = \{0, \dots, N-1\}$ ;
$p : [N] \to \mathbb{R}$ ;
$J \subseteq [N]$ ;
$q : [N] \to \mathbb{R}$ .

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$ ;
the complement $J^c$ is nonempty;
$q$ is a reduced weight for $J$ : $q_j \ge 0$ for $j \notin J$ and $\sum_{j \notin J} q_j = 1$ .

The conclusion is

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

The minimum is a genuine minimum because $J^c \neq \emptyset$ .

Here $D(J; 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 \in [N]$ ;
$\sum_{i \in [N]} \eta_{ij} = q_j$ for every $j \notin J$ .

It takes the value $0$ if no such $\eta$ exists or the set is unbounded below.

Degenerate cases:

$N = 0$ . The hypotheses are unsatisfiable, so the statement is vacuous.
$J^c \neq \emptyset$ is redundant. This hypothesis also follows from $\sum_{j \notin J} q_j = 1$ .
$J = \emptyset$ . The left side is an empty sum, and the claim reduces to $0 \le D(\emptyset; q)$ .
Values on $J$ . The values $q_j$ for $j \in J$ are arbitrary and do not enter.

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