All missions

Motivation

Sampling from a Gibbs distribution $\pi_U\propto e^{-U}\,d\lambda_d$ on $\mathbb R^d$ is a basic task in Bayesian statistics, statistical physics and machine learning. A standard approach simulates the Langevin diffusion $dX_t=-\nabla U(X_t)\,dt+\sqrt2\,dB_t$, whose invariant distribution is $\pi_U$, through its Euler scheme, and averages a test function $f$ along one long trajectory. The discretization introduces a bias of the order of the step size, so a single-step-size average with accuracy $\varepsilon$ costs more than $\varepsilon^{-2}$ steps. Dalalyan (arXiv:1412.7392) and Durmus–Moulines (arXiv:1605.01559) quantified this for strongly log-concave targets; for occupation measures of the Euler scheme the best previous bound was of order $d\varepsilon^{-4}$ (Durmus–Moulines, Bernoulli 2019, denoted [DM19] in the paper).

Egéa and Panloup (arXiv:2109.07753, Math. Oper. Res., 2025) combine Giles's multilevel Monte Carlo idea (Oper. Res. 2008) with pathwise averages. Each level is one long trajectory, not many independent samples. This mission formalizes their result for a uniformly strongly contractive, twice differentiable drift. In that case the multilevel occupation measure reaches accuracy $\varepsilon$ at a cost of order $d\varepsilon^{-2}$, the order of an unbiased Monte Carlo method.

Setting

Let $b:\mathbb R^d\to\mathbb R^d$ be $L$-Lipschitz and satisfy Assumption $(\mathbf C_\alpha)$: $\langle b(y)-b(x),y-x\rangle\le-\alpha|x-y|^2$ for all $x,y$, with $\alpha\in(0,L\wedge1]$. Let $\sigma>0$. The additive diffusion is $X^x_t=x+\int_0^tb(X^x_s)\,ds+\sigma B_t$, driven by a standard $d$-dimensional Brownian motion $B$. Let $\pi$ be its invariant distribution. Its Euler scheme with step $\gamma$ is $\bar X^{\gamma,x}_0=x$, $\bar X^{\gamma,x}_{(n+1)\gamma}=\bar X^{\gamma,x}_{n\gamma}+\gamma b(\bar X^{\gamma,x}_{n\gamma})+\sigma(B_{(n+1)\gamma}-B_{n\gamma})$, with invariant distribution $\pi^\gamma$. Write $\underline s_\eta=\eta\lfloor s/\eta\rfloor$ and $[f]_1$ for the Lipschitz constant of $f$.

Given a first step $\gamma_0$, steps $\gamma_r=\gamma_02^{-r}$, horizons $T_0>\dots>T_R$, a warm start $\tau$, and independent Brownian motions $B^{(0)},\dots,B^{(R)}$, the multilevel occupation measure (7) is

$$\mathcal Y(f)=\frac1{T_0-\tau}\int_\tau^{T_0}f(\bar X^{\gamma_0}_{\underline s_{\gamma_0}})ds+\sum_{r=1}^R\frac1{T_r-\tau}\int_\tau^{T_r}\big(f(\bar X^{\gamma_r}_{\underline s_{\gamma_{r-1}}})-f(\bar X^{\gamma_{r-1}}_{\underline s_{\gamma_{r-1}}})\big)ds,$$

where both schemes of level $r$ start at $x_0$ and are driven by $B^{(r)}$. Its cost is $\mathcal C(\mathcal Y)=T_0/\gamma_0+\sum_{r=1}^R(T_r/\gamma_r+T_r/\gamma_{r-1})$.

When $b$ is $\mathcal C^2$ with bounded derivatives, set $\|\nabla b\|_{2,\infty}=\sup_x\|\nabla b(x)\|_F$ (Frobenius norm of the Jacobian) and $\|\Delta b\|^2_{2,\infty}=\sup_x\sum_i|\Delta b_i(x)|^2$. The constant (19) is

$$\Upsilon_2^2=\max\Big(1,\ \frac{|b(x_0)|^2}{\alpha^2}+\frac{\sigma\sqrt\alpha}{L^3}\|\nabla b\|_{2,\infty}|b(x_0)|+\frac{\sigma^4}{L^4}\|\Delta b\|^2_{2,\infty}+\frac{\sigma^2\alpha\sqrt d}{L^3}\|\nabla b\|_{2,\infty}+\frac{\sigma^2d}{\alpha}\Big).$$

Formalization targets

Goal: Theorem 2.3

Take $\gamma_0\in(0,\frac\alpha{2L^2}\wedge\frac12]$, $R_\varepsilon=\lceil\log_2(\Upsilon_2/\varepsilon)\rceil$, $T_r=\Upsilon_2^2\log(\gamma_0^{-1})\alpha^{-1}\varepsilon^{-2}2^{-3r/2}$ and $\tau=\alpha^{-1}|\log\varepsilon|+(2\alpha)^{-1}\log\Upsilon_2$. There is a universal constant $\mathfrak C_1$ such that for every $\varepsilon\in(0,1)$ with $\sqrt2\log(\Upsilon_2\varepsilon^{-2})\le\log(\gamma_0^{-1})(\Upsilon_2/\varepsilon)^{1/2}$,

$$\|\mathcal Y(f)-\pi(f)\|_2\le\mathfrak C_1[f]_1\varepsilon,\qquad\mathcal C(\mathcal Y)\le\frac{\frac12+\sqrt2}{\sqrt2-1}\,\frac{\Upsilon_2^2\log(\gamma_0^{-1})}{\gamma_0\alpha}\,\varepsilon^{-2}.$$

The constant $\mathfrak C_1$ is the same for all $d$, $b$, $\sigma$, $f$, $x_0$, $\gamma_0$ and $\varepsilon$.

Companion: (22)

Under $\alpha/L^2\le1$, $\sigma^2\alpha^{-1}d\ge1$ and dimension-free bounds on $|b(x_0)|$, $\|\nabla b\|_{2,\infty}$ and $\|\Delta b\|_{2,\infty}$, the choice $\gamma_0=\alpha/(2L^2)$, $\tilde\Upsilon_2^2=\sigma^2\alpha^{-1}d$ gives $\mathcal C(\mathcal Y)\le\frac{2\sqrt2+1}{\sqrt2-1}\frac{\sigma^2L^2}{\alpha^3}\log\frac{2L^2}{\alpha}\,d\varepsilon^{-2}$.

Milestones

The milestones follow the paper's proof in order:

• Lemma 5.1 (i), (iii): stability of the scheme and the assumptions $(\mathbf H_1)$, $(\mathbf H_4)$.
• Lemma 5.2 (ii): a one-step error of order $\gamma^3$.
• Proposition 5.1 (ii), (iii): a uniform-in-time strong error $\beta_2(x)\gamma^2$ and $(\mathbf H_2)$ with $\mathfrak a=2$.
• Proposition 5.2: $\mathcal W_1(\pi,\pi^\gamma)\le\sqrt{\beta_2(x^\star)}\gamma$.
• Proposition 2.2: $(\mathbf H_2)$–$(\mathbf H_4)$ with constants controlled by $\Upsilon_2$.
• Remark 4.1: the paper's general complexity theorem, with constants known up to universal factors.

Significance

The result. Theorem 2.3 gives an explicit algorithm whose cost to reach $L^2$ accuracy $\varepsilon$ on $\pi(f)$ is of order $\varepsilon^{-2}$, uniformly over Lipschitz $f$. Under (22) the cost is $O(d\varepsilon^{-2})$. Apart from constants depending on $\alpha$ and $L$, this is the complexity of a Monte Carlo method without bias, an improvement over the $d\varepsilon^{-4}$ known for single-level occupation measures. Corollary 2.2 of the paper applies it to Gibbs distributions with a $\mathcal C^3$ potential.

Formalizing it. The theorem is proved in the paper. A machine-checked version needs a formal multilevel estimator over infinite horizons, uniform-in-time strong error bounds for the Euler scheme, and an application of Itô's formula to $b(y+\sigma B_t)$, none of which exists in Lean. Formalizing also checks the paper's constants. For instance, the printed exponential rate in the $\mathcal W_2$ contraction behind $(\mathbf H_1)$ is $\alpha$, while its proof gives $\alpha/2$, and the milestone states $\alpha/2$. No part of this result has been machine-checked.

Difficulty

Two steps resist a direct approach. First, the order-one strong error (Lemma 5.2(ii), Proposition 5.1(ii)). Bounding the one-step error by the Lipschitz constant alone gives order $\gamma^2$ per step, hence order $\gamma^{1/2}$ globally; this is Lemma 5.2(i) and the $\mathfrak a=1$ regime, with an extra $\log^3\varepsilon$ in the cost. The gain to $\gamma^3$ needs the second-order structure of $b$ along the Brownian path, through a martingale term and the Laplacian of $b$. Second, the error must be controlled uniformly over infinite horizons. Every estimate has to combine the contraction $(\mathbf C_\alpha)$ with the step-size restriction $\gamma\le\alpha/(2L^2)$; a Gronwall argument on a finite horizon gives constants that grow with time.

For the goal itself, the cost bound (21) is arithmetic once the parameters are fixed. The content is the error bound with a constant that is universal, not merely independent of $\varepsilon$.

Formalization scope

• $\mathbb R^d$ is the published EthierKurtz.SDEState d, and Brownian motions are the published EthierKurtz.IsStandardBrownian.
• The diffusion is a pathwise solution of $X_t=x+\int_0^tb(X_s)ds+\sigma W_t$ with continuous paths. No stochastic integral appears in any statement.
• $\pi$ is a probability measure invariant for the diffusion's transition laws. $\pi^\gamma$ is any probability invariant for the Euler step $x\mapsto x+\gamma b(x)+\sigma\sqrt\gamma Z$, with $Z$ standard Gaussian.
• $\|\cdot\|_2$ is eLpNorm · 2 P, valued in $[0,\infty]$. The schemes are evaluated at grid times, except in $(\mathbf H_4)$ and (47), which use the continuous-time scheme.
• $\mathcal C^2$ with bounded partial derivatives is ContDiff ℝ 2 b plus a uniform bound on the first and second Fréchet derivatives.
• $\|\nabla b\|_{2,\infty}$ and $\|\Delta b\|^2_{2,\infty}$ follow pp. 31–32, which correct the misplaced squares of (18).
• "$\lesssim_{uc}$" is an existential constant quantified before every datum.
• The $\varepsilon_0$ of Theorem 2.3 is read as membership in its defining set.
• The cost formula is used for every $T_r$.
• Added hypotheses: $\sigma>0$ wherever the page leaves it implicit; $\mathcal C^2$ regularity in Lemma 5.2(ii) and Propositions 5.1–5.2; $\gamma<1$ in Proposition 5.2; $d\ge1$ in Proposition 5.1(iii); $\alpha\le1$ in Proposition 2.2.

The goal does not assume $(\mathbf H_1)$–$(\mathbf H_4)$, Proposition 2.2 or any variance or bias estimate. It assumes only $(\mathbf C_\alpha)$, Lipschitz and $\mathcal C^2$ regularity of $b$, $\sigma>0$, invariance of $\pi$ and the parameter choices. Those results appear only as milestones.

Contributions that would be reusable elsewhere: uniform-in-time moment and strong-error bounds for Euler schemes of contractive SDEs, Itô's formula for a $\mathcal C^2$ function of Brownian motion, and the general multilevel complexity theorem (Remark 4.1). Proofs of the milestones are welcome independently.

Selected references

• M. Egéa, F. Panloup, Multilevel-Langevin pathwise average for Gibbs approximation, Math. Oper. Res., 2025; arXiv:2109.07753v2. https://arxiv.org/abs/2109.07753
• M. B. Giles, Multilevel Monte Carlo path simulation, Oper. Res. 56(3), 2008. https://doi.org/10.1287/opre.1070.0496
• A. Durmus, É. Moulines, High-dimensional Bayesian inference via the unadjusted Langevin algorithm, Bernoulli 25(4A), 2019. https://doi.org/10.3150/18-BEJ1073
• A. S. Dalalyan, Theoretical guarantees for approximate sampling from smooth and log-concave densities, J. R. Stat. Soc. B 79(3), 2017. https://arxiv.org/abs/1412.7392
• A. Durmus, É. Moulines, Nonasymptotic convergence analysis for the unadjusted Langevin algorithm, Ann. Appl. Probab. 27(3), 2017. https://arxiv.org/abs/1507.05021

Motivation

In a principal–agent problem with moral hazard, a principal (an employer) pays an agent whose effort she cannot observe; she sees only an output process whose drift the effort controls. Continuous-time versions of the problem, starting with Holmström–Milgrom (1987) and Sannikov (2008), are solved by turning the agent's continuation utility into a state variable and writing a Hamilton–Jacobi–Bellman (HJB) equation for the principal's value.

Most of this literature assumes two-sided commitment: the agent cannot leave. In labour markets the agent can quit whenever an outside offer beats his continuation utility, and the principal must then hire someone else. Zhang and Zhu (arXiv:2208.06473; Mathematics of Operations Research, 2025) study this one-sided commitment: the principal is committed to the contract, the agent is free to quit at a stopping time of his choice, and after each quitting the principal pays a cost and hires a new agent, possibly of another type. The principal's value then depends on every future hire, and the paper characterises it by a coupled system of HJB equations.

Setting

Fix a horizon $T>0$ and a payment cap $C_0>0$. A standard Brownian motion $B$ on $(\Omega,\mathcal F,\mathbb P)$ is the output. Agents have types $\theta\in\Theta$. An agent of type $\theta$ receiving a payment rate $\eta\le C_0$ and exerting effort $\alpha$ has running utility $f(\theta;s,\eta)$ and running cost $h(\theta;s,\alpha)$; $f$ is increasing and concave in $\eta$, $h$ is convex in $\alpha$ (Assumption 2.2). Effort shifts the drift of $B$ through the Girsanov measure $\mathbb P^\alpha$ (weak formulation). The agent's optimal effort against a sensitivity process $Z$ is $\alpha=I^h(\theta;\cdot,Z)$, the inverse of $\partial_\alpha h$, and $\mathbb E^{\theta,Z}$ denotes expectation under the corresponding measure.

A contract started at time $t$ is described in forward form by $(\eta,Z)$: the agent's continuation utility is

$$\mathcal X^{\theta;t,x,\eta,Z}_s=x-\int_t^s\big[f(\theta;r,\eta_r)+H(\theta;r,Z_r)\big]dr+\int_t^sZ_r\,dB_r,$$

with $H(\theta;s,z)=\sup_\alpha[\alpha z-h(\theta;s,\alpha)]$ and the constraint $\mathcal X_T=0$. The agent's utility is capped by the upper barrier $\overline L^\theta_t=\int_t^Tf(\theta;s,C_0)\,ds$. He quits at the first time $\mathcal X$ reaches the lower barrier $\underline L^\theta_t=R^\theta_t-c^\theta_t$, where $R^\theta$ is his market value and $c^\theta\ge1/\Lambda_0$ his quitting cost (Assumptions 2.7, 3.1). The relevant domain is

$$D_\theta=\{(t,x):0\le t<T,\ \underline L^\theta_t<x\le\overline L^\theta_t\}.$$

When the $i$-th agent quits at $\tau_i<T$, the principal pays $c^P_{\tau_i}$ and hires an agent of type $\zeta_{\tau_i}$ at utility $R^{\zeta_{\tau_i}}_{\tau_i}$ (the quitting sequence (5.8)). The principal's value is

$$u_\infty(\theta;t,x)=\sup_{(\eta,Z,\zeta)}\mathbb E^{\zeta,Z}\Big[\int_t^T\big[I^h(\zeta_s;s,Z_s)-\eta_s\big]ds-\sum_{i\ge1}c^P_{\tau_i}\mathbf 1_{\{\tau_i<T\}}\Big],$$

and the value of the best new hire at time $t$ is $\overline u_\infty(t)=\sup_\theta u_\infty(\theta;t,R^\theta_t)-c^P_t$.

Formalization targets

Goal: Theorem 6.3

The family $\{u_\infty(\theta;\cdot,\cdot)\}_{\theta\in\Theta}$ is the minimal continuous viscosity solution of

$$\partial_tu+\sup_{\eta\le C_0,\ z\in\mathbb R}\Big[\tfrac12|z|^2\partial_{xx}u-\big[f(\theta;t,\eta)+\tilde H(\theta;t,z)\big]\partial_xu+I^h(\theta;t,z)-\eta\Big]=0\quad\text{on }D_\theta,\ \theta\in\Theta,$$

with boundary conditions

$$u(\theta;t,\overline L^\theta_t)=-C_0(T-t),\qquad u(\theta;T-,x)=0,\qquad u(\theta;t,\underline L^\theta_t+)\ge\sup_{\theta'}u(\theta';t,R^{\theta'}_t)-c^P_t.$$

The last condition couples the equations for different types. The goal also asserts that the value sets in (6.1) are nonempty and bounded above, so that $u_\infty$ is a genuine real-valued function.

Milestones

1. Lemma 3.4: explicit contracts with $\int_t^T[C_0-\eta_s]ds\le\delta$ under which the agent never quits.
2. Lemma 2.5 (2.20): a priori estimates for admissible contracts.
3. Proposition 2.8 and Lemma 3.6: the self-enforcing value $V^P_0$ and the new-hire value $\overline u_0$ are uniformly continuous with modulus $C\sqrt\rho$.
4. Theorem 4.5: with at most one quitting, $u_1$ is the minimal continuous viscosity solution of the same equation with boundary datum $\overline u_0$.
5. Proposition 5.4: a non-recursive representation of $u_n$ (at most $n$ quittings).
6. Proposition 6.1: $\mathbb P^{\zeta,Z}(\tau_n<T)\le C/n$, and $|u_n-u_\infty|\le C/n$.
7. Proposition 6.2: monotonicity and uniform continuity of $u_\infty$, regularity of $\overline u_\infty$, and the boundary conditions.
8. (6.7): the dynamic programming principle for $u_\infty$.

Significance

The theorem identifies the principal's value under one-sided commitment as a PDE object, which makes it computable and comparable with other contracting regimes. Along the way the paper shows that the principal sees only finitely many quittings (Proposition 6.1) and that tolerating more quittings never lowers her value, so contracts that prevent quitting altogether (self-enforcing contracts) are in general suboptimal. The coupling through $\overline u_\infty$ turns the problem into an infinite system of HJB equations indexed by agent types, a structure that also appears in switching and re-hiring problems.

The result is proved in the paper; none of it is formalized. A formalization would add to the platform a continuous-time moral-hazard model in the weak formulation, hitting-time stopping driven by an Itô integral, a quitting sequence with random restarts and type switching, and a viscosity-solution notion for a fully nonlinear HJB equation on a time-dependent domain. The paper's own proof leaves several steps to the reader (the dynamic programming principle, the viscosity property, comparison for a truncated equation), so a complete development would also supply these.

Difficulty

The obvious route is "dynamic programming principle, then viscosity property, then comparison". Each step is harder here than in a textbook control problem. The control $z$ is unbounded, so the Hamiltonian can be $+\infty$ and the viscosity property must be derived without a finite Hamiltonian. The process is stopped at a hitting time of a moving barrier and restarted at a random level with a new type, so the dynamic programming principle must handle restarts. Minimality cannot come from a standard comparison principle, because the boundary datum at $\underline L^\theta$ depends on the competitor itself and no growth condition is imposed on competitors; the paper argues through approximation by $u_n$ and Theorem 4.5 instead.

Formalization scope

All objects are defined in the namespace DynPrincipalAgent.HJB. Process time is $\mathbb R_{\ge0}$; deterministic data are functions of real time. The Itô integral is the published Peng1990.SMP.IsItoIntegral, with a continuous version required wherever hitting times read paths. Controls started at $t$ are progressively measurable for the filtration $\mathbb F^t$ of $B_s-B_t$. Value functions are real suprema of value sets that record an expectation only when it is genuine (integrable payoffs, almost surely integrable drifts and running rewards, summable quitting costs); these conditions hold for every admissible control.

Pinned readings, all disclosed in the items: viscosity solutions are the standard Crandall–Ishii–Lions notion with $C^2$ test functions on $\mathbb R^2$, tested on the interior of $D_\theta$, with the supremum in the HJB operator never formed; the boundary condition at $\underline L^\theta$ requires a real right limit compared against every $u(\theta';t,R^{\theta'}_t)-c^P_t$; $\Theta$ carries a σ-algebra and $f$, $h$, $\partial_\alpha h$ are jointly measurable; Assumption 2.7 (ii) is read as $|R^\theta_s-R^\theta_{s'}|\le\rho(|s-s'|)$; a modulus of continuity is nondecreasing, vanishes at $0^+$ and satisfies $\rho(\delta)\ge\delta$; generic constants depend only on $(T,C_0,\Lambda_0,\Lambda_1)$ and are fixed before the model; $H$ and $\tilde H$ take the closed forms of (2.11)–(2.12). The agent's BSDE and reflected BSDE (Propositions 2.3, 3.2), §7's standard contracts and the economic interpretation of $R^\theta$, $c^\theta$, $c^P$ are out of scope.

A formalization in which a value function equals a junk value (an empty or unbounded real supremum, a Bochner integral of a non-integrable payoff, a hitting time of an empty set) or in which the viscosity notion is vacuous does not count: the goal states that the value sets are nonempty and bounded, and the definitions avoid junk by construction. Competitors in the minimality clause satisfy exactly the printed boundary conditions, with no added growth bound.

Reusable infrastructure: Girsanov measures for BMO drifts, forward utility processes, hitting times of continuous semimartingales, and viscosity solutions of HJB equations on non-cylindrical domains. Contributions on any milestone, and on general lemmas such as the dynamic programming principle for controlled diffusions stopped at hitting times, are welcome.

Selected references

• J. Zhang, Z. Zhu, A Dynamic Principal Agent Problem with One-sided Commitment, Mathematics of Operations Research, 2025. Preprint arXiv:2208.06473v3. https://arxiv.org/abs/2208.06473
• Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008). https://doi.org/10.1111/j.1467-937X.2008.00486.x
• B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987). https://doi.org/10.2307/1913238
• M. G. Crandall, H. Ishii, P.-L. Lions, User's guide to viscosity solutions of second order partial differential equations, Bull. AMS 27 (1992). https://doi.org/10.1090/S0273-0979-1992-00266-5

Motivation

Mean-variance (MV) preferences, $U_\theta(X)=\mathbb E[X]-\frac\theta2\mathrm{Var}(X)$, are the standard objective of portfolio selection since Markowitz. They are not monotone: an investor can prefer a terminal wealth $X$ to a wealth $X'\ge X$ that is larger in every state, because the extra upside raises the variance. Monotone mean-variance (MMV) preferences (Maccheroni, Marinacci, Rustichini and Taboga, 2009) repair this. They are the largest monotone preferences that agree with MV preferences on the domain of monotonicity $\mathcal G_\theta=\{f\in\mathcal L^2:f-\mathbb E[f]\le1/\theta\}$.

A natural question is when switching from MV to MMV changes the optimal investment. In continuous-time markets driven only by Brownian motions, the optimal strategies under the two preferences coincide (Trybuła and Zawisza, 2019, for a stochastic factor model; Strub and Li, 2020, for continuous semimartingale markets), and whether this persists with jumps was left open by Trybuła and Zawisza. Li, Liang and Pang study a market whose risky asset also jumps and whose coefficients depend on a stochastic factor. They show that the two problems agree if and only if a pathwise condition on the jumps, Assumption 1, holds.

Setting

On a probability space $(\Omega,\mathcal F,\mathbb P)$ live two independent Brownian motions $W^1,W^2$ and an independent Poisson random measure $N(\mathrm ds,\mathrm dp)$ with finite Lévy measure $\nu$ and compensated measure $\tilde N$. The filtration $\{\mathcal F_t\}$ is generated by $W^1,W^2,N$. A stochastic factor follows

$$\mathrm dZ_s=a(Z_s)\,\mathrm ds+b(Z_s)(\rho_W\,\mathrm dW^1_s+\bar\rho_W\,\mathrm dW^2_s),\qquad Z_t=z,$$

with $\rho_W^2+\bar\rho_W^2=1$. Investing the amount $\pi_s$ in the risky asset gives the (discounted) wealth

$$\mathrm dX^\pi_s=\pi_s(\mu(Z_s)-r)\,\mathrm ds+\pi_s\sigma(Z_s)\,\mathrm dW^1_s+\pi_s\int_{\mathbb R}\gamma(Z_s,p)\,\tilde N(\mathrm ds,\mathrm dp),\qquad X_t=x,$$

on $[t,T]$, with $\gamma>-1$. Write $\Sigma(z)=\sigma(z)^2+\int\gamma(z,p)^2\nu(\mathrm dp)$ and $\lambda(z)=(\mu(z)-r)^2/\Sigma(z)$.

The MMV preference is

$$V_\theta(X)=\inf_{\mathbb Q}\Big\{\mathbb E^{\mathbb Q}[X]+\frac1{2\theta}\Big(\mathbb E^{\mathbb P}\Big[\Big(\frac{\mathrm d\mathbb Q}{\mathrm d\mathbb P}\Big)^2\Big]-1\Big)\Big\}.$$

The infimum runs either over the Doléans-Dade measures $\mathcal Q^t$ or over all of $\mathcal Q_0=\{\mathbb Q\ll\mathbb P:\mathbb E[(\mathrm d\mathbb Q/\mathrm d\mathbb P)^2]<\infty\}$. A measure in $\mathcal Q^t$ has density $\mathcal E_T$, where $\mathcal E$ is the stochastic exponential of $\int\eta_1\mathrm dW^1+\int\eta_2\mathrm dW^2+\int\!\int\phi\,\mathrm d\tilde N$ with $\mathcal E_T\ge0$, $\mathbb E[\mathcal E_T]=1$ and $\mathcal E_T\in L^2$.

The optimal utilities from $(x,z,t)$ are suprema over the admissible strategies of the paper's Definitions 2 and 3: predictable $\pi$ whose wealth has $\mathbb E[\sup_s|X^\pi_s|^2]<\infty$, under $\mathbb P$ for MV and under every $\mathbb Q\in\mathcal Q^t$ for MMV. Both solutions are expressed through the solution $G=-e^F$ of the nonlinear parabolic PDE (20),

$$G_t+\alpha(z)G_z+\tfrac12b(z)^2G_{zz}-\beta(z)b(z)^2\frac{G_z^2}{G}+\lambda(z)G=0,\qquad G(z,T)=-1.$$

Through $\zeta(z,s)=-(\mu(z)-r-\sigma(z)b(z)\rho_WG_z/G)/\Sigma(z)$ it also enters Assumption 1. Let $\tau$ be the first jump time after $t$ at which $\zeta(Z_s,s)\gamma(Z_s,\Delta L_s)=-1$. Assumption 1 requires $\zeta\gamma\ge-1$ at every jump in $(t,T]$ up to time $\tau$.

Formalization targets

Goal: Theorem 9

$$\sup_{\pi\in\mathcal B_{x,z,t}}U_\theta(X^\pi_T)=\sup_{\pi\in\mathcal A_{x,1/(2\theta),z,t}}V_\theta(X^\pi_T)\iff\text{Assumption 1 holds at }(z,t).$$

The same holds when $V_\theta$ ranges over $\mathcal Q_0$ instead of $\mathcal Q^t$.

Milestones

1. Theorem 3 links the market player's density process to the wealth: $2Y_sG(Z_s,s)=X^{\pi^*}_s-x+2yG(z,t)$.
2. Theorem 4 solves the MMV problem: the value is $V(x,y,z,t)=-x+G(z,t)y$, with an explicit saddle point.
3. Theorem 6 solves the auxiliary quadratic problem: $U_D(x,z,t)=-(x-D)^2/G(z,t)$.
4. Theorem 7 gives the Lagrange multiplier and the optimal target.
5. (39) gives the optimal MV strategy.
6. The moment identities $\mathbb E[R_T]=\mathbb E[R_T^2]=H(z,t)=-1/G(z,t)$.
7. Theorem 8: under Assumption 1 the optimal strategies coincide.
8. Lemma 4: the optimal MV wealth lies in $\mathcal G_\theta$ if and only if Assumption 1 holds.
9. (44)–(45): the mean and variance of the optimal wealth.

Significance

The result separates the two preferences by an observable property of the market. The Brownian theory gives agreement for free. With jumps the MV-optimal wealth can leave $\mathcal G_\theta$, and that happens exactly when a jump of size $\zeta\gamma<-1$ can occur before the first jump with $\zeta\gamma=-1$. In that case MMV and MV investors hold different portfolios. The paper's §5.4 examines in market data whether Assumption 1 is reasonable. The explicit closed forms (the value $-x+G(z,t)y$, the variance $-(G(z,t)+1)/\theta^2$ of the optimal wealth, the efficient frontier) are what applied work uses.

The result is proved on paper, in an arXiv preprint later published in Mathematics of Operations Research (2025). None of it is machine-checked. A formal proof would check the verification arguments for a stochastic differential game with jumps, a Feynman–Kac representation with a jump density, and the comparison with Maccheroni et al.'s monotone hull. The paper's own proofs are brief at several of these steps. The underlying infrastructure (Itô calculus with Poisson jumps, Doléans-Dade exponentials, verification theorems) would be reusable for most of continuous-time portfolio theory.

Difficulty

The obvious argument would show $U_\theta=V_\theta$ along the optimal wealth and conclude. Lemma 4 shows this argument breaks: the optimal MV wealth need not lie in $\mathcal G_\theta$. Remark 7 also notes that membership in $\mathcal G_\theta$ alone does not identify the optimal values; both optimal strategies must be found and compared.

Finding them needs a verification theorem for a two-player stochastic differential game with jumps (Theorems 1 and 4). That in turn needs Itô's formula for jump diffusions and martingale properties of Doléans-Dade exponentials that may vanish (Lemma 2, Mémin's criterion). Identifying the two strategies needs the moment identities $\mathbb E[R_T]=\mathbb E[R_T^2]=H$, which come from a Feynman–Kac argument with a jump-driven density (Lemma 3). The converse direction needs a stopping argument at the first "bad" jump. None of this exists in Mathlib, which has Brownian motion but no stochastic integral and no Poisson process.

Formalization scope

• Time is $[0,\infty)$; every process lives on $[t,T]$ with $t<T$, and $\int_t^s$ is a difference of integral processes whose integrands vanish before $t$.
• Brownian integrals are the $L^2$ Itô integrals of Peng1990.SMP.Stochastic. The admissible classes $\mathcal A$, $\mathcal B$, $\mathcal M^t$ therefore contain only strategies whose Brownian integrands are in $L^2$; all strategies used in the paper qualify.
• The Poisson random measure is JacodTodorov10.LLN.IsFPoisson with $\nu$ finite and $\nu(\{0\})=0$. The compensated integral is the pathwise sum over atoms minus the compensator integral.
• The filtration is the natural (uncompleted) filtration of $(W^1,W^2,N)$.
• Processes are adapted with càdlàg paths; $X_{s-}$ is Mathlib's Function.leftLim. Feedback strategies come with an existence claim, never as bare assumptions.
• All optimal values are infima/suprema in EReal over the full admissible classes. Measures in $\mathcal Q_0$ are probability measures.
• $\mathcal M^t$ is defined by the defining equation (5) of the stochastic exponential. The printed formula (4) has $\Delta X$ where $\Delta M$ is meant and is not used.
• Proposition 1 is not formalized: its hypotheses do not deliver a classical solution. $G$ is a hypothesis: $G=-e^F$ with $F$ bounded, $C^{2,1}$ with bounded derivatives, solving (20). The Conditions of Proposition 1 are kept as printed. $\Sigma,\lambda,\beta>0$ is a standing hypothesis (implicit on p. 12).
• Assumption 1 uses $\tau$ in $[0,\infty]$ ($\inf\emptyset=\infty$), and "a.s." holds simultaneously for all $s\in(t,T]$.
• Printed slips: (37) evaluates $G_z/G$ at $(Z_s,t)$; it is read at $(Z_s,s)$. Lemma 4's "Equation (1)" means (20)/(21).
• Divisions by $1-\mathbb E[R_T]$ and $\mathrm{Var}[R_T]$ carry the hypotheses $\mathbb E[R_T]\neq1$, $\mathrm{Var}[R_T]>0$.

A formalization that replaces either optimal utility by a closed form or by the utility of one fixed strategy is out of scope: it assumes Theorems 4 and 7 and empties the goal. So is one that removes the jumps, freezes the factor, or replaces Assumption 1 by a sufficient condition such as $\gamma\ge0$; each of these makes the "only if" vacuous or false. Contributions that build general infrastructure (an Itô formula for jump diffusions, Doléans-Dade exponentials, a Feynman–Kac theorem) are especially welcome.

Selected references

• B. Li, Z. Liang, L. Pang, Comparison Between Mean-Variance and Monotone Mean-Variance Preferences Under Jump Diffusion and Stochastic Factor Model, arXiv:2211.14473v2, 2023. https://arxiv.org/abs/2211.14473
• F. Maccheroni, M. Marinacci, A. Rustichini, M. Taboga, Portfolio selection with monotone mean-variance preferences, Mathematical Finance 19(3):487–521, 2009. https://doi.org/10.1111/j.1467-9965.2009.00376.x
• J. Trybuła, D. Zawisza, Continuous-time portfolio choice under monotone mean-variance preferences—stochastic factor case, Mathematics of Operations Research 44(3):966–987, 2019 (cited as [Trybuła and Zawisza 2019] in arXiv:2211.14473v2).
• M. S. Strub, D. Li, A note on monotone mean–variance preferences for continuous processes, Operations Research Letters 48(4):397–400, 2020 (cited as [Strub and Li 2020] in arXiv:2211.14473v2).
• P. Protter, Stochastic Integration and Differential Equations, 2nd ed., Springer, 2005, ISBN 978-3-662-10061-5.

Motivation

Sampling from a Gibbs distribution $\pi_U \propto e^{-U}\,d\lambda_d$ on $\mathbb R^d$, or computing integrals $\pi(f)$ against it, is a basic task of Bayesian statistics, statistical physics and stochastic optimization. A standard route is to simulate a diffusion whose invariant law is the target, for instance the overdamped Langevin equation $dX_t = -\nabla U(X_t)\,dt + \sqrt2\,dB_t$, discretize it with the Euler scheme, and average a function along one long trajectory. Discretization introduces a bias of order of the step size, and the long-time average introduces a variance that decays like the inverse of the horizon, so reaching root-mean-square accuracy $\varepsilon$ with a single Euler scheme costs more than $\varepsilon^{-2}$ steps.

Egéa and Panloup (arXiv:2109.07753, Mathematics of Operations Research, 2025) adapt Giles's multilevel Monte Carlo idea (Giles 2008) to this infinite-horizon setting: they combine a coarse pathwise average with corrections between coupled Euler schemes of successively halved steps, run over decreasing horizons. Their general complexity theorem (Theorem 2.1) is stated under four abstract assumptions (H₁)–(H₄). This mission formalizes the first concrete instance the paper gives: an additive diffusion with a strongly contractive drift, where the assumptions are verified with explicit dependence on the dimension and the cost is of order $\varepsilon^{-2}\log^3(\varepsilon^{-1})$.

Setting

Let $|\cdot|$ and $\langle\cdot,\cdot\rangle$ be the Euclidean norm and inner product on $\mathbb R^d$. Let $b:\mathbb R^d\to\mathbb R^d$ be $L$-Lipschitz and satisfy the contractivity assumption $(\mathbf C_\alpha)$:

$$\langle b(y)-b(x),y-x\rangle\le-\alpha|x-y|^2\qquad(x,y\in\mathbb R^d),$$

with $0<\alpha\le L$. For $b=-\nabla U$ this is uniform strong convexity of $U$. Let $\sigma>0$ and let $W$ be a standard $d$-dimensional Brownian motion. The additive diffusion started at $x$ is $X^x_t = x+\int_0^t b(X^x_s)\,ds+\sigma W_t$; a probability $\pi$ is invariant for it if $\int\mathbb P(X^x_t\in A)\,\pi(dx)=\pi(A)$ for all $t$ and Borel $A$.

The Euler scheme with step $\gamma>0$ is $\bar X^{\gamma,x}_0=x$, $\bar X^{\gamma,x}_{(n+1)\gamma}=\bar X^{\gamma,x}_{n\gamma}+\gamma b(\bar X^{\gamma,x}_{n\gamma})+\sigma(W_{(n+1)\gamma}-W_{n\gamma})$, extended to continuous time by $\bar X_t=x+\int_0^t b(\bar X_{\underline s})\,ds+\sigma W_t$, $\underline s=\gamma\lfloor s/\gamma\rfloor$. A probability $\pi^\gamma$ invariant for one step of the scheme is its invariant distribution.

The multilevel occupation measure with start $x_0$, coarse step $\gamma_0$, levels $r=0,\dots,R$, steps $\gamma_r=\gamma_02^{-r}$, horizons $T_r$ and warm-start time $\tau$ is

$$\mathcal Y(f)=\frac1{T_0-\tau}\int_\tau^{T_0}f(\bar X^{\gamma_0}_{\underline s_{\gamma_0}})\,ds+\sum_{r=1}^R\frac1{T_r-\tau}\int_\tau^{T_r}\big(f(\bar X^{\gamma_r}_{\underline s_{\gamma_{r-1}}})-f(\bar X^{\gamma_{r-1}}_{\underline s_{\gamma_{r-1}}})\big)\,ds,$$

where level $r$ uses its own Brownian motion $B^{(r)}$, independent across levels, and both schemes of a level share it. Its cost is $\mathcal C(\mathcal Y)=T_0/\gamma_0+\sum_{r=1}^R(T_r/\gamma_r+T_r/\gamma_{r-1})$, the number of simulated Euler steps. Write $[f]_1$ for the Lipschitz constant of $f$ and

$$\Upsilon_1^2=1\vee\big(\alpha^{-2}|b(x_0)|^2+\alpha^{-1}\sigma^2d\big).$$

Formalization targets

Goal: Theorem 2.2

There is a universal constant $\mathfrak C_1$ such that, for $\alpha\in(0,L\wedge1]$, $\gamma_0\in(0,\frac\alpha{2L^2}\wedge\frac12]$, the parameters

$$r_0=\Upsilon_1,\quad R_\varepsilon=\lceil2\log_2(r_0\varepsilon^{-1})\rceil,\quad T_r=\frac{\Upsilon_1^2\log(\gamma_0^{-1})}{\alpha}\varepsilon^{-2}R_\varepsilon^22^{-r},\quad \tau=\frac2\alpha|\log\varepsilon|+\frac1\alpha\log\Upsilon_1,$$

and every $\varepsilon\in(0,1)$ with $2\log(\Upsilon_1\varepsilon^{-2})\le\log(\gamma_0^{-1})R_\varepsilon^2$,

$$\|\mathcal Y(f)-\pi(f)\|_2\le\mathfrak C_1[f]_1\varepsilon,\qquad\mathcal C(\mathcal Y)\le\frac{5\log(\gamma_0^{-1})}{2\alpha\gamma_0}\Upsilon_1^2\varepsilon^{-2}\lceil\log_2(\Upsilon_1^2\varepsilon^{-2})\rceil^3.$$

The constant $\mathfrak C_1$ does not depend on $d$, $b$, $\sigma$, $f$, $x_0$ or $\varepsilon$; all dependence on the problem sits in the explicit cost.

Milestones

1. Lemma 5.1 (i)–(iii): uniform second-moment bound (47), existence and uniqueness of $\pi^\gamma$, the $L^2$ contraction $\mathbb E|\bar X^{\gamma,x}_t-\bar X^{\gamma,y}_t|^2\le|x-y|^2e^{-\alpha t}$, the bound $\mathcal W_2(\delta_x,\pi^\gamma)\le c_1(x)$, and from these (H₁) and (H₄).
2. Lemma 5.2 (i): the one-step error between diffusion and Euler step.
3. Proposition 5.1 (i) and (iii) with $\mathfrak a=1$: $\|X^x_{n\gamma}-\bar X^{\gamma,x}_{n\gamma}\|_2^2\le\beta_1(x)\gamma$ uniformly in $n$, hence (H₂).
4. Proposition 5.2 with $\mathfrak a=1$, $\delta=\frac12$: $\mathcal W_1(\pi,\pi^\gamma)\le\sqrt{\beta_1(x^\star)\gamma}$, hence (H₃).
5. Proposition 2.1: all four assumptions with $\max(\alpha c_2^2/L^2,\alpha c_3^2/L^2,c_4^2)\lesssim\Upsilon_1^2$.
6. Remark 4.1: Theorem 2.1 (ii) for the additive scheme when the constants are known up to universal factors.
7. Theorem 2.2 (15): the refinement with $\tilde\Upsilon_1^2=\sigma^2\alpha^{-1}d$ and $\gamma_0=\alpha/(2L^2)$.

Significance

The goal gives a complexity of order $\varepsilon^{-2}\log^3(\varepsilon^{-1})$ for approximating $\pi(f)$ by a pathwise average of Euler schemes, within a logarithmic factor of the $\varepsilon^{-2}$ of an unbiased Monte Carlo method, with constants explicit in $d$, $\alpha$, $L$, $\sigma$. When $|b(x_0)|\lesssim\sqrt d$, the cost is of order $d\varepsilon^{-2}(\log^3d+\log^3\varepsilon)$. The intermediate results (uniform-in-time strong error of the Euler scheme, Wasserstein bias of its invariant law, step-independent contraction) are standard tools of Langevin Monte Carlo and are reusable on their own.

The results are proved in the paper; none of them is machine-checked. A formal proof would certify both the abstract multilevel argument as instantiated here and the explicit constants. The formal statements also pin three printed slips: the ceiling in (14) (cube of the ceiling, not ceiling of the cube), the first line of (12) (the function $c_1$ of Lemma 5.1 (ii)), and the factor in (15).

Difficulty

The obvious argument controls bias and variance separately for each level. The bias of a pathwise average involves the long-time behaviour of the scheme, and the variance of a correcting level involves the $L^2$ distance between two coupled schemes over an unbounded horizon: both require estimates uniform in time, which fail for a merely Lipschitz drift (the strong error of the Euler scheme grows exponentially on finite horizons). Contractivity is what makes the strong error $O(\sqrt\gamma)$ uniformly in $n$, and the delicate point is to obtain this with constants that do not degrade with $d$ or with the step. The complexity bound then requires balancing $R_\varepsilon$, the horizons and the warm start so that the long-time bias, the discretization bias and the variances all sit at level $\varepsilon$, with a universal constant.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) (published EthierKurtz.SDEState); Brownian motions are published EthierKurtz.IsStandardBrownian, one per level, mutually independent as path-valued variables. The diffusion is a pathwise solution of the integral equation with continuous paths; no Itô integral is needed because the noise is additive. Invariance of $\pi$ and $\pi^\gamma$ is stated through transition probabilities. $L^2$ norms are eLpNorm … 2 in $[0,\infty]$, so an infinite moment is never read as zero. $\mathcal W_1$ is used in its Kantorovich–Rubinstein form, $\mathcal W_2(\delta_x,\cdot)$ as an explicit integral, and the clause $\mathcal W_2(\mathcal L(\bar X_{\underline t}),\pi^\gamma)\le\mathcal W_2(\delta_x,\pi^\gamma)e^{-\alpha\underline t}$ as the existence of a coupling with that quadratic cost (Mathlib has no Wasserstein distance; optimal couplings exist, so the forms agree). (H₁)–(H₃) are stated at grid times, (H₄) over all $t\ge0$. "$\lesssim_{uc}$" is an existential constant quantified before every datum.

Standing assumptions carried as hypotheses: $b$ $L$-Lipschitz, $(\mathbf C_\alpha)$, $0<\alpha\le L$ (and $\alpha\le1$ where the paper requires it), $\sigma>0$. Added and disclosed: the §5.1 hypotheses in Lemma 5.2, $\gamma<1$ in Proposition 5.2 (needed by Proposition 5.1), integrability of $f$ under $\pi$, existence of $\pi^\gamma$ and $\tilde c_4>0$ in Remark 4.1. The goal's $\varepsilon_0$ (a maximum of a set that need not be an interval) is replaced by the inequality defining it.

The goal assumes only the contractive setting, the diffusion's invariance of $\pi$ and the parameter choices; it does not assume (H₁)–(H₄), a bias or a variance bound, which appear only as milestones, so it cannot be discharged by restating its hypotheses.

A complete development needs: second-moment and Grönwall estimates for the Euler scheme and the diffusion, existence and uniqueness of invariant laws of Feller chains under a Lyapunov condition, independence and variance decompositions for the multilevel estimator, and the abstract Theorem 2.1. The Gaussian-increment and Wasserstein tools are reusable well beyond this mission. Proofs of any milestone, and a Mathlib-style $\mathcal W_2$ for general laws, are welcome.

Selected references

• M. Egéa, F. Panloup, Multilevel-Langevin pathwise average for Gibbs approximation, Mathematics of Operations Research, 2025; preprint arXiv:2109.07753v2, 2024. https://arxiv.org/abs/2109.07753
• M. B. Giles, Multilevel Monte Carlo path simulation, Operations Research 56(3), 2008. https://doi.org/10.1287/opre.1070.0496
• A. S. Dalalyan, Theoretical guarantees for approximate sampling from smooth and log-concave densities, J. R. Stat. Soc. B 79(3), 2017. https://doi.org/10.1111/rssb.12183
• A. Durmus, É. Moulines, Nonasymptotic convergence analysis for the unadjusted Langevin algorithm, Ann. Appl. Probab. 27(3), 2017. https://doi.org/10.1214/16-AAP1238

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.