Probability

Motivation

Large systems of interacting diffusions — neurons, oscillators, agents in a network game, particles in a queueing or load-balancing model — are usually analysed through their mean-field limit: as the population grows, each particle interacts with the empirical law of the others, and the system is replaced by a single nonlinear (McKean–Vlasov) equation. The classical theory assumes that every particle interacts with every other one with the same strength. Real networks are heterogeneous and sparse: particle $i$ interacts with particle $j$ only through an edge of a random graph, and the number of neighbours of a particle is much smaller than the population size.

Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) describe the heterogeneity by a graphon and prove laws of large numbers and rates of convergence for such systems. This mission is the fifth of a series formalizing that paper. Its subject is the paper's quantitative result for not-so-dense graphs: when the edges are sampled from a Lipschitz graphon and then thinned by a sparsity factor $\beta_n$, the average mean-square distance between each particle and its graphon limit is of order $(n\beta_n)^{-1/q}$ for every $q>1$.

Setting

Let $I=[0,1]$ with Lebesgue measure. A graphon is a measurable symmetric function $G:I\times I\to[0,1]$. Fix a horizon $T>0$ and write $\mathcal C_d=C([0,T]:\mathbb R^d)$ with the norm $\|x\|_{*,T}=\sup_{0\le s\le T}|x_s|$.

One probability space carries, for every label $u\in I$, an initial state $X_u(0)$ with law $\mu_u(0)$ and a standard $d$-dimensional Brownian motion $B_u$, the whole family $\{X_u(0),B_u:u\in I\}$ being independent. The limit system (4.2) is a continuum of diffusions, one per label:

$$X_u(t)=X_u(0)+\int_0^t\!\int_I\!\int_{\mathbb R^d}b(X_u(s),x)\,G(u,v)\,\mu_{v,s}(dx)\,dv\,ds+\int_0^t\sigma(X_u(s))\,dB_u(s),\qquad \mu_{u,t}=\mathcal L(X_u(t)).$$

The particles are independent but not identically distributed; their laws are coupled through the $dv$-integral.

The not-so-dense $n$-particle system (4.1) uses the same initial states and Brownian motions at the labels $i/n$:

$$X^n_i(t)=X_{i/n}(0)+\int_0^t\frac{1}{n\beta_n}\sum_{j=1}^n\xi^n_{ij}\,b(X^n_i(s),X^n_j(s))\,ds+\int_0^t\sigma(X^n_i(s))\,dB_{i/n}(s),\qquad i=1,\dots,n.$$

The edges are percolated samples of $G$ (Condition 4.3): $\xi^n_{ij}=\xi^n_{ji}\sim\mathrm{Bernoulli}(\beta_nG(i/n,j/n))$, independent for $1\le i\le j\le n$ and independent of the noise. A particle has about $n\beta_n$ neighbours, which is why the interaction is scaled by $1/(n\beta_n)$.

The standing hypotheses are Condition 4.1 — $u\mapsto\mu_u(0)$ measurable with bounded second moments; $b$ bounded and Lipschitz; $\sigma$ bounded, Lipschitz and invertible with bounded inverse; $\beta_n\in(0,1]$ and $n\beta_n\to\infty$ — and Condition 2.3: on finitely many intervals $I_1,\dots,I_N$ covering $I$, the map $u\mapsto\mu_u(0)$ is Lipschitz in the Wasserstein distance $W_2$, and $G$ is Lipschitz on every block $I_i\times I_j$.

Formalization targets

Goal: Theorem 4.2

Under Conditions 2.3, 4.1 and 4.3, for each $q\in(1,\infty)$ there is $\kappa(q)\in(0,\infty)$ with

$$\frac1n\sum_{i=1}^n\mathbb E\big\|X^n_i-X_{i/n}\big\|_{*,T}^2\le\frac{\kappa(q)}{(n\beta_n)^{1/q}}\qquad\text{for all }n\in\mathbb N .$$

The constant depends on $q$ and on the data, never on $n$. The bound is on the average over particles, not on the maximum.

Milestones

1. Lemma 7.1: all moments of the coupling error are bounded uniformly in $n$ and $i$.
2. (7.10): $\mathbb E[\xi^n_{ij}|X^n_j(s)-X_{j/n}(s)|^2]\le\big(2\mathbb E|X^n_j(s)-X_{j/n}(s)|^2+\kappa(q)(n\beta_n)^{-1/q}\big)\beta_nG(i/n,j/n)$.
3. (7.15): the interaction error $R^{n,2}_s$ is at most $(\kappa/n)\sum_j\mathbb E|X^n_j(s)-X_{j/n}(s)|^2+\kappa(q)(n\beta_n)^{-1/q}$.
4. Theorem 2.1(b) for (4.2): $W_{2,T}(\mu_u,\mu_v)\le\kappa|u-v|$ for $u,v$ in one interval $I_i$.
5. §7.3 display: the discretization error $R^{n,4}_s$ is at most $\kappa/n^2$.

Significance

Theorem 4.2 gives an explicit rate for the convergence of a particle system on a sparse random graph to its graphon limit. Its companion, Theorem 4.1 (mission IV), proves the law of large numbers under weaker hypotheses but without a rate. The rate says that the effective sample size is $n\beta_n$, the typical degree, not $n$: graphs with $\beta_n\to0$ still approximate the graphon system as long as the degree grows. Results of this type justify replacing a large heterogeneous network by its graphon limit in control and game problems, such as graphon mean-field games, where the error of the replacement must be quantified.

The paper proves the theorem by hand; none of its results has a machine-checked proof. The formalization produces precise statements of the not-so-dense model, of the estimates of §7.1 that hold for any sparsity, and of the discretization bound, each usable on its own. The milestones (7.10) and (7.15) are the paper's key estimates for sparse interactions and are shared with mission IV.

Difficulty

The obvious approach is to compare each $X^n_i$ with $X_{i/n}$ by Gronwall's inequality, after bounding the difference of drifts. That step fails at the interaction term: the edge $\xi^n_{ij}$ and the error $X^n_j-X_{j/n}$ are dependent, because the edge enters the dynamics of particle $j$. A plain Cauchy–Schwarz bound loses a factor $1/\beta_n$ and gives nothing when $\beta_n\to0$. Estimates (7.10) and (7.15) quantify how weak this dependence is, and they are where the hypotheses that $\sigma$ is invertible with bounded inverse and that $n\beta_n\to\infty$ are needed. The discretization term needs the Lipschitz regularity of the limit laws in the label (Theorem 2.1(b)), itself a fixed-point estimate on a space of measure-valued maps.

Formalization scope

The Lean development uses Mathlib's unitInterval for $I$, Fin d → ℝ with its sup norm for $\mathbb R^d$ (all constants are existential, so the choice of norm does not matter), time ℝ≥0, and the path space $\mathcal C_d$ as continuous maps on $[0,T]$ with the sup norm. Brownian motions, Itô integrals and Itô processes are those of the published Peng1990.SMP.Stochastic; Wasserstein distances are the published WassersteinDRO.Duality.wassersteinDistance, valued in $[0,\infty]$. Particle $i$ is Lean's i : Fin n with label $(i+1)/n$.

Committed conventions:

• A solution of (4.2) has continuous paths, AE-measurable path maps, and path laws in the class $\mathcal M$ (measurable in $u$, bounded second moments); each $X_u$ is a strong solution for the filtration of $(X_u(0),B_u)$. A solution of (4.1) is a strong solution for the filtration of the edges, the initial states and the Brownian motions of the $n$ labels.
• The edges are $\{0,1\}$-valued, symmetric, with the diagonal included, mutually independent over $i\le j$, and independent of the σ-algebra of the noise.
• Condition 4.1(d) is required for $n\ge1$; the invertibility of $\sigma$ is that of a $d\times d$ matrix; the intervals of Condition 2.3 are order-connected subsets of $I$.
• Expectations of nonnegative quantities are lower Lebesgue integrals, so no expectation is silently $0$ for a non-integrable integrand.

The solution predicates are not vacuous: the zero-coefficient system $X_u(t)=X_u(0)$ satisfies both, Condition 4.1 and Condition 4.3 are satisfiable, and every statement quantifies over solutions rather than assuming the conclusion. The constant $\kappa(q)$ is chosen after $q$ and before $n$, so it cannot depend on $n$, and the bound is the paper's average over $i$, not a weaker or a stronger form. At $n=0$ both sides of every rate are $0$.

The paper's proofs are in its §5 (Theorem 2.1), §7.1 (Lemma 7.1, (7.10), (7.15)) and §7.3 (Theorem 4.2). Stochastic analysis at that level — Burkholder–Davis–Gundy and Rosenthal inequalities, Girsanov's theorem for these SDEs, Gronwall arguments for measure-valued fixed points — is mostly absent from Mathlib, and contributions of such infrastructure are welcome, as are proofs of any milestone.

Selected references

• E. Bayraktar, S. Chakraborty, R. Wu, Graphon mean field systems, Ann. Appl. Probab. 33(5):3587–3619, 2023. https://doi.org/10.1214/22-AAP1901
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060
• B. Bollobás, C. Borgs, J. Chayes, O. Riordan, Percolation on dense graph sequences, Ann. Probab. 38(1):150–183, 2010. https://doi.org/10.1214/09-AOP478
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4):966–979, 1990. https://doi.org/10.1137/0328054

Motivation

Join-the-shortest-queue (JSQ) is the load-balancing rule in which each arriving job is sent to a server with the fewest jobs. It is a baseline in the design of server farms and data centers, and in the many-server Halfin–Whitt regime, where the load per server approaches one at rate $1/\sqrt n$, it combines near-full utilization with vanishing waiting. Eschenfeldt and Gamarnik (arXiv:1502.00999, 2015) proved that the suitably scaled JSQ process converges, over bounded time intervals, to a two-dimensional reflected diffusion; Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) gave the form of the result that Braverman quotes as Theorem 1. Process-level convergence over bounded time intervals says nothing about the stationary distribution. To conclude that the stationary distributions converge as well, one needs tightness of the scaled stationary distributions, uniformly in the number of servers $n$.

Braverman (arXiv:1801.05121, Math. Oper. Res. 45(3), 2020) supplied this, together with positive recurrence of the diffusion limit. This mission formalizes the first of the two main results, Theorem 2, and the chain of lemmas the paper uses to prove it.

Setting

There are $n$ identical servers, each with its own infinite buffer. Jobs arrive as a Poisson process of rate $n\lambda$ and service times are i.i.d. exponential with mean one. An arriving job joins a server with the fewest jobs, ties broken arbitrarily. The Halfin–Whitt regime is

$$\lambda = 1 - \beta/\sqrt n,\qquad \beta > 0 \text{ fixed}.$$

For $i \ge 1$, $Q_i$ is the number of servers with at least $i$ jobs. The process $Q = (Q_1, Q_2, \dots)$ is a continuous-time Markov chain on

$$S = \Big\{ q \in \{0,1,\dots,n\}^\infty \ \Big|\ q_i \ge q_{i+1},\ \textstyle\sum_i q_i < \infty \Big\}.$$

Its generator $G_Q$ sends $q$ to $q + e^{(i)}$ at rate $n\lambda$ when $q_1 = \dots = q_{i-1} = n > q_i$, and to $q - e^{(i)}$ at rate $q_i - q_{i+1}$. The fluid-scaled coordinates are $X_1 = (Q_1 - n)/n \le 0$, the negative of the fraction of idle servers, and $X_i = Q_i/n$ for $i \ge 2$. The diffusion-scaled coordinates are $\sqrt n X_i$. Expectations $\mathbb E$ are taken under a stationary distribution $\pi$ of the chain.

The proof works with functions on $\Omega = (-\infty, 0] \times [0, \infty)$ and with the first-order operator

$$Lf(x) = (-x_1 + x_2 - \beta/\sqrt n) f_1(x) - x_2 f_2(x),$$

where $f_i$ is the partial derivative in $x_i$, taken one-sided on $\partial\Omega$.

Formalization targets

Goal: Theorem 2

For each $\beta > 0$ there is a constant $C(\beta)$ such that for all $n \ge 1$ with $\beta < \sqrt n$ and every stationary distribution,

$$\mathbb E\big|\sqrt n X_i\big| \le C(\beta),\ \ i = 1, 2,\qquad \mathbb E\big|n X_i\big| \le C(\beta),\ \ i \ge 3.$$

The constant depends on $\beta$ only, not on $n$, the stationary distribution, or $i$.

Milestones, in the order the proof uses them

1. Lemma 1: $\mathbb E\,G_Q f(Q) = 0$ whenever $\mathbb E|f(Q)| < \infty$.
2. Lemma 2: $\mathbb E Q_1 = n\lambda$ and $\mathbb E Q_i = n\lambda\,\mathbb P(Q_1 = \dots = Q_{i-1} = n)$.
3. Lemma 3: the generator, applied to $f(x_1, x_2)$, equals $Lf(x) + (f_2 - f_1)(x)\lambda 1(x_1 = 0) + \varepsilon(x)$ with an explicit remainder $\varepsilon$ built from second weak derivatives.
4. Lemmas 5 and 6: the curve $\Gamma^{(\kappa)}$ and the hitting time $\tau(x)$ of the fluid model; existence and uniqueness, finiteness, derivative formulas and monotonicity in $\kappa$.
5. Lemma 7 and Lemma 4: for $\kappa > \beta$, the explicit function $f^*$ of (4.14) solves

$$Lf(x) = -\big((x_2 - \kappa/\sqrt n)\vee 0\big)\ \text{on } \Omega,\qquad f_1(0, x_2) = f_2(0, x_2),$$

with $f^*_{11}, f^*_{12}, f^*_{22} \ge 0$, vanishing second derivatives for $x_2 \le \kappa/\sqrt n$, and explicit upper bounds of order $\sqrt n/\beta$ above that level. 6. (3.18): $\mathbb E\big((X_2 - \kappa/\sqrt n)\vee 0\big) \le \frac{1}{\beta\sqrt n}\big(12 + \frac{6\kappa}{\kappa - \beta}\big)\mathbb P(X_2 \ge \kappa/\sqrt n - 1/n)$. 7. Theorem 2, (2.2): the $i = 1, 2$ half of the goal.

Significance

Theorem 2 shows that in steady state the number of idle servers and the number of servers holding two or more jobs are $O(\sqrt n)$ on average, and the number of servers holding $i \ge 3$ jobs is $O(1)$ on average, uniformly in $n$. Combined with the process-level limit and the positive recurrence of the limiting diffusion (Theorem 3, the companion mission), it yields Proposition 1: the diffusion-scaled stationary distribution converges to the stationary distribution of the diffusion. This justifies the diffusion as a steady-state approximation for JSQ.

The method is the generator-comparison or Stein's-method approach: a Lyapunov function solving a first-order PDE for the fluid model, with explicit bounds on its derivatives. It applies to other many-server systems, and the paper is an example of that approach on an infinite-dimensional chain whose diffusion limit is two-dimensional.

The result is proved in the paper; no machine-checked proof is known to exist. The work remaining is to formalize the known proof: the adjoint relation for a countable-state chain with bounded rates, the Taylor expansion of the generator, and the explicit analysis of $f^*$ through the fluid curves.

Difficulty

The obvious route is to bound $\mathbb P(Q_1 = \dots = Q_{i-1} = n)$ in Lemma 2 directly. The paper notes that no good handle on these probabilities exists. The PDE route needs a solution whose second derivatives are bounded by $O(\sqrt n)$. General results that give such bounds require a continuous fluid vector field, and the JSQ fluid model is discontinuous because of the reflection at $x_1 = 0$. So $f^*$ is constructed explicitly from the fluid paths, and its derivatives must be bounded by hand through the implicitly defined $\tau(x)$ and $\nu^*(x_1)$.

A second difficulty is dimensional: the chain is infinite-dimensional while the PDE is two-dimensional, so the remainder of Lemma 3 contains a term with $q_3$ that is controlled only by combining Lemma 2 with the monotonicity of $f^*_2$.

Formalization scope

• Model. States are functions ℕ → ℕ with 0-based indices: Lean q.1 i is the paper's $q_{i+1}$, so the goal's "$i \ge 3$" is Lean index $\ge 2$. Each state is bounded by $n$, nonincreasing and eventually zero. The generator genQ is the displayed formula on p. 6.
• Stationarity. No process is constructed. A stationary distribution is a probability $\pi$ on $S$ satisfying global balance $\pi G_Q = 0$, which characterizes stationarity for this chain with bounded rates. Such a $\pi$ exists, since the chain is positive recurrent for $\lambda < 1$ (Bramson 2011), so statements quantifying over it are not vacuous. Expectations are sums against $\pi$. Lemma 1 keeps its integrability hypothesis, and all other expectations are of bounded functions.
• Parameters. $\lambda = 1 - \beta/\sqrt n$ with $0 < \beta < \sqrt n$, so that $\lambda > 0$; $\lambda$ is free in Lemmas 1–2. Constants are quantified as $\exists C$ after $\beta$ and before $n$.
• Misprint. The printed Theorem 2 omits $\mathbb E$. Read as an almost-sure bound it is false, so the expectation version, which the paper proves, is the target.
• Derivatives. Points of $\Omega$ are pairs in ℝ × ℝ. Partial derivatives are named functions asserted to be one-sided derivatives along coordinate lines (HasDerivWithinAt on Set.Iic 0 or Set.Ici 0). Weak second derivatives are a.e. derivatives of absolutely continuous functions, in integral form on compact intervals. A "solution" of the PDE whose derivatives are the junk values of a derivative operator is thereby excluded. The PDE needs genuine derivatives, and Lemma 7 is about the explicit $f^*$ of (4.14), not about an arbitrary function.
• Fluid objects. $\nu^*, \eta^*$ are the components of the unique solution of (4.8). $\tau$ is valued in WithTop ℝ, with $\infty$ as ⊤, so a missing solution is never read as $0$. $f^*$ is an if cascade, and Lemma 7 states the agreement of its branches. $f^*$ is defined by the closed form (4.14), not through the fluid model (4.1).
• Not included. Lemma 9 (via the Lambert W function, which Mathlib lacks), the bootstrapping argument of App. A.4 (not a numbered result), Theorems 1 and 3, and Proposition 1.

Contributions of reusable infrastructure are welcome: the adjoint relation for countable-state chains with bounded rates, and FTC/Taylor lemmas for absolutely continuous first derivatives.

Selected references

• A. Braverman, Steady-State Analysis of the Join-the-Shortest-Queue Model in the Halfin–Whitt Regime, Math. Oper. Res. 45(3), 2020; arXiv:1801.05121v2. https://arxiv.org/abs/1801.05121
• P. Eschenfeldt, D. Gamarnik, Join the Shortest Queue with Many Servers. The Heavy Traffic Asymptotics, arXiv preprint, 2015. https://arxiv.org/abs/1502.00999
• D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of Load Balancing Schemes on the Diffusion Scale, J. Appl. Probab. 53, 1111–1124, 2016. https://projecteuclid.org/euclid.jap/1481132840
• M. Bramson, Stability of Join the Shortest Queue Networks, Ann. Appl. Probab. 21, 1568–1625, 2011. https://doi.org/10.1214/10-AAP726
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Oper. Res. 29(3), 1981. https://doi.org/10.1287/opre.29.3.567

Motivation

Large networks are often modeled through a graphon, a measurable function that records how likely two labeled vertices are to interact. For interacting diffusions, this lets one ask whether a finite random network has a predictable population limit. Bayraktar, Chakraborty and Wu study that question for graphon weighted systems, including graphs obtained by independently retaining potential edges with a sparsity parameter $\beta_n$. Their not-so-dense regime allows $\beta_n$ to decrease, provided the typical interaction scale $n\beta_n$ diverges. Theorem 4.1 is the paper's law of large numbers for this regime; its two conclusions distinguish convergence of the population's empirical law from mean-square closeness of each particle to a coupled graphon limit. Bayraktar, Chakraborty and Wu, 2023.

The authors present three main convergence results: continuity of the continuum graphon system in Section 2, a dense-system law of large numbers in Section 3, and the percolated-system law of large numbers in Section 4. Section 7 establishes the latter. The graphon and cut-metric framework used here follows the graph-limit treatment cited by the paper. Bayraktar, Chakraborty and Wu, 2023; Lovász, 2012.

Setting

Let $I=[0,1]$. A graphon is a symmetric measurable $G:I^2\to[0,1]$. The cut norm $\|W\|_\square$ measures the largest absolute integral of $W$ over a measurable rectangle $S\times U$. A sequence of step graphons $G_n$ approaches $G$ when $\|G_n-G\|_\square\to0$. The related operator norm $\|W\|_{\infty\to1}$ measures the effect of $W$ on bounded measurable functions. Remark 2.1 says cut convergence implies convergence in this operator norm. Bayraktar, Chakraborty and Wu, 2023, Remark 2.1.

Fix a dimension $d\ge1$ and horizon $T>0$. A label $u\in I$ has an initial state $X_u(0)\in\mathbb R^d$ and an independent $d$-dimensional Brownian motion $B_u$. The initial states are independent of each other and of the Brownian motions. The limiting graphon particle $X_u$ is a continuous path whose drift averages $b(X_u(s),x)G(u,v)$ against the time-$s$ laws of all labels $v$, and whose diffusion matrix is $\sigma(X_u(s))$. The time-$s$ law at label $v$ is $\mu_{v,s}=\mathcal L(X_v(s))$. The family of path laws $\mu_u=\mathcal L(X_u)$ is measurable in $u$ and has uniformly bounded second moments. Bayraktar, Chakraborty and Wu, 2023, (4.2).

For $n$ particles, label $i$ means $i/n$, with $1\le i\le n$. Each undirected edge weight $\xi^n_{ij}=\xi^n_{ji}$ is Bernoulli with mean $\beta_nG_n(i/n,j/n)$; diagonal weights are included. These edge variables are independent of the Brownian motions and initial states. The finite particle $X_i^n$ uses the same initial state and Brownian motion as $X_{i/n}$. Its drift is the sum of $\xi^n_{ij}b(X_i^n,X_j^n)$ divided by $n\beta_n$; its diffusion is $\sigma(X_i^n)$. The coefficients $b$ and $\sigma$ are bounded and Lipschitz, and $\sigma(x)$ is invertible with uniformly bounded inverse. Initial laws have uniformly bounded second moments, $0<\beta_n\le1$, and $n\beta_n\to\infty$. Bayraktar, Chakraborty and Wu, 2023, Conditions 4.1–4.2.

Formalization targets

Let $\mathcal C_d=C([0,T];\mathbb R^d)$, $\mu^n=n^{-1}\sum_{i=1}^{n}\delta_{X_i^n}$, and $\bar\mu=\int_I\mu_u\,du$. The main target, Theorem 4.1, first asserts convergence in probability in the weak topology on $\mathcal P(\mathcal C_d)$:

$$\mu^n\xrightarrow{\mathbb P}\bar\mu.$$

This uses Condition 2.2(a): on each of finitely many intervals covering $I$, the initial law varies continuously in Wasserstein distance $W_2$. If the graphon also satisfies Condition 2.2(b), its stated sectional continuity outside null sets, the theorem adds

$$\frac1n\sum_{i=1}^{n}\mathbb E\|X_i^n-X_{i/n}\|_{*,T}^2\longrightarrow0, \qquad \|x\|_{*,T}=\sup_{0\le s\le T}|x_s|.$$

The milestones record the paper's cut-to-operator observation, uniform coupling moments, the one-edge and two-edge estimates, the bound on the second interaction-error term, the quantitative coupling lemma, and the empirical law of large numbers for the independent limiting particles. The second displayed limit is conditional on 2.2(b); the first is not. Bayraktar, Chakraborty and Wu, 2023, Theorem 4.1.

Significance

The first conclusion identifies the population-level limit even when the sampled network has a decreasing edge-retention probability. It gives a deterministic law on path space, rather than only a limit at one time. The second conclusion is stronger: it compares each finite particle with the limiting particle built from the same initial state and Brownian motion, averaged over all labels. This comparison is available when the extra graphon continuity assumption holds. Bayraktar, Chakraborty and Wu, 2023, Theorem 4.1 and Remark 4.1.

The mathematical results were proved in the published paper. The present mission asks for machine-checked Lean proofs of its specified statements; the draft theorems themselves currently contain sorry. Reusable outputs would include the percolated-edge model, a path-law formulation of graphon diffusions, and estimates for random interactions that depend on the particle states they influence. The paper's proofs appear in Sections 5–7, with the sparse-system argument in Section 7. Bayraktar, Chakraborty and Wu, 2023.

Difficulty

The edge variables are independent of the driving noise, but a particle's state depends on its incident edges. Therefore an expression such as $\mathbb E[\xi^n_{ij}|X_j^n-X_{j/n}|^2]$ cannot be factored into the edge mean times the error moment. The same dependence affects pairs of edges in the squared interaction sum. Equations (7.10), (7.14), and (7.15) quantify the discrepancy. A second difficulty is that cut convergence controls integrals against fixed bounded tests, while the dynamics and their path laws supply tests that vary with the system. The paper's regularity conditions and quantitative estimates are needed to connect those forms of control. Bayraktar, Chakraborty and Wu, 2023, Sections 7.1–7.2.

Formalization scope

Lean represents $I$ by Mathlib's unit interval, $\mathbb R^d$ by Fin d → ℝ, and continuous paths by maps from $[0,T]$ into that vector space. The chosen vector and matrix norms are fixed sup-type norms; finite-dimensional norm equivalence preserves the limit statements and the estimates with existential constants. The horizon and dimension are explicitly positive. Particle index i : Fin n denotes the paper's $(i+1)$st particle, and empirical laws use positive sizes $n+1$ to avoid division by zero. Wasserstein distances use extended nonnegative reals, while nonnegative expectations use lower integrals.

The noise lives on one probability space. The continuum equation uses the natural filtration of its own initial state and Brownian motion. The finite equation uses the natural filtration of its edge array, sampled initial states, and Brownian motions. A solution carries a measurable continuous-path law family in the paper's class $\mathcal M$; this prevents a nonmeasurable pushforward or a default-zero integral from silently satisfying an equation. Edge symmetry, Bernoulli marginals, independence, and diagonal self-loops are explicit. The zero-coefficient system has a separate sorry-free Lean witness for both solution predicates, ruling out a vacuous solution concept.

The formalization uses the published Peng1990.SMP.Stochastic Itô interface and WassersteinDRO.Duality.wassersteinDistance definition. Contributions can prove the listed estimates, strengthen their reusable stochastic and measure-theoretic infrastructure, or connect this mission's local setting to the other graphon missions after their definitions are published. The auxiliary changed-measure particles of Section 7.1 are outside the initial milestone list. Bayraktar, Chakraborty and Wu, 2023, Sections 4 and 7.

Selected references

• E. Bayraktar, S. Chakraborty and R. Wu, Graphon mean field systems, Annals of Applied Probability 33(5):3587–3619, 2023. DOI.
• L. Lovász, Large Networks and Graph Limits, American Mathematical Society Colloquium Publications 60, 2012. DOI.

Motivation

Many stochastic dynamic programs in operations research, such as inventory control with partially observed demand or the pricing of American options, are too large to solve exactly. A heuristic policy gives a lower bound on the optimal expected reward; to judge whether it is good enough one needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) build such bounds by information relaxation: let the decision maker see more than she would in reality, and charge a penalty for using the extra information. The construction generalizes the martingale duality for optimal stopping of Haugh and Kogan (Oper. Res. 2004), Rogers (Math. Finance 2002) and Andersen and Broadie (Manage. Sci. 2004).

In applications, the analyst chooses both the relaxation and the penalty, trading the quality of the bound against the cost of computing it. Proposition 2.3 of the paper collects four properties that govern this choice. The first is the subject of this mission.

Setting

Uncertainty is a probability space $(\Omega,\mathcal F,\mathbb P)$, and decisions are made in periods $t=0,\dots,T$. The natural filtration $\mathbb F=(\mathcal F_0,\dots,\mathcal F_T)$ records what is known in each period, with $\mathcal F_0=\{\emptyset,\Omega\}$. An action sequence is $a=(a_0,\dots,a_T)$, chosen from feasible sets $A_t(a_0,\dots,a_{t-1})$. Period rewards $r_t(a_0,\dots,a_t)$ are $\mathcal F_t$-measurable random variables and the total reward is $r(a)=\sum_t r_t(a)$.

A policy is a map $\alpha:\Omega\to A$ from outcomes to feasible action sequences. It is adapted to a filtration $\mathbb G$ if the period-$t$ action is $\mathcal G_t$-measurable; $\mathcal A_{\mathbb G}$ denotes these policies. A filtration $\mathbb G$ with $\mathcal F_t\subseteq\mathcal G_t\subseteq\mathcal F$ for all $t$ is a relaxation of $\mathbb F$, written $\mathbb F\subseteq\mathbb G$. A penalty is a function $z(a,\omega)$; it is dual feasible if $\mathbb E[z(\alpha_F)]\le0$ for every $\alpha_F\in\mathcal A_{\mathbb F}$. For any relaxation $\mathbb G$ and dual feasible $z$, the dual bound

$$\sup_{\alpha_G\in\mathcal A_{\mathbb G}}\mathbb E\big[r(\alpha_G)-z(\alpha_G)\big]$$

is at least the optimal value $\sup_{\alpha_F\in\mathcal A_{\mathbb F}}\mathbb E[r(\alpha_F)]$ (weak duality, Lemma 2.1).

The paper's main source of penalties is Proposition 2.2. Given generating functions $w_t(a)$ depending only on $a_0,\dots,a_t$, set

$$z_t(a)=\mathbb E[w_t(a)\mid\mathcal G_t]-\mathbb E[w_t(a)\mid\mathcal F_t],\qquad z(a)=\sum_{t=0}^T z_t(a).$$

Such a penalty has zero mean along every nonanticipative policy, and its dual bound is computed by the backward recursion (10), the Bellman recursion with rewards $r_t-z_t$ and conditional expectations given $\mathcal G_t$.

Formalization targets

Goal: Proposition 2.3(i)

For filtrations $\mathbb F\subseteq\mathbb G^1\subseteq\mathbb G^2$ and one common sequence of generating functions $(w_0,\dots,w_T)$, let $z^i$ be the Proposition 2.2 penalty of $(\mathbb G^i,w)$. Then

$$\sup_{\alpha_G\in\mathcal A_{\mathbb G^1}}\mathbb E\big[r(\alpha_G)-z^1(\alpha_G)\big]\le\sup_{\alpha_G\in\mathcal A_{\mathbb G^2}}\mathbb E\big[r(\alpha_G)-z^2(\alpha_G)\big].\qquad(12)$$

With a common generating function, a looser relaxation gives a weaker bound.

Milestones

1. Equation (10). For a Proposition 2.2 penalty under a relaxation $\mathbb G$, the expectation of the initial dual value function $V^{\mathbb G}_0$ equals the dual bound.
2. Proposition 2.3(ii). For dual feasible $z^1,z^2$ and one relaxation $\mathbb G$, the difference of the two dual bounds lies between $\inf_{\alpha_G}\mathbb E[z^2(\alpha_G)-z^1(\alpha_G)]$ and $\sup_{\alpha_G}\mathbb E[z^2(\alpha_G)-z^1(\alpha_G)]$, eq. (13).
3. Proposition 2.3(iii). For $\mathbb F\subseteq\mathbb F'\subseteq\mathbb G$, the penalty $z_t(a)=\mathbb E[w_t(a)\mid\mathcal G_t]-\mathbb E[w_t(a)\mid\mathcal F'_t]$ still satisfies the conclusions of Proposition 2.2.
4. Proposition 2.3(iv). If $\hat z_t(a)$ are unbiased estimates of the terms $z_t(a)$ of a dual feasible penalty, $\mathbb E[\hat z_t(a)\mid\mathcal G_t]=z_t(a)$, and the relaxation $\widehat{\mathbb G}$ additionally reveals the estimates, then the dual bound of $(\mathbb G,z)$ is at most that of $(\widehat{\mathbb G},\hat z)$, eq. (14).

Milestone 1 is on the goal's path; milestones 2–4 are the remaining parts of the same proposition.

Significance

Proposition 2.3(i) tells the analyst how to read a weak bound. If a cheap generating function (for instance $w_t=0$, the zero penalty) gives a satisfactory bound under some relaxation, it will give a bound at least as tight under any less informative relaxation that still contains $\mathbb F$; conversely, moving to a looser relaxation without improving the generating function can only weaken the bound. Part (ii) is a continuity statement: penalties close to the ideal penalty give bounds close to the optimal value. Part (iii) permits the subtracted conditional expectation to be computed under an intermediate filtration, which the paper uses when volatility is unobserved in its option-pricing example. Part (iv) is the justification for estimating penalties by nested simulation, as in the methods of Haugh–Kogan and Andersen–Broadie: unbiased estimates yield valid, if weaker, upper bounds.

The results are proved in the paper's electronic companion. To our knowledge none of them, nor the information-relaxation duality framework itself, has a machine-checked proof. Formalizing them requires a usable theory of policies adapted to a filtration, penalties evaluated along random action sequences, and backward recursions with conditional expectations, all of which are reusable for other duality results in stochastic dynamic programming.

Difficulty

The obvious argument for (12) compares the two suprema policy by policy: $\mathcal A_{\mathbb G^1}\subseteq\mathcal A_{\mathbb G^2}$. This fails, because the two bounds use different penalties: for a fixed $\mathbb G^1$-adapted policy, $\mathbb E[z^1(\alpha)]$ and $\mathbb E[z^2(\alpha)]$ need not agree, so the larger policy set alone does not order the bounds. The penalty changes with the relaxation exactly so as to remove part of the value of the extra information, and the statement asserts that it never removes more than that information is worth. Even the representation (10) of a dual bound by a backward recursion is nontrivial: it requires near-optimal actions to be selected measurably in every period.

In Lean, the further difficulty is the composition of an action-indexed family of conditional expectations with a random action: $\omega\mapsto z_t(\alpha(\omega))(\omega)$, where each $z_t(a)$ is only defined almost surely. Countability of the action set is what makes this composite well defined up to null sets.

Formalization scope

Periods are Fin (T + 1); an action sequence is a function Fin (T + 1) → X for one countable action type X with the discrete σ-algebra (the disjoint union of the per-period action sets). Filtrations are Mathlib Filtrations of the ambient σ-algebra; a relaxation is 𝔽 ≤ 𝔾. Policies are maps Ω → (Fin (T + 1) → X) with values in the feasible set, adapted when each action is measurable for the corresponding σ-algebra. Conditional expectations are Mathlib's μ[f | m], so identities between them hold almost surely. Dual bounds are suprema in EReal over the adapted policy sets, so an infinite bound is represented and no junk value $0$ arises from an unbounded supremum.

Pinned regularity, beyond the paper's text: period rewards and generating functions are uniformly bounded (almost surely for the latter) and measurable, so that every expectation exists; in part (iv), the estimates are measurable and uniformly bounded. In part (ii), the difference of two dual bounds is taken in EReal, and the case where both bounds are $+\infty$ (where the page's difference is undefined) is excluded.

The penalties $z^1,z^2$ of the goal are computed from $w$ by the formula of Proposition 2.2; stating the goal for arbitrary penalties with Proposition 2.2's properties would be a different and false claim. Likewise $\widehat{\mathbb G}$ in part (iv) is constructed from $\mathbb G$ and the estimates.

The definitions duplicate those of mission 1 of this series (the framework, the recursive model, the penalty construction); they are expected to be merged. Contributions of reusable lemmas about adapted policies over countable action sets and about backward recursions with conditional expectations are welcome.

Selected references

• D. B. Brown, J. E. Smith, P. Sun, Information Relaxations and Duality in Stochastic Dynamic Programs, Operations Research, Articles in Advance, 2010. https://doi.org/10.1287/opre.1090.0796
• M. B. Haugh, L. Kogan, Pricing American Options: A Duality Approach, Operations Research 52(2), 2004. https://doi.org/10.1287/opre.1030.0070
• L. Andersen, M. Broadie, Primal-Dual Simulation Algorithm for Pricing Multidimensional American Options, Management Science 50(9), 2004. https://doi.org/10.1287/mnsc.1040.0258
• L. C. G. Rogers, Monte Carlo Valuation of American Options, Mathematical Finance 12(3), 2002. https://doi.org/10.1111/1467-9965.02010

Motivation

A probability distribution on the real line is self-decomposable (of class L) if its characteristic function satisfies $\varphi(t)=\varphi(\alpha t)\,\varphi_\alpha(t)$ for every $\alpha\in(0,1)$, with $\varphi_\alpha$ again a characteristic function. Equivalently, a random variable $X$ can be written as $X\overset{d}{=}\alpha X'+X_\alpha$ with $X'$ a copy of $X$ independent of $X_\alpha$. Class L consists exactly of the limit laws of normalized sums of independent summands, and its members are infinitely divisible, absolutely continuous (when nondegenerate) and unimodal.

None of this transfers to counting variables: apart from $X\equiv0$, no random variable on $\mathbb N_0=\{0,1,2,\dots\}$ satisfies $X=\alpha X'+X_\alpha$, because $\alpha X'$ leaves the lattice. Steutel and van Harn (Memorandum COSOR 78-07, 1978; Ann. Probab. 7 (1979) 893–899) replaced scalar multiplication by binomial thinning, which keeps the variable integer valued. The resulting notion of discrete self-decomposability later became the basis of integer-valued autoregressive (INAR) time-series models (Al-Osh and Alzaid, 1987).

Timeline:

• 1968: Feller, An Introduction to Probability Theory and Its Applications, vol. 1, 3rd ed., characterizes the infinitely divisible distributions on $\mathbb N_0$ as the compound Poisson distributions.
• 1971: Steutel, On the zeros of infinitely divisible densities (Ann. Math. Statist. 42), and 1977: van Harn and Steutel, Generalized renewal sequences and infinitely divisible lattice distributions (Stoch. Proc. Appl. 5), give the recursive criterion $(n+1)p_{n+1}=\sum_k p_k r_{n-k}$ with $r_n\ge0$.
• 1978–1979: Steutel and van Harn introduce discrete self-decomposability and discrete stability and prove the canonical form (Theorem 2.2, the goal of this mission), unimodality, and the characterization of the discrete stable laws.

Setting

A distribution on $\mathbb N_0$ is a sequence $p_n\ge0$ with $\sum_n p_n=1$; its probability generating function (p.g.f.) is $P(z)=\sum_{n\ge0}p_nz^n$. The generating function of a sequence $(g_n)$ is written $G$.

The $\alpha$-thinning of a variable $X$ with p.g.f. $P$ is $\alpha\circ X=\sum_{j=1}^{X}N_j$ with independent Bernoulli($\alpha$) variables $N_j$; its p.g.f. is $P(1-\alpha+\alpha z)$. A distribution with p.g.f. $P$ is discrete self-decomposable (Definition 2.1) if for every $\alpha\in(0,1)$

$$P(z)=P(1-\alpha+\alpha z)\,P_\alpha(z)\qquad(|z|\le1)$$

with $P_\alpha$ a p.g.f.; in variables, $X\overset{d}{=}\alpha\circ X'+X_\alpha$.

A distribution is infinitely divisible if for every $n\ge1$ its p.g.f. is the $n$-th power of a p.g.f. When $p_0>0$, its canonical sequence $(r_n)$ is the unique solution of

$$(n+1)\,p_{n+1}=\sum_{k=0}^{n}p_k\,r_{n-k}\qquad(n\in\mathbb N_0).$$

Throughout §2 the paper assumes $0<p_0<1$.

Formalization targets

Goal: Theorem 2.2

For a distribution $(p_n)$ with $0<p_0<1$:

$$(p_n)\ \text{discrete self-dec}\iff P(z)=\exp\Big\{-\lambda\int_z^1\frac{1-G(u)}{1-u}\,du\Big\}\quad(0\le z<1)$$

for some $\lambda>0$ and some p.g.f. $G$ of a distribution with $G(0)=0$, the pair $(\lambda,G)$ being unique; and

$$(p_n)\ \text{discrete self-dec}\iff (p_n)\ \text{inf div and } (r_n)\ \text{nonincreasing}.$$

Milestones

1. Lemma 1.1: $\lim_{x\uparrow1}(1-x)P'(x)=0$ for every p.g.f.
2. Lemma 1.2: for $0<p_0<1$, $P$ is infinitely divisible iff $P(z)=\exp\{\lambda(G(z)-1)\}$ (unique $\lambda>0$, $G(0)=0$), iff $P(z)=\exp\{-\int_z^1R(u)\,du\}$ with $R=\sum r_nu^n$, $r_n\ge0$ (necessarily $\sum r_n/(n+1)<\infty$), iff the canonical sequence is nonnegative.
3. (2.6): if $P$ is discrete self-decomposable, $\exp\{-r(1-z)P'(z)/P(z)\}$ is a p.g.f. for every $r>0$.
4. (2.7)–(2.8): the form (2.4) gives $P'/P=\lambda(1-G)/(1-z)$, infinite divisibility, and $r_n=\lambda\sum_{j>n}g_j$, nonincreasing.
5. The converse (pp. 3–4): if $P$ is infinitely divisible with nonincreasing $r_n$, then $P(z)/P(1-\alpha+\alpha z)$ is an infinitely divisible p.g.f. for each $\alpha\in(0,1)$.

Significance

Theorem 2.2 reduces discrete self-decomposability, a condition quantified over all $\alpha\in(0,1)$ and over unknown factors $P_\alpha$, to a single monotonicity condition on the sequence $(r_n)$ computed recursively from $(p_n)$. It is the entry point of the rest of the paper: combined with Theorem 2.3 it gives unimodality of every discrete self-decomposable distribution (Corollary 2.4), and §3 shows that discrete stable distributions are discrete self-decomposable. In time-series modelling it identifies the marginals that a stationary INAR(1) process $X_t=\alpha\circ X_{t-1}+\varepsilon_t$ can have for every $\alpha\in(0,1)$.

The result has been proved since 1979; to our knowledge none of it is formalized in any proof assistant, and Mathlib has neither probability generating functions on $\mathbb N_0$ nor infinite divisibility. The mission produces a machine-checked version of the canonical form together with the compound-Poisson characterization of infinite divisibility on $\mathbb N_0$ (Lemma 1.2), which the paper only cites.

Difficulty

The forward direction is not a consequence of (2.1) for any single $\alpha$: one factorization $P(z)=P(1-\alpha+\alpha z)P_\alpha(z)$ constrains $P$ very little, and the information sits in the whole family of factors $P_\alpha$, $\alpha\in(0,1)$, which are not given explicitly. Turning that family into a statement about $P$ needs a passage to a limit of p.g.f.'s, and the fact that such a limit is again a p.g.f. (the continuity theorem for p.g.f.'s, Feller vol. 1, p. 280) is not in Mathlib. The paper does not prove Lemma 1.2 either; it cites Feller and Steutel. For the converse, nonnegativity of the canonical sequence is not enough: the obvious attempt to show that $P(z)/P(1-\alpha+\alpha z)$ has nonnegative coefficients fails for infinitely divisible $P$ in general, and the monotonicity of $r_n$ is exactly what is needed. Finally, every identity is stated between real functions on $[0,1]$, and passing to identities between coefficients requires the uniqueness of power-series coefficients on a real interval.

Formalization scope

• A distribution is p : ℕ → ℝ with ∀ n, 0 ≤ p n and HasSum p 1; the p.g.f. is the real function pgf p z = ∑' n, p n * z ^ n. All identities between p.g.f.'s are required for real $z\in[0,1]$ (or $[0,1)$ for (1.4), (2.4), (2.6), (2.7)), not for complex $|z|\le1$; p.g.f.'s agreeing on $[0,1]$ have equal coefficients, so this is equivalent. $P'$ is Lean's deriv of pgf p.
• Infinite divisibility follows Feller: for every $n\ge1$ an $n$-th root that is the p.g.f. of a distribution on $\mathbb N_0$. It is not defined as $r_n\ge0$ or as the form (1.3); those are Lemma 1.2.
• The canonical sequence is defined by the recursion $r_n=((n+1)p_{n+1}-\sum_{k=1}^np_kr_{n-k})/p_0$; every statement using it assumes $p_0>0$.
• The standing assumption $0<p_0<1$ of §2 is a hypothesis of Theorem 2.2 and of the §2 milestones.
• The improper integrals in (1.4) and (2.4) carry an explicit integrability clause on $(z,1)$, and the series $R$ an explicit convergence clause on $[0,1)$. Lean's integral of a non-integrable function, and the sum of a divergent series, are $0$; without these clauses the forms (1.4) and (2.4) could hold vacuously, so a formalization that drops them does not state the theorem.
• Uniqueness of $(\lambda,G)$ in (1.3) and (2.4) is part of the statements.

Reusable beyond this mission: the p.g.f. and infinite-divisibility vocabulary, Lemma 1.2 (compound Poisson characterization), and Lemma 1.1. A continuity theorem for p.g.f.'s on $\mathbb N_0$, and the uniqueness of power-series coefficients from values on $[0,1)$, are welcome as independent contributions.

Selected references

• F. W. Steutel, K. van Harn, Discrete analogues of self-decomposability and stability, Memorandum COSOR 78-07, Technische Hogeschool Eindhoven, 1978. https://pure.tue.nl/ws/files/1719387/340666.pdf — published as Ann. Probab. 7(5) (1979) 893–899. https://doi.org/10.1214/aop/1176994950
• W. Feller, An Introduction to Probability Theory and Its Applications, vol. 1, 3rd ed., Wiley, New York, 1968 (XII.2; continuity theorem p. 280).
• F. W. Steutel, On the zeros of infinitely divisible densities, Ann. Math. Statist. 42 (1971) 812–815.
• K. van Harn, F. W. Steutel, Generalized renewal sequences and infinitely divisible lattice distributions, Stochastic Process. Appl. 5 (1977) 47–55.
• M. A. Al-Osh, A. A. Alzaid, First-order integer-valued autoregressive (INAR(1)) process, J. Time Series Anal. 8 (1987) 261–275. https://doi.org/10.1111/j.1467-9892.1987.tb00438.x

Pricing while learning demand

A vendor holding a finite stock of a product must set prices over time without knowing how many customers will come. Each price does two things: it earns revenue now, and through the sales it generates it reveals information about demand that improves future prices. This tension between earning and learning is central in revenue management with demand uncertainty, in retail markdown pricing, and in online selling. Optimal Bayesian policies for such problems are characterized by a Hamilton–Jacobi–Bellman equation that has no closed-form solution, so practice relies on heuristics, and the question is which heuristics come with guarantees.

Farias and Van Roy introduced decay balancing and proved that, for exponentially distributed reservation prices and a Gamma prior on the arrival rate, it earns at least one third of the optimal expected discounted revenue, uniformly over all problem parameters (V. F. Farias, B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010, doi:10.1287/opre.1090.0729). They describe it as the first heuristic for problems of this type with a uniform performance guarantee. This mission formalizes that guarantee and the chain of results leading to it. The source is the authors' manuscript of January 20, 2009 (MIT DSpace); its printed page numbers coincide with the PDF page numbers, and all theorem and page numbers below refer to it.

The model

Customers arrive according to a Poisson process with rate $\lambda$. Each has an independent reservation price with density $f$ and tail $\bar F(p) = 1-F(p)$; a customer facing price $p$ buys one unit if it is available and $p$ is at most his reservation price, and otherwise leaves. The hazard rate is $\rho(p) = f(p)/\bar F(p)$. Assumption 1 (p. 5) asks that $f$ be differentiable with support $\mathbb R_+$ and that $\rho$ be non-decreasing. The exponential law with mean $r$ has $\bar F(p) = e^{-p/r}$.

The vendor starts with $x$ units and a Gamma prior on $\lambda$ with shape $a$ and rate $b$ (density $b^a\lambda^{a-1}e^{-\lambda b}/\Gamma(a)$, mean $\mu(z) = a/b$). After $n_t$ sales the posterior is Gamma with $a_t = a+n_t$ and $b_t = b+\int_0^t\bar F(p_s)\,ds$, so the state is $z = (x,a,b)$. A policy $\pi(x,a,b)\ge0$ sets the price; the expected discounted revenue at rate $\alpha>0$ is

$$J^\pi(z) = E_{z,\pi}\Big[\sum_{k:\,t_k\le\tau_0}e^{-\alpha t_k}p_{t_k-}\Big],\qquad J^*(z) = \sup_\pi J^\pi(z),$$

the supremum over all measurable non-negative policies. With $\lambda$ known, the same problem has value $J^*_\lambda(x)$. Assumption 2 (p. 9) asks that $J^*_\lambda(x)$ be differentiable in $\lambda$.

Decay balancing uses the approximation $\tilde J(z) = E[J^*_\lambda(x)]$, $\lambda\sim\mathrm{Gamma}(a,b)$, and posts the price $\pi_{\rm db}(z)$ solving the balance equation (5), p. 13,

$$\frac{\bar F(\pi_{\rm db}(z))}{\rho(\pi_{\rm db}(z))}\,\mu(z) = \alpha\tilde J(z).$$

The optimal price $\pi^*(z)$ solves the same equation with $J^*(z)$ in place of $\tilde J(z)$. The constant

$$\kappa(a) = \frac{a\Gamma(a)}{\Gamma(a+1)-\Gamma(a+1,a)+a\Gamma(a,a)},\qquad \Gamma(s,y) = \int_y^\infty t^{s-1}e^{-t}\,dt,$$

measures the cost of uncertainty for a prior of shape $a$.

Formalization targets

Goal: Theorem 3 (p. 24)

For exponential reservation prices with mean $r>0$, every $\alpha>0$, $x>1$, $a>0$, $b>0$:

$$J^*(z)<\infty\qquad\text{and}\qquad \frac{J^{\pi_{\rm db}}(z)}{J^*(z)}\ \ge\ \frac13 .$$

Milestones

In attack order:

1. Known-rate value. Lemma 2: $J^*_\lambda(x)$ is increasing and concave in $\lambda$.
2. Bounds and well-posedness. Lemma 3 gives $J^*\le\tilde J\le J^*_{\mu(z)}(x)\le\bar F(p^*)p^*\mu(z)/\alpha$. Lemma 4 says the balance equation has a unique solution. Lemma E.6(2), with Theorems E.1–E.2, says the balance-price policy $\pi^*$ is optimal.
3. Normalizations. Lemma 5 rescales the discount rate and Lemma 10 rescales the mean reservation price.
4. No-learning comparison. Lemmas 7 and 8, and Theorem 1: $J^{nl}(z)\ge J^*_{a/b}(x)/\kappa(a)$.
5. Quality of the approximation. $1\ge J^*(z)/\tilde J(z)\ge1/\kappa(a)$, and $\kappa$ is decreasing.
6. Prices and revenues. Corollary 1: $1/(1+\log\kappa(a))\le\pi_{\rm db}/\pi^*\le1$. Lemma 9: $J^{ub}\ge J^*$. Theorem 2: $1/(1+\log\kappa(a))\le J^{\pi_{\rm db}}/J^*\le1$.
7. Inventory. Lemma 12: $J^*(x,a,b)\le2.05\,J^*(x-1,a,b)$ for $x>1$, $a>1$.

Significance

Theorem 2 gives a guarantee that depends only on the coefficient of variation $1/\sqrt a$ of the prior. Theorem 3 removes even that dependence for exponential reservation prices: whatever the inventory, prior, discount rate and price scale, decay balancing loses at most a factor of three. The analysis also yields reusable facts about Bayesian pricing: knowing the rate helps ($J^*\le\tilde J$), the decay-balance characterization of optimal prices, and comparison with a vendor who does not learn.

All results are proved in the source, using Dynkin's formula, an HJB verification argument (Appendix E) and a coupling of sales processes. None of them is machine-checked. The mission asks for a formal development of the known proofs.

Difficulty

The obvious route to Theorem 3 would chain Theorem 2 at the initial state. That fails because $\kappa(a)$ blows up as $a\to0$, so for a diffuse prior Theorem 2 gives no constant bound. The paper instead compares the two systems only up to the first sale, after which the shape parameter is at least $a+1>1$. This needs two things: a coupling in which the optimal system never sells first, and Lemma 12, which bounds the value of one extra unit without a decreasing-returns property in $x$ (none is known). Lemma 12 itself rests on a numerical inequality involving the Lambert $W$ function.

At the foundational level, neither Mathlib nor the platform has a counting process whose intensity is a random rate times a state-feedback price. Defining $J^\pi$ and $J^*$ faithfully is part of the mission.

Formalization scope

• Sales process. The process is built exactly in the b-clock. Given $\lambda$, sales are a rate-$\lambda$ Poisson process in the variable $b$, so $\lambda\sim\mathrm{Gamma}(a,b)$ and i.i.d. $\mathrm{Exp}(1)$ clocks $E_j$ give the $b$-values of the sales, $B_{j+1} = B_j + E_{j+1}/\lambda$. The real-time length of each stage is $\int d\beta/\bar F(\pi(\cdot,\beta))$.
• Values. Revenue is the sum over sales of the discounted pre-sale price (p. 6; the compensated-integral form of p. 7 is equal to it). Values and suprema live in $[0,\infty]$. $J^*$ and $J^*_\lambda$ are suprema over policies; they are never defined by the HJB equation or by the Lambert-$W$ formula (2). Such a definition would trivialize the mission and is ruled out.
• Policies. Policies are non-negative, measurable in $(a,b)$, and Markov in $z$. $\pi^*$ and $\pi_{\rm db}$ are the balance prices of p. 13, not "some optimal policy".
• Prior and normalizations. The prior is a single Gamma, the case of §6; $b$ is a rate. The general statements carry Assumptions 1 and 2. Statements are made for general $\alpha>0$ and $r>0$, as p. 18 claims, not under the normalizations $\alpha = e^{-1}$, $r = 1$.
• Ratios. Ratio bounds are stated multiplicatively, together with finiteness of $J^*$. This rules out the vacuous reading $J^* = \infty$.
• Added hypotheses and corrections.
  • Lemma 4 is false as printed at $x = 0$ ($\tilde J = 0$ while $\bar F/\rho>0$), so $x\ge1$ is added. Its location claim $p\ge p^*$ (proof, p. 35) is included.
  • Corollary 1 needs $x\ge1$, because the prices are undefined at $x=0$.
  • The logit halves of Corollary 1 and Theorem 2 are not stated: the logit family is never defined, contradicts Assumption 1, and comes with the rounded constant 1.27.
  • Lemma 9 uses general $\alpha$ where p. 21 has $\alpha = e^{-1}$.
  • Lemma 2's "increasing" is strict for $x\ge1$.
  • Appendix E is represented by Lemma E.6(2), p. 47: the balance-price (greedy) policy attains $J^*$. The if-and-only-if of Theorem E.2 over all policies is not stated, since the generator $H^\pi$ is not formalized.
• Not included. The integrated form of Lemma 11 (the first-sale coupling bound) is not a milestone; it is the natural next target. Lemma 6, Appendix D and the Lambert-$W$ identities are out of scope.

Reusable pieces are the Gamma–Poisson sales process in the b-clock, the incomplete Gamma function, and the known-rate pricing problem. Proofs of any milestone, of the p. 6 revenue identity, and of Assumptions 1–2 for the exponential law are welcome.

Related platform work in other models: Gallego–van Ryzin known-demand pricing (GVRPricing), Talluri–van Ryzin (RevenueManagement), Bitran–Caldentey (PricingRM.DetHeuristic), and the Bayesian bounds of Satia–Lave (SatiaLave.Bayes).

Selected references

• V. F. Farias, B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010. https://doi.org/10.1287/opre.1090.0729 (manuscript of January 20, 2009, MIT DSpace: https://dspace.mit.edu)
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• V. F. Araman, R. Caldentey, Dynamic Pricing for Nonperishable Products with Demand Learning, Operations Research 57(5):1169–1188, 2009. https://doi.org/10.1287/opre.1090.0669
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8

Why information relaxations

Most stochastic dynamic programs that arise in operations research are too large to solve exactly. In practice one computes a heuristic policy and estimates its expected reward by simulation, which gives a lower bound on the optimal value. To know whether the heuristic is good enough one also needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) give a general way to produce such bounds: relax the requirement that decisions use only the information available when they are made, and charge a penalty for using the extra information.

The idea grew out of option pricing. Rogers (Math. Finance 2002) and Haugh and Kogan (Oper. Res. 2004) bounded the price of an American option from above by letting the holder see the whole future and subtracting a martingale; Andersen and Broadie (Manag. Sci. 2004) built such martingales from approximate exercise policies. Brown, Smith and Sun (2010) extended this to general finite-horizon dynamic programs, to arbitrary penalties, and to imperfect information relaxations in which the decision maker learns some, but not all, of the future. The paper illustrates the framework on an adaptive inventory problem and on pricing American options under stochastic volatility and interest rates.

Setting

Uncertainty is a probability space $(\Omega,\mathcal F,\mathbb P)$. Time is $t=0,\dots,T$. The natural filtration $\mathbb F=(\mathcal F_0,\dots,\mathcal F_T)$ describes what the decision maker knows at the start of each period, with $\mathcal F_0=\{\emptyset,\Omega\}$. An action sequence is $a=(a_0,\dots,a_T)$, and $A$ is the set of feasible sequences. A policy $\alpha:\Omega\to A$ chooses a sequence for each outcome; it is adapted to a filtration $\mathbb G$ if each action $\alpha_t$ is $\mathcal G_t$-measurable. The adapted policies form $\mathcal A_{\mathbb G}$; the measurable policies form $\mathcal A$. The total reward is $r(a,\omega)=\sum_t r_t(a,\omega)$, and the primal problem (1) is

$$\sup_{\alpha\in\mathcal A_{\mathbb F}}\mathbb E[r(\alpha)].$$

A filtration $\mathbb G$ is a relaxation of $\mathbb F$ if $\mathcal F_t\subseteq\mathcal G_t\subseteq\mathcal F$ for all $t$; the perfect-information relaxation has $\mathcal G_t=\mathcal F$. A penalty is a function $z(a,\omega)$; it is dual feasible, $z\in\mathcal Z_{\mathbb F}$, if $\mathbb E[z(\alpha_F)]\le0$ for every $\alpha_F\in\mathcal A_{\mathbb F}$. The dual bound of $(\mathbb G,z)$ is $\sup_{\alpha_G\in\mathcal A_{\mathbb G}}\mathbb E[r(\alpha_G)-z(\alpha_G)]$.

In recursive form, the feasible actions in period $t$ form a set $A_t(a_0,\dots,a_{t-1})$, each $r_t$ is $\mathcal F_t$-measurable and depends on $a_0,\dots,a_t$, and the value functions are $V_{T+1}=0$ and

$$V_t(a_0,\dots,a_{t-1})=\sup_{a_t\in A_t(a_0,\dots,a_{t-1})}\big\{r_t(a_0,\dots,a_t)+\mathbb E[V_{t+1}(a_0,\dots,a_t)\mid\mathcal F_t]\big\}.\qquad(2)$$

Given generating functions $w_t(a)$ depending on $a_0,\dots,a_t$, Proposition 2.2 builds the penalty

$$z_t(a)=\mathbb E[w_t(a)\mid\mathcal G_t]-\mathbb E[w_t(a)\mid\mathcal F_t],\qquad z=\sum_t z_t.$$

The ideal penalty $z^\star$ is this penalty for $w_t(a)=V_{t+1}(a_0,\dots,a_t)$.

Formalization targets

Goal: Theorem 2.3 (The Ideal Penalty)

For every relaxation $\mathbb G$ of $\mathbb F$, $z^\star\in\mathcal Z_{\mathbb F}$ and

$$\sup_{\alpha_F\in\mathcal A_{\mathbb F}}\mathbb E[r(\alpha_F)]=\sup_{\alpha_G\in\mathcal A_{\mathbb G}}\mathbb E[r(\alpha_G)-z^\star(\alpha_G)];\qquad(11)$$

a primal-optimal $\alpha^*_F$ also attains the right side; and under perfect information $r(\alpha^*_F)-z^\star(\alpha^*_F)=\mathbb E[r(\alpha^*_F)]$ almost surely.

Milestones, in the order of the paper

1. §2.1 (p. 3): $V_0$ equals the optimal value of (1).
2. Lemma 2.1 (weak duality, p. 3): $\mathbb E[r(\alpha_F)]\le\sup_{\alpha_G\in\mathcal A_{\mathbb G}}\mathbb E[r(\alpha_G)-z(\alpha_G)]$ for $\alpha_F\in\mathcal A_{\mathbb F}$, $z\in\mathcal Z_{\mathbb F}$.
3. Theorem 2.1 (strong duality, p. 4): the primal value equals $\inf_{z\in\mathcal Z_{\mathbb F}}$ of the dual bound, attained when the primal is bounded.
4. Theorem 2.2 (complementary slackness, p. 4).
5. Proposition 2.1 (structured policies, p. 5).
6. Proposition 2.2(i), (ii) (p. 5): generated penalties have zero $\mathcal F_t$-conditional mean along nonanticipative policies, and their components are $\mathbb G$-adapted and nonanticipative in the actions.
7. Eq. (10) (p. 5): the recursion (2) run with rewards $r_t-z_t$ and filtration $\mathbb G$ solves the dual problem, and $\mathbb E[V^{\mathbb G}_0]$ bounds (1).
8. §2.3 (p. 5): with $w_t=V_{t+1}$, $V^{\mathbb G}_t=V_t$ almost surely.

Significance

Theorems 2.1 and 2.3 say that information-relaxation duality has no gap: the optimal value of a dynamic program can be computed, in principle, as a minimum over penalties of a problem in which the decision maker sees more. Theorem 2.3 adds that the gap is closed by one explicit penalty, built from the value functions, simultaneously for every relaxation. This is the justification for the practical recipe of the paper and of the literature that followed: choose generating functions that approximate the true value functions, and the resulting dual bound approaches the optimum. Under perfect information, part 4 of the goal says the ideal penalty removes all randomness from the penalized reward of an optimal policy.

The paper defers its proofs to an electronic companion; none of these results has a machine-checked proof. This mission produces a checked version of the duality layer for general finite-horizon dynamic programs on a filtered probability space, with conditional expectations as in Mathlib. Weak duality, strong duality and complementary slackness are stated for arbitrary feasible sets and rewards and are reusable for any information-relaxation argument; the recursive statements give a verified link between the Bellman recursion and the primal problem.

Difficulty

The duality statements of §2.2 are elementary once expectations exist; the work is in §2.1 and §2.3. The claim that $V_0$ is the optimal value of (1) needs two facts that the paper asserts without proof: that the supremum in (2) is $\mathcal F_t$-measurable, and that near-optimal actions can be selected measurably, so that a nonanticipative policy comes within $\varepsilon$ of $V_0$ even when the suprema are not attained. Neither holds for general action spaces without measurable-selection arguments, which is why this mission fixes a countable action set. A second difficulty is the evaluation of action-indexed conditional expectations at a random action: $\mathbb E[z_t(\alpha_F)\mid\mathcal F_t]$ conditions $\omega\mapsto z_t(\alpha_F(\omega))(\omega)$, where each $z_t(a)$ is only defined up to null sets, one for each $a$. The induction $V^{\mathbb G}_t=V_t$ must also carry these almost-sure identities through suprema over actions.

Formalization scope

The Lean development lives in the namespace InfoRelax.IdealPenalty. Periods are Fin (T + 1); actions take values in one type X (the disjoint union of the per-period action sets); filtrations are Mathlib Filtrations of the ambient $\sigma$-algebra; conditional expectation is condExp. Primal values, dual bounds and dual values are in EReal, taken over the adapted-policy sets, so that no supremum or infimum silently returns $0$. Penalties in $\mathcal Z$ are required to be integrable along every measurable policy, and the reward is assumed integrable along every policy in the general statements: without this, a Bochner integral of a non-integrable function is $0$ and the statements become vacuous. The value functions (2), the dual value functions (10), the penalty of Proposition 2.2 and $z^\star$ are definitions computed from the data, never variables constrained by hypotheses.

The recursive statements fix a countable action set with the discrete $\sigma$-algebra, bounded period rewards, and generating functions bounded almost everywhere. Identities between value functions are almost sure. The general results (Lemma 2.1, Theorems 2.1–2.2, Proposition 2.1) assume none of this. The optional identity (5), which exchanges a supremum over policies with an expectation of a pathwise supremum, is not formalized: for a general dual feasible penalty the pathwise supremum need not be integrable.

Contributions welcome: the measurable-selection lemma for countable action sets, the tower-property argument for action-indexed conditional expectations evaluated at adapted policies, and proofs of the milestones in any order.

Selected references

• D. B. Brown, J. E. Smith, P. Sun, Information Relaxations and Duality in Stochastic Dynamic Programs, Operations Research, Articles in Advance, 2010. https://doi.org/10.1287/opre.1090.0796
• L. C. G. Rogers, Monte Carlo valuation of American options, Mathematical Finance 12(3), 2002. https://doi.org/10.1111/1467-9965.02010
• M. B. Haugh, L. Kogan, Pricing American Options: A Duality Approach, Operations Research 52(2), 2004. https://doi.org/10.1287/opre.1030.0070
• L. Andersen, M. Broadie, Primal-Dual Simulation Algorithm for Pricing Multidimensional American Options, Management Science 50(9), 2004. https://doi.org/10.1287/mnsc.1040.0258