Lemma 3.3 — deleting elements at most $(r-1)/r$ preserves $FFD(L)>rL^*+d$ (and likewise for BFD)

Proved

BinPacking.Decreasing.delete_small_items

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

approximation-algorithmsbin-packingp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $L$ be a list of real numbers in $(0,1]$ , let $r\ge 1$ and $d\ge 1$ be real numbers, and let $L'$ be the list obtained from $L$ by deleting all elements not exceeding $(r-1)/r$ , i.e. keeping exactly the elements $a$ with $a>(r-1)/r$ (in their original order).

If $FFD(L)>rL^*+d$ , then $FFD(L')>rL'^*+d$ .
If $BFD(L)>rL^*+d$ , then $BFD(L')>rL'^*+d$ .

In symbols, for $A\in\{FFD, BFD\}$ ,

A(L)>r\,L^*+d\ \Longrightarrow\ A(L')>r\,L'^*+d .

With $r=11/9$ one has $(r-1)/r=2/11$ , so a counterexample to Theorem 3.2 would survive the deletion of all elements at most $2/11$ ; the lemma reduces Theorem 3.2 to lists contained in $(2/11,1]$ .

Preamble

import Mathlib
import Definitions.Def_BinPacking_Decreasing_Model

Formal statement

namespace BinPacking.Decreasing

/-- Lemma 3.3 (p. 309): if `FFD(L) > r L* + d` with `r, d ≥ 1`, then the list `L'` obtained
from `L` by deleting all elements not exceeding `(r − 1)/r` also has `FFD(L') > r L'* + d`;
the same holds with BFD in place of FFD. -/
theorem delete_small_items (L : List ℝ) (hL : IsList L) (r d : ℝ) (hr : 1 ≤ r) (hd : 1 ≤ d) :
    ((FFD L : ℝ) > r * (optBins L : ℝ) + d →
      (FFD (L.filter (fun a => decide ((r - 1) / r < a))) : ℝ) >
        r * (optBins (L.filter (fun a => decide ((r - 1) / r < a))) : ℝ) + d) ∧
    ((BFD L : ℝ) > r * (optBins L : ℝ) + d →
      (BFD (L.filter (fun a => decide ((r - 1) / r < a))) : ℝ) >
        r * (optBins (L.filter (fun a => decide ((r - 1) / r < a))) : ℝ) + d) := by sorry

end BinPacking.Decreasing

Source

Johnson, Demers, Ullman, Garey, Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3(4) (1974), p. 309, Lemma 3.3

Read-back

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

Notation:

$L$ is a list of reals with every entry in $(0,1]$ .
$r$ and $d$ are real numbers with $r \ge 1$ and $d \ge 1$ .
$L'$ is the sublist of $L$ that keeps, in their original order, exactly the entries $a$ with $a > (r-1)/r$ . It deletes every entry $\le (r-1)/r$ .
$L^*$ is the least number of unit-capacity bins into which the entries of $L$ can be assigned with every bin sum $\le 1$ .
$FFD(L)$ is the number of bins produced by first-fit applied to $L$ sorted into nonincreasing order. First-fit processes the items in that order and puts each into the lowest-indexed existing bin whose current sum plus the item is $\le 1$ , opening a new bin otherwise.
$BFD(L)$ is defined the same way, except that each item goes into the fullest existing bin that still fits it (ties broken by lowest index), opening a new bin otherwise.

The statement asserts both of the following implications:

FFD(L) > r\,L^* + d \;\Longrightarrow\; FFD(L') > r\,(L')^* + d,

BFD(L) > r\,L^* + d \;\Longrightarrow\; BFD(L') > r\,(L')^* + d.

Degenerate cases:

$r = 1$ . The threshold is $0$ , so $L' = L$ and both implications are trivially true.
Empty $L$ . $FFD = BFD = L^* = 0$ , and $0 > d \ge 1$ is false, so both implications hold vacuously.
Division. No division by zero occurs, because $r \ge 1$ .
Parameters. $r$ and $d$ are arbitrary reals, not required to be integers.

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

Lemma 3.3 — deleting elements at most (r−1)/r(r-1)/r(r−1)/r preserves FFD(L)>rL∗+dFFD(L)>rL^*+dFFD(L)>rL∗+d (and likewise for BFD)

Lemma 3.3 — deleting elements at most $(r-1)/r$ preserves $FFD(L)>rL^*+d$ (and likewise for BFD)