Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 2, p. 17 — (1 − 1/e)σ⁽¹⁾ < 1 − e^{−σ⁽¹⁾} < 1 − e^{−α⁽¹⁾}, 1/(1 + ln(r⁽ᵐ⁾/r⁽¹⁾)) < σ⁽¹⁾, and 1 − e^{−α} < 1 − e^{−α⁽¹⁾}

Proved
MultiPriceOnline.Ratios.proposition_2

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

booking-limitscompetitive-ratioonline-matchingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1real-analysis

Let m≥2m \ge 2m≥2 and let 0<r(1)<⋯<r(m)0 < r^{(1)} < \dots < r^{(m)}0<r(1)<⋯<r(m) be a price set. Let α(1),…,α(m)\alpha^{(1)}, \dots, \alpha^{(m)}α(1),…,α(m) be its booking limits (positive, summing to 111, satisfying (7)) and σ(1),…,σ(m)\sigma^{(1)}, \dots, \sigma^{(m)}σ(1),…,σ(m) its Ball–Queyranne limits (positive, summing to 111, satisfying (8)). Then

(1−1e)σ(1)<1−e−σ(1)<1−e−α(1),(11)\Bigl(1 - \frac1e\Bigr)\sigma^{(1)} < 1 - e^{-\sigma^{(1)}} < 1 - e^{-\alpha^{(1)}}, \qquad (11)(1−e1​)σ(1)<1−e−σ(1)<1−e−α(1),(11) 11+ln⁡(r(m)/r(1))<σ(1),(12)\frac{1}{1 + \ln\bigl(r^{(m)}/r^{(1)}\bigr)} < \sigma^{(1)}, \qquad (12)1+ln(r(m)/r(1))1​<σ(1),(12)

and, for the real number α\alphaα solving 1−e−α=(1−α)/ln⁡(r(m)/r(1))1 - e^{-\alpha} = (1 - \alpha)/\ln(r^{(m)}/r^{(1)})1−e−α=(1−α)/ln(r(m)/r(1)),

1−e−α<1−e−α(1).(13)1 - e^{-\alpha} < 1 - e^{-\alpha^{(1)}}. \qquad (13)1−e−α<1−e−α(1).(13)

The proposition places the paper's tight ratio F(P)=1−e−α(1)F(\mathcal P) = 1 - e^{-\alpha^{(1)}}F(P)=1−e−α(1) among known ratios: σ(1)\sigma^{(1)}σ(1) is the tight ratio for a single item with price set P\mathcal PP and 1−1/e1 - 1/e1−1/e the tight ratio for many single-price items, and (11) shows that F(P)F(\mathcal P)F(P) strictly exceeds their naive combination (1−1/e)σ(1)(1 - 1/e)\sigma^{(1)}(1−1/e)σ(1). Inequalities (12) and (13) say that restricting the price continuum [r(1),r(m)][r^{(1)}, r^{(m)}][r(1),r(m)] to the discrete set P\mathcal PP 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 111; by Proposition 1 these are the paper's α(j)\alpha^{(j)}α(j), σ(j)\sigma^{(j)}σ(j). The constant 1−1/e1 - 1/e1−1/e is written 1−e−11 - e^{-1}1−e−1. Clause (13) is stated for every real root aaa of 1−e−a=(1−a)/ln⁡(r(m)/r(1))1 - e^{-a} = (1-a)/\ln(r^{(m)}/r^{(1)})1−e−a=(1−a)/ln(r(m)/r(1)); since this equation has exactly one real root for m≥2m \ge 2m≥2 (milestone (34)), this is the paper's statement about "the unique solution", and it is not vacuous. The hypothesis m≥2m \ge 2m≥2 is the paper's: for m=1m = 1m=1 one has σ(1)=α(1)=1\sigma^{(1)} = \alpha^{(1)} = 1σ(1)=α(1)=1 and ln⁡(r(m)/r(1))=0\ln(r^{(m)}/r^{(1)}) = 0ln(r(m)/r(1))=0.

Preamble
import Mathlib
import Definitions.Def_MultiPriceOnline_Ratios_Setting
Formal statement
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
Source
Ma, Simchi-Levi, Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-dependent Competitive Ratios, arXiv:1905.04770v1, p. 17, Proposition 2, (11)–(13)
Human review
  • Endorsed by Shuze Chen · Oct 10, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 10, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me