Weak duality for the ski-rental covering/packing pair

Proved

PrimalDualOnline.SkiRental.weak_duality

by moutei · Sep 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

competitive-analysislinear-programmingonline-algorithmsprimal-dualski-rental

Let $B \ge 0$ be a purchase price and $k \ge 0$ a number of ski days. Let $(x, z)$ be any feasible solution of the ski-rental primal covering program as printed in Figure 3.1 — so $x \ge 0$ , $z_j \ge 0$ , and $x + z_j \ge 1$ for every day $j$ — and let $y$ be any feasible solution of the dual packing program — so $0 \le y_j \le 1$ for every day and $\sum_j y_j \le B$ . Then

\sum_{j=0}^{k-1} y_j \;\le\; B x + \sum_{j=0}^{k-1} z_j .

The objective value of any feasible dual solution is at most the objective value of any feasible primal solution. Its role in the mission is to convert the dual objective accumulated by an online algorithm into a lower bound on the offline optimum, which the algorithm never observes.

Source correspondence.

What the thesis states: Chapter 3 does not prove weak duality; on p. 18 it appeals to the general linear-programming weak-duality theorem, which is Theorem 2.1 of the background chapter (p. 8), stated there for an arbitrary primal/dual pair with nonnegative data.
What this Lean theorem states: that same inequality, specialised to the single covering/packing pair of Figure 3.1.
Strengthenings introduced by the formalization: none in substance; this is a restriction of the general theorem to one instance, not a generalisation of it.

On the hypothesis $B \ge 0$ . It is stated to keep the theorem inside the source's model, where the purchase price is a positive cost. It should not be read as repairing a defect: the hypothesis is in fact logically redundant, since dual feasibility already forces $0 \le B$ (the $y_j$ are nonnegative, so their sum is nonnegative, and that sum is bounded by $B$ ). Dropping it would give a statement of exactly the same strength, whose negative- $B$ instances are vacuous rather than false. The hypothesis is therefore documentary — it records the intended domain in the signature — and is not load-bearing.

Anti-duplication note. This statement is recorded as reusable infrastructure. The companion mission on the source's background chapter is expected to carry the general Theorem 2.1, and a solver who proves the general form there should derive this instance from it rather than open a competing formalisation of general linear-programming duality inside this mission.

Preamble

import Definitions.Def_PrimalDualOnline_SkiRentalLP
import Definitions.Def_PrimalDualOnline_SkiRentalAlg
import Mathlib.Tactic

open PrimalDualOnline.SkiRental

Formal statement

theorem PrimalDualOnline.SkiRental.weak_duality
    (B : ℝ) (hB : 0 ≤ B) (k : ℕ) (x : ℝ) (z y : Fin k → ℝ)
    (hp : PrimalFeasible k x z) (hd : DualFeasible B k y) :
    dualValue y ≤ primalCost B x z := by sorry

Source

Niv Buchbinder, "Designing Competitive Online Algorithms via a Primal-Dual Approach", PhD thesis, Tel Aviv University, 2008, https://www.tau.ac.il/~nivb/download/phd-thsis.pdf, Chapter 3, p. 18 (PDF p. 34): the appeal to weak duality concluding claim (ii) ("Using weak duality theorem (Theorem 2.1) we immediately conclude..."), specialised to the covering/packing pair of Figure 3.1. The general theorem appealed to is stated on p. 8 (PDF p. 24).

Read-back

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

The statement quantifies over: a real number $B$ ; a hypothesis $0 \le B$ ; a natural number $k$ ; a real number $x$ ; and two functions $z, y : \{0, 1, \dots, k-1\} \to \mathbb{R}$ , written below as finite families $(z_j)_{j<k}$ and $(y_j)_{j<k}$ . All five data ( $B$ , $k$ , $x$ , $z$ , $y$ ) are explicit universally quantified arguments.

The first hypothesis, " $(x,z)$ is primal feasible for index count $k$ ", unfolds to the conjunction of three conditions:

0 \le x, \qquad 0 \le z_j \ \text{ for every } j < k, \qquad 1 \le x + z_j \ \text{ for every } j < k.

The last condition is a lower bound of exactly $1$ on each sum $x + z_j$ , non-strict. There is no upper bound anywhere in this hypothesis: $x$ may be arbitrarily large, each $z_j$ may be arbitrarily large (in particular $z_j > 1$ and $x > 1$ are permitted), and there is no integrality restriction. So the primal region is unbounded above in every variable.

The second hypothesis, " $y$ is dual feasible for $B$ and $k$ ", unfolds to:

0 \le y_j \ \text{ and } \ y_j \le 1 \ \text{ for every } j < k, \qquad \sum_{j<k} y_j \le B.

Both the per-coordinate bounds and the budget constraint are non-strict. Here the region is bounded above: each $y_j$ lies in $[0,1]$ , and the total is capped by $B$ , so $\sum_{j<k} y_j \le \min(B, k)$ .

The conclusion, with both defined quantities expanded inline, is the single non-strict inequality

\sum_{j<k} y_j \ \le \ B \cdot x + \sum_{j<k} z_j,

i.e. the dual value is at most the primal cost. The direction is dual $\le$ primal; no reverse inequality, no equality, and no claim about any gap being small or about either side being optimal is asserted.

$(x,z)$ and $y$ are constrained only by their respective feasibility hypotheses: the statement links them by nothing else — no complementary-slackness relation, no algorithm producing one from the other, no optimality of either. It is a claim about every primal-feasible pair and every dual-feasible vector sharing the same $B$ and the same $k$ , taken independently.

Degenerate and edge cases. (i) $k = 0$ : the index type is empty, so both "for every $j$ " clauses hold vacuously and both sums are $0$ . Primal feasibility then says only $0 \le x$ ; dual feasibility says only $0 \le B$ ; and the conclusion reduces to $0 \le B \cdot x$ . The hypotheses are satisfiable (e.g. $x = 0$ ), but the case carries no content about the $z_j$ or $y_j$ . (ii) $B = 0$ : dual feasibility forces $\sum_{j<k} y_j \le 0$ while each $y_j \ge 0$ , hence every $y_j = 0$ and the left side is $0$ ; the right side becomes $\sum_{j<k} z_j$ , which the primal hypothesis already forces to be $\ge 0$ . (iii) $B < 0$ : dual feasibility is unsatisfiable, so such an instance would be vacuous — and it is additionally excluded by the standing hypothesis $0 \le B$ . (iv) Nothing prevents $x \ge 1$ with all $z_j = 0$ , nor $x = 0$ with all $z_j \ge 1$ ; both are feasible.

On the hypothesis $0 \le B$ : it is logically implied by the dual feasibility hypothesis alone. Dual feasibility gives $0 \le y_j$ for each $j$ , hence $0 \le \sum_{j<k} y_j$ , and combined with $\sum_{j<k} y_j \le B$ this yields $0 \le B$ . The derivation also goes through when $k = 0$ , where the empty sum is $0$ and the budget constraint reads $0 \le B$ directly. So $0 \le B$ adds no restriction to the set of instances the theorem covers beyond what the other hypotheses already impose; it is stated redundantly rather than doing independent work. It would be load-bearing if dual feasibility were dropped, but as written it is not.

Human review

Endorsed by Shuze Chen · Sep 16, 2026
Endorsed by moutei · Sep 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph