Proposition 2, p. 17 — (1 − 1/e)σ⁽¹⁾ < 1 − e^{−σ⁽¹⁾} < 1 − e^{−α⁽¹⁾}, 1/(1 + ln(r⁽ᵐ⁾/r⁽¹⁾)) < σ⁽¹⁾, and 1 − e^{−α} < 1 − e^{−α⁽¹⁾}
ProvedMultiPriceOnline.Ratios.proposition_2Let and let be a price set. Let be its booking limits (positive, summing to , satisfying (7)) and its Ball–Queyranne limits (positive, summing to , satisfying (8)). Then
and, for the real number solving ,
The proposition places the paper's tight ratio among known ratios: is the tight ratio for a single item with price set and the tight ratio for many single-price items, and (11) shows that strictly exceeds their naive combination . Inequalities (12) and (13) say that restricting the price continuum to the discrete set strictly raises the tight ratio, for one item and for many items respectively.
Formalization Note The booking limits enter as arbitrary families satisfying (7) resp. (8) with positivity and sum ; by Proposition 1 these are the paper's , . The constant is written . Clause (13) is stated for every real root of ; since this equation has exactly one real root for (milestone (34)), this is the paper's statement about "the unique solution", and it is not vacuous. The hypothesis is the paper's: for one has and .
import Mathlib import Definitions.Def_MultiPriceOnline_Ratios_Setting
namespace MultiPriceOnline.Ratios
theorem proposition_2 (m : ℕ) (hm : 2 ≤ m) (r : ℕ → ℝ) (hr : MultiPriceOnline.Balance.IsPriceSet m r)
(α : ℕ → ℝ) (hα : MultiPriceOnline.Balance.IsBookingLimits m r α) (σ : ℕ → ℝ) (hσ : MultiPriceOnline.Balance.IsBQLimits m r σ) :
((1 - Real.exp (-1)) * σ 1 < 1 - Real.exp (-σ 1) ∧
1 - Real.exp (-σ 1) < 1 - Real.exp (-α 1)) ∧
1 / (1 + Real.log (r m / r 1)) < σ 1 ∧
∀ a : ℝ, 1 - Real.exp (-a) = (1 - a) / Real.log (r m / r 1) →
1 - Real.exp (-a) < 1 - Real.exp (-α 1) := by sorry
end MultiPriceOnline.Ratios
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.