Analysis

Motivation

Optimal stopping with partial information sits between two classical problems. In the secretary problem a decision maker sees values in random order, knows nothing about how they are generated, and must stop on the best one; the optimal guarantee is $1/e$. In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee, relative to the expected maximum, is the constant $\alpha^*\approx 0.745$: Hill and Kertz (1982) and Kertz (1986) showed that no stopping rule does better on every distribution, and Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017, doi:10.1145/3033274.3085137) gave a rule that achieves it. Practical settings, such as pricing from historical data, lie in between: the distribution is unknown, but samples of it are available.

Correa, Cristi, Epstein and Soto (arXiv:2011.06516v2) interpolate between the two problems with the $p$-sample-driven optimal stopping problem: each of $N$ adversarial values is independently revealed in advance (a sample) with probability $p$, and the remaining values arrive online in random order. At $p=0$ this is the secretary problem; as $p\to1$ it approaches the i.i.d. prophet inequality. They show that the optimal competitive ratio $\alpha(p)$ of the limit problem is the value of an infinite-dimensional linear program, and they construct an explicit threshold rule whose guarantee $\tilde\alpha(p)$ is the root of a scalar equation.

Prior work on learning a distribution from samples obtained guarantees $\alpha^*-O(\varepsilon)$ with $O(n^2/\varepsilon)$ samples (Correa, Dütting, Fischer, Schewior, 2019) and with $O(n/\varepsilon^6)$ samples (Rubinstein, Wang, Weinberg, 2020). Theorem 9 of the paper, the goal of this mission, gives such a guarantee with $O(n/\varepsilon)$ samples.

Setting

Fix $p\in(0,1)$. The guarantee of the explicit threshold rule is the number $\tilde\alpha(p)\in(0,1)$ solving

$$\ln p+\frac{\tilde\alpha(1-p)^2}{p}=\sum_{i=1}^{\infty}\frac{\ln\bigl(1-\tilde\alpha+\tilde\alpha[(i+1)p^i-ip^{i+1}]\bigr)}{i(i+1)}.\tag{19}$$

Lemma 7 of the paper shows that (19) has exactly one root in $(0,1)$. The i.i.d. prophet constant $\alpha^*\in(0,1)$ is the solution of

$$\int_0^1\frac{dy}{y(1-\ln y)+1/\alpha^*-1}=1 .$$

The proof of Theorem 9 (Appendix B.9) works with three auxiliary functions of $p$, each depending on $\alpha^*$ as a parameter:

$$a(p)=\sum_{i\ge1}\frac{\ln\bigl(\tfrac1p-\alpha^*(1-p^i(1+i(1-p)))\bigr)}{i(i+1)}+\alpha^*(2p-p^2),\qquad b(p)=\frac1{p^2}\sum_{i\ge1}\frac{1}{i(i+1)\bigl(\tfrac1p-\alpha^*(1-p^i(1+i(1-p)))\bigr)},$$ $$c(p)=\sum_{i\ge1}\frac{p^{i-1}-p^i}{\tfrac1{p\alpha^*}-1+p^i(1+i(1-p))}.$$

Appendix B.7 also names the two sides of (19): $f(p,\alpha)=\ln p+\alpha(1-p)^2/p$ and $g(p,\alpha)=\sum_{i\ge1}\ln(1+\alpha(p^i(1+i(1-p))-1))/(i(i+1))$. In Lean, IsAlphaTilde p a and IsAlphaStar s are shared predicates in SampleDrivenOS.Limit; aB9 s p, bB9 s p, cB9 s p, fB7 p α, and gB7 p α are in SampleDrivenOS.Linear.

Formalization targets

Goal: Theorem 9 (p. 17)

$$\text{for every }p\in(0,1):\qquad \tilde\alpha(p)\ \ge\ \alpha^*p .$$

It is stated for every root $\tilde\alpha$ of (19) and every solution $\alpha^*$ of the integral equation; neither existence nor uniqueness is assumed.

Milestones (Appendix B.7 and B.9, in the order the proof uses them)

1. B.7: $f(p,\cdot)$ is strictly increasing on $[0,1]$ and $g(p,\cdot)$ non-increasing on $[0,1)$.
2. B.9: if (19) holds with "$\le$" at $\alpha^*p$ in place of $\tilde\alpha$ (after the substitution $\tilde\alpha=f(p)p$), then $\tilde\alpha(p)\ge\alpha^*p$.
3. B.9: that inequality is equivalent to $\alpha^*\le a(p)$.
4. B.9: $a$ is differentiable on $(0,1)$ with $a'(p)=2\alpha^*(1-p)-b(p)+c(p)$, also in term-by-term form.
5. B.9: $b(p)\ge 1/p$.
6. B.9: $c(p)\le\frac1p\int_0^1\frac{dy}{1/(p\alpha^*)-1+y(1-p\ln y)}-\alpha^*(1-p)$.
7. B.9: using the defining equation of $\alpha^*$,

$$\frac1p\int_0^1\frac{dy}{\tfrac1{p\alpha^*}-1+y(1-p\ln y)}\le\frac1p-\frac{1-p}{p}\Bigl(\frac1{p\alpha^*}-\frac1e\Bigr)\ln\frac{\tfrac1{p\alpha^*}+\tfrac pe}{\tfrac1{p\alpha^*}+\tfrac pe-1}.$$

8. B.9: for all $s\in[0.74,0.75]$ and $p\in(0,1)$, $\bigl(\frac1{ps}-\frac1e\bigr)\ln\frac{1/(ps)+p/e}{1/(ps)+p/e-1}\ge0.8$.
9. B.9: if $\alpha^*\in[0.74,0.75]$, then $c(p)\le\frac1p-\alpha^*(1-p)(1+\frac1p)$.
10. B.9: under the same hypothesis, $\frac{d}{dp}a(p)\le0$ on $(0,1)$.

Significance

The explicit rule's guarantee $\tilde\alpha(p)$ is a lower bound on the optimal ratio $\alpha(p)$, and Theorem 8 (a separate mission of this series) shows $\tilde\alpha(p)\to\alpha^*$ as $p\to1$. Theorem 9 makes that convergence quantitative and uniform: the guarantee is at least linear in $p$, so with $p=1-\varepsilon$, an online set of size $n=\varepsilon N$ and $O(n/\varepsilon)$ samples the rule earns $\alpha^*-O(\varepsilon)$ of the expected maximum. This improves the sample complexity of the earlier learning-based results by a polynomial factor, in a model more general than theirs.

The theorem is proved in the paper; it has no machine-checked proof. The proof is elementary real analysis on explicit series and integrals, and one of its steps is a numerical check that the paper does not carry out in print. A formalization turns that numerical claim into a certified inequality and checks a chain of estimates in which one inequality sign is misprinted (see Formalization scope).

Difficulty

The statement is about two implicitly defined numbers. $\tilde\alpha(p)$ has no closed form, and $\alpha^*$ is defined by an integral equation. Evaluating both numerically at finitely many $p$ proves nothing for the remaining $p$, and the inequality is tight at $p=1$ ($\tilde\alpha(1)=\alpha^*$), so no uniform slack is available near $p=1$.

Concavity of $\tilde\alpha$ would give the result immediately, and the paper reports it numerically, but the authors were unable to prove it; the argument must avoid it. The remaining work handles infinite series whose terms depend on $p$ through both $p^i$ and $i(1-p)$: differentiating such a series term by term requires uniform control of the derivative series, comparing it with an integral needs a monotonicity argument, and one step needs a bound valid on an entire two-parameter region rather than at a point.

Formalization scope

• Numbers, not processes. No probability, program or algorithm appears in Lean. Everything is a real-valued function on $\mathbb R$.
• Predicates, not choice. $\tilde\alpha(p)$ and $\alpha^*$ enter as IsAlphaTilde p a (with $0<a<1$) and IsAlphaStar s (with $0<s<1$). Statements quantify over every solution. Both exist, so the goal is not vacuous: existence of $\tilde\alpha$ is Lemma 7 (posed in the second mission of this series), and existence and uniqueness of $\alpha^*=1/\beta^*$ are posed as CorreaThreshold.Adaptive.beta_star_existsUnique (512ff915-7ec1-4d24-87b3-bc8adfee6bad).
• Series. Every series is a Lean tsum over i : ℕ with the paper's index $i\ge1$ shifted to i + 1. For parameters in $(0,1)$ all series are summable, so tsum is the true sum; summability is part of what solvers prove, never a hypothesis. Differentiability of $a$ is likewise a conclusion (HasDerivAt), never assumed.
• Total functions. Real.log 0 = 0 makes the integrands' values at $y=0$ equal their limits, so the interval integrals are the true integrals. Every division ($1/p$, $1/(ps)$) is at a positive argument under the stated ranges, and every logarithm's argument is positive.
• $\alpha^*\approx0.745$. The paper uses this approximation through the interval $\alpha^*\in[0.74,0.75]$ of its numerical check. Milestones 9 and 10 carry that interval as a hypothesis; the goal does not. The lower bound $\alpha^*>0.745$ is posed as CorreaThreshold.Adaptive.inv_beta_star_gt (ce70487c-b155-4e47-9ce8-8348dc1b1645). The upper bound $\alpha^*\le0.75$ (numerically $\alpha^*\approx0.74544$) is posed nowhere and is welcome as a lemma.
• A printed slip. The paper prints the conclusion of milestone 9 as "$c(p)\ge\dots$". The surrounding argument requires and announces "$\le$", and the formal statement uses $\le$.
• Ruled-out trivializations. Fixing $p$, replacing $\alpha^*$ by the numeral $0.745$ (a weaker statement, since $0.745<\alpha^*$), stating $a$'s monotonicity through deriv (which is $0$ at non-differentiable points), or replacing $\tilde\alpha$ by a chosen value all change the theorem. None is used.
• Reusable infrastructure. Welcome contributions include term-by-term differentiation of tsums under a dominating series, Riemann-sum comparisons for monotone integrands, a Chebyshev-type integral inequality for two decreasing functions, and certified interval arithmetic for a two-variable inequality such as milestone 8.

Selected references

• J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021 (journal version: Mathematics of Operations Research, 2024). https://arxiv.org/abs/2011.06516v2
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted Price Mechanisms for a Random Stream of Customers, ACM EC 2017; Mathematics of Operations Research 46(4), 2021. https://doi.org/10.1145/3033274.3085137
• T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Annals of Probability 10(2), 1982 (reference [26] of the paper). https://doi.org/10.1214/aop/1176993767
• R. P. Kertz, Stop rule and supremum expectations of i.i.d. random variables: a complete comparison by conjugate duality, Journal of Multivariate Analysis 19, 1986 (reference [28] of the paper).
• J. Correa, P. Dütting, F. Fischer, K. Schewior, Prophet Inequalities for I.I.D. Random Variables from an Unknown Distribution, ACM EC 2019. https://doi.org/10.1145/3328526.3329627
• A. Rubinstein, J. Z. Wang, S. M. Weinberg, Optimal Single-Choice Prophet Inequalities from Samples, ITCS 2020. https://doi.org/10.4230/LIPIcs.ITCS.2020.60

Motivation

Optimal stopping with samples sits between two classical problems. In the secretary problem a decision maker sees items in random order, knows nothing about their values, and must stop on one; the best guarantee is $1/e$. In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee against the expected maximum is the constant $\alpha^*\approx0.745$: Hill and Kertz (1982) and Kertz (1986) showed that no stopping rule does better, and Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017) showed that it is achieved. Real decision makers usually have neither nothing nor everything: they have a history of past observations.

Correa, Cristi, Epstein and Soto (arXiv:2011.06516v2) model this as $p$-DOS (sample-driven optimal stopping): each of $N$ items is independently placed in a history set with probability $p$, the decision maker sees the history first and then the remaining items online, and must stop on one online item. At $p=0$ this is the secretary problem; as $p\to1$ the history reveals the distribution and the problem approaches the i.i.d. prophet setting. This mission formalizes the paper's Theorem 8, which makes the second statement precise: the optimal guarantee tends to $\alpha^*$.

Timeline. Hill and Kertz (1982) compared stop-rule and supremum expectations for i.i.d. variables; Kertz (1986) completed the comparison, giving the worst-case constant $\approx0.745$ through the integral equation used below; Correa et al. (2017) gave a matching algorithm. Kaplan, Naori and Raz (2020) studied the sample-driven model with a weaker bound for small $p$; Correa, Dütting, Fischer and Schewior (2019) and Rubinstein, Wang and Weinberg (2020) studied i.i.d. values with samples from an unknown distribution. The present paper (2020–2021) gives the exact limit program and Theorem 8.

Setting

Fix $p\in(0,1)$. A stopping rule is a nonnegative function $q(t,\ell)$ of a time $t\in[p,1]$ and a rank $\ell\ge1$. For $k\ge1$ let

$$F_k(q)=\sum_{\ell=1}^{k}\int_p^1 q(t,\ell)\sum_{j=\ell}^{k}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^{\ell}\,dt .$$

The limit program SDCLP$_p$ maximizes $\alpha\in[0,1]$ over pairs $(q,\alpha)$ with

$$t\,q(t,\ell)+\int_p^t\sum_{s\ge1}q(\tau,s)\,d\tau\le1\quad(t\in[p,1],\ \ell\ge1),\qquad \alpha\le\frac{F_k(q)}{1-p^k}\quad(k\ge1).$$

Its optimal value is $\alpha(p)$. The paper obtains SDCLP$_p$ as the limit $N\to\infty$ of the linear programs that describe the best algorithm for $p$-DOS with adversarial values (§4.1–4.2); Theorem 8 is a statement about the program's value.

Two constants are defined by equations. $\tilde\alpha(p)$ is the unique root in $(0,1)$ of

$$\ln p+\frac{\tilde\alpha(1-p)^2}{p}=\sum_{i=1}^{\infty}\frac{\ln\bigl(1-\tilde\alpha+\tilde\alpha[(i+1)p^i-ip^{i+1}]\bigr)}{i(i+1)},\qquad(19)$$

and $\alpha^*$ is the solution of $\int_0^1\frac{dy}{y(1-\ln y)+1/\alpha^*-1}=1$. A threshold rule (12) is given by times $p=t_1\le t_2\le\cdots\le1$ with $T_i=\prod_{j\le i}t_j$: on $[t_i,t_{i+1})$ it equals $T_i/t^{i+1}$ for ranks $\ell\le i$ and $0$ for larger ranks.

Formalization targets

Goal: Theorem 8

$$0\le\tilde\alpha(p)\le\alpha(p)\le\alpha^*\quad(p\in(0,1)),\qquad \lim_{p\to1^-}\tilde\alpha(p)=\lim_{p\to1^-}\alpha(p)=\alpha^*.$$

Milestones, in the order the proof uses them

1. B.4: $\sum_{\ell=1}^{j}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^\ell=t$.
2. Lemma 4: a maximal $\alpha$ satisfies $\alpha\ge\inf_{k\ge1}\frac{1}{1-p^k}\sum_{j\le k}\int_p^1 t\,q(t,j)\,dt$ when $q$ is non-increasing in $\ell$.
3. Lemma 5: for a threshold rule, the system "every term of that infimum equals $\alpha$" is equivalent to explicit equations (15)–(16).
4. Lemma 6 (i), (ii): the times $t_1=p$, $t_2=pe^{\alpha(1-p)^2/p}$, $(t_k/t_{k+1})^{k-1}=\gamma_k/\gamma_{k-1}$ increase, and their limit is at most $1$ exactly under condition (18).
5. B.6: $T_i/t_i^{i-1}=p\gamma_{i-1}$ and $\mu_k=p(1-\alpha+\alpha p^{k-2})/(k-2)$.
6. Lemma 6 (iii): under (18) the threshold rule is feasible with value $\alpha$.
7. Lemma 7: (19) has a unique root, continuous in $p$.
8. B.8: the ratio $h(p,\eta)$ of the two sides of (19) tends to $\int_0^1\frac{dy}{y(1-\ln y)+1/\eta-1}$ as $p\to1$.

Significance

The result. Theorem 8 shows that sample access interpolates continuously between the secretary and prophet worlds and that, with almost full information, no more than the known-distribution guarantee $\alpha^*$ is lost or gained. The explicit rule behind $\tilde\alpha(p)$ is a concrete threshold algorithm, and the companion Theorem 9 of the paper ($\tilde\alpha(p)\ge\alpha^*p$, a separate mission) turns it into sample-complexity bounds: $O(n/\varepsilon)$ samples suffice for $\alpha^*-O(\varepsilon)$.

Formalizing it. The result is proved on paper; no part of it is machine-checked. A formal proof contributes a verified treatment of an infinite-dimensional linear program over $L^1([p,1]\times\mathbb N)$, of series defined through implicit equations, and of a Riemann-sum limit obtained by l'Hôpital's rule. One clause, $\alpha(p)\le\alpha^*$, is not proved in the paper: it is imported from the i.i.d. prophet inequality literature via the interpretation of $\alpha(p)$ as a competitive ratio. A formal proof of that clause directly from SDCLP$_p$ would be new.

Difficulty

The lower bound $\tilde\alpha(p)\le\alpha(p)$ needs an explicit feasible point of an infinite program; checking feasibility of the threshold rule requires exact telescoping of series with products of the times $t_k$, which are defined recursively through fractional powers. The limit $\tilde\alpha(p)\to\alpha^*$ is a $0/0$ limit of infinite series whose terms change scale as $p\to1$: every individual term tends to zero, so termwise passage to the limit gives no information, and the integral in the defining equation of $\alpha^*$ appears only in an aggregate limit of the whole series. The upper bound $\alpha(p)\le\alpha^*$ cannot come from evaluating any single solution: it is a statement about every feasible $q$, and the paper obtains it only through an external argument.

Formalization scope

• A stopping rule is q : ℝ → ℕ → ℝ; ranks are 1-based (values at rank $0$ are never used), and constraints are imposed pointwise on $[p,1]$ as printed. The integral of the series in (10) is a lower Lebesgue integral of an $[0,\infty]$-valued series, so it cannot collapse to a junk value; each $q(\cdot,\ell)$ is required integrable on $[p,1]$.
• $\alpha(p)$ is sSup of the set of feasible $\alpha$; it contains $0$ and is bounded by $1$, so it is the true supremum (checked in a sorry-free verification file). The program ranges over all feasible $q$, never only threshold rules.
• (11) is quantified over $k\ge1$ only, so $1-p^k\neq0$.
• Threshold rules use the half-open intervals $[t_i,t_{i+1})$ of (7); (12) prints closed intervals, which overlap at the $t_i$.
• The series in (18), (19), (26) and $\mu_k$ are written with the summation index shifted to start at $0$; with $p,\alpha\in(0,1)$ every logarithm's argument lies in $[1-\alpha,1]$, so they converge absolutely and tsum is the true sum.
• Lemma 6's recursion is $t_{k+1}=t_k(\gamma_{k-1}/\gamma_k)^{1/(k-1)}$ for $k\ge2$, the unique positive solution of (17).
• $\tilde\alpha$ and $\alpha^*$ are predicates (IsAlphaTilde, IsAlphaStar), not chosen functions; the goal holds for every root selection. Existence and uniqueness of $\alpha^*$ (with $\beta=1/\alpha^*$) is already posed as the open item CorreaThreshold.Adaptive.beta_star_existsUnique and is not posed again.
• "$p\to1$" is the one-sided filter 𝓝[<] 1.
• Lemma 6 (iii) carries hypothesis (18), which the paper states in the sentence after the lemma; without it the claim is false.

Trivializing formalizations are ruled out: replacing $\alpha(p)$ by $\tilde\alpha(p)$ or by the value of a truncated program, fixing $p$, restricting $q$ to threshold rules in the definition of $\alpha(p)$, or replacing $\alpha^*$ by $0.745$ each changes the theorem and is not done.

A complete development needs: binomial identities, interval integrals of $t^{-i}$ and of piecewise-defined functions, real powers and logarithms of recursively defined sequences, summability of series in $\ell^1$, continuity of the root of a monotone family of equations, and limits of Riemann-type sums on $(0,1]$. The last two are reusable beyond this mission. Proofs of individual milestones are welcome independently of the goal.

Selected references

• J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021. https://arxiv.org/abs/2011.06516v2
• T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, The Annals of Probability 10(2), 336–345, 1982 (reference [26] of the paper).
• R. P. Kertz, Stop rule and supremum expectations of i.i.d. random variables: a complete comparison by conjugate duality, Journal of Multivariate Analysis 19, 88–112, 1986 (reference [28]).
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted price mechanisms for a random stream of customers, ACM EC 2017 (reference [17]).
• H. Kaplan, D. Naori, D. Raz, Competitive analysis with a sample and the secretary problem, SODA 2020 (reference [27]).
• J. Correa, P. Dütting, F. Fischer, K. Schewior, Prophet inequalities for i.i.d. random variables from an unknown distribution, ACM EC 2019 (reference [15]).
• A. Rubinstein, J. Z. Wang, S. M. Weinberg, Optimal single-choice prophet inequalities from samples, ITCS 2020 (reference [40]).

Motivation

Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu picks the option that maximizes his utility, however small the advantage over the next-best option. In many settings this is implausible. Agents may face cognitive or computational costs, or the designer may only be able to certify incentives approximately, as in algorithmic mechanism design where exact incentive compatibility is replaced by ε-incentive compatibility: no deviation gains more than $\varepsilon$.

Balseiro, Besbes and Castro (arXiv:2103.03403v2; Operations Research, 2024) ask how much a revenue-maximizing seller can gain when the buyer is only an $\varepsilon$-optimizer, in the most basic setting: one seller, one item, one buyer. Without the relaxation the answer is classical: by Myerson (1981) and Riley–Zeckhauser (1983) the optimal mechanism is a posted price. The rounding argument usually attributed to Nisan shows that the gain from the relaxation is $O(\varepsilon^{1/2})$ for every distribution. This mission formalizes the paper's first main theorem, which shows that for regular instances the gain is much smaller and is determined by the local curvature of the revenue curve at the optimal price.

Setting

The buyer's value $v$ has a density $f$ on $S=[0,\bar v]$, with $\bar v>0$, $f\ge 0$, $f=0$ off $S$ and $\int_0^{\bar v}f=1$. Assumption 1 requires in addition that $f$ has bounded variation on $S$. Write $F(v)=\int_0^v f$, $\bar F=1-F$, the revenue function $R(v)=v\bar F(v)$ (the revenue of a posted price $v$), and $\dot R(v)=\bar F(v)-vf(v)$.

A mechanism $m=(x,t)$ assigns to every report $v\in S$ an allocation probability $x(v)\in[0,1]$ and a payment $t(v)\in\mathbb R$. It is individually rational (IR) if $v x(v)-t(v)\ge 0$ for all $v\in S$, and ε-incentive compatible (IC$_\varepsilon$) if

$$v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\forall v,v'\in S .$$

$\mathcal M(\varepsilon)$ is the set of such mechanisms, $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ the expected revenue, and $\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m)$.

Definition 1 (local α-power envelopes). $R$ has a unique maximizer $p^\star\in(0,\bar v)$ on $S$, and there are $\alpha>1$, $\kappa_L,\kappa_U>0$ and a neighborhood $\mathcal N_\ell=(p^\star-\ell,p^\star+\ell)\subset(0,\bar v)$ with

$$\kappa_L\alpha|v-p^\star|^\alpha\le(p^\star-v)\dot R(v)\le\kappa_U\alpha|v-p^\star|^\alpha\qquad\forall v\in\mathcal N_\ell .$$

For the uniform distribution on $[0,1]$, $p^\star=1/2$ and $\alpha=2$.

Formalization targets

Goal: Theorem 1 (p. 16)

Under Assumption 1, local $\alpha$-power envelopes at $p^\star$ and $\inf_{p\in S\setminus\mathcal N_\ell}|\dot R(p)|>0$,

$$\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))=\tilde O\big(\varepsilon^{\alpha/(2\alpha-1)}\big),$$

where $\tilde O$ allows a factor $\log(1/\varepsilon)$ and the constants depend on the instance but not on $\varepsilon$.

Milestones

The paper's argument passes through the following stated results, in attack order:

1. $\mathcal M(\varepsilon)\subseteq\mathcal M_{\text{path}}(\varepsilon)$ for the relaxation that keeps IR on $[0,\mu]$ and IC only along a path $v\mapsto v^\star(v)$ (p. 17);
2. Lemma 1 (weak duality): $\Pi(m)\le\Phi_1(\lambda)+\Phi_2(\lambda)$ for every $m\in\mathcal M_{\text{path}}(\varepsilon)$ and every dual-feasible $\lambda$;
3. Lemma 2: an explicit dual solution $\lambda^\star(v)=\frac{d}{dv}\sum_{j\le k}F(w^j(v))$ on the $k$-th step, where $w$ inverts $v^\star$;
4. Lemma 3: $\Phi_1(\lambda^\star)\le C\varepsilon K$, $K$ the number of steps;
5. Lemma 4: $\int_x^{\bar v}\Delta\le R(x)+2(w(x)-x)$ when the dual virtual value $\Delta$ is nonnegative on $[x,\nu_0]$;
6. Proposition 2: for the piecewise-linear path of eq. (9), $K=O(\log(1/\varepsilon)/\varepsilon^\beta)$;
7. the sandwich $vf-\bar F-C_L\varepsilon^\beta\le\Delta\le vf-\bar F+C_U\varepsilon^\beta$ a.e. on $[p^\star,\nu_0]$ (p. 48);
8. $\Delta\le-\dot R+C\varepsilon^\beta$ a.e. on $[0,p^\star]$ (pp. 51–52).

Significance

Theorem 1 is an instance-dependent impossibility result: no $\varepsilon$-IC mechanism can extract more than $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ beyond the optimal posted price. Since $\alpha/(2\alpha-1)>1/2$ for every $\alpha>1$, it strictly improves the universal $O(\varepsilon^{1/2})$ bound for these distributions; for $\alpha=2$ (a revenue curve with nonzero second derivative at $p^\star$) the rate is $\varepsilon^{2/3}$. Together with Theorem 3 of the same paper, a matching $\Omega(\varepsilon^{\alpha/(2\alpha-1)})$ lower bound by a randomized mechanism, it identifies the exact rate up to the logarithm. The authors conjecture that the logarithmic factor can be removed.

The result is proved in the paper; no machine-checked proof of it or of any of its lemmas exists. A formalization would check an appendix argument of several pages of explicit estimates, and would produce reusable components: a weak duality theorem for a mechanism-design program over a path of incentive constraints, an explicit solution of the functional equation $\lambda(v)=f(v)+\dot w(v)\lambda(w(v))$ by iterates of $w$, and estimates of iterated piecewise-linear maps.

Difficulty

The obvious approach is to bound the gain by perturbing the optimal posted price, which yields only the $\varepsilon^{1/2}$ rate of the rounding argument. Getting the exponent $\alpha/(2\alpha-1)$ requires an upper bound that is tight to first order, i.e. a nearly optimal dual certificate for an infinite-dimensional program. The dual depends on the choice of path: the paper's analysis shows that a parallel shift $w(x)=x+\delta$ cannot beat $\varepsilon^{1/2}$, so the path must approach the diagonal near $p^\star$ while keeping the number of steps $K$ controlled. The estimates for $\Delta$ in milestones 7–8 require tracking $\lambda^\star(w(v))$ through $K=O(\log(1/\varepsilon)/\varepsilon^\beta)$ iterations of $w$, with a bounded-variation (possibly discontinuous) density. Measure-theoretic details absent from the paper also have to be supplied: changes of variables along a Lipschitz path, almost-everywhere differentiability of iterated compositions, and integrability of the dual variable.

Formalization scope

The Lean development lives in namespace ApproxIC.UpperBound. Every function of the value is a total function ℝ → ℝ and every condition quantifies over $S$ only. Committed conventions:

• $F$ is the interval integral of $f$; $\dot R$ is the explicit expression $\bar F(v)-vf(v)$, not a derivative of $R$.
• Mechanisms are required to be measurable (disclosed: $\mathbb E_v[t(v)]$ presumes it). $\Pi^\star$ is an sSup of the revenue image, which is nonempty and bounded above by $\bar v$.
• The goal is stated as $\forall m\in\mathcal M(\varepsilon),\ \Pi(m)-\Pi^\star(\mathcal M(0))\le C\varepsilon^{\alpha/(2\alpha-1)}\log(1/\varepsilon)$ for all $\varepsilon\in(0,\varepsilon_0]$, with $C,\varepsilon_0$ chosen after the instance and before $\varepsilon$. The infimum hypothesis on $|\dot R|$ ranges over $S\setminus\mathcal N_\ell$.
• Definition 1's constants are parameters of a predicate LocalPowerEnvelope.
• Paths carry an added, disclosed assumption: $w$ is Lipschitz on $[0,\nu_0]$ (eq. (9)'s $w$ is). $\dot w$ is deriv w.
• The thresholds are $\mathbb N$-indexed with index $0$ equal to $\bar v$, so the paper's $\nu_k$ is index $k+1$.
• Lemma 1's printed sign $(v-w(v))$ in $\Phi_2$ is read as $(w(v)-v)$, as in its proof and in Lemma 4. Lemma 4's printed "$\Phi_2(\lambda)=\int_x^{\bar v}\Delta$" is read as $\int_x^{\bar v}\Delta^+=\int_x^{\bar v}\Delta$. Lemmas 3 and 4 are stated for Lemma 2's explicit $\lambda^\star$.

The goal imports only the model file; paths, the dual and eq. (9) appear only in the milestones. A formalization in which $\tilde O$'s constants are chosen after $\varepsilon$, $\Pi^\star(\mathcal M(0))$ is replaced by a constant, or the revenue integral is allowed to vanish on non-measurable mechanisms is not this theorem and is ruled out by the statement.

A complete development needs interval integrals and the fundamental theorem of calculus for absolutely continuous functions, change of variables along monotone Lipschitz maps, BoundedVariationOn, real powers and logarithms, and iterates Nat.iterate. The duality lemma and the functional-equation solution are reusable for other single-agent screening problems with relaxed incentive constraints. Contributions to any milestone, and alternative proofs of the goal that bypass the path construction, are welcome.

Selected references

• S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• J. Riley, R. Zeckhauser, Optimal Selling Strategies: When to Haggle, When to Hold Firm, Quarterly Journal of Economics 98(2), 1983. https://doi.org/10.2307/1885622

Motivation

Firms that outsource work to an agent whose effort they cannot observe often punish poor performance by suspending the relationship for a while, even though restarting costs money: a new set-up, re-training, re-mobilisation. Cao, Sun and Tian (Management Science, 2024) study this trade-off in a continuous-time principal–agent model with Poisson arrivals and a fixed switching cost paid every time work (re)starts. They characterise the optimal dynamic contract in three regimes: never hire the agent, hire and keep the agent working forever, or a control-band contract with suspension episodes of fixed length. The model extends the Poisson-arrival contracting framework of Sun and Tian (2018) by adding the switching cost.

The proof follows a guess-and-verify pattern. A stochastic verification theorem (Theorem 1 of the paper) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value. Propositions 2–7 then supply such a pair in each parameter region. This mission covers one region: the agent is much more impatient than the principal (Condition 2) and the switching cost is high.

Setting

A principal earns revenue $R$ per arrival of a Poisson process. Without the agent's effort the arrival rate is $\underline\mu\ge0$; with effort it is $\mu>\underline\mu$, and effort costs the agent $b>0$ per unit of time. While the agent works, the principal's total cost rate is $c\ge b$. Each time work starts or restarts, the principal pays a switching cost $K>0$. The principal discounts at rate $r$ and the agent at rate $\rho$, with $0<r\le\rho$. Write $\Delta\mu=\mu-\underline\mu$. Assumption 1 is $R\Delta\mu>c$.

The derived constants are

$$\beta=\frac{b}{\Delta\mu},\qquad \bar w=\frac{\beta\mu}{\rho},\qquad \underline v=\frac{\underline\mu R}{r},\qquad \bar V=\frac{R\mu-c-(\rho-r)\bar w}{r},\qquad \bar K_2=\bar V-\underline v-\bar w .$$

The variable $w\ge0$ is the agent's promised utility. The revenue threshold is

$$\hat R=\Big[\frac cb+\frac{(\rho-r)\mu}{\Delta\mu(\rho-r-\mu)}\cdot\frac{\rho-\mu}{\rho}\Big]\beta .$$

Condition 2 is: $\mu<\rho-r$ and $R\ge\hat R$.

For a function $f$ on $\mathbb R_+$ with left derivative $f'$, the working-state operator and the suspension-state operator are

$$(\mathcal A_I f)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,$$ $$(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu .$$

The first is a delay-differential operator: it evaluates $f$ at $w+\beta$. A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if

$$(\mathcal A_IV_I)(w)\ge0,\quad(\mathcal A_\emptyset V_\emptyset)(w)\ge0,\qquad 0\le V_I(w)-V_\emptyset(w)\le K,\qquad V_I(0)\ge\underline v,\ V_\emptyset(0)\ge\underline v .$$

Formalization targets

Goal: Proposition 4

Under Condition 2, let $V_I$ be the line from $\underline v$ at $w=0$ to $\bar V$ at $w=\bar w$, and let $V_I$ be constant $\bar V$ beyond $\bar w$ (display (31)). Then

$$K>\bar V-\underline v\ \Longrightarrow\ (V_I,\ V_\emptyset\equiv\underline v)\ \text{satisfies (20)–(22)},$$ $$\bar K_2<K\le\bar V-\underline v\ \Longrightarrow\ (V_I,\ V_\emptyset)\ \text{satisfies (20)–(22)},$$

where in the second case $V_\emptyset$ is the line from $\underline v$ to $\bar V-K$ on $[0,\bar w]$, constant $\bar V-K$ beyond (display (32)).

Milestones

1. Lemma EC.2(vi), second claim: if $\rho>r+\mu$, then $\bar V-\frac{\rho-r}{\rho-r-\mu}\bar w\ge\underline v$ if and only if $R\ge\hat R$.
2. Proposition 4, first part: the case $K>\bar V-\underline v$.
3. Proposition 4, second part: the case $\bar K_2<K\le\bar V-\underline v$.

Significance

Through the paper's verification theorem, Proposition 4 yields the "not hiring" half of the main Theorem 2 in the Condition 2 regime. If $K\ge\bar K_2$, the principal's value is at most $\underline v$, so it is optimal never to engage the agent (Theorem 3). The threshold $\bar K_2=\bar V-\underline v-\bar w$ is the switching cost above which the value of hiring, net of the set-up cost and of the agent's promised rent, falls below the outside value. Together with the companion missions of this series (Condition 1 with high cost, Condition 2 with medium cost, and the low-cost control-band regime), this result completes the partition of the parameter space behind Theorem 2.

The result is proved in the paper and has no machine-checked proof yet. This mission states the analytic certificate of the guess-and-verify argument, not the contract-optimality theorem. The contribution it asks for is a formal proof that these explicit functions satisfy the quasi-variational inequalities, including the left-derivative behaviour at the kink $w=\bar w$ and the algebra that links Condition 2 to the sign of $\mathcal A_IV_I$.

Difficulty

The functions are piecewise linear, so the difficulty is not analytic depth but bookkeeping that is easy to get wrong:

• The operator $\mathcal A_I$ is non-local. It evaluates $V_I$ at $w+\beta$, and which branch of (31) applies there depends on how $\bar w$ compares with $\beta$, which Condition 2 settles.
• At the kink $w=\bar w$ the functions are not differentiable, so the left-derivative convention must be used explicitly.
• The sign of $\mathcal A_IV_I$ on $[0,\bar w]$ reduces to an inequality between $\bar V$, $\underline v$ and $\bar w$, and showing that this inequality is the revenue condition $R\ge\hat R$ requires unfolding (8)–(10) and (28).

The naive check, that $\mathcal A_IV_I$ vanishes or is positive because $V_I$ is "close to" a solution of the delay equation, does not work: $V_I$ is not a solution of (25), and the inequality is strict in general.

Formalization scope

All parameters are real numbers in one structure Params. Its predicate Standing collects the paper's standing assumptions: $0\le\underline\mu<\mu$, $0<b\le c$, $K>0$, $0<r\le\rho$ and $R\Delta\mu>c$. Two of these are added to the page and disclosed: $\underline\mu\ge0$, since it is an arrival rate, and $b>0$, since (31)–(32) divide by $\bar w=\beta\mu/\rho$.

Functions are ℝ → ℝ, and every condition is quantified over $w\ge0$ only. The derivative in $\mathcal A_I$ and $\mathcal A_\emptyset$ is the left derivative derivWithin f (Set.Iic w) w, as the paper prescribes on p. 15. Inequality (20) is required for $w>0$: on $\mathbb R_+$ the left derivative at $0$ does not exist. Inequalities (21) and (22) are required exactly as printed. "Satisfy the optimality condition (20)–(22)" means exactly these three conditions; the paper's Theorem 1 additionally asks for monotonicity and concavity, but Proposition 4 does not claim them and they are not added.

The threshold $\hat R$ is the printed formula. Its denominator $\rho-r-\mu$ is positive under Condition 2, so Lean's convention $x/0=0$ never applies there.

None of the conditions is weakened: (21) keeps both bounds, (22) is kept, and the operators are not pre-simplified with the closed form of $\bar V$. A formal proof therefore has to carry out the sign computation itself. The stochastic contract model (Poisson point processes, promise keeping, incentive compatibility), the verification Theorem 1 and the optimality Theorems 2–3 are not formalized.

Two hat symbols elsewhere in the paper are distinct objects from those used here: $\hat{\mathrm w}$ of Lemma 3 and the bold $\hat{\mathbf w}$ of Proposition 6. Neither appears in this mission. Proofs of the milestones, and proofs of the goal that use them, are welcome.

Selected references

• P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845
• P. Sun, F. Tian, Optimal Contract to Induce Continued Effort, Management Science 64(9), 4193–4217, 2018. https://doi.org/10.1287/mnsc.2017.2795