Control Theory

Motivation

Social-media influencers earn money by endorsing products to their followers. An endorsement of a product that does not fit the audience brings in money today but costs followers, and followers are also what spreads awareness of the influencer to new people. Nistor, Selove and Villas-Boas (Influencer Authenticity: To Grow or to Monetize, Management Science, 2024) model this trade-off as a deterministic, infinite-horizon, discounted optimal-control problem with a single binary control. In their base model (§3) the optimal policy is to grow first and monetize later: authentic while awareness is small, permanently inauthentic once awareness passes a threshold.

Section 4.2 of the paper asks how this changes when the audience is not permanent: users join and leave the platform, or the influencer covers a topic that interests people only for a while. With follower turnover the influencer never reaches full awareness, and Proposition 3 says that if turnover is fast enough she never monetizes at all. The model gives a testable prediction: influencers on platforms with rapid user turnover, or in product categories with short-lived interest, should stay authentic.

Setting

Time is $t \in [0, \infty)$. There is a unit mass of potential followers, and $A_t \in [0,1]$ is the share of them who are aware of the influencer, starting from $A_0$. At each time she is either authentic or inauthentic. Following Table 1 of the paper:

• authentic: $F_t = A_t$ followers and instantaneous profit $\pi_t = A_t$;
• inauthentic: $F_t = \gamma A_t$ followers and profit $\pi_t = \gamma\varphi A_t$,

with $0 < \gamma < 1$ and $\varphi > 1$. These are the reduced-form parameters of §3.1: a fraction $\gamma$ of aware people follow an inauthentic influencer, who earns $\varphi$ per follower, and authentic profit per follower is normalized to $1$. The paper assumes $\gamma\varphi > 1$ "for the remainder of the paper", so that being inauthentic pays more today.

Potential followers leave and are replaced at a turnover rate $x \in (0, \beta)$, and awareness follows equation (6):

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

where $\beta > 0$ is the word-of-mouth rate. Under the always-authentic policy this is the logistic equation $\frac{dA_t}{dt} = A_t(\beta - x - \beta A_t)$, with steady state $\frac{\beta - x}{\beta}$. The influencer maximizes the discounted profit (2), $\int_0^\infty e^{-rt}\pi_t\,dt$, with discount rate $r > 0$.

In the Lean development (namespace InfluencerAuth.Turnover) a policy is a measurable set $S \subseteq \mathbb R$ of the times at which she is inauthentic, so $S = \emptyset$ is "always authentic". IsPath β γ x A₀ S A says $A$ is an admissible awareness path, discountedProfit γ φ r S A is (2) at time $0$, and IsOptimalFrom β γ φ r x A₀ S A says that $(S, A)$ earns at least as much as every measurable policy with any admissible path from the same $A_0$. authValue β x r is the closed form $\overline V$ of Lemma 5, and Condition2 γ φ β r x is

$$\frac{(1-\gamma)x}{r + \beta - x} > \gamma\varphi - 1 .$$

Formalization targets

Goal: Proposition 3 (p. 9)

Under the standing assumptions $0<\gamma<1$, $\varphi>1$, $\gamma\varphi>1$, $\beta>0$, $r>0$, with $0 < x < \beta$ and Condition 2,

$$\forall A_0 \in \Bigl(0, \tfrac{\beta - x}{\beta}\Bigr),\quad \exists A,\ \ (\emptyset, A) \text{ is optimal from } A_0 .$$

The range of $A_0$ is the paper's set of "all feasible levels of awareness". The statement fixes no constant beyond those of Condition 2.

Milestone: Lemma 5 (p. 9)

For $0 < A_0 < 1$ and every admissible always-authentic path $A$ from $A_0$,

$$\int_0^\infty e^{-rt} A_t\,dt = \overline V(A_0) = \int_0^\infty \frac{e^{-rs}}{\frac{\beta}{\beta - x} + \frac{1 - A_0\beta/(\beta - x)}{A_0} e^{-(\beta - x)s}}\,ds .$$

Milestone: display (7) (p. 9)

$$\left.\frac{d\overline V(A)}{dA}\right|_{A = \frac{\beta - x}{\beta}} = \int_0^\infty e^{-(r + \beta - x)s}\,ds = \frac{1}{r + \beta - x}.$$

Significance

Proposition 3 is the paper's result on when the grow-then-monetize pattern of the base model breaks down. Without turnover the influencer always monetizes once she is large enough (Proposition 1, §3). With turnover there is a whole parameter region, given by Condition 2, where monetizing is never optimal. The condition compares the extra current profit from being inauthentic, $\gamma\varphi - 1$, with the awareness lost by being inauthentic, $(1-\gamma)x$, valued at the marginal value of awareness at the steady state, $1/(r+\beta-x)$ from (7).

The proofs are in an online appendix that is not part of the published article, and this result has no machine-checked proof. The mission provides a precise statement of the control problem: optimality over every measurable switching pattern, with the dynamics in integral form. It also gives the closed-form always-authentic value and its derivative as separate targets. A complete development would be one of the first formal optimality proofs for an infinite-horizon, discounted, continuous-time deterministic control problem.

Difficulty

Optimality is claimed against every measurable policy, not only against constant or threshold policies. The natural argument is a verification theorem: show that $\overline V$ satisfies the Hamilton–Jacobi–Bellman inequality on the feasible range, then integrate along an arbitrary competitor path. Condition 2 is stated only at the steady state $(\beta-x)/\beta$, where (7) gives the marginal value of awareness. At a lower awareness level the inequality comparing the two actions involves $\overline V'(A)$ at that level, so it does not follow from Condition 2 alone; it needs control of $\overline V'$ on the whole interval. A competitor path may also switch infinitely often, so its awareness is only absolutely continuous, and the comparison must work almost everywhere. Above the steady state the always-authentic policy is in general not optimal, so any argument must use the restriction $A_0 < (\beta - x)/\beta$.

Formalization scope

• Policies and dynamics. A policy is a measurable Set ℝ. An admissible path is continuous on $[0,\infty)$, starts at $A_0$, stays in $[0,1]$, and satisfies $A_t = A_0 + \int_0^t (\beta f_S(s) A_s(1-A_s) - xA_s)\,ds$ for $t \ge 0$, with $f_S = \gamma$ on $S$ and $1$ off $S$. This is the Carathéodory form of (6). A derivative everywhere is not required, because that would exclude every switching policy. The clause $A_t\in[0,1]$ follows from the equation and is stated to make integrability explicit.
• Objective. discountedProfit is $\int_{(0,\infty)} e^{-rt} p_S(t) A_t\,dt$ with $p_S = \gamma\varphi$ on $S$ and $1$ off $S$; the paper's value from time $t$ is the same object after the shift $s = u - t$. No optimal value is defined as a real supremum; optimality is a comparison with every competitor.
• Hypotheses. The goal carries every standing assumption of the paper: $0<\gamma<1$, $\varphi>1$, $\gamma\varphi>1$, $\beta>0$, $0<x<\beta$. It also assumes $r>0$, which is how "discount rate $r$" is read and which makes (2) finite. The milestones drop $\gamma$, $\varphi$ and their assumptions, which the always-authentic value does not involve.
• No trivialization. The goal produces the optimal path existentially, so it cannot hold for lack of an admissible path. The competitor class is nonempty (the logistic solution is admissible), and every competitor's profit is the integral of a bounded measurable function, so no competitor collapses to the junk value $0$. Widening $A_0$ to $(0,1)$ would make the statement false, not stronger.
• Infrastructure. The development needs the explicit logistic solution with turnover, differentiation under the integral sign for $\overline V$, and a comparison or verification argument for scalar ODEs with measurable coefficients. The verification lemma for discounted bang-bang control of a one-dimensional state is reusable for chunk 1 of this series and for similar marketing-diffusion models. Proofs of either milestone, a sanity proof that the logistic path is admissible, and the verification argument are all welcome contributions.

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), 1969, 215–227. https://doi.org/10.1287/mnsc.15.5.215
• W. H. Fleming, R. W. Rishel, Deterministic and Stochastic Optimal Control, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7

Motivation

Industries in which capacity can be built but not sold back (energy generation, manufacturing, mining) are studied through irreversible investment models: a firm controls a nondecreasing investment process and trades the cost of capacity against uncertain future revenues. When many small firms compete, each firm's revenue depends on aggregate production through the market price, and the natural equilibrium notion is a mean-field equilibrium: every firm optimizes against a given aggregate, and the aggregate generated by the optimal behaviour is the one that was assumed.

Aïd, Basei and Ferrari (arXiv:2305.00541; Operations Research, 2025) add a macroeconomic regime to this picture. The economy switches between two states according to a continuous-time Markov chain, and volatilities and prices depend on the state. They prove that a stationary mean-field equilibrium exists and is unique, and that the equilibrium firm invests at regime-dependent barriers. Related stationary mean-field games with singular controls include Cao and Guo (Stochastic Processes and their Applications, 2022) and Cao, Dianetti and Ferrari (doi:10.1287/moor.2022.1323); the stability of the reflected regime-switching diffusions that appear in the equilibrium is due to Budhiraja and Liu (Mathematics of Operations Research, 2012).

Setting

A real Brownian motion $B$ and an independent two-state Markov chain $\varepsilon$ with generator

$$P=\begin{pmatrix}-p_1&p_1\\p_2&-p_2\end{pmatrix},\qquad \pi=\Big(\frac{p_2}{p_1+p_2},\frac{p_1}{p_1+p_2}\Big),\qquad p_1,p_2\in(0,1),$$

live on a complete probability space; $\mathbb F$ is their augmented natural filtration. A control $I$ is an adapted, nonnegative, nondecreasing càdlàg process with $I_{0-}=0$. The production capacity is

$$X^I_t=x\exp\Big(-\Big(\delta t+\tfrac12\int_0^t\sigma^2_{\varepsilon_s}ds\Big)+\int_0^t\sigma_{\varepsilon_s}dB_s+I_t\Big),\qquad x>0,$$

and investment costs $\kappa\,X^I_t\circ dI_t$, the integral (2.3) that charges a jump $\Delta I_t$ the amount $X^I_{t-}(e^{\Delta I_t}-1)$. Given aggregate productions $Q=(Q_1,Q_2)\in(0,\infty)^2$, the price in regime $i$ is $\eta_i=\varphi_i+\zeta_iQ_i^{-\alpha}$, and a firm starting from $(x,i)$ maximizes, over the admissible set $\mathcal A$ of (2.5),

$$J_{(x,i)}(I,Q)=\mathbb E_{(x,i)}\Big[\int_0^\infty e^{-\rho t}\big(\eta_{\varepsilon_t}X^I_tdt-c(X^I_t)^2dt-\kappa X^I_t\circ dI_t\big)\Big].$$

A stationary mean-field equilibrium (Definition 2.2) is a pair $(I^\star,Q^\star)$ such that $I^\star$ maximizes $J_{(x,i)}(\cdot,Q^\star)$ over $\mathcal A$, and the controlled pair $(X^{I^\star}_t,\varepsilon_t)$ has a stationary distribution $p_\infty$ with

$$Q^\star_j=\frac1{\pi_j}\int_0^\infty x\,p_\infty(dx,j),\qquad j=1,2.$$

The barrier control at levels $a_1,a_2>0$ is

$$I^\star_t=0\vee\sup_{0\le s\le t}\Big(\ln(a_{\varepsilon_s}/x)+\int_0^s\big(\delta+\tfrac12\sigma^2_{\varepsilon_u}\big)du-\int_0^s\sigma_{\varepsilon_u}dB_u\Big),$$

the minimal investment keeping $X^{I^\star}_t\ge a_{\varepsilon_t}$. Finally $\phi_i(\theta)=\frac12\sigma_i^2\theta^2+(\delta+\frac12\sigma_i^2)\theta-p_i$ and $\bar\phi=\phi_1\phi_2-p_1p_2$, whose negative roots are $\theta_1<\theta_2<0$.

Formalization targets

Goal: Theorem 4.1

Under Assumption 2.1, $\rho>2\max\{\sigma_1^2,\sigma_2^2\}$, and $1+\theta_2<0$: for every $(x,i)$ there are barriers $a^\star\in(0,\infty)^2$ and $Q^\star\in(0,\infty)^2$ with

$$(I^\star(a^\star),Q^\star)\ \text{a stationary MFE, and every stationary MFE } (I,Q)\text{ has } Q=Q^\star,\ I=I^\star\ \text{a.s.}$$

Milestones, in the order the proof uses them

1. Proposition 4.1: a $C^2$ solution of the free-boundary problem (4.10) is the value function, and the barrier control is optimal.
2. Proposition 4.2 (corrected): the stopping problem (4.13) has threshold regions, a $C^1$ value satisfying (4.17), and an optimal hitting time.
3. Proposition 4.3 ((4.18) corrected): $V(x,i)=k_i+\int_{a_i}^xv(y,i)dy$.
4. The root structure of (4.29): $\theta_1<\theta_2<0<\theta_4$ are the nonzero roots of $\bar\phi$.
5. Proposition 4.6: the stationary distribution function of the capacity reflected at $0<a_1<a_2$ is the explicit $\Pi(\ln x,i)$ of (4.32).
6. Corollary 4.7: the regime-wise stationary means (4.35)–(4.36).
7. Step 1 of the proof of Theorem 4.1: the stopping value and the barriers decrease in $Q$.
8. Theorem 2.4(ii): $\mathbb P(X_\infty\ge x)/x^{\theta_2}\to C>0$.

Significance

The theorem gives a fully explicit equilibrium in a model with common noise in the form of regime switching: the barriers solve a finite system of algebraic equations, and the stationary distribution of capacities is known in closed form, with a Pareto tail of exponent $\theta_2$. This makes comparative statics of market concentration and of the industry's response to regime persistence computable, which is what Section 3 of the paper does numerically.

The result is proved on paper; none of it is formalized. A complete development would yield a machine-checked verification theorem for regime-switching singular control, a checked link between singular control and optimal stopping, and a checked stationary law for a reflected regime-switching geometric Brownian motion. The printed text contains slips the formalization corrects in the open: the continuation and stopping regions of Proposition 4.2 are printed swapped, a term of (4.18) carries a spurious factor $a_i$, and an integration by parts in the proof drops $\kappa$.

Difficulty

The obvious route, solving the variational inequality (4.8) by guessing a smooth-fit solution, fails here: the two regimes couple the ordinary differential equations, and the smooth-fit and smooth-pasting equations become nonlinear in both barriers at once, so existence and uniqueness of their solution cannot be read off. The regularity a verification argument needs ($C^2$ value, a threshold structure of the investment region) is therefore the hard part, and with regime switching it is not covered by the one-dimensional theory. The stationary law requires positive recurrence of a reflected diffusion with switching and the identification of its limit law. The fixed point $Q=\mathcal RQ$, where $(\mathcal RQ)_j=\pi_j^{-1}\int_0^\infty x\,p^Q_\infty(dx,j)$ is built from the stationary law under the barrier control optimal for $Q$, needs continuity and a priori bounds of $\mathcal R$ for existence, and a monotonicity argument for uniqueness; the printed uniqueness argument treats ordered pairs of fixed points explicitly, and uniqueness of the optimal control itself is not argued on the page but is part of the goal.

Formalization scope

Lean represents regimes as Fin 2 (index 0 is regime 1) and time as $\mathbb R_{\ge0}$. The model consists of: the chain, pinned by its closed-form transition function $e^{tP}$; Mathlib's IsBrownianReal for $B$; independence of $B$ and $\varepsilon$; the augmented filtration; $M=\int\sigma_\varepsilon dB$ through the platform relation EthierKurtz.HasBrownianItoIntegral, with continuous paths; the state (2.4); the integral (2.3), computed as $\int e^{-\rho t}Y_t\,d(e^{I})_t$; the admissible set (2.5) with $[0,\infty]$-valued expectations; $J$ of (2.6); Definition 2.2; and the barrier control (4.11). $\mathbb E_{(x,i)}$ is the expectation conditioned on $\varepsilon_0=i$.

Standing constants: $\delta,\sigma_i,\rho,c,\kappa,\varphi_i,\zeta_i>0$, $p_i\in(0,1)$, $0<\alpha<1$, $\min_i\varphi_i>\rho+\delta$, and Assumption 2.1. The root condition $1+\theta_2<0$ is stated as "$\bar\phi$ has no root in $[-1,0)$". Pinned hypotheses, each disclosed in the item that carries it: the stationary distribution is the weak limit of the time-$t$ laws; $Q_i>0$; $a_i>0$ wherever (4.11) is used; $0<a_1<a_2$ for the §4.2 statements; $(\rho+\delta)\kappa<\varphi_i$ on the goal; and "$\sim$" in Theorem 2.4(ii) as a ratio tending to a positive constant.

The equilibrium is defined from the model: optimality against every admissible control, including those with an initial jump, and the limit law of the actually controlled process. It is never defined through the paper's closed forms (4.23) or (4.32), which would make the goal a statement about formulas. The barrier control is the printed formula, not an arbitrary control keeping $X\ge a$.

Not formalized: Section 3 (numerics), Proposition 4.4 and Corollary 4.5 (semi-explicit value functions), the continuity part of Step 1, and Steps 2–4 of the proof as separate items. Contributions toward a general verification theorem for regime-switching singular control, regularity of regime-switching stopping problems, and stationary laws of reflected switching diffusions are reusable beyond this mission.

Selected references

• R. Aïd, M. Basei, G. Ferrari, A Stationary Mean-Field Equilibrium Model of Irreversible Investment in a Two-Regime Economy, arXiv:2305.00541v1, 2023; Operations Research, 2025. https://arxiv.org/abs/2305.00541
• A. Budhiraja, X. Liu, Stability of constrained Markov-modulated diffusions, Mathematics of Operations Research 37(4):626–653, 2012.
• H. Cao, X. Guo, MFGs for partially reversible investment, Stochastic Processes and their Applications 150:995–1014, 2022.
• H. Cao, J. Dianetti, G. Ferrari, Stationary discounted and ergodic mean-field games of singular controls, Mathematics of Operations Research, 2022. https://doi.org/10.1287/moor.2022.1323
• G. Ferrari, N. Rodosthenous, Optimal control of debt-to-GDP ratio in an N-state regime switching economy, SIAM Journal on Control and Optimization 58(2):755–786, 2020.

Motivation

A fund manager who tracks a benchmark (a stock index, a price index, the cost of higher education) wants the managed wealth to stay above the benchmark at all times. Under a strict floor constraint $V_t\ge M_t$ the set of admissible strategies can be empty when the benchmark is random. Bo, Huang and Yu (arXiv:2302.08302, Math. Oper. Res.) relax the constraint: the manager may inject capital $A_t$ so that $V_t+A_t\ge M_t$, and pays $\beta>0$ per unit injected. The problem becomes a consumption–investment problem with a running-maximum cost, of the type studied with viscosity methods by Barron–Ishii (1989) and Bokanowski et al. (2015). The paper obtains instead a classical solution of the associated HJB equation and an explicit optimal feedback control. The reduction from the constrained problem to the auxiliary problem below is due to Bo, Liao and Yu (2021) and is not part of this mission.

Setting

A market has $d$ risky assets with return vector $\mu\ne0$ and invertible volatility matrix $\sigma$; the riskless rate is $0$. On a filtered probability space satisfying the usual conditions with a $d$-dimensional Brownian motion $W$, write $W^\gamma=\sum_j\gamma_jW^j$ and $W^\eta=\sum_j\eta_jW^j$ with $|\gamma|=|\eta|=1$. The benchmark is $M_t=m_t+Z_t$, where $Z$ is a geometric Brownian motion with drift $\mu_Z$ and volatility $\sigma_Z\ge0$ driven by $W^\eta$, and $m_t$ is the running maximum of $B_t=b+\mu_Bt+\sigma_BW^\gamma_t$, $\sigma_B\ge0$.

A strategy $(\theta,c)$ invests $\theta_t\in\mathbb R^d$ and consumes at rate $c_t\ge0$; the class $\mathbb U^r$ consists of progressively measurable pairs for which the wealth equation is well defined on every bounded interval. The auxiliary states are the reflected wealth surplus $X\ge0$, started at $x$,

$$X_t=x+\int_0^t\theta_s^\top\mu\,ds+\int_0^t\theta_s^\top\sigma\,dW_s-\int_0^tc_s\,ds-(Z_t-z)-(m_t-m_0)+L^X_t,$$

where $L^X$ is the minimal nondecreasing process keeping $X\ge0$ (the injected capital), and the reflected distance $I_t=m_t-B_t\ge0$ started at $h$. With power utility $U(c)=c^p/p$, $p\in(-\infty,0)\cup(0,1)$, and discount rate $\rho>0$, the objective is

$$J(x,h,z;\theta,c)=\mathbb E\Big[\int_0^\infty e^{-\rho t}U(c_t)\,dt-\beta\int_0^\infty e^{-\rho t}dL^X_t\Big].$$

The candidate value function is built from a probabilistic representation. On a space with independent Brownian motions $B^0,B^1,B^2$, let $R^r$ be a reflected drifted Brownian motion $r+(\alpha^2/2-\rho)t+\alpha B^1_t+L^r_t\ge0$, let $H^h$ be a correlated one with local time $K^h$, and let $N^z$ be a geometric Brownian motion. With the coefficients $\alpha,\kappa_1,\kappa_2,\varrho_1,\varrho_2$ of (2.9) and (3.4),

$$v(r,h,z)=\tfrac{1-p}p\beta^{-\frac p{1-p}}\mathbb E\Big[\int_0^\infty e^{-\rho s+\frac p{1-p}R^r_s}ds\Big]+\beta(\kappa_2-\mu_Z)\mathbb E\Big[\int_0^\infty e^{-\rho s-R^r_s}N^z_sds\Big]-\beta\mathbb E\Big[\int_0^\infty e^{-\rho s-R^r_s}dK^h_s\Big],$$

$\hat u(y,h,z)=v(-\ln(y/\beta),h,z)$ for $y\in(0,\beta]$, and

$$u(x,h,z)=\inf_{y\in(0,\beta]}\{\hat u(y,h,z)+yx\}.$$

Formalization targets

Goal: Theorem 4.1 (verification theorem)

For model parameters with $\mu_Z>\kappa_2$ and $\sigma_B\ne0$ there is $\rho_0>0$ such that for every $\rho>\rho_0$: (i) $u$ is a classical solution of the HJB equation (4.2) with the Neumann conditions $u_x(0,h,z)=\beta$ and $u_h(x,0,z)=u_x(x,0,z)$, with $u_x>0$ and $u_{xx}<0$; (ii) for every admissible strategy and every $(x,h,z)\in\mathbb R^3_+$,

$$J(x,h,z;\theta,c)\le u(x,h,z),$$

with equality for the feedback strategy $\theta^*=-(\sigma\sigma^\top)^{-1}\frac{\mu u_x-\sigma_B\sigma\gamma u_{xh}+\sigma_Z\sigma\eta z(u_{xx}-u_{xz})}{u_{xx}}$, $c^*=u_x^{1/(p-1)}$ along a solution of the reflected feedback system (4.4). The threshold $\rho_0$ is asserted to exist, not fixed: the paper's formula (4.45) for it depends on $\rho$ and is not self-contained.

Milestones, in the order of the proof

1. Lemma 3.2. The first two terms $l(r,z)$ of $v$ solve the Neumann problem (3.8) and equal the explicit form (3.9).
2. Lemma 3.4. For $\sigma_B\ne0$, $\varphi(r,h)=-\beta\mathbb E[\int_0^\infty e^{-\rho s-R^r_s}dG^h_s]$ is $C^2$ on $\mathbb R^2_+$, where $G^h$ is the local time of a reflected Brownian motion independent of $R^r$.
3. Lemma 3.3. $G^h$ and $R^r$ are independent and $\varphi$ solves the Neumann problem (3.15).
4. Proposition 3.5. $\psi=\varphi+\xi$ solves (3.38), and every bounded classical solution of (3.38) equals the last term of $v$.
5. Remark 3.6. $\psi_r+\psi_{rr}>0$.
6. Theorem 3.1. $\hat u$ is strictly convex in $y$ and solves the dual PDE (2.8) with (2.10), (2.11).
7. Theorem 4.1(i) and (4.7): the linear growth $|\theta^*|\le C_o(1+x+z)$, $|c^*|\le C_q(1+x)$.

Significance

The theorem settles two questions about the relaxed tracking formulation: the optimal portfolio–consumption pair exists in feedback form, and the value function is a classical (not only viscosity) solution of an HJB equation with two Neumann boundary conditions. Together with the paper's Lemma 4.4, it shows that the expected discounted capital injection of the optimal strategy is finite, so the relaxed problem is well posed. The dual representation also gives the value in a separated form, three expectations of functionals of reflected Brownian motions, which is what makes the derivatives and the feedback explicit.

The result is proved in the paper; nothing here is open. No part of it is formalized. A formal proof would need Itô's formula for reflected processes, the smoothness of expectations of local-time functionals, and the duality argument; any of the milestones on its own is a self-contained target.

Difficulty

The last term of $v$ couples the reflected process $R^r$ with the local time $K^h$ of a second reflected process correlated with it through $\varrho_1$. Differentiating $\mathbb E[\int e^{-\rho s-R^r_s}dK^h_s]$ in $(r,h)$ directly fails: the local time is not differentiable in its starting point in any pathwise sense, and the correlation prevents conditioning one process on the other. The paper first treats the independent case (Lemmas 3.3–3.4), where the expectation factors through the law of $G^h$, and then removes the correlation by a homogenization of the Neumann conditions (Proposition 3.5). A second difficulty is the verification step itself: the admissible class is unbounded and the state reflects at two boundaries, so the local martingale terms must be controlled by moment bounds that depend on the growth (4.7) of the feedback.

Formalization scope

• Parameters. One structure holds $\mu,\sigma,\mu_Z,\sigma_Z,\mu_B,\sigma_B,\gamma,\eta,\beta,p$; the standing assumptions are $d\ge1$, $\det\sigma\ne0$, $\mu\ne0$, $\sigma_Z,\sigma_B\ge0$, $\gamma\cdot\gamma=\eta\cdot\eta=1$, $\beta>0$, $p<1$, $p\ne0$. All coefficients ($\alpha,\kappa_1,\kappa_2,\varrho_1,\varrho_2,C_1,C_2,\ell$) are definitions.
• Carriers. $v$, $\hat u$, $u$ are defined on any probability space with a standard 3-dimensional Brownian motion (published EthierKurtz.IsStandardBrownian), and every statement holds for every such space. The control problem lives on any filtered space satisfying the usual conditions with an $\mathbb F$-Brownian motion (published RankBasedSDI.LoadBalancing.UsualConditions, IsFBrownian).
• Processes in closed form. $R^r,H^h,K^h,L^r,G^h$ are given by Skorokhod formulas (published skorokhodReg), $Z$ and $N^z$ as explicit exponentials. The only stochastic integral is $\int\theta^\top\sigma\,dW$, through the published EthierKurtz.HasBrownianItoIntegral with a continuous version required.
• Expectations and objective. Expectations of nonnegative integrands are lintegrals; statements about $v$ assert their finiteness. Stieltjes integrals use the Lebesgue–Stieltjes measure of the path. The objective is compared in the extended reals as $\text{utility}\le u+\beta\cdot\text{cost}$, which agrees with $J\le u$ whenever $J$ is defined and never produces $\infty-\infty$; $c^p$ is computed in $[0,\infty]$ so that $0^p=\infty$ for $p<0$.
• Classical solutions. $C^2$ on the closed domain (ContDiffOn ℝ 2), the PDE on the open set the paper names, Neumann conditions pointwise on the faces; derivatives are taken within the closed coordinate domains. The suprema in (4.2) are least upper bounds (IsLUB), the consumption supremum over $c>0$.
• Added hypotheses. $\mu_Z>\kappa_2$ and $\sigma_B\ne0$ in Theorem 4.1 and $\sigma_B\ne0$, $\rho>\alpha^2|p|/(2(1-p))+\mu_Z$ in Theorem 3.1 are used by the proofs but not printed in the statements; they are added. Lemma 3.2 and the milestone Theorem 4.1(i) also carry Theorem 3.1's $\rho>\alpha^2p/(2(1-p))$: when $\mu_Z<0$ Lemma 3.2's printed condition does not imply it, and without it the first expectation in $v$ is infinite.
• Ruled out. Defining $u$ as the supremum of $J$ would make (ii) circular, and specializing to $d=1$, $\sigma_B=0$, $\varrho_1=0$ or a fixed $\rho$ changes the theorem; none of these is used. A statement "for every solution of (4.4)" would be vacuous if (4.4) had no solution, so the optimal pair is asserted to exist.

The definitions of reflected processes, Stieltjes integrals against local times, and classical Neumann solutions are reusable beyond this mission. Proofs of any milestone, and of the deterministic facts ($0<\ell<1$, $|\varrho_i|\le1$, (3.9) solving (3.8)), are welcome.

Selected references

• G. Bo, Y. Huang, X. Yu, Stochastic control problems with state-reflections arising from relaxed benchmark tracking, arXiv:2302.08302v4 (Math. Oper. Res.). https://arxiv.org/abs/2302.08302
• L. Bo, H. Liao, X. Yu, Optimal tracking portfolio with a ratcheting capital benchmark, SIAM J. Control Optim. 59(3), 2346–2380, 2021.
• J. M. Harrison, Brownian Motion and Stochastic Flow Systems, Wiley, New York, 1985.
• W. Łaukajtys, L. Słomiński, Penalization methods for the Skorokhod problem and reflecting SDEs with jumps, Bernoulli 19(5A), 1750–1775, 2013.
• E. N. Barron, H. Ishii, The Bellman equation for minimizing the maximum cost, Nonlinear Anal. TMA 13(9), 1067–1090, 1989.

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

An investor who does not know the expected return of a stock faces two kinds of uncertainty: risk (the randomness of returns given the model) and ambiguity (uncertainty about which model is true). The smooth ambiguity criterion of Klibanoff, Marinacci and Mukerji (Econometrica 2005) separates the two: the investor first computes the expected utility $\mathbb E[U(X_T)\mid Z=z]$ under each candidate model $z$, then averages a transformation $\phi$ of these values over her belief about $Z$. Risk aversion lives in $U$, ambiguity aversion in the curvature of $\phi$.

When the investor also learns $Z$ from prices, her belief changes over time and the nonlinear $\phi$ makes the problem time-inconsistent: a strategy that is optimal today is no longer optimal tomorrow. Following Strotz and the continuous-time game-theoretic approach of Björk, Khapko and Murgoci (Finance and Stochastics 2017), the paper of Guan, Liang and Xia (arXiv:2302.08181, Mathematics of Operations Research, 2025) looks for an equilibrium strategy: a rule that no short deviation can improve to first order. It derives a verification theorem and, for a Gaussian prior with CARA utility and power or logarithmic $\phi$, the equilibrium in closed form.

Setting

A bond pays the constant rate $r$. The stock satisfies $dS_t/S_t=Z\,dt+\sigma\,dW_t$ with volatility $\sigma>0$, a standard Brownian motion $W$, and an unknown constant drift $Z$ with prior $N(\beta_0,\sigma_0^2)$, $\sigma_0>0$. The horizon is $T>0$. Observing prices, the investor's posterior at time $t$ is $N(\beta_t,\zeta(t))$ with

$$\zeta(t)=\frac{\sigma^2\sigma_0^2}{\sigma^2+t\sigma_0^2}.$$

A strategy is a feedback function $\pi(t,x,\beta)$: the amount held in the stock given time, wealth $x$ and posterior mean $\beta$.

The inside system fixes a hypothetical drift value $z$ and starts at $(t,x,\beta)$: the posterior mean evolves by $d\beta^z_s=\frac{\zeta(s)}{\sigma^2}[(z-\beta^z_s)ds+\sigma dW_s]$ and the wealth by

$$dX_s=rX_s\,ds+\pi(s,X_s,\beta^z_s)(z-r)\,ds+\pi(s,X_s,\beta^z_s)\,\sigma\,dW_s .$$

Utility is CARA, $U(x)=-\frac1ke^{-kx}$ with $k>0$, and $\phi(u)=-\frac1\alpha(-u)^\alpha$ for $\alpha\ne0$, $\phi(u)=-\log(-u)$ for $\alpha=0$, on $u<0$; $\phi$ is concave for $\alpha>1$, linear for $\alpha=1$ and convex for $\alpha<1$. The inside expected utility is $g^{z,\pi}(t,x,\beta)=\mathbb E[U(X^{z,\pi}_T)\mid X_t=x,\beta^z_t=\beta]$, and the objective is

$$J(t,x,\beta,\pi)=\int\phi\big(g^{z,\pi}(t,x,\beta)\big)\,N(\beta,\zeta(t))(dz).$$

A strategy is admissible ($\pi\in\Pi$, Definition 5.1) if the wealth equation is well posed and certain exponential and power moments are bounded by $Ce^{\epsilon z^2}$ over short horizons. $\pi^*\in\Pi$ is an equilibrium strategy (Definition 2.1) if for every $(t,x,\beta)$ and $\pi\in\Pi$, the spike $\pi_{t,h}$ (equal to $\pi$ on $[t,t+h)$ and $\pi^*$ afterwards) satisfies

$$\limsup_{h\to0^+}\frac{J(t,x,\beta,\pi_{t,h})-J(t,x,\beta,\pi^*)}{h}\le0 .$$

Formalization targets

Goal: Theorem 5.5

Let $\alpha^*<0$ be the unique solution of $\big(1+\sigma_0^{-2}\sigma^2T^{-1}\big)\int_0^\infty e^{-x}(1+(1-\alpha^*)x)^{\alpha^*/(1-\alpha^*)}dx=1$ and assume $\alpha>\max\{\alpha^*,1-0.5\sigma_0^{-2}\sigma^2T^{-1}\}$. Let $m_1,\dots,m_6$ solve the ODE system (5.10) and put $a_1(t,m_2,m_3)=\frac{(1+\zeta m_2)(\zeta^{-1}+\alpha m_2)}{\zeta^{-1}-\alpha m_3}$. Then

$$\pi^*(t,x,\beta)=\frac{e^{-r(T-t)}}{k\sigma^2}\big\{a_1(t,m_2(t),m_3(t))+\zeta(t)m_1(t)\big\}(\beta-r)$$

is an equilibrium strategy, and its inside expected utility is

$$g^z(t,x,\beta)=-\frac1k\exp\Big\{-ke^{r(T-t)}x+\tfrac12m_1\beta^2+m_2\beta z+\tfrac12m_3z^2+m_4\beta+m_5z+m_6\Big\}.$$

Milestones

The milestones follow the paper's proof: the Gaussian moment formula (Lemma C.2) and short-horizon bounds on $\beta^z$ (Lemma C.1); admissibility under a growth bound (Proposition 5.2) and of $\pi^*$; the critical exponent, unique solvability and closed form of the reduced system (5.16) with its sign bounds (Proposition 5.4); the closed-form remaining coefficients (5.18); the extended HJB conditions (Lemma 5.3); and three verification steps of Appendix G (a martingale property, uniform integrability, and continuity (G.5)).

Significance

Theorem 5.5 gives an explicit, time-consistent investment rule under learning and smooth ambiguity. The rule is linear in the posterior mean, and its coefficient splits into the myopic Merton demand and two hedging demands, one against ambiguity in $Z$ and one against changes in $\beta$; the paper's numerical section uses this decomposition to study how ambiguity attitude changes the demand for the risky asset. At $\alpha=1$ the criterion is expected utility and $\pi^*$ is the Bayesian-learning Merton rule. The critical exponent $\alpha^*$ marks how much ambiguity seeking the closed form can tolerate.

The result is proved in the paper (Appendices C–G) but not formalized. The formalization would add to the platform its first smooth-ambiguity preference, its first equilibrium notion for a time-inconsistent continuous-time control problem with feedback strategies, and its first Bayesian drift-learning model. Lemma C.2 and the posterior-mean process are reusable beyond this paper.

Difficulty

Every quantity in the equilibrium inequality is a law-level functional of a controlled SDE: $g^{z,\pi}$ is an expectation over the wealth under the hypothetical drift, and $J$ integrates $\phi(g^{z,\pi})$ against the Gaussian posterior over $z$. The obvious route, a Taylor expansion of $J(\pi_{t,h})$ in $h$, needs to interchange the limit $h\to0^+$ with two nested expectations, one of which ranges over an unbounded drift $z$. Exponential utility makes $g^z$ grow like $e^{cz^2}$, so every estimate has to be uniform in $z$ up to a factor $e^{\epsilon z^2}$ that the Gaussian posterior can absorb, and the convex case $\alpha<1$ needs the extra lower bound on $\alpha$. On the deterministic side, the six-dimensional Riccati-type system (5.10) is nonlinear; its solvability on all of $[0,T]$ is not automatic and fails beyond the critical exponent $\alpha^*$.

Formalization scope

Time is real, with $t\in[0,T]$ explicit; Mathlib's Brownian motion IsBrownianReal is indexed by $\mathbb R_{\ge0}$ and read at s.toNNReal. Every statement holds on every probability space carrying a Brownian motion. Standing hypotheses: $\sigma,\sigma_0,T,k>0$; $Z$ ranges over $\mathbb R$.

Conventions committed to:

1. Conditioning on a state $\mathbb E[\cdot\mid X_t=x,\beta_t=\beta]$ is the inside system started at $(t,x,\beta)$ and driven by $W_s-W_t$, as the paper's appendices use it; $\mathbb E[\cdot\mid\beta_t=\beta]$ for functions of $Z$ is the posterior $N(\beta,\zeta(t))$, cited from Bismuth, Guéant and Pu (2019), not re-derived.
2. $\beta^z$ is the explicit formula (C.1). The wealth is a strong solution of (5.2) with the published Itô integral EthierKurtz.HasBrownianItoIntegral against the shifted Brownian motion.
3. Definition 5.1(i) is read on the inside system: for every $z$ and every start, the wealth equation is uniquely solvable.
4. The equilibrium predicate requires $J$ to be finite (for $\pi^*$, and for spikes with small $h$), the $\limsup$ is in $\epsilon$-form, and $t\in[0,T)$.
5. Every ODE solution keeps $\zeta^{-1}-\alpha m_3>0$ on $[0,T]$; time derivatives are taken within $[0,T]$.
6. Suprema claimed to equal $0$ are least upper bounds; $\Psi^{-1}$ is written as an equation for $\Psi$.

Each of these rules out a trivializing formalization: a Bochner expectation of a non-integrable utility is $0$ in Lean, which would make $\phi(0)$ and $J$ meaningless; a ⨆ of an unbounded set is $0$, the claimed value; an ODE "solution" through a zero of the denominator would solve a junk system; and a goal over an empty set of $\alpha^*$ or of ODE solutions would be vacuous, which Proposition 5.4 and (5.18) exclude. Corrected readings of printed slips (the conditioning $X^{\pi^*}_T=x$ in Theorems 3.5/4.5 read as $X^{\pi^*}_t=x$; Step 1 stated from every start) are disclosed in the items.

The proofs use, beyond Mathlib: Itô's formula, the Burkholder–Davis–Gundy inequality, Novikov's criterion, the generalized Gronwall inequality (Willett–Wong 1965, Theorem 2), and the Gaussian filter. Contributions of these tools as separate results are welcome. Not included: Lemmas C.3 and D.1, Steps 2, 4 and 5 of Appendix G, and the verification Theorems 3.5 and 4.5.

Selected references

• G. Guan, Z. Liang, J. Xia, Equilibrium Portfolio Selection for Smooth Ambiguity Preferences, Mathematics of Operations Research, 2025; preprint arXiv:2302.08181v1, 2023. https://arxiv.org/abs/2302.08181
• P. Klibanoff, M. Marinacci, S. Mukerji, A Smooth Model of Decision Making under Ambiguity, Econometrica 73(6), 2005. https://doi.org/10.1111/j.1468-0262.2005.00640.x
• T. Björk, M. Khapko, A. Murgoci, On time-inconsistent stochastic control in continuous time, Finance and Stochastics 21(2), 331–360, 2017. https://arxiv.org/abs/1612.03650
• A. Bismuth, O. Guéant, J. Pu, Portfolio choice, portfolio liquidation, and portfolio transition under drift uncertainty, Mathematics and Financial Economics 13(4), 661–719, 2019. https://arxiv.org/abs/1611.07843
• D. Willett, J. S. W. Wong, On the discrete analogues of some generalizations of Gronwall's inequality, Monatshefte für Mathematik 69(4), 362–367, 1965. https://doi.org/10.1007/BF01297622

Motivation

Heavy-traffic analysis is the standard tool for scheduling queues whose servers are almost always busy: after diffusion scaling, a multiclass queue is approximated by a reflected Brownian motion, and asymptotically optimal policies are read off a limiting control problem. Classical results of this kind, such as the asymptotic optimality of the cµ rule (serve the class with the largest holding cost times service rate first; van Mieghem, 1995), assume that the job-size distributions are known.

In practice the first moments of service times are usually estimated well, while their variability is not. Atar, Castiel and Shadmi study a high-uncertainty regime: the means of the job-size distributions are pinned down to within $O(n^{-1/2})$, but their variances are uncertain at order one, and an adversary chooses them job by job with full knowledge of the past. The scheduler wants to minimize, and the adversary to maximize, a discounted holding cost. The paper solves this game asymptotically: the nonpreemptive cµ policy is asymptotically optimal against every adversary, and the value of the game converges to the value at $0$ of a one-dimensional Hamilton–Jacobi–Bellman (HJB) equation.

Setting

There are $L$ job types and one server. In the $n$-th system one job of each type arrives at each time $k/n$, $k=1,2,\dots$, and the server works at rate $n$, so that a job of size $x$ occupies it for $x/n$ time units. The system starts empty.

Adversary. For each $n$ and type $\ell$ an uncertainty class $\Pi^{\ell n}$, a nonempty closed set of probability distributions on $[0,\infty)$, is given. At each epoch $k/n$ the adversary chooses $\pi^{\ell n}_k\in\Pi^{\ell n}$ for every $\ell$, based on the past job sizes, and the job sizes $J^{\ell n}_k$ are then drawn independently across types from these distributions. The set of such controls is $\mathcal A^n$.

Scheduler. The scheduler chooses the cumulative effort $B^{\ell n}_t$ devoted to each type, an $L$-dimensional Lipschitz path whose increments over $[s,t]$ lie in $(t-s)\cdot\{x\in[0,1]^L:\sum_\ell x_\ell\le 1\}$. An admissible strategy $\beta^n\in\mathbb B^n$ is a measurable, non-anticipating, work-conserving map from the adversary's control path to such an effort path that never serves more work than has arrived.

Cost and value. With $A^{\ell n}_t=\sum_{k\le nt}J^{\ell n}_k$, the workload is $W^{\ell n}_t=A^{\ell n}_t-nB^{\ell n}_t$, the queue length $Q^{\ell n}_t$ is the number of arrived type-$\ell$ jobs not yet completed, and hats denote scaling by $n^{-1/2}$. For holding costs $h^\ell>0$,

$$C^n(\beta^n(a^n),a^n)=\mathbb E\Big[\int_0^\infty e^{-t}\,h\cdot\hat Q^n_t\,dt\Big],\qquad V^n=\inf_{\beta^n\in\mathbb B^n}\sup_{a^n\in\mathcal A^n}C^n(\beta^n(a^n),a^n).$$

Assumptions. With $\xi^\pi$ the mean and $q^\pi$ half the variance of $\pi$, and $b^{\pi\ell n}=n^{1/2}(\xi^\pi-1/\mu^\ell)$, the sets $K^{\ell n}=\{(b^{\pi\ell n},q^\pi):\pi\in\Pi^{\ell n}\}$ converge in the Hausdorff distance to compact sets $K^\ell\subset\mathbb R\times(0,\infty)$; fourth moments are uniformly bounded; $\sum_\ell 1/\mu^\ell=1$ (heavy traffic); and types are labelled so that $h^1\mu^1\le\dots\le h^L\mu^L$, with $h^1\mu^1=1$.

HJB equation. With $H^\ell(v_1,v_2)=\max_{(b,q)\in\mathrm{ch}(K^\ell)}(bv_1+qv_2)$,

$$\sum_{\ell=1}^L H^\ell(u'(w),u''(w))-u(w)+w=0,\quad w\ge0,\qquad u'(0)=0,\quad \limsup_{w\to\infty}|u(w)|/w<\infty .$$

Formalization targets

Goal: Theorem 2.1

$$V^n\longrightarrow u(0)\qquad(n\to\infty),$$

for the classical solution $u$ of the HJB equation. The paper states $V^n\to\mathsf V(0)=u(0)$ with $\mathsf V$ the value of a martingale control problem; the goal uses the $u(0)$ form, which leaves the martingale problem out of the statement.

Milestones

• β*ⁿ ∈ 𝔹ⁿ: the nonpreemptive cµ strategy is admissible.
• Lemma 2: the total workload does not depend on the strategy.
• Lemma 3: second moments of the scaled workload and queue length grow at most like $(t+1)^2$, uniformly in $n$, the control and the strategy.
• Lemma 4: $\hat Q^{\ell n}-\mu^\ell\hat W^{\ell n}\to0$ uniformly in probability over strategies (the snapshot principle).
• Lemma 5: under the cµ policy the workload of types $2,\dots,L$ vanishes.
• Theorem 1: $\inf_{\beta^n}C^n(\beta^n(a^n),a^n)-C^n(\beta^{*n}(a^n),a^n)\to0$ for every adversary.
• Proposition 1.1: the HJB equation has a unique classical solution. Proposition 1.3: it is nonnegative, non-decreasing and convex.
• (47): $\limsup_nC^n(\beta^{*n}(a^n),a^n)\le u(0)$ for every control sequence.
• Theorem 2.2: measurable selectors $\psi^{\ell n}$ attaining the prelimit Hamiltonian.
• (55): for the feedback control $\pi^{\ell n}_k=\psi^{\ell n}(\mathsf W^n_{k-1})$, $u(0)\le\liminf_nC^n(\beta^{*n}(a^{*n}),a^{*n})$.

Significance

The result gives the first-order asymptotics of a scheduling game with model uncertainty: the scheduler loses nothing by ignoring the adversary and using the cµ rule, and the adversary's best response is a state-feedback choice of drift and variance determined by $u'$ and $u''$. Theorem 1 is a robustness statement for one of the most widely used scheduling rules; Theorem 2 reduces a game on path space to a scalar nonlinear ODE.

The paper's proofs are complete, so the remaining work is formalization. No part of this result, and none of its objects (heavy-traffic queues with adversarial service distributions, the nonpreemptive cµ policy as a map on path space, the HJB equation of a reflected controlled diffusion), has a known machine-checked statement or proof.

Difficulty

The statement is a limit of a real sequence, but each term is an infimum over measurable, causal, work-conserving maps on path space of a supremum over feedback choices of distributions. The proofs (§§4–7 and the appendix) use uniform C-tightness of prelimit processes, weak convergence in $D[0,\infty)$, the existence theory for fully nonlinear uniformly elliptic equations (Gilbarg–Trudinger, Thm 17.18), martingale characterizations of limits (Jacod–Shiryaev, Cor. VI.6.30; Karatzas–Shreve, Thm 5.5.15), measurable selection (Budhiraja–Dupuis, Lemma 8.10), and Taylor expansion of $u$ along the prelimit workload. The obvious route through the uncontrolled diffusion limit fails because the adversary's variance choice is state dependent, so no single limiting Brownian motion describes all adversaries; the limit is a control problem, not a process.

Formalization scope

The Lean development lives in the namespace HighUncertHT.Game. Types are Fin L, 0-based (the paper's type 1 is index 0). Distributions are ProbabilityMeasure ℝ with no mass on $(-\infty,0)$, with the weak topology. Systems are indexed by $n\ge1$; the class at $n=0$ is required to satisfy the same conditions so that control sequences indexed by $\mathbb N$ exist. Costs and values are in $[0,\infty]$ (lower Lebesgue integrals), sup norms are in $[0,\infty]$, the Hausdorff distance is the extended one, and derivatives of $u$ are one-sided on $[0,\infty)$.

An adversary control is encoded by its feedback map from past job sizes to distributions and the measurable Markov kernel it induces; its law is the Ionescu–Tulcea trajectory measure. By (5), the Doob–Dynkin lemma and (7), this has the same laws, hence the same costs, as the paper's $\mathcal A^n$. Strategies are measurable for the product σ-algebras. The cµ strategy $\beta^{*n}$ is defined explicitly by an event recursion over service decisions.

The standing assumptions (Assumptions 1–2, labelling (14), $h^1\mu^1=1$) are fields of the Setting and hold in every statement. Corrected printed slips: the priority rule serves the highest index (p. 9 prints "lowest", contradicting the cµ rule and Lemma 5); the departure count is capped at the number of arrived jobs (p. 6); "→ 0 in probability" for processes is read as convergence of the sup norm on compact intervals (Lemma 5); (55) is stated for the control (61), not (15).

Trivializing formalizations are ruled out: $\mathbb B^n$ is nonempty because $\beta^{*n}\in\mathbb B^n$ is a milestone; the HJB has a classical solution (Proposition 1.1), so the goal is not vacuous; no expectation is a Bochner integral that could vanish for non-integrable integrands; $u'$ is not a junk deriv; and (55) asserts that its feedback control exists.

Needed infrastructure: diffusion-scaled processes and their tightness in $D[0,\infty)$, the one-dimensional Skorokhod map and its Lipschitz property, martingale estimates for sums of conditionally centred job sizes, and the existence theory for the HJB equation. The Skorokhod map, the queue primitives and the cµ policy are reusable for other heavy-traffic missions. Contributions on any milestone, or on general lemmas they need, are welcome. Not included: Lemmas 1, 6, 7, 8, Proposition 1.2, Proposition 2, Theorem 2.3 and the martingale control problem.

Selected references

• R. Atar, E. Castiel, Y. Shadmi, Scheduling in the High Uncertainty Heavy Traffic Regime, Mathematics of Operations Research, 2025; preprint arXiv:2204.05733v1, 2022. https://arxiv.org/abs/2204.05733v1
• J. A. van Mieghem, Dynamic scheduling with convex delay costs: the generalized cμ rule, Annals of Applied Probability 5(3), 1995. https://doi.org/10.1214/aoap/1177004702
• M. I. Reiman, Some diffusion approximations with state space collapse, in Modelling and Performance Evaluation Methodology, Springer LNCIS 60, 1984. https://doi.org/10.1007/BFb0005161
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer, 2001. https://doi.org/10.1007/978-3-642-61798-0
• A. Budhiraja, P. Dupuis, Analysis and Approximation of Rare Events, Springer, 2019. https://doi.org/10.1007/978-1-4939-9579-0