Theorem 3 (prescribed redistribution): D(J; q) ≤ Σ_{i∈J} p_i Σ_{j∉J} λ_j c(ω_i, ω_j), equality if #J = 1 and c satisfies the triangle inequality

Proved

ScenarioReduction.Redistribution.prescribed_redistribution

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, fix $J\subset\{1,\dots,N\}$ and redistribution weights $\lambda_j\ge0$ , $j\notin J$ , with $\sum_{j\notin J}\lambda_j=1$ . Redistribute the deleted mass $p_J=\sum_{i\in J}p_i$ by the rule (12),

q_j=p_j+\lambda_jp_J\qquad(j\notin J).

Then

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

Moreover, equality holds if $\#J=1$ and $c$ satisfies the triangle inequality $c(a,d)\le c(a,b)+c(b,d)$ for all $a,b,d\in\Omega$ .

The theorem bounds the distance when the reduced weights are prescribed (for instance, to keep a uniform distribution uniform) instead of optimized as in Theorem 2.

Formalization Note $J$ may be empty; $\sum_{j\notin J}\lambda_j=1$ already forces at least one kept scenario. The triangle inequality is a hypothesis of the equality clause only, and is required on all of $\Omega$ as in the paper. Measurability, (C3) and (C4) are dropped as in the other items.

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_Redistribution_transportValue

open Finset

Formal statement

namespace ScenarioReduction.Redistribution

theorem prescribed_redistribution {Ω : 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)) (lam : Fin N → ℝ) (hlam : ∀ j ∉ J, 0 ≤ lam j) (hlam1 : ∑ j ∈ Jᶜ, lam j = 1) :
    transportValue c ω p J (prescribedWeights p J lam) ≤ ∑ i ∈ J, p i * ∑ j ∈ Jᶜ, lam j * c (ω i) (ω j) ∧
      (J.card = 1 → (∀ a b d : Ω, c a d ≤ c a b + c b d) →
        transportValue c ω p J (prescribedWeights p J lam) = ∑ i ∈ J, p i * ∑ j ∈ Jᶜ, lam 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, Theorem 3 and eq. (12)

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]$ ;
$\lambda : [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$ ;
$\lambda_j \ge 0$ for every $j \notin J$ , and $\sum_{j \notin J} \lambda_j = 1$ . Nothing is required of $\lambda_j$ for $j \in J$ .

Define the prescribed weights

q^\lambda_j = p_j + \lambda_j \sum_{i \in J} p_i.

Here $D(J; q^\lambda)$ 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} = q^\lambda_j$ for $j \notin J$ .

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

The theorem asserts:

Upper bound.

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

Equality for one deleted index. If $|J| = 1$ and $c$ satisfies the triangle inequality $c(a, d) \le c(a, b) + c(b, d)$ for all $a, b, d \in \Omega$ , then equality holds in (1).

Degenerate cases:

$N = 0$ . The statement is vacuous.
$J = [N]$ . The condition $\sum_{j \notin J} \lambda_j = 1$ is an empty sum equal to $1$ , which is impossible, so the statement is vacuous.
$J = \emptyset$ . Then $q^\lambda = p$ and part (1) reads $D(\emptyset; p) \le 0$ . Part (2) is vacuous because $|J| = 0 \ne 1$ .
Values on $J$ . The values $\lambda_j$ for $j \in J$ affect only $q^\lambda_j$ for $j \in J$ , which does not enter $D$ .

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