Optimum of the canonical fractional ski-rental program is $\min(B,k)$

Proved

PrimalDualOnline.SkiRental.lp_optimum_box

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

competitive-analysislinear-programmingonline-algorithmsprimal-dualski-rental

Let $B \ge 0$ be the purchase price and $k \ge 0$ the number of ski days. Consider the canonical fractional primal program, whose feasible solutions are the pairs $(x, z)$ with

0 \le x \le 1, \qquad 0 \le z_j \le 1, \qquad x + z_j \ge 1 \qquad (0 \le j < k),

and whose objective is $B x + \sum_{j<k} z_j$ . Then the least objective value attained over this region is exactly

\min(B, k).

The claim has two halves, both part of the target. The value is attained: some feasible pair achieves it. And it is a lower bound: no feasible pair costs less. Because attainment is included, this is a statement about a least element, not merely an infimum.

This supplies the benchmark for the whole mission. Competitiveness is a comparison against the offline optimum, and this is what certifies that the quantity named $\min(B,k)$ is that optimum rather than an arbitrary stand-in.

Source correspondence.

What the thesis states (p. 17): "Note that the optimal solution is always integral, and thus the relaxation has no integrality gap." The claim is made in one sentence and the optimal value is not displayed.
What this Lean theorem states: that $\min(B,k)$ is the least attained objective value of the $[0,1]$ -bounded program.
Introduced by the formalization: naming the optimum. The source asserts the absence of a gap between the integer program and its relaxation; this theorem asserts the value, $\min(B,k)$ , which is the cost of the better of the two integral strategies. Identifying the two is the formalization's step, and it is what makes the benchmark usable downstream.

Formalization Note. In the ski-rental model the purchase price is a natural number, and every use site of this theorem instantiates $B$ as a cast natural — the mission's goal applies it as lp_optimum_box (B : ℝ) (Nat.cast_nonneg B) k. The hypothesis $B \ge 0$ is therefore discharged automatically wherever the theorem is used, and costs a solver nothing. It is stated because these LP declarations take a general real cost coefficient, while the algorithm declarations take $B : \mathbb{N}$ .

For completeness: the hypothesis is not actually required for this bounded region, and an earlier version of this note wrongly claimed it was. It is required for the companion statement over the unbounded region of Figure 3.1, where $x$ may grow without limit. That distinction matters only if someone reuses these statements outside the ski-rental setting.

Nothing here is asserted about the unbounded region, and no uniqueness of a minimiser is claimed.

Preamble

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

open PrimalDualOnline.SkiRental

Formal statement

theorem PrimalDualOnline.SkiRental.lp_optimum_box
    (B : ℝ) (hB : 0 ≤ B) (k : ℕ) :
    IsLeast (primalValues B k) (offlineOpt B k) := 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. 17 (PDF p. 33): the no-integrality-gap remark ("Note that the optimal solution is always integral, and thus the relaxation has no integrality gap"), over the [0,1]-bounded region described in the same paragraph.

Read-back

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

Ambient data and binders. The statement quantifies universally over a real number $B$ , a hypothesis $h_B : 0 \le B$ , and a natural number $k$ . There are no other binders, no implicit arguments, no typeclass assumptions. $B$ is an arbitrary nonnegative real (not required to be an integer, nor bounded above), and $k$ is arbitrary (not required to be positive). Where $k$ appears arithmetically it is the cast into $\mathbb{R}$ .

The feasible region, unfolded. A pair consisting of a real $x$ and a family $z = (z_j)_{j \in \{0,\dots,k-1\}}$ is box-feasible exactly when

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

All six inequalities are weak ( $\le$ , never $<$ ). The variables range over $\mathbb{R}$ ; no integrality is imposed.

The objective, unfolded. $\mathrm{cost}_B(x, z) = B \cdot x + \sum_{j} z_j$ : the single variable $x$ carries coefficient $B$ and each of the $k$ variables $z_j$ carries coefficient exactly $1$ .

The set under consideration, unfolded. $V(B,k) \subseteq \mathbb{R}$ is the set of achievable cost values:

V(B,k) = \bigl\{\, v \in \mathbb{R} \;\bigm|\; \exists\, x,\ \exists\, z,\ (x,z) \text{ box-feasible and } B x + \textstyle\sum_j z_j = v \,\bigr\}.

This is a set of values, not of feasible points.

The claimed value. $\mathrm{opt}(B,k) = \min(B, k)$ , the smaller of the reals $B$ and $k$ .

What is asserted. That $\mathrm{opt}(B,k)$ is a least element of $V(B,k)$ , which unfolds to a conjunction of exactly two claims:

Attainment (membership). $\min(B,k) \in V(B,k)$ — there exist $x$ and $(z_j)_j$ box-feasible whose cost equals $\min(B,k)$ exactly.
Lower bound. For every $v \in V(B,k)$ , $\min(B,k) \le v$ ; equivalently, for every box-feasible pair, $\min(B,k) \le B x + \sum_j z_j$ .

Because membership is part of the claim, this is a statement about a minimum (least element), not merely an infimum: the value is asserted to be achieved, which is strictly stronger than being the greatest lower bound. In particular it entails $V(B,k)$ is nonempty.

Degenerate and boundary cases. $k = 0$ — the index type is empty, the constraints on $z$ are vacuous, the sum is $0$ , and box-feasibility reduces to $0 \le x \le 1$ ; then $V(B,0) = \{B x : 0 \le x \le 1\}$ and the asserted least value is $\min(B,0) = 0$ . $B = 0$ — permitted by $h_B$ ; the objective becomes $\sum_j z_j$ and the asserted least value is $0$ . $B > k$ — the asserted least value is the real number $k$ . $B < k$ — it is $B$ itself. $B = k$ — both arguments coincide; nothing distinguishes which feasible pair realises it. $B$ non-integer or arbitrarily large — fully included. $B < 0$ is excluded by $h_B$ .

What is NOT asserted. Nothing about any other feasible region: the only region mentioned is the boxed one, and no claim is made about the region obtained by dropping the upper bounds, in particular no claim that the two regions have equal optimal value, equal value sets, or the same minimisers. Nothing about uniqueness of a minimiser: clause 1 is a bare existential and does not exhibit or constrain the attaining pair. Nothing about integral or $\{0,1\}$ -valued solutions, any dual program, weak or strong duality, complementary slackness, any online or algorithmic procedure, any competitive ratio, or any interpretation of $B, k, x, z$ beyond their role in the inequalities. No monotonicity, continuity, or convexity of $B \mapsto \mathrm{opt}(B,k)$ .

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

Optimum of the canonical fractional ski-rental program is min⁡(B,k)\min(B,k)min(B,k)

Optimum of the canonical fractional ski-rental program is $\min(B,k)$