Theorem 4 (bounds): greedy backward/forward bounds on the optimal deletion problem (13)

Proved

ScenarioReduction.Redistribution.bounds

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

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

Under the standing assumptions of Section 3, fix $k\in\mathbb N$ with $1\le k<N$ and consider the optimal deletion problem (13),

\min\{D_J: J\subset\{1,\dots,N\},\ \#J=k\},

where $D_J$ is the optimal-weights value of Theorem 2. Choose indices recursively:

$l_1,\dots,l_k$ such that for $i=1,\dots,k$ , $l_i$ solves $\min_{l\in\{1,\dots,N\}\setminus\{l_1,\dots,l_{i-1}\}}p_l\min_{j\neq l}c(\omega_l,\omega_j)$ — (16);
$u_1,\dots,u_{N-k}$ such that for $j=1,\dots,N-k$ , $u_j$ solves

\min_{u\notin\{u_1,\dots,u_{j-1}\}}\ \sum_{i\notin\{u_1,\dots,u_{j-1},u\}}p_i\min_{l\in\{u_1,\dots,u_{j-1},u\}}c(\omega_l,\omega_i)\qquad(17),

and put $J_u=\{1,\dots,N\}\setminus\{u_1,\dots,u_{N-k}\}$ . Then

\sum_{i=1}^kp_{l_i}\min_{j\neq l_i}c(\omega_{l_i},\omega_j)\le\min\{D_J:\#J=k\}\le\sum_{i\in J_u}p_i\min_{j\notin J_u}c(\omega_i,\omega_j).

Moreover, $\{l_1,\dots,l_k\}$ is a solution of (13) if for each $i=1,\dots,k$ the set $\arg\min_{j\neq l_i}c(\omega_{l_i},\omega_j)\setminus\{l_1,\dots,l_{i-1},l_{i+1},\dots,l_k\}$ is nonempty.

The two recursions are the backward-reduction and forward-selection heuristics of the paper; the theorem certifies the quality of their output.

Formalization Note Indices are 0-based: $l:\mathrm{Fin}\,k\to\mathrm{Fin}\,N$ and $u:\mathrm{Fin}(N-k)\to\mathrm{Fin}\,N$ , where the natural-number subtraction $N-k$ is exact because $k<N$ . The recursions are hypotheses: each $l_i$ (resp. $u_j$ ) is distinct from the earlier ones and minimizes (16) (resp. (17)) over the remaining indices. In (16) and in the lower bound the inner minimum ranges over all $j\neq l$ , not over kept indices. The value of (13) is the infimum of $D_J$ over $\#J=k$ , a finite nonempty set of reals; "solution of (13)" is stated as $\#\{l_1,\dots,l_k\}=k$ and $D_{\{l_1,\dots,l_k\}}$ equal to that value.

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_Redistribution_transportValue

open Finset

Formal statement

namespace ScenarioReduction.Redistribution

theorem bounds {Ω : 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)
    (k : ℕ) (hk1 : 1 ≤ k) (hkN : k < N)
    (l : Fin k → Fin N)
    (hl : ∀ i : Fin k, l i ∉ (univ.filter (fun i' => i' < i)).image l ∧
      ∀ m ∉ (univ.filter (fun i' => i' < i)).image l,
        p (l i) * minOver {l i}ᶜ (fun j => c (ω (l i)) (ω j)) ≤ p m * minOver {m}ᶜ (fun j => c (ω m) (ω j)))
    (u : Fin (N - k) → Fin N)
    (hu : ∀ j : Fin (N - k), u j ∉ (univ.filter (fun j' => j' < j)).image u ∧
      ∀ m ∉ (univ.filter (fun j' => j' < j)).image u,
        ∑ i ∈ (insert (u j) ((univ.filter (fun j' => j' < j)).image u))ᶜ,
            p i * minOver (insert (u j) ((univ.filter (fun j' => j' < j)).image u)) (fun l' => c (ω l') (ω i))
          ≤ ∑ i ∈ (insert m ((univ.filter (fun j' => j' < j)).image u))ᶜ,
            p i * minOver (insert m ((univ.filter (fun j' => j' < j)).image u)) (fun l' => c (ω l') (ω i))) :
    ∑ i : Fin k, p (l i) * minOver {l i}ᶜ (fun j => c (ω (l i)) (ω j)) ≤ optimalDeletionValue c ω p k ∧
      optimalDeletionValue c ω p k ≤
        ∑ i ∈ (univ.image u)ᶜ, p i * minOver (univ.image u) (fun j => c (ω i) (ω j)) ∧
      ((∀ i : Fin k, ∃ j : Fin N, j ≠ l i ∧ (∀ i' : Fin k, i' ≠ i → j ≠ l i') ∧
          ∀ j' : Fin N, j' ≠ l i → c (ω (l i)) (ω j) ≤ c (ω (l i)) (ω j')) →
        (univ.image l).card = k ∧ optWeightsValue c ω p (univ.image l) = optimalDeletionValue c ω p k) := 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. 503, Theorem 4, eqs. (16)–(17); problem (13) on p. 502

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}$ ;
$k \in \mathbb{N}$ ;
a sequence $l_0, \dots, l_{k-1} \in [N]$ ;
a sequence $u_0, \dots, u_{N-k-1} \in [N]$ .

The standing 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$ ;
$1 \le k < N$ .

Write:

$\varphi(m) = p_m \min_{j \ne m} c(\omega_m, \omega_j)$ ;
$L_{<i} = \{l_{i'} : i' < i\}$ and $L = \{l_0, \dots, l_{k-1}\}$ ;
$U_{<j} = \{u_{j'} : j' < j\}$ and $U = \{u_0, \dots, u_{N-k-1}\}$ ;
for a nonempty $S \subseteq [N]$ ,

F(S) = \sum_{i \notin S} p_i \min_{l' \in S} c(\omega_{l'}, \omega_i).

The sequences $l$ and $u$ must satisfy:

Condition on $l$ . For each $i < k$ : $l_i \notin L_{<i}$ , and $\varphi(l_i) \le \varphi(m)$ for every $m \notin L_{<i}$ . So each $l_i$ is a new index minimizing $\varphi$ among the indices not yet chosen.
Condition on $u$ . For each $j < N - k$ : $u_j \notin U_{<j}$ , and $F(U_{<j} \cup \{u_j\}) \le F(U_{<j} \cup \{m\})$ for every $m \notin U_{<j}$ .

The theorem also uses the following quantities:

$D(J; q)$ is the infimum, over matrices $\eta$ with $\eta_{ij} \ge 0$ for $j \notin J$ , $\sum_{j \notin J} \eta_{ij} = p_i$ for all $i$ , and $\sum_i \eta_{ij} = q_j$ for $j \notin J$ , of $\sum_i \sum_{j \notin J} c(\omega_i, \omega_j)\, \eta_{ij}$ .
$D_J$ is the infimum of $D(J; q)$ over all $q$ with $q_j \ge 0$ for $j \notin J$ and $\sum_{j \notin J} q_j = 1$ .
$D^*_k$ is the infimum of $D_J$ over all $J \subseteq [N]$ with $|J| = k$ .

Every infimum is $0$ if its set is empty or unbounded below.

The theorem asserts all three of the following:

Lower bound.

\sum_{i=0}^{k-1} p_{l_i} \min_{j \ne l_i} c(\omega_{l_i}, \omega_j) \;\le\; D^*_k.

Upper bound.

D^*_k \;\le\; \sum_{i \notin U} p_i \min_{j \in U} c(\omega_i, \omega_j).

Note the argument order: here it is $c(\omega_i, \omega_j)$ with the non- $U$ index first, whereas $F$ in the condition on $u$ uses $c(\omega_{l'}, \omega_i)$ with the $U$ -index first. 3. Conditional optimality of $L$ . Suppose that for every $i < k$ there is an index $j$ with all of the following properties:

$j \ne l_i$ ;
$j \ne l_{i'}$ for every $i' \ne i$ ;
$c(\omega_{l_i}, \omega_j) \le c(\omega_{l_i}, \omega_{j'})$ for every $j' \ne l_i$ .

Then $|L| = k$ and $D_L = D^*_k$ .

Degenerate cases:

Size of $N$ . The hypothesis $1 \le k < N$ forces $N \ge 2$ . So every set $\{m\}^c$ is nonempty and $\varphi$ is a genuine minimum.
Size of $U$ . $N - k \ge 1$ , so $u$ has at least one entry. Every set $U_{<j} \cup \{\cdot\}$ in the condition on $u$ is nonempty, as is $U$ itself.
Empty complement of $U$ . If $U = [N]$ , which can happen only if $u$ repeats no index and $N - k = N$ (impossible since $k \ge 1$ ), the sum in (2) would be empty. In fact $U^c \neq \emptyset$ in every admissible case.
No subtraction truncation. The length $N - k$ is an ordinary difference because $k < N$ .
$k = 1$ . Part (1) reads $\varphi(l_0) \le D^*_1$ , where $l_0$ is a global minimizer of $\varphi$ .
Repeated points. $\omega$ may be non-injective. If two indices share a point, the corresponding $\varphi$ values are $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