Optimization

Motivation

Social media influencers earn money by endorsing products to their followers. An influencer who endorses only products that fit her organic content keeps her audience; one who accepts every sponsorship offer earns more per follower today but loses part of her audience and grows more slowly. Practitioners describe this as the choice between growing and monetizing, and the marketing literature documents both sides of it: followers unsubscribe after poorly fitting sponsored posts (Cheng and Zhang 2022), and small influencers have deeper engagement than large ones (Bentley et al., J. Global Marketing 34(3), 2021, cited in the paper).

Nistor, Selove and Villas-Boas (Management Science, Articles in Advance 2024) turn this trade-off into a deterministic continuous-time control problem. Awareness of the influencer spreads by word of mouth as in the Bass (1969) diffusion model, and the influencer's authenticity is the control. The paper's first main result, Proposition 1, characterizes the optimal policy completely: depending on two explicit conditions, the influencer is always authentic, always inauthentic, or authentic until her awareness reaches a threshold and inauthentic forever after. This mission formalizes Proposition 1 and the lemmas of §3.3 that lead to it.

Setting

Time is $t\in[0,\infty)$ and the mass of potential followers is one. The influencer's awareness $A_t\in[0,1]$ is the fraction of potential followers who know her, starting from $0<A_0<1$. At each time she is authentic or inauthentic. Following Table 1 of the paper, with parameters $0<\gamma<1$ and $\varphi>1$ (the reduced-form parameters of §3.1, which aggregate the offer arrival rate, the share of good-fit offers and the followers' tolerance of bad-fit posts):

• an authentic influencer has $F_t=A_t$ followers and instantaneous profit $\pi_t=A_t$;
• an inauthentic influencer has $F_t=\gamma A_t$ followers and instantaneous profit $\pi_t=\gamma\varphi A_t$.

Awareness grows according to the equation of motion (1),

$$\frac{dA_t}{dt}=\beta F_t(1-A_t),\qquad\beta>0,$$

so it grows at rate $\beta A_t(1-A_t)$ when she is authentic and $\gamma\beta A_t(1-A_t)$ when she is inauthentic. With discount rate $r>0$ the influencer maximizes the discounted profit (2),

$$V_t=\int_t^\infty e^{-r(u-t)}\pi_u\,du ,$$

and $V(A)$ is the value of starting at awareness $A$ and following the optimal policy.

Two closed-form objects enter the main result. The value of always being inauthentic from awareness $A$ is (Lemma 3)

$$\underline V(A)=\int_0^\infty \frac{e^{-rs}\gamma\varphi}{1+\frac{1-A}{A}e^{-\gamma\beta s}}\,ds ,$$

and its derivative is (3)

$$m(A)=\frac{d\underline V(A)}{dA}=\int_0^\infty \frac{e^{-(\gamma\beta+r)s}\gamma\varphi}{\big[A+(1-A)e^{-\gamma\beta s}\big]^2}\,ds .$$

Condition 1 (with footnote 4) holds if $\gamma\beta\ge r$ or $\big[\frac{\beta-\gamma\beta}{r-\gamma\beta}\big]\gamma\varphi>\gamma\varphi-1$.

Formalization targets

Goal: Proposition 1

For $0<\gamma<1$, $\varphi>1$, $\beta>0$, $r>0$:

1. if $\gamma\varphi\le1$, always being authentic is optimal from every $A_0\in(0,1)$;
2. if $\gamma\varphi>1$ and Condition 1 fails, always being inauthentic is optimal from every $A_0\in(0,1)$;
3. if $\gamma\varphi>1$ and Condition 1 holds, there is $A^*\in(0,1)$ with

$$m(A^*)=\frac{\gamma\varphi-1}{(1-\gamma)\beta(1-A^*)},$$

and for all sufficiently small $A_0$ the policy "authentic while $A_t<A^*$, inauthentic once $A_t\ge A^*$" is optimal.

Milestones

In the paper's order: Lemma 1 (corrected) bounds the growth of $V$ above awareness $\tfrac12$; Lemma 2 (corrected) shows that permanent inauthenticity is optimal at large awareness; Lemma 3 gives $\underline V$ in closed form; (3) identifies $m$ as its derivative; (4) computes the limit of $m$ at zero awareness,

$$\lim_{A\to0^+}m(A)=\frac{\gamma\varphi}{r-\gamma\beta}\ \ (\gamma\beta<r),\qquad m(A)\to+\infty\ \ (\gamma\beta\ge r),$$

which is where Condition 1 comes from.

Significance

Proposition 1 is the benchmark of the paper: each of the six model extensions of §4 (celebrities, follower turnover, partial authenticity, viral content, two segments, commitment) is read against it. Its third clause explains an observed pattern in influencer marketing, that small influencers post fitting content and large ones accept most sponsorships, as an optimal policy rather than a change in preferences, and Condition 1 makes explicit when growth potential outweighs current profits; the paper notes it always holds when $\beta>r$. The numerical example of §3.5 (Table 2) places the switch at about 73% awareness.

The proofs are in an online appendix and have not been machine-checked. Formalizing them requires an optimality argument against every measurable switching pattern, not only threshold policies. The mission also records two corrections: Lemma 1 and Lemma 2 are false as printed when $\gamma\varphi>1$ (explicit counterexamples are in the milestone statements), and they are stated here with the constant $\gamma\varphi/r$ that the paper's own argument gives.

Difficulty

The natural argument compares, at each instant, the extra profit from inauthenticity, $(\gamma\varphi-1)A_t$, with the value of the extra growth from authenticity, $(1-\gamma)\beta A_t(1-A_t)V'(A_t)$. This requires knowing the value function $V$, its differentiability, and the Bellman equation it satisfies, none of which is given; replacing $V$ by $\underline V$ is only justified along the part of the trajectory after the switch. The comparison must also hold against every measurable switching pattern, under which awareness solves (1) only almost everywhere. Clause 3 additionally needs the threshold equation to have a single crossing and the optimal trajectory to cross it exactly once. Optimality of a constant policy cannot be read off from instantaneous profits alone when $\gamma\varphi>1$: the instantaneously better choice (inauthenticity) can be the wrong one for a small influencer.

Formalization scope

• Policies are measurable sets $S\subseteq\mathbb R$ of times at which the influencer is inauthentic; constant policies are $\emptyset$ and $\mathbb R$.
• Admissible paths are continuous on $[0,\infty)$, start at $A_0$, take values in $[0,1]$, and solve (1) in integral (Carathéodory) form, because a measurable control makes $dA/dt$ exist only almost everywhere. The $[0,1]$ clause is implied by the equation and makes every profit stream bounded.
• Discounted profit is (2) at $t=0$, an integral over $(0,\infty)$; the paper's shift $s=u-t$ is notation. The value function $V$ of Lemma 1 is the real supremum over admissible pairs, nonempty and bounded above by $\gamma\varphi/r$ at every $A_0\in[0,1]$.
• Optimality is against every admissible pair from the same $A_0$, and every goal clause produces the optimal pair existentially. The threshold policy is the set $\{t\ge0: A_t\ge A^*\}$ of the same path it drives; a free switching time would not express a feedback rule.
• Standing assumptions. $0<\gamma<1$, $\varphi>1$, $\beta>0$, $0<A_0<1$ (§3.1–3.2); $r>0$ is the reading of "discount rate"; $\gamma\varphi>1$ is assumed in every milestone ("for the remainder of the paper", p. 5) but not in the goal, whose first clause is $\gamma\varphi\le1$. Condition 1 is the disjunction of footnote 4. Lemma 1 and Lemma 2 carry the corrected constant $\gamma\varphi/r$.

A trivializing formalization is ruled out: optimality is never assumed, the competitor class contains the constant policies' logistic paths, the threshold $A^*$ must solve the equation of (3) inside $(0,1)$, and measurability of policies keeps every profit integral meaningful. The microfoundations of §3.1 ($\mu$, $\theta$, $\omega$, $\hat U$, $c$) do not enter any statement.

The development needs Carathéodory solutions of a scalar ODE with a measurable switching coefficient, comparison and uniqueness for such solutions, differentiation under an improper integral, and a verification argument for a one-dimensional deterministic control problem with bang-bang control. The last two are reusable for other continuous-time marketing and diffusion models. Proofs of any milestone are welcome, as are proofs of the logistic closed form underlying Lemma 3.

Selected references

• C. Nistor, M. Selove, J. M. Villas-Boas, Influencer Authenticity: To Grow or to Monetize, Management Science, Articles in Advance, 2024. https://doi.org/10.1287/mnsc.2023.03479
• F. M. Bass, A new product growth for model consumer durables, Management Science 15(5):215–227, 1969. https://doi.org/10.1287/mnsc.15.5.215
• M. Cheng, S. Zhang, Reputation burning: Analyzing the impact of brand sponsorship on social influencers, preprint, 2022. https://doi.org/10.2139/ssrn.4071188

Motivation

A portfolio manager who observes today's value $x_0$ of a covariate (a market signal, a macroeconomic indicator) wants to choose a portfolio that performs well conditionally on that observation: the relevant risk is $\mathbb E[\ell(Y,\alpha,\beta)\mid X=x_0]$ of the asset return $Y$, not its unconditional mean. With finitely many historical pairs $(\hat x_i,\hat y_i)$, the empirical conditional distribution at a new $x_0$ is usually empty or rests on one or two samples, so estimating it directly is unreliable. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451v3, Operations Research 2025) hedge it with distributionally robust optimization: they take the worst case of the conditional expectation over all joint laws of $(X,Y)$ within an optimal-transport ball around the empirical measure that still put a prescribed amount of mass on the conditioning event.

The objective is a ratio of two linear functionals of the law, so the standard strong-duality theorems for Wasserstein distributionally robust optimization (Mohajerin Esfahani and Kuhn, 2018; Blanchet and Murthy, 2019; Gao and Kleywegt, 2023) do not apply directly. This mission formalizes the paper's answer in the singular case where the conditioning event is the single point $\{x_0\}$ and the event must keep mass at least $\varepsilon>0$.

Setting

Let $\mathcal X$ (covariates) and $\mathcal Y$ (returns) be spaces with ground costs $\mathbb D_{\mathcal X}$, $\mathbb D_{\mathcal Y}$, combined into the separable cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$. The data are $N$ samples $(\hat x_i,\hat y_i)$, $i\in[N]$, with empirical measure $\hat{\mathbb P}=N^{-1}\sum_i\delta_{(\hat x_i,\hat y_i)}$.

• The optimal transport cost between laws $\mathbb Q_1,\mathbb Q_2$ is $\mathbb W(\mathbb Q_1,\mathbb Q_2)=\inf\{\mathbb E_\pi[\mathbb D(\xi_1,\xi_2)]:\pi\in\Pi(\mathbb Q_1,\mathbb Q_2)\}$, the infimum over couplings.
• The ambiguity set is $\mathbb B_\rho=\{\mathbb Q:\ \mathbb W(\mathbb Q,\hat{\mathbb P})\le\rho\}$ for a radius $\rho\ge0$.
• The fiber of radius $\gamma$ is $\mathcal N_\gamma(x_0)\times\mathcal Y$ with $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$; here $\gamma=0$, so the fiber is $\{x_0\}\times\mathcal Y$.
• The minimum radius $\rho_{\min}(x_0,\gamma,\varepsilon)=\inf\{\mathbb W(\mathbb Q,\hat{\mathbb P}):\mathbb Q(X\in\mathcal N_\gamma(x_0))\ge\varepsilon\}$ is the smallest radius at which some law in the ball meets the mass requirement.
• Assumption 2.4 of the paper: the costs are symmetric, non-negative and continuous, $\mathbb D$ vanishes exactly on the diagonal, each $\hat x_i$ has a unique projection onto $\mathcal N_\gamma(x_0)$ with cost $\kappa_i$, and boundary points of $\mathcal N_\gamma(x_0)$ can be left at arbitrarily small cost.

For a loss $\ell(y)=\ell(y,\alpha,\beta)$ at a fixed decision, the object of study is the worst-case conditional expected loss

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X=x_0)\ge\varepsilon}\ \mathbb E_{\mathbb Q}[\ell(Y)\mid X=x_0],\qquad \mathbb E_{\mathbb Q}[\ell(Y)\mid X=x_0]=\frac{\mathbb E_{\mathbb Q}[\ell(Y)\mathbb 1_{\{x_0\}}(X)]}{\mathbb Q(X=x_0)} .$$

Formalization targets

Goal: Theorem 3.2 (p. 15)

For $\varepsilon\in(0,1]$ and $\rho>\rho_{\min}(x_0,0,\varepsilon)$,

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X=x_0)\ge\varepsilon}\mathbb E_{\mathbb Q}[\ell(Y)\mid X=x_0] =\inf_{\lambda_1\ge0,\ \lambda_2\in\mathbb R}\Big\{\rho\lambda_1+\varepsilon\lambda_2+\frac1N\sum_{i\in[N]}\Big(\sup_{y\in\mathcal Y}\big\{\varepsilon^{-1}\ell(y)-[\mathbb D_{\mathcal X}(x_0,\hat x_i)+\mathbb D_{\mathcal Y}(y,\hat y_i)]\lambda_1-\lambda_2\big\}\Big)^+\Big\}.$$

The loss is arbitrary (measurable, real-valued), and both sides may be $+\infty$.

Milestones

1. Representation (24) (p. 47): $\mathbb Q\in\mathbb B_\rho$ iff $\mathbb Q=N^{-1}\sum_i\pi_i$ for probability measures $\pi_i$ with $N^{-1}\sum_i\mathbb E_{\pi_i}[\mathbb D(\cdot,(\hat x_i,\hat y_i))]\le\rho$.
2. Proposition 2.5 (p. 11): $\rho_{\min}$ is the value of the fractional knapsack program $\min\{N^{-1}\sum_i\kappa_i\upsilon_i:\upsilon\in[0,1]^N,\sum_i\upsilon_i\ge N\varepsilon\}$, and the problem is feasible iff $\rho\ge\rho_{\min}$.
3. Lemma A.4 (p. 36): in a linear-fractional program over $[0,1]^N$, the constraint $\sum_i\upsilon_i\ge\varepsilon N$ may be replaced by $\sum_i\upsilon_i=\varepsilon N$.
4. Proposition A.5 (p. 36): the worst case equals a supremum over weights $\upsilon$ with $\sum_i\upsilon_i=N\varepsilon$ and over laws $\mu_0^i$ on $\mathcal Y$ of the linear objective $(N\varepsilon)^{-1}\sum_i\upsilon_i\mathbb E_{\mu_0^i}[\ell]$ under one transport budget.
5. Inner duality (p. 41): for fixed strictly feasible weights, the inner supremum over $(\mu_0^i)$ equals its moment-problem dual over $\lambda_1\ge0$ and $\theta\in\mathbb R^N$.

Significance

Theorem 3.2 reduces an infinite-dimensional, fractional worst-case problem to a two-multiplier convex program whose only infinite-dimensional pieces are $N$ suprema over $\mathcal Y$. For piecewise-linear losses and norm costs the paper turns this into the conic programs of Propositions 3.3–3.4, which are what make the robust conditional portfolio model solvable in practice. It also compares the formulation with the trimming approach of Esteban-Pérez and Morales (Mathematical Programming, 2022), whose adversary may only pick laws with fiber mass exactly $\varepsilon$; Proposition A.5 shows that, at $\gamma=0$, the more powerful adversary allowed $\mathbb Q(X=x_0)\ge\varepsilon$ attains the same value.

The result is proved in the paper; nothing here is open mathematics. None of it is formalized. A complete development would add to the platform a first conditional (fractional) distributionally robust duality, a decomposition of optimal-transport balls around empirical measures (milestone 1, reusable by every finite-sample Wasserstein result), and a moment-problem duality with one budget constraint (milestone 5).

Difficulty

The ratio objective is the obstacle: neither the numerator nor the denominator alone determines the worst case, and a law that is optimal for the numerator may violate the mass constraint. The step "fix the fiber mass at $\varepsilon$" (Proposition A.5) is where the obvious argument fails: an optimal law may put more than $\varepsilon$ on $\{x_0\}$, and reducing that mass requires moving sample points off $x_0$ at vanishing transport cost, which needs points of $\mathcal X$ arbitrarily close to $x_0$. Milestone 1 needs the existence of optimal couplings, which Mathlib lacks. Milestone 5 is an infinite-dimensional Lagrangian duality whose Slater point degenerates on the boundary of the weight set, so the final interchange of supremum and infimum must avoid that boundary.

Formalization scope

$\mathcal X$ and $\mathcal Y$ are Polish spaces with their Borel σ-algebras; samples are indexed by Fin N with $N\ge1$, repeats allowed. The optimal transport cost is the published RWPI.SqrtLasso.transportCost (an infimum of lower integrals of the $[0,\infty]$-valued cost; attainment is not built in), and every expectation of the loss is the published ModelRiskOT.Duality.extIntegral, $\int\ell^+-\int\ell^-$ in $[-\infty,\infty]$. Worst-case values and duals are EReal suprema and infima. The loss is a measurable L : Y → ℝ standing for $\ell(\cdot,\alpha,\beta)$ at an arbitrary decision.

Hypotheses beyond the page, all disclosed in the statements:

• Assumption 2.4 is a hypothesis of every statement, as the paper makes it "throughout".
• NotIsolated: for every $r>0$ there is $x\ne x_0$ with $\mathbb D_{\mathcal X}(x,x_0)\le r$. This is Assumption 2.4(iii) at $\gamma=0$ read with the ambient boundary of $\{x_0\}$, as the paper's remark on p. 11 does; with the topological frontier in $\mathcal X$, (iii) is vacuous at an isolated $x_0$, and Theorem 3.2 is then false.
• Measurability of the loss, used because the dual side integrates $\ell$ against arbitrary laws on $\mathcal Y$.
• Milestone 5 requires the strict budget inequality $\sum_i\upsilon_i\mathbb D_{\mathcal X}(x_0,\hat x_i)<N\rho$; the page's Slater argument covers only that case.

Trivializing formalizations are ruled out: conditional expectations are only taken at laws with fiber mass at least $\varepsilon>0$ (never at mass $0$, where a real division would return $0$); expectations are never Bochner integrals, which would be $0$ for a non-integrable loss; the radius enters through ENNReal.ofReal ρ only where $\rho\ge0$ or $\rho>\rho_{\min}$ forces $\rho>0$; and every supremum ranges over exactly the paper's feasible set.

Needed infrastructure: existence of optimal couplings on Polish spaces (Villani, Theorem 4.1), a Lagrangian duality for moment problems, and Mathlib's Sion minimax theorem for the interchange. Contributions to any of these, and proofs of the milestones in any order, are welcome.

Selected references

• V. A. Nguyen, F. Zhang, S. Wang, J. Blanchet, E. Delage, Y. Ye, Robustifying conditional portfolio decisions via optimal transport, Operations Research, 2025; arXiv:2103.16451v3, 2024. https://arxiv.org/abs/2103.16451
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44, 2019. https://doi.org/10.1287/moor.2018.0936
• R. Gao, A. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, Mathematics of Operations Research 48, 2023. https://doi.org/10.1287/moor.2022.1275
• A. Esteban-Pérez, J. M. Morales, Distributionally robust stochastic programs with side information based on trimmings, Mathematical Programming, 2022.
• A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer, 2001, pp. 135–165.
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8, 1958, pp. 171–176.
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

Motivation

Large online retailers such as Amazon run two businesses on one storefront. They sell products themselves, and they host a marketplace on which third-party sellers sell, paying the platform a percentage of their revenue. A retailer that also runs the marketplace can decide which products to sell itself, and it controls which offer most consumers see. Competition authorities have asked whether this dual role lets the platform appropriate third-party sellers' business, and empirical work (Zhu and Liu, 2018) finds that Amazon enters only a small, high-performing subset of marketplace products.

Hervas-Drane and Shelegia (Retailer-Led Marketplaces, Management Science, 2025) give a model in which these choices can be computed. Its main result, Proposition 2, says which products the platform sells itself when its assortment is limited. This mission formalizes that proposition together with the pricing and entry results it rests on.

Setting

There is a unit mass of products. Each product is an independent market indexed by its consumers' valuation $v$. Valuations are distributed according to a probability measure $\mu$ on $[c,\infty)$ with CDF $G(v)=\mu((-\infty,v])$. Every unit costs $c>0$ to supply. Each market has a unit mass of unit-demand consumers, who buy at a price $p$ only if $p\le v$.

The monopolist retailer $M$ sets an ad valorem fee $f\in[0,1]$ on the third-party seller's revenue. He can steer a share $\lambda$ of consumers (the inattentive ones) to the seller of his choice; the remaining $1-\lambda$ buy from the cheapest offer, with ties going to $M$. He has capacity $k\in[0,1]$: he can supply at most a fraction $k$ of all products.

The game has three stages. In Stage 1 $M$ sets $f$. In Stage 2 each product's third-party seller $T$ decides whether to enter, and then $M$ chooses which products to enter. In Stage 3, in each market both present firms price sequentially: $T$ quotes first, then $M$ quotes and steers. The solution concept is subgame perfect equilibrium.

Proposition 1 solves Stage 3. A product supplied by $M$ alone (SBM) earns him $\pi_M^{SBM}=v-c$. A product supplied by $T$ alone (SBT) earns her $(1-f)v-c$ and earns him the fee $\pi_M^{SBT}=fv$. When both supply it (SBMT), $T$ charges

$$\bar p_T=\frac{\lambda v+c(1-\lambda)}{1-f(1-\lambda)},$$

and $M$ earns $\pi_M^{SBMT}=\lambda(v-c)+(1-\lambda)f\bar p_T$. Lemma 1 says $T$ enters exactly the products $v\ge v_T=c/(1-f)$, the marketplace products. An allocation of $M$ is any measurable set $A$ of products with $\mu(A)\le k$. His total profit is the SBM profit on $A$ below $v_T$, plus the SBMT profit on $A$ above $v_T$, plus the fee on marketplace products outside $A$.

Formalization targets

Goal: Proposition 2

Assume $\lambda\ge\tfrac12$ (Assumption 1) and $f<1$. Let $\Delta\pi(v)=\pi_M^{SBMT}(v)-\pi_M^{SBT}(v)$ and

$$v^*=\frac{c\lambda}{(1-f)^2(\lambda-f(1-\lambda))},\qquad \underline k=1-G(v^*).$$

Then:

• Mode I. If $k\le\underline k$, the optimal allocation is unique up to $\mu$-null sets and equals $[v_K,\infty)$ with $1-G(v_K)=k$ (empty if $k=0$).
• Mode II. If $k>\underline k$, it is $[v_L,v_T)\cup[v_H,\infty)$, where

$$\pi_M^{SBM}(v_L)=\Delta\pi(v_H),\qquad (1-G(v_H))+(G(v_T)-G(v_L))=k.$$

Milestones

1. Proposition 1, its three supply configurations: the SBM monopoly price, the SBT equilibrium, and the SBMT subgame perfect equilibrium, which is unique for $0<\lambda<1$ and $v(1-f)>c$.
2. Lemma 1 with (1) and Property 1: the entry threshold $v_T$.
3. The closed form of $\Delta\pi$, its positivity above $v_T$, and its monotonicity in $v$ and in $f$.
4. (A.2): $\Delta\pi(v^*)=\pi_M^{SBM}(v_T)$, and $v^*\ge v_T$.
5. The $(v_L,v_H)$ system has a unique solution when $k>\underline k$.

Significance

Proposition 2 is the step that the rest of the paper builds on. Display (4) writes the monopolist's profit as a function of the fee by plugging in the thresholds $v_L$, $v_T$, $v_H$, $v_K$ of Proposition 2. The optimal fee (Lemma 2, Proposition 3) and the policy comparisons of §6 (a pure-retailer response, fee regulation, steering bans) are all statements about that function. The two modes are also the paper's empirical prediction. A platform with little capacity, effective steering and a high fee competes only in the top marketplace products. With more capacity it also takes products no third party sells.

The paper proves Proposition 2 in Appendix A. The proof is an informal capacity-allocation argument. No machine-checked version exists. A formal proof has to turn the argument about entering the products of highest marginal profitability first into a statement about all measurable allocations of mass at most $k$. It must also prove uniqueness up to null sets, and handle the corners $k=0$, $k=1$ and $f=0$ that the prose passes over.

Difficulty

The obvious argument ranks products by the marginal profitability of entry and fills capacity from the top. Two facts make this harder than it looks. First, the ranking is not monotone in $v$. Below $v_T$ the gain is $v-c$; above $v_T$ it is $\Delta\pi(v)$, which starts again from $0$ at $v_T$. So the optimal set is an upper level set of a piecewise function, and in Mode II it has two components. Second, the claim is about every measurable set of mass at most $k$, not about thresholds. Optimality needs an exchange argument against arbitrary sets, and uniqueness needs the level sets of the gain to be $\mu$-null. Locating the thresholds also needs continuity and strict monotonicity of $G$, which come from the density and the full-support hypothesis.

Proposition 1 has its own subtlety. At $p_T=\bar p_T$ the monopolist is indifferent between matching $T$'s price and charging $v$. $T$'s best price exists only if $M$'s strategy breaks this tie in $T$'s favour, so the equilibrium has to be stated for strategies defined at every price of $T$.

Formalization scope

Products form a probability measure μ : Measure ℝ. The standing hypotheses are:

• $\mu((-\infty,c))=0$, $\mu\ll$ Lebesgue (the density $g$), and Integrable (fun v => v) μ, which the paper never states but which is needed for profits to be finite;
• $\mu$ charges every nonempty open interval of $[c,\infty)$, the reading of $G^{-1}$ in (3);
• $c>0$, $f\in[0,1)$, $\lambda\in[\tfrac12,1]$, $k\in[0,1]$.

The foreclosed corner $f=1$ ($v_T=\infty$) is not covered. Marketplace products are encoded as $\{v: c\le v(1-f)\}$. Optimal allocations quantify over all measurable sets of mass at most $k$, and uniqueness is up to $\mu$-null sets. Restricting allocations to intervals or to unions of two intervals would assume the conclusion, and the formalization does not do it.

In Proposition 1, $M$'s strategy is a function of $T$'s price that is a best response at every price, and $T$'s price is optimal against it. Uniqueness of the SBMT outcome is stated only for $0<\lambda<1$ and $v(1-f)>c$, where it holds. Lemma 1's duopoly clause likewise needs $0<\lambda<1$.

Two definition files carry the model:

• Model: $G$, the marketplace set, the Proposition 1 payoffs, $\Delta\pi$, $v^*$, $\underline k$, allocations and profit;
• PricingGame: the three pricing games and their equilibria.

The bathtub-type lemma behind Proposition 2 is reusable beyond this mission: among measurable sets of mass at most $k$, an upper level set of a weight maximizes its integral. Contributions of that lemma, of the milestones, and of alternative proofs are welcome.

Selected references

• A. Hervas-Drane, S. Shelegia, Retailer-Led Marketplaces, Management Science, Articles in Advance, 2025. https://doi.org/10.1287/mnsc.2023.00315
• F. Zhu, Q. Liu, Competing with Complementors: An Empirical Look at Amazon.com, Strategic Management Journal 39:2618–2642, 2018. https://doi.org/10.1002/smj.2932
• A. Hervas-Drane, S. Shelegia, Price Competition with a Stake in Your Rival, International Journal of Industrial Organization 84:102862, 2022 (the simultaneous-pricing variant of the pricing game). https://doi.org/10.1016/j.ijindorg.2022.102862

Motivation

Consumers judge a price against a reference price, an internal benchmark formed from the prices they have seen before. A price above the reference is perceived as a loss and depresses demand; a price below it is perceived as a gain and stimulates it. Because today's prices shape tomorrow's reference prices, a seller facing reference effects solves a dynamic problem even when demand is otherwise stationary. The single-product theory is classical: Popescu and Wu (2007) showed, for a broad class of demand models, that loss-averse consumers make optimal and myopic price paths converge monotonically, and Hu, Chen and Hu (2016) studied the cyclic behaviour that gain-seeking consumers can induce under linear demand.

Retailers sell many substitutable products, and the standard model of substitution is the multinomial logit (MNL). Guo, Jiang and Shen (2025) combine the two: each product has its own reference price and its own asymmetric sensitivities to gains and losses, and consumers choose among the products by MNL. This mission formalizes the paper's first set of results, on the myopic pricing policy, which maximises the current period's revenue at the current reference prices and ignores the effect on the future. Myopic pricing is both a widely used heuristic and the benchmark against which the optimal policy is measured later in the paper.

Setting

There are $n$ products $N=\{1,\dots,n\}$. Product $i$ has an intrinsic utility $a_i\in\mathbb R$, a price sensitivity $b_i>0$, and reference sensitivities $c_i^+\ge0$ (to gains) and $c_i^-\ge0$ (to losses). At price vector $p$ and reference price vector $r$ the deterministic utility of product $i$ is

$$u_i(p,r)=a_i-b_ip_i+c_i^+(r_i-p_i)_+-c_i^-(p_i-r_i)_+ ,$$

the market share of product $i$ is $q_i(p,r)=e^{u_i}/(1+\sum_k e^{u_k})$, and the single-period revenue is $\Pi(p,r)=\sum_i p_i\,q_i(p,r)$. Product $i$ is loss-averse if $c_i^+<c_i^-$, loss-neutral if $c_i^+=c_i^-$, and gain-seeking if $c_i^+>c_i^-$; the three sets are $N_l,N_n,N_g$.

Prices and reference prices lie in the box $\mathcal P^n=[0,p_H]^n$ with ceiling $p_H>0$. A myopic policy $p^m$ assigns to each $r\in\mathcal P^n$ a maximiser of $\Pi(\cdot,r)$ over $\mathcal P^n$; the maximum value is the optimal single-period revenue $\Pi^m(r)$. Reference prices follow exponential smoothing with memory $\alpha\in[0,1]$:

$$r^{t+1}=\alpha r^t+(1-\alpha)\,p^m(r^t),$$

and $\{p^m(r^t)\}_{t\ge0}$ is the myopic price path. A policy has a steady state if $p^m(r)=r$ for some $r\in\mathcal P^n$.

The paper assumes throughout that $p_H\ge\hat p_H$, where $\hat p_H$ is the unique root of the scalar equation (9), $p=\chi+\sum_i \frac{1}{b_i+c_i^+}e^{a_i-b_ip+(b_i+c_i^+)\chi-1}$ with $\chi=\max_i 1/(b_i+\min\{c_i^+,c_i^-\})$. This ceiling assumption makes the ceiling non-binding for the myopic problem.

Formalization targets

Goal: Theorem 3, long-run behaviour of the myopic policy

For every myopic policy $p^m$ and every $r^0\in\mathcal P^n$:

$$N_g=\emptyset\ \Longrightarrow\ p^m(r^t)\to L\in\mathcal P^n,\ \text{and } p^m(L)=L \text{ when } \alpha<1;$$ $$N_g\neq\emptyset\ \Longrightarrow\ p^m(r)\neq r\ \ \forall r\in\mathcal P^n,\ \text{and the path does not converge when } \alpha<1 .$$

Milestones

1. Proposition 1.2 (p. 10): (9) has a unique root $\hat p_H$, and for $p_H\ge\hat p_H$ the maximisers of $\Pi(\cdot,r)$ over $\mathcal P^n$ are its maximisers over $\mathbb R^n$.
2. Theorem 2 (p. 13): every myopic price is $\Pi^m(r)$ plus an explicit constant that depends on the product's type and on where $r_i$ lies relative to thresholds such as $\Pi^m(r)+Z_i$, $Z_i=\frac{\log(b_i+c_i^+)-\log(b_i+c_i^-)}{c_i^+-c_i^-}$.
3. Theorem 1 (p. 12): $\Pi^m(r)$ is the unique root of the scalar equation (13).
4. Corollary 1 (p. 12): the right-hand side of (13) is non-increasing in $\Pi$.
5. §3.1, p. 13: $\Pi^m(r)$ is non-decreasing in $r$.
6. Corollary 2 (p. 16): if every product is loss-neutral, the myopic policy has a unique steady state $p_i^{m\star}=\Pi^{m\star}+1/(b_i+c_i)$, with $\Pi^{m\star}$ the unique root of (18), and the price paths of all products move synchronously.

Significance

Theorem 3 separates two regimes by consumer type alone. With loss-averse and loss-neutral consumers a seller who reprices myopically settles at a stable price vector; with even one gain-seeking product no price vector is self-reproducing, and myopic prices keep oscillating. Theorems 1 and 2 are the structural results behind this: they reduce a non-concave, non-smooth $n$-dimensional optimisation to one scalar equation with a monotone right-hand side, which is also how the myopic policy is computed in practice. The same structure is used later in the paper to bound the gap between myopic and optimal revenue.

All results are proved in the paper; the proofs are in its online supplement (Appendices B.1–B.5), which is not part of the source file used here. None of the results is formalized. The work in this mission is the first machine-checked treatment of MNL pricing with reference effects: global optimality of a candidate maximiser for a non-concave revenue, the analysis of a scalar root equation with piecewise definitions, and the dynamics of a map that is continuous without gain-seeking products and discontinuous with them.

Difficulty

The obvious route to Theorem 2, setting the gradient of $\Pi(\cdot,r)$ to zero, fails twice. The revenue has kinks at $p_i=r_i$, so a maximiser may sit at a kink where no gradient exists; this is the middle branch $p_i^m=r_i$ for loss-averse products. And the revenue is not concave in prices: for a gain-seeking product the first-order conditions have several solutions, and a global maximiser must be singled out among them. The usual reformulation of MNL pricing in market-share variables, which restores concavity without reference effects, does not survive the kinks.

For Theorem 3 the difficulty is dynamic. Without gain-seeking products the myopic map is continuous, but the flat middle branch of (14) makes it non-contracting, so the standard contraction arguments do not apply, and the limit depends on the starting point. With a gain-seeking product the map jumps at the threshold $\Pi^m+Z_i$, so continuity-based arguments about the limit of the path are unavailable.

Formalization scope

Products are indexed by Fin n (0-based); vectors are Fin n → ℝ with the product topology and the coordinatewise order. The standing hypotheses $b_i>0$, $c_i^\pm\ge0$, $\alpha\in[0,1]$, $p_H>0$ and the ceiling assumption (as "some root of (9) is at most $p_H$") appear as hypotheses of every theorem that needs them; Corollary 1 needs only $b>0$, $c^\pm\ge0$. The market shares (3) are defined directly, without the Gumbel derivation. $\chi$ is an indexed supremum over Fin n (zero when $n=0$). The three sums of (13) are written as one sum whose term is chosen by product type.

Maximisers need not be unique, so a myopic policy is any selection of maximisers, and every statement holds for all selections; $\Pi^m(r)$ is the revenue of an arbitrary maximiser. "The unique solution" is split into "is a solution" and "every solution equals it". The following deviations are disclosed in the items: at the threshold $r_i=\Pi^m+Z_i$ of (16) both prices are maximisers, so only "one of the two" is claimed there; the fixed-point property of the limit in Theorem 3, and every limit claim of Corollary 2, require $\alpha<1$, since at $\alpha=1$ the price path is the constant $p^m(r^0)$; the non-convergence clause in Theorem 3.2 is an addition to the literal "no steady state". "Monotone decreasing" (Corollary 1) and "monotone increasing" (Corollary 2, §3.1) are read non-strictly.

A trivializing formalization is ruled out: Theorem 3.2 quantifies over every reference price in the box and every myopic selection, Theorem 3.1 asserts convergence from every initial reference price rather than the existence of some fixed point, and Theorems 1–3 keep the ceiling assumption, without which the maximiser can sit on the boundary and (14)–(16) fail.

A complete development needs: continuity and compactness facts for the MNL revenue on a box; optimality conditions for the kinked, non-concave revenue; one-variable analysis of the piecewise-exponential right-hand side of (13); and convergence results for monotone or continuous recursions in $\mathbb R^n$. The MNL and reference-price infrastructure is reusable by the five other missions of this series. Contributions to any milestone, and alternative proofs, are welcome.

Selected references

• M. A. Guo, H. Jiang, Z.-J. M. Shen, Multi-Product Dynamic Pricing with Reference Effects Under Logit Demand, Manufacturing & Service Operations Management, 2025; source used: SSRN 4189049, version of 2024-05-25. https://ssrn.com/abstract=4189049, https://doi.org/10.1287/msom.2024.0801
• I. Popescu, Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3), 2007. https://doi.org/10.1287/opre.1070.0393
• Z. Hu, X. Chen, P. Hu, Dynamic Pricing with Gain-Seeking Reference Price Effects, Operations Research 64(1), 2016. https://doi.org/10.1287/opre.2015.1446
• D. McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in Frontiers in Econometrics, Academic Press, 1974.

Why optimize a quantile of a black box

Risk-sensitive decisions are often judged by a quantile of an outcome rather than by its mean: the 95th percentile of waiting time in a service system, the value-at-risk of a portfolio, the tail of a project's completion time. When the outcome is produced by a stochastic simulation or another black box, its distribution is unknown and only samples are available, so neither the quantile nor its gradient can be evaluated. Hu, Song and Fu (arXiv:2308.07607, Operations Research, 2025) propose a local search method for this problem that uses three samples per iteration in any dimension, and they prove that its iterates converge almost surely and at an explicit rate.

Earlier approaches estimate the quantile gradient by finite differences of order statistics, which requires sample sizes growing to infinity (Kibzun and Matveev 2012), or run a multi-timescale stochastic approximation driven by direct gradient estimators such as perturbation analysis or likelihood ratios (Hu, Peng, Zhang and Zhang 2022), which a black box does not provide. The present paper estimates the gradient from indicator differences along a simultaneous perturbation in the spirit of Spall's SPSA (1992), using a coordinate-wise variant (SDQO) as a baseline whose cost grows with the dimension $d$, and, by its own account (p. 5), gives the first convergence rate for a three-timescale stochastic approximation scheme.

Setting

For every input $\theta\in\mathbb R^d$ a black box returns a random output $Y(\theta)$ with c.d.f. $F(y;\theta)$ and density $f(y;\theta)=\partial F(y;\theta)/\partial y$. For a fixed level $\varphi\in(0,1)$ the quantile function $q(\theta)$ solves $F(q(\theta);\theta)=\varphi$, and the problem is

$$\min_{\theta\in\Theta} q(\theta),$$

where the parameter set $\Theta=\{\theta: h_j(\theta)\le0,\ j=1,\dots,m\}$ is compact and convex, with each $h_j$ continuously differentiable and $\nabla h_j\ne0$ on $\{h_j=0\}$. Under smoothness, $\nabla q(\theta)=-\nabla_\theta F(y;\theta)|_{y=q(\theta)}/f(q(\theta);\theta)$.

Algorithm SPQO keeps a quantile estimate $q_k$, a gradient estimate $D_k$ and the decision $\theta_k$. With step sizes $\alpha_k,\beta_k,\gamma_k$, perturbation sizes $c_k$, the adaptive perturbation $\bar c_k=c_k/\max\{1,\|D_k\|/\sqrt d\}$ and a random direction $\Delta_k\in\{\pm1\}^d$ with independent uniform signs,

$$\begin{aligned} q_{k+1}&=q_k+\gamma_k\big(\varphi-I\{Y(\theta_k)\le q_k\}\big),\\ D_{k+1}&=D_k+\beta_k\,\frac{-I\{Y(\theta_k+\bar c_k\Delta_k)\le q_k+\bar c_kD_k^T\Delta_k\}+I\{Y(\theta_k-\bar c_k\Delta_k)\le q_k-\bar c_kD_k^T\Delta_k\}}{2\bar c_k\Delta_k},\\ \theta_{k+1}&=\Pi_\Theta(\theta_k-\alpha_kD_k), \end{aligned}$$

with division by $\Delta_k$ taken componentwise and $\Pi_\Theta$ the Euclidean projection onto $\Theta$. The timescales are separated by $\alpha_k=o(\gamma_k)$ and $\gamma_k=o(\beta_k)$.

The analysis rests on assumptions A1–A3 (local smoothness of $F$ and a lower bound on $f$ near the iterates; Rademacher directions; step-size conditions) and, for rates, B1–B3 (two-sided bounds on $f$ between $q_k$ and $q(\theta_k)$; Lipschitz continuity of $f$ and $\nabla_\theta F$ in $y$; a lower bound $\varrho>0$ on the smallest eigenvalue of the Hessian $H(\theta)=\nabla^2q(\theta)$ along the segments $[\theta_k,\theta^*]$). Section 4 uses step sizes $\alpha_k=a/k^\alpha$, $\beta_k=b/k^\beta$, $\gamma_k=r/k^\gamma$, $c_k=c/k^\tau$ with exponents in $(0,1)$.

Formalization targets

Goal: Theorem 3 (p. 19)

Under A1–A3 and B1–B3, with the Section 4 step sizes, $q$ twice continuously differentiable and $\theta^*$ the unique equilibrium of the projected gradient ODE (25), lying in the interior of $\Theta$,

$$E\big[\|\theta_k-\theta^*\|\big]=O\Big(\frac{\alpha_k}{\gamma_k}\Big)+O\big(c_k^2\big)+O\Big(\frac{\beta_k^{1/2}}{c_k}\Big).$$

The constants are left unspecified: the goal asserts the shape of the rate, which is what the paper proves.

Milestones

1. Display (4): the quantile gradient formula.
2. Lemma 1: $\sup_kE\|D_k\|^2<\infty$ and $\sup_k\|D_k\|<\infty$ almost surely.
3. Lemma 2: the conditional bias of the simultaneous-perturbation estimator is $O(c_k^2)$ almost surely and in mean.
4. Theorem 1 (strictly convex case): $\theta_k\to\theta^*$ almost surely.
5. Lemma 3: $\sum_{i=1}^k\big[\prod_{j=i+1}^k(1-a/j^p)\big](a/i^p)w(i)=O(k^{-s})$ when $w(i)=O(i^{-s})$.
6. Lemma 4: $\sqrt{E[(q_k-q(\theta_k))^2]}=O(\alpha_k/\gamma_k)+O(\gamma_k^{1/2})$.
7. Lemma 5: $\sqrt{E\|D_k-\nabla q(\theta_k)\|^2}=O(\alpha_k/\gamma_k)+O(c_k^2)+O(\beta_k^{1/2}/c_k)$.

Significance

The rate (27) makes the trade-off among the three timescales explicit: $\alpha_k/\gamma_k$ is the cost of tracking a moving quantile, $c_k^2$ the bias of the perturbation, and $\beta_k^{1/2}/c_k$ its noise. Balancing them selects the step-size exponents, and the special cases recover the $O(1/\sqrt k)$ rate of recursive quantile estimation and Spall's SPSA rate. The intermediate results (moment bounds for a gradient tracker with adaptive perturbation, an $O(c_k^2)$ bias bound for an indicator-based SPSA estimator, and the weighted-sum estimate of Lemma 3) apply to other multi-timescale stochastic approximation schemes.

The theorem is proved in the paper; no machine-checked version exists. A formalization would check a rate argument for three coupled recursions, a setting in which hypotheses are easily lost: the paper's own proofs use a bound on $\nabla_\theta F$ that A1 does not list, and one step of the proof of Theorem 3 (display (29)) treats a conditional mean as an unconditional one. The statement survives both, as recorded in the formalization notes.

Difficulty

The three recursions are coupled in both directions. The gradient tracker $D_k$ is driven by indicator differences whose perturbation is itself scaled by $D_k$, so the $O(c_k^2)$ bias holds only once $D_k$ is known to be bounded, and boundedness must be shown with the adaptive $\bar c_k$. The natural first idea, analyzing each recursion with the slower ones frozen, gives convergence but not rates: the targets $q(\theta_k)$ and $\nabla q(\theta_k)$ move, and the error of each tracker must be bounded in mean square while the tracker it depends on is still converging. The rate also needs the almost-sure convergence of Theorem 1, which is an ODE-method argument for a projected, coupled scheme.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with $d\ge1$. The black box is a family of laws $\mu_\theta$ on $\mathbb R$, defined for every $\theta\in\mathbb R^d$ because SPQO samples outside $\Theta$. A run lives on a probability space with a general filtration; initial values are deterministic with $\theta_0\in\Theta$; the sampling model fixes the conditional law of each output given the past (and $\Delta_k$), which covers independent sampling and common random numbers. Expectations are Lebesgue integrals in $[0,\infty]$, and the bias of Lemma 2 is an explicit average over the $2^d$ sign vectors. $O(\cdot)$ is the paper's one-sided notion: a constant, depending on the instance and the run but not on $k$, times the rate, for all large $k$.

The following departures from the page are disclosed in every affected statement:

• D1 the quantile step is projected onto a closed interval $I\supseteq q(\Theta)$, the truncation the paper recommends on p. 13; $I=\mathbb R$ is the printed recursion;
• D2 step sizes use $k+1$ in place of $k$;
• D3 A1 bounds the first derivatives of $F$, which the proofs use;
• D4 only conditional marginal laws of the outputs are imposed;
• D5 $\theta_0\in\Theta$;
• D6 the Section 4 standing assumption (a unique globally asymptotically stable equilibrium $\theta^*$ of the projected ODE (25) in the interior of $\Theta$) is stated in its equivalent first-order form: $\theta^*$ is interior and is the only $\theta\in\Theta$ with $-\nabla q(\theta)$ in the normal cone of $\Theta$ at $\theta$ (the equilibria of (25); $q$ is a Lyapunov function for (25), so uniqueness gives global asymptotic stability);
• D7 joint continuity of $f$ is required on $\mathbb R\times\Theta$.

B3 is stated as the quadratic-form bound $v^TH(\theta)v\ge\varrho\|v\|^2$, equivalent to the eigenvalue bound for the symmetric Hessian. Theorem 1 is formalized only in its strictly convex clause.

Several trivializing formalizations are ruled out. Without the truncation of D1 no run satisfies A1(b) or B1, so the untruncated statement would be vacuous. No statement takes a Bochner expectation or conditional expectation of a possibly non-integrable quantity. Gradients and Hessians of $q$ are read only where $q$ is $C^2$. No $O$-constant may depend on $k$.

A complete development needs stochastic approximation tools that Mathlib lacks: Robbins–Siegmund-type supermartingale convergence, the ODE method for projected recursions, and second-moment recursions for coupled trackers. These are reusable beyond this mission. Contributions are welcome for any milestone, and Lemma 3 is pure real analysis.

Selected references

• J. Hu, M. Song, M. C. Fu, Quantile Optimization via Multiple Timescale Local Search for Black-box Functions, Operations Research, 2025; arXiv:2308.07607v1, 2023. https://arxiv.org/abs/2308.07607
• J. C. Spall, Multivariate stochastic approximation using a simultaneous perturbation gradient approximation, IEEE Transactions on Automatic Control 37(3):332–341, 1992. https://doi.org/10.1109/9.119632
• M. C. Fu, L. J. Hong, J.-Q. Hu, Conditional Monte Carlo estimation of quantile sensitivities, Management Science 55(12):2019–2027, 2009. https://doi.org/10.1287/mnsc.1090.1090
• J. Hu, Y. Peng, G. Zhang, Q. Zhang, A stochastic approximation method for simulation-based quantile optimization, INFORMS Journal on Computing 34(6):2889–2907, 2022.
• A. I. Kibzun, E. Matveev, Optimization of the quantile criterion for the convex loss function by a stochastic quasi-gradient algorithm, Annals of Operations Research 200(1):183–198, 2012.

Motivation

During the COVID-19 pandemic most U.S. payers began reimbursing a telehealth consultation at the same rate as the corresponding office visit, a policy called pay parity. Many states have since made it permanent, on the stated ground that it improves patients' access to care. In acute care (primary and urgent care) a telehealth visit sometimes cannot resolve the problem and the patient must also come to the office: a duplicate visit. Duplicate visits are paid as well, and they consume office capacity.

Çakıcı and Mills (MSOM 2024; this mission follows the SSRN working-paper version of August 19, 2024) model a provider who splits capacity between an office and a telehealth channel, and patients who choose a channel strategically. Their main finding for the setting in which demand exceeds capacity is that pay parity can make the provider's revenue-maximizing choice and the access-maximizing choice disagree: for a moderate duplicate-visit probability the provider prefers telehealth while patients are better served by an office-only practice. This mission formalizes that result and the equilibrium analysis on which it rests.

Setting

A provider serves at total rate $\mu$ and devotes the fraction $\theta\in[0,1]$ of its capacity, the telehealth commitment, to telehealth. Episodes of care arrive at rate $\lambda$. Each patient balks (value $0$), visits the office, or uses telehealth; a telehealth visit needs a duplicate office visit with probability $q$. A resolved episode is worth $V$; waiting costs $h$ per unit of sojourn time; the co-payments are $c_O$ and $c_T$; an office visit costs an extra inconvenience $\tau$. With $\pi^O,\pi^T$ the proportions choosing the office and telehealth, the expected sojourn times are

$$W^O=\frac{1}{(1-\theta)\mu-(\pi^O+q\pi^T)\lambda},\qquad W^T=\frac{1}{\theta\mu-\pi^T\lambda},$$

and the expected utilities are $V-c_O-\tau-hW^O$ (office) and $V-c_T-hW^T-q(c_O+\tau+hW^O)$ (telehealth). A patient equilibrium is a split $(\pi^B,\pi^O,\pi^T)$ in which every action used is a best response.

The paper assumes $V>h/\mu+c_O+\tau$, $c_T<c_O+\tau$, and, with $\kappa(q)=\frac{h/\mu}{V-c_T-q(c_O+\tau)}$, that $0<\kappa(q)\le 1/(1+\sqrt q)^2$. In the large-market setting some patients balk at every $\theta$. There the equilibrium is of one of four types, by region of $\theta$: balk/office on $[0,\theta^T]$, balk/office/telehealth on $(\theta^T,\theta^O)$, balk/telehealth on $[\theta^O,\bar\theta)$, all-balk on $[\bar\theta,1]$, with explicit thresholds $\theta^T,\theta^O,\bar\theta$ and explicit proportions $\pi^O(\theta),\pi^T(\theta)$. The patient access rate and the provider's revenue rate under telehealth reimbursement $r$ (office revenue $R$) are

$$A(\theta)=\bigl(\pi^O(\theta)+\pi^T(\theta)\bigr)\lambda,\qquad F(r,\theta)=\bigl(R\pi^O(\theta)+(r+Rq)\pi^T(\theta)\bigr)\lambda .$$

The commitment that maximizes telehealth usage in the balk/telehealth region is $\theta^*=\bigl(1-\kappa(q)(1-q)\sqrt q\bigr)/(1+q)$.

Formalization targets

Goal: Proposition 4 with the thresholds of Proposition 3

Fix all parameters except $\theta$ and $q$, with $R>0$. There are thresholds $0<q^\dagger<q^*<1$ such that, for every admissible $q$, pay-parity revenue $F(R,\cdot)$ is maximized over $[0,1]$ at $\theta^*$ when $q<q^*$ and at $0$ when $q>q^*$; access $A$ is maximized at $\theta^*$ when $q<q^\dagger$ and at $0$ when $q>q^\dagger$; and for $q^\dagger<q<q^*$

$$A(\theta^*)<A(0)\qquad\text{and}\qquad F(R,0)<F(R,\theta^*).$$

The thresholds are existential; no closed form is fixed, so the statement survives any later computation of them.

Milestones

In attack order: Lemma 2 (order of $\theta^T,\theta^O$); Theorems 1–3 (where each equilibrium type occurs) and Lemma 3 ($\bar\theta<1$); Theorem 4 (shape of $F$ in $\theta$); Corollaries 1–2 (the maximizers of $F$ and $A$ are $0$ or $\theta^*$); Proposition 3 (the two thresholds). Two further items are not milestones: the uniqueness of the large-market equilibrium proportions, and Proposition 5 (the reimbursement $\tilde r=R(1-q)$ aligns the two objectives).

Significance

The result is the paper's argument against pay parity in acute care: when duplicate visits are neither rare nor frequent, paying telehealth at parity induces the provider to adopt it although fewer patients are then seen. Proposition 5 shows the misalignment disappears under the less-than-parity reimbursement $R(1-q)$, which pays the same per patient seen through either channel. The thresholds $q^*$ and $q^\dagger$ are what turn this into a policy statement about measurable duplicate-visit rates.

The paper proves these results by hand. None of them has a machine-checked proof, and nothing about strategic channel choice with duplicate service exists on Prove2Me. Formalizing them checks a case analysis with four regions, two square-root closed forms and an intermediate-value argument in $q$. The formalization has already exposed two places where the printed statements need a hypothesis (see Formalization scope).

Difficulty

Each step is elementary; the difficulty is bookkeeping. The equilibrium characterization requires solving the indifference conditions in each region and choosing the root of a quadratic that gives stable queues. The shape results require continuity of $A$ and $F$ across region boundaries and concavity of a function of the form $c\theta-\sqrt{\kappa^2+(a-b\theta)^2}$. The obvious comparison of the closed-form values at $0$ and at $\theta^*$ does not suffice on its own: the closed-form value at $\theta^*$ is the revenue only when $\theta^*$ lies in the balk/telehealth region, which fails for some admissible parameters. Whether that failure matters for the maximization is the central question.

Formalization scope

All objects are real-valued closed forms in the namespace TelehealthParity.Access. The definition Setting holds the parameters (the arrival rate is lam, since λ is a Lean keyword), $\kappa,\theta^T,\theta^O,\bar\theta,\theta^*$, the region-wise proportions, $A$, $F$, the large-market condition and the predicate Admissible p q. The definition Equilibrium holds the sojourn times, utilities and the equilibrium predicate. Conventions:

• Lemma 1 (the sojourn times) is adopted as the model, as in the paper; no queueing theory is formalized.
• A channel whose queue is unstable is unavailable: it cannot be used and constrains nothing. This is how the paper discards the unstable root in the balk/telehealth region.
• "Large market" (stated verbally on p. 12) is encoded as $A(\theta)<\lambda$ for all $\theta\in[0,1]$.
• Admissible p q collects $0<q<1$, assumption (6), Lemma 2's ordering condition, the large market, and $(1-q)V-c_T>0$. The last is not printed; the proof of Lemma 2 presumes it, and Lemma 2 fails without it.
• $R>0$ is added where strictness needs it: Theorem 4, the goal, and Proposition 5. The paper allows $R\ge0$.
• Corollary 1 carries the added hypothesis "$r\le R$ or $\theta^O\le\theta^*$". As printed, for every $r>0$, it is false for some $r>R$, where the maximizer is $\theta^O$.
• "Maximized at" is IsMaxOn over $[0,1]$; "linear" is affine.

Excluded trivializations. $A$, $F$ and $\theta^*$ are closed forms, not suprema or argmaxes. The goal states the strict misalignment and the full threshold characterization, not a comparison with one point. A sorry-free sanity check shows that the hypotheses hold on an admissible instance in the misaligned range ($V=4$, $c_T=c_O=\tau=1$, $h=1/2$, $\mu=1$, $\lambda=2$, $q=1/25$).

Welcome contributions are proofs of any milestone. The real-analysis lemmas (concavity of $c\theta-\sqrt{\kappa^2+(a-b\theta)^2}$, maximization of piecewise functions that are continuous across region boundaries) are reusable beyond this mission.

Selected references

• Ö. E. Çakıcı and A. F. Mills, Telehealth in Acute Care: Pay Parity and Patient Access, Manufacturing & Service Operations Management, 2024. https://doi.org/10.1287/msom.2022.0345 (SSRN working paper, version of August 19, 2024, followed here).