Ski rental problem

AbbreviationDeterministic ski-rental strategy#✓fully proved

A deterministic strategy is either a day \(t \in \mathbb{N}\) on which to buy the skis, after renting on the days before it, or the choice to rent forever. Days are numbered from \(1\); the value \(t = 0\) is also a strategy, and the cost treats it as renting forever.

abbrev Strategy := Option ℕ

Used by 4

Used byBreak-even strategy · Cost of a ski-rental strategy · Lower bound · The offline optimum bounds every strategy's cost

DefinitionCost of a ski-rental strategy#✓fully proved

Renting skis costs \(1\) per day and buying them costs a natural number \(B\). The cost \(\mathrm{cost}_B(s, d) \in \mathbb{N}\) of a strategy \(s\) for a season of \(d \in \mathbb{N}\) days is \((t - 1) + B\) if \(s\) buys on a day \(t\) with \(1 \le t \le d\) (rent for \(t - 1\) days, then buy), and \(d\) otherwise, that is, if \(s\) rents forever or buys on a day \(t\) with \(t = 0\) or \(t > d\) (rent every day).

def cost (B : ℕ) : Strategy → ℕ → ℕ
  | some t, d => if 1 ≤ t ∧ t ≤ d then (t - 1) + B else d
  | none, d => d

Uses 1 · Used by 4

Statement usesDeterministic ski-rental strategy

Used bySki-rental upper bound for the break-even strategy · The break-even strategy pays at most twice the optimum · Lower bound · The offline optimum bounds every strategy's cost

DefinitionOffline optimum for ski rental#✓fully proved

For a purchase price \(B \in \mathbb{N}\) and a season of \(d \in \mathbb{N}\) days, the offline optimum is \(\mathrm{opt}_B(d) = \min(d, B)\): rent every day or buy on day one, whichever is cheaper.

def opt (B d : ℕ) : ℕ := min d B

Used by 4

Used bySki-rental upper bound for the break-even strategy · The break-even strategy pays at most twice the optimum · Lower bound · The offline optimum bounds every strategy's cost

DefinitionBreak-even strategy#✓fully proved

For a purchase price \(B\), the break-even strategy is the deterministic strategy that buys on day \(B\).

def breakEven (B : ℕ) : Strategy := some B

Uses 1 · Used by 2

Statement usesDeterministic ski-rental strategy

Used bySki-rental upper bound for the break-even strategy · The break-even strategy pays at most twice the optimum

TheoremThe offline optimum bounds every strategy's cost#✓fully proved

For every purchase price \(B\), every deterministic strategy \(s\) and every season length \(d\), the offline optimum \(\mathrm{opt}_B(d)\) is at most the cost \(\mathrm{cost}_B(s, d)\) of \(s\) for a season of \(d\) days.

theorem opt_le_cost (B : ℕ) (s : Strategy) (d : ℕ) : opt B d ≤ cost B s d

Uses 3

Statement usesDeterministic ski-rental strategy · Cost of a ski-rental strategy · Offline optimum for ski rental

TheoremSki-rental upper bound for the break-even strategy#✓fully proved

For every purchase price \(B \ge 1\) and every season length \(d\), the break-even strategy \(\mathrm{breakEven}_B\) pays at most \(2 - 1/B\) times the offline optimum \(\mathrm{opt}_B(d)\): its cost \(\mathrm{cost}_B(\mathrm{breakEven}_B, d)\) for a season of \(d\) days satisfies \(B \cdot \mathrm{cost}_B(\mathrm{breakEven}_B, d) \le (2B - 1) \cdot \mathrm{opt}_B(d)\).

theorem cost_breakEven_le {B : ℕ} (hB : 1 ≤ B) (d : ℕ) :
    B * cost B (breakEven B) d ≤ (2 * B - 1) * opt B d

Uses 3 · Used by 1

Statement usesBreak-even strategy · Cost of a ski-rental strategy · Offline optimum for ski rental

Used byThe break-even strategy pays at most twice the optimum

TheoremThe break-even strategy pays at most twice the optimum#✓fully proved

For every purchase price \(B \ge 1\) and every season length \(d \in \mathbb{N}\), the cost \(\mathrm{cost}_B(\mathrm{breakEven}_B, d)\) of the break-even strategy for a season of \(d\) days is at most \(2 \cdot \mathrm{opt}_B(d)\), twice the offline optimum \(\mathrm{opt}_B(d)\). In particular, the break-even strategy is \(2\)-competitive.

theorem cost_breakEven_le_two_mul {B : ℕ} (hB : 1 ≤ B) (d : ℕ) :
    cost B (breakEven B) d ≤ 2 * opt B d

Uses 4

Statement usesBreak-even strategy · Cost of a ski-rental strategy · Offline optimum for ski rental

Proof usesSki-rental upper bound for the break-even strategy

TheoremLower bound#✓fully proved

Every deterministic strategy pays at least (2 - 1/B) times the optimum on some season, (2 B - 1) * opt ≤ B * cost.

theorem exists_cost_ge {B : ℕ} (hB : 1 ≤ B) (s : Strategy) :
    ∃ d, (2 * B - 1) * opt B d ≤ B * cost B s d

Uses 3

Statement usesDeterministic ski-rental strategy · Cost of a ski-rental strategy · Offline optimum for ski rental

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.