Probability

Why conformal welding by quantum length

Liouville quantum gravity (LQG) equips a planar domain with a random area measure $\mu_h$ and a random boundary length measure $\nu_h$. Both are built from an instance $h$ of the Gaussian free field (GFF). The Schramm–Loewner evolution $\mathrm{SLE}_\kappa$ is the conformally invariant random curve that describes interfaces in critical planar models. Sheffield's paper (arXiv:1012.4797, Ann. Probab. 44 (2016)) shows that the two are linked by a conformal welding. Zipping up a free boundary GFF by a reverse Loewner flow glues two boundary arcs of equal quantum length, and the glued seam is an $\mathrm{SLE}_\kappa$ curve.

This "quantum zipper" is the starting point of the mating-of-trees programme (Duplantier–Miller–Sheffield, arXiv:1409.7055). It is also the mechanism behind the conjectured, and partly proved, scaling limits of random planar maps decorated by statistical-physics models.

Timeline:

• 2005 — reverse Loewner flows are studied by Rohde and Schramm (RS05). They show that for $\kappa<4$ the SLE trace is simple and its complement is a Hölder domain.
• 2000 — Jones and Smirnov show that boundaries of Hölder domains are conformally removable (JS00).
• 2011 — Duplantier and Sheffield construct $\mu_h$ and $\nu_h$ as almost sure limits along dyadic scales and prove the KPZ relation (DS11a).
• 2010–2016 — this paper (arXiv v1 2010, v2 2015, journal 2016) proves the welding theorem (Theorem 1.3) and the quantum-length zipper (Theorem 1.8).

Setting

$\mathbb H=\{z:\operatorname{Im}z>0\}$, and the free boundary Green's function is $G(y,z)=-\log|y-z|-\log|y-\bar z|$. Fix $\kappa\in(0,4)$ and put $\gamma=\sqrt\kappa$ and $Q=2/\gamma+\gamma/2$.

• Reverse Loewner flow. For a standard Brownian motion $B$, $f_t=g_t-\sqrt\kappa B_t$, where $\partial_tg_t(z)=-2/(g_t(z)-\sqrt\kappa B_t)$ and $g_0(z)=z$. Then $f_T$ maps $\mathbb H$ onto $\mathbb H\setminus\eta_T$, and $\eta_T$ is a simple curve.
• The coupled field. Let $\mathfrak h_t(z)=\frac2{\sqrt\kappa}\log|f_t(z)|+Q\log|f_t'(z)|$. With $\tilde h$ a free boundary GFF independent of $B$,

$$h=\mathfrak h_T+\tilde h\circ f_T ,$$

which by Theorem 1.2 has the law of $\frac2{\sqrt\kappa}\log|\cdot|+\tilde h$ modulo additive constants.

• Quantum length. $h_\varepsilon(x)$ is the mean of $h$ on the upper semicircle of radius $\varepsilon$ around $x\in\mathbb R$. Then

$$\nu_h=\lim_{n\to\infty}\varepsilon_n^{\gamma^2/4}e^{\gamma h_{\varepsilon_n}(x)/2}\,dx,\qquad \varepsilon_n=2^{-n},$$

as a vague limit. The area measure $\mu_h$ is the analogous limit with circle averages and exponent $\gamma^2/2$.

• Quantum wedges. An $\alpha$-quantum wedge is the doubly marked surface $(\mathbb H,h)$ with $h=h^\dagger+Q(-\log|\cdot|)+A_{-\log|\cdot|}$ (1.10). Here $h^\dagger$ is the lateral part of the GFF and $A$ is a two-sided drifted Brownian motion. A surface is identified with its canonical description, normalized by $\mu_h(B_1(0))=1$.

Formalization targets

Goal: Theorem 1.3

Almost surely, for every $z$ on $\eta_T$ and the two real points $z_-<0<z_+$ that $f_T$ maps to $z$,

$$\nu_h\big([z_-,0]\big)=\nu_h\big([0,z_+]\big).$$

The statement is scale free: it does not depend on the additive constant of $h$.

Milestones

1. Theorem 4.5. Reverse $\mathrm{SLE}_{\kappa,\rho}$ zipping preserves the law of $\hat{\mathfrak h}_0+\tilde h$, with $\hat{\mathfrak h}_t=\mathfrak h_t+\frac1{2\sqrt\kappa}\int G_t(y,\cdot)\rho(dy)$.
2. Proposition 5.4. Under $e^{(h^0,\rho)}\Gamma$, the zipper is the modified SLE of Theorem 4.5.
3. Proposition 1.6. Zooming in at a $\nu_h$-typical boundary point gives a $\gamma$-quantum wedge.
4. Proposition 1.7. The $\gamma$-wedge is stationary under shifting the origin by a fixed quantum length.
5. Lemma 5.6. Sampling $x$ from $\nu_h[-\delta,0]$ under $\Gamma$ turns the zipper into $\mathrm{SLE}_{\kappa,\rho}$ with $\rho=\gamma^2\delta_x-\gamma^2\sigma_{0,1}$.
6. Theorem 1.8, length clause. On a $(\gamma-2/\gamma)$-quantum wedge with an independent $\mathrm{SLE}_{\gamma^2}$, the quantum lengths of the two sides of the curve agree.

Significance

Theorem 1.3 says that reverse SLE zipping is a welding by quantum length. Combined with the removability of $\mathrm{SLE}_\kappa$ for $\kappa<4$, it gives Theorem 1.4: the field $h$ determines the curve $\eta_T$. The same equality of boundary lengths on the two sides of an SLE is the defining property of the quantum-zipper and mating-of-trees constructions, which build random surfaces by welding wedges together.

All results here are proved in the paper, and none has a machine-checked proof. The proofs are partly sketches: Proposition 5.5 ends with a limiting estimate, and the zero–one step of Theorem 1.8 is delegated to [DMS14a, Lemma 8.2]. A formal development would therefore check the most cited welding argument in random conformal geometry. The definitions it needs (arc averages of a GFF, $\nu_h$, quantum wedges, conditionally Gaussian fields) are reusable for any LQG statement.

Difficulty

The obvious argument tries to compare the left and right boundary measures directly, ball by ball along the curve. It fails because the two measures depend on the field near the curve in the same way (5.1): nothing local distinguishes them, and nothing local forces them to agree. The paper instead builds a stationary picture (Lemma 5.6, Proposition 5.5, Figure 1.7). It shows that the curve splits a $(\gamma-2/\gamma)$-wedge into two independent $\gamma$-wedges, and it uses the ergodic theorem with scale invariance to force the ratio of the two lengths to be a constant $c$, which symmetry makes equal to $1$. The last step transfers the result from the wedge to the field of Theorem 1.3 by absolute continuity. Every step uses Gaussian conditioning on random conformal images of the field, which current libraries lack.

Formalization scope

Conventions committed to in Lean:

• Time is $\mathbb R_{\ge0}$, and Brownian motion is Mathlib's IsBrownianReal. Flows are pathwise ODE solutions, with no stochastic integrals.
• A field is a random map $\Psi(\omega,\mu)=(h,\mu)$ on admissible measures: finite, bounded support in $\mathbb H$, finite logarithmic energy. Its law is given in characteristic-function form, as "conditionally Gaussian given $\mathcal G$ with mean $m$ and covariance $C$". The arc averages $h_\varepsilon(z)=(h,\sigma_{z,\varepsilon})$ are continuous in $(z,\varepsilon)$.
• Additive constants are fixed by $h_1(0)=0$ (semicircle of radius $1$), the paper's normalization (5.9).
• $\nu_h$ and $\mu_h$ are predicates: the a.s. vague limits along $2^{-n}$ with locally integrable densities. The measure $\nu\equiv0$ cannot satisfy them vacuously, and the sanity file proves that adding $C$ to the field multiplies $\nu$ by $e^{\gamma C/2}$.
• The points $z_\pm$ are encoded by radial boundary limits of $f_T$. "Agree in law" means equality of the laws of all pairings, and convergence of random surfaces means convergence of the finite-dimensional laws of $\int f\,d\mu^{\mathrm{can}}$.
• $\Gamma$ is encoded by its restriction to $(h^0,(f_t)_{t\ge0})$. The forward SLE of Theorem 1.8 is the platform definition OAI.SLEExactGauge.IsOrdinaryChordalSLE.

Disclosed readings of the text:

• "$\alpha<0$" in (1.10) is read as $\alpha<Q$.
• The force set $\mathcal C$ of Theorem 4.5 lies in $\overline{\mathbb H}$.
• Proposition 5.4 uses the measure $2\sqrt\kappa\,\rho$ in (4.4)–(4.6).
• The "unit circle" of Lemma 5.6 is the upper unit semicircle.
• $\gamma=0$ is excluded in Proposition 1.6.

Contributions are welcome on any of the following:

• existence of the predicates ($\nu_h$, wedges, $\Gamma$);
• Gaussian conditioning on conformal images;
• the Itô computations behind Theorem 4.5;
• the milestones themselves.

Selected references

• S. Sheffield, Conformal weldings of random surfaces: SLE and the quantum gravity zipper, Ann. Probab. 44(5), 2016. https://arxiv.org/abs/1012.4797 (v2), https://doi.org/10.1214/15-AOP1055
• B. Duplantier, S. Sheffield, Liouville quantum gravity and KPZ, Invent. Math. 185, 2011. https://arxiv.org/abs/0808.1560
• S. Rohde, O. Schramm, Basic properties of SLE, Ann. of Math. 161, 2005. https://arxiv.org/abs/math/0106036
• P. Jones, S. Smirnov, Removability theorems for Sobolev functions and quasiconformal maps, Ark. Mat. 38, 2000. https://doi.org/10.1007/BF02384490
• B. Duplantier, J. Miller, S. Sheffield, Liouville quantum gravity as a mating of trees, Astérisque 427, 2021. https://arxiv.org/abs/1409.7055
• S. Sheffield, Gaussian free fields for mathematicians, Probab. Theory Related Fields 139, 2007. https://arxiv.org/abs/math/0312099

Motivation

Linear-quadratic (LQ) control is the setting in which stochastic optimal control has a closed-form answer: the optimal control is a linear feedback of the state, and the feedback gain comes from a Riccati differential equation. In the mean-field version, the expectation $\mathbb E[X]$ of the state and $\mathbb E[u]$ of the control appear in the dynamics and in the cost. Mean-field SDEs go back to Kac (1956) and McKean (1966) as models of interacting particle systems. A cost containing $\mathbb E[X]$ can penalize the variance $\operatorname{var}(X)=\mathbb E|X|^2-|\mathbb E[X]|^2$ of the state, which is what is wanted when the optimal state should not be too sensitive to the noise (mean–variance portfolio selection is the standard example). With such a cost the problem is no longer a classical LQ problem: the weights on $\mathbb E[X]$ may be negative definite, and the cost is not an expectation of a function of the state path, so the classical Riccati theory does not apply as it stands.

J. Yong (SIAM J. Control Optim. 51(4), 2013, pp. 2809–2838) solved the problem with deterministic coefficients. He derives the optimality system, a linear mean-field forward–backward SDE, and decouples it with two Riccati equations. One governs the deviation $X-\mathbb E[X]$, the other the mean $\mathbb E[X]$. The optimal control is then an explicit state feedback.

Timeline:

• 1956, 1966: Kac and McKean introduce the McKean–Vlasov (mean-field) SDE.
• 1968–1998: the classical stochastic LQ problem and its Riccati equation (Wonham 1968; Chen, Li and Zhou 1998; Yong–Zhou 1999, the paper's reference [38]).
• 2009–2011: maximum principles for mean-field SDE control (Buckdahn–Djehiche–Li; Andersson–Djehiche; Meyer-Brandis–Øksendal–Zhou).
• 2013: Yong, the mean-field LQ problem solved by two Riccati equations (this mission).

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a complete probability space carrying a one-dimensional standard Brownian motion $W$, and let $\mathbb F$ be the natural filtration of $W$ augmented by the $\mathbb P$-null sets. Fix a horizon $T>0$. An admissible control is an $\mathbb F$-progressively measurable $u:[0,T]\times\Omega\to\mathbb R^m$ with $\mathbb E\int_0^T|u|^2ds<\infty$; the set of them is $\mathcal U[0,T]$. For $x\in\mathbb R^n$ the state solves

$$dX=\big(AX+\bar A\,\mathbb E[X]+Bu+\bar B\,\mathbb E[u]\big)ds+\big(CX+\bar C\,\mathbb E[X]+Du+\bar D\,\mathbb E[u]\big)dW,\qquad X(0)=x,$$

with deterministic matrix-valued coefficients. The cost is

$$J(x;u)=\mathbb E\Big\{\int_0^T\big[\langle QX,X\rangle+\langle\bar Q\,\mathbb E[X],\mathbb E[X]\rangle+\langle Ru,u\rangle+\langle\bar R\,\mathbb E[u],\mathbb E[u]\rangle\big]ds+\langle GX(T),X(T)\rangle+\langle\bar G\,\mathbb E[X(T)],\mathbb E[X(T)]\rangle\Big\}.$$

Problem (MF-LQ): minimize $J(x;\cdot)$ over $\mathcal U[0,T]$. The assumptions are:

• (H1): the eight coefficients are in $L^\infty(0,T)$.
• (H2): the weights are bounded and symmetric, and for some $\delta>0$, $Q,\ Q+\bar Q\ge0$, $R,\ R+\bar R\ge\delta I$ and $G,\ G+\bar G\ge0$.

The weights $\bar Q,\bar R,\bar G$ themselves need not be semidefinite.

With $\Sigma_0=R+D^TPD$ and $\Sigma_1=R+\bar R+(D+\bar D)^TP(D+\bar D)$, the two Riccati equations are

$$\dot P+PA+A^TP+C^TPC+Q-(PB+C^TPD)\Sigma_0^{-1}(B^TP+D^TPC)=0,\qquad P(T)=G,\tag{4.8}$$ $$\dot\Pi+\Pi(A+\bar A)+(A+\bar A)^T\Pi+(C+\bar C)^TP(C+\bar C)+Q+\bar Q-\big[\Pi(B+\bar B)+(C+\bar C)^TP(D+\bar D)\big]\Sigma_1^{-1}\big[(B+\bar B)^T\Pi+(D+\bar D)^TP(C+\bar C)\big]=0,\tag{4.9}$$

with $\Pi(T)=G+\bar G$. Write $K_0=\Sigma_0^{-1}(B^TP+D^TPC)$ and $K_1=\Sigma_1^{-1}[(B+\bar B)^T\Pi+(D+\bar D)^TP(C+\bar C)]$.

Formalization targets

Goal: Theorem 4.1 (p. 2827)

Under (H1)–(H2), (4.8) and (4.9) have unique solutions $P$ and $\Pi$ on $[0,T]$. The closed-loop system obtained by substituting

$$u^*=-K_0\big(X^*-\mathbb E[X^*]\big)-K_1\,\mathbb E[X^*]$$

into the state equation has a unique solution $X^*$. With $Y=P(X^*-\mathbb E[X^*])+\Pi\,\mathbb E[X^*]$ and the explicit $Z$, the 4-tuple $(X^*,u^*,Y,Z)$ solves the optimality system, and $(X^*,u^*)$ is optimal. Moreover

$$\inf_{u\in\mathcal U[0,T]}J(x;u)=\langle\Pi(0)x,x\rangle\qquad\forall x\in\mathbb R^n.\tag{4.10}$$

Milestones

1. Proposition 2.6: the state equation is well posed in $\widehat{\mathcal X}[0,T]$.
2. Proposition 2.8: $J(0;u)\ge\delta\,\mathbb E\int_0^T|u|^2ds$, and (MF-LQ) has a unique optimal control.
3. Theorem 3.1: the necessary condition, i.e. the MF-BSDE (3.1) and the stationarity condition (3.2).
4. Theorem 3.2: the sufficient condition.
5. Corollary 3.3: unique solvability of the MF-FBSDE (3.3).
6. §4, p. 2825: (4.8) has a unique solution $P\ge0$.
7. §4, p. 2825: the matrix identity $P-P\widetilde D\Sigma_1^{-1}\widetilde D^TP=P^{1/2}(I+P^{1/2}\widetilde D\widetilde R^{-1}\widetilde D^TP^{1/2})^{-1}P^{1/2}\ge0$.
8. §4, p. 2826: (4.9) has a unique solution $\Pi\ge0$.
9. Proof of Theorem 4.1, p. 2828: the completion-of-squares identity $J(x;u)-\langle\Pi(0)x,x\rangle=\mathbb E\int_0^T(\langle\Sigma_0w_0,w_0\rangle+\langle\Sigma_1w_1,w_1\rangle)ds$.

The Woodbury identity used on p. 2826 is already proved on the platform (FamousTheorems.woodbury_identity) and is referenced.

Significance

The result. Theorem 4.1 reduces a mean-field stochastic control problem, whose state law enters the dynamics, to two matrix ODEs. The optimal control is computable offline: integrate $P$ and $\Pi$ backward, then feed back the state and its mean. The value $\langle\Pi(0)x,x\rangle$ is explicit, so cost comparisons between the mean-field problem and its classical counterpart become comparisons between Riccati solutions; §5 of the paper does exactly this for variance-penalized costs. When all barred coefficients vanish, $\Pi=P$ and the classical stochastic LQ feedback is recovered.

Formalizing it. The result is proved, not open; this mission formalizes the known proof. No continuous-time stochastic LQ theorem exists on the platform. The mission builds on the published stochastic calculus of Peng1990.SMP.Stochastic (Itô integrals, SDE and BSDE solutions, $L^2_{\mathbb F}$) and adds a reusable mean-field LQ setting, matrix Riccati equations in integral form, and a verification theorem. None of the statements has a machine-checked proof yet.

Difficulty

The Riccati equations are nonlinear matrix ODEs with only $L^\infty$ coefficients. Local existence is routine, but global existence on $[0,T]$ needs an a priori bound, which a local fixed-point argument does not give. The bound comes from the control interpretation of the equation, and it requires semidefiniteness of $P$. The second equation contains $P$, and its quadratic term is only controlled when $\Sigma_1\ge\delta I$, which in turn needs $P\ge0$. Its "state weight" is semidefinite only through the identity of milestone 7, even though $\bar Q$ itself may be negative definite. On the stochastic side, the verification step (milestone 9) and the duality arguments of Theorems 3.1–3.2 apply Itô's product rule to $\langle P(X-\mathbb E X),X-\mathbb E X\rangle$ and to $\langle X,Y\rangle$ for processes driven by the same Brownian motion, with an absolutely continuous (not differentiable) $P$. Itô's formula is not yet available on the platform: it is the open goal EthierKurtz.ito_formula. Existence in Proposition 2.8 needs a minimizer of a coercive continuous quadratic functional on the Hilbert space $L^2_{\mathbb F}(0,T;\mathbb R^m)$.

Formalization scope

States are Fin n → ℝ, controls Fin m → ℝ, time is ℝ≥0, and the horizon satisfies $T>0$. The probability space is complete. $W$ is Peng1990.SMP.IsStdBrownian with one coordinate, and $\mathbb F$ is ReflectedBSDE.Existence.augmentedFiltration. $\mathbb E[X(s)]$ is the Bochner integral of the solution itself. Every mean-field term is a closure over the process being solved for, never a free deterministic input. Solutions of the forward and backward equations are the published SolvesSDE/SolvesBSDE notions: progressive, square-integrable, with the integral identity at each $t\in[0,T]$ almost surely. Controls and $Z$-components are identified up to $ds\otimes d\mathbb P$-null sets.

Other conventions:

• $L^\infty$ coefficients are measurable functions with an entrywise bound on $[0,T]$.
• (H2) is transcribed literally, with nothing assumed on $\bar Q,\bar R,\bar G$ alone.
• Riccati equations are stated in integral form $P(t)=G+\int_t^TF(s,P(s))ds$ with an integrable right-hand side, since solutions are only absolutely continuous.
• The class of (4.8) is the regular class $\Sigma_0\ge\varepsilon I$, so that Matrix.inv is a true inverse. For (4.9), $\Sigma_1\ge\delta I$ follows from (H2) once $P\ge0$.
• The value (4.10) is stated as a lower bound for every admissible control together with equality at $u^*$, not as an infimum of a set of reals.
• The page's "positive definite" for $P$ and $\Pi$ is false in general ($G=Q=0$ gives $P\equiv0$); the milestones assert positive semidefiniteness.

A formalization in which the mean $\mathbb E[X]$ is an independent input, or in which a Riccati "solution" may use the junk value $0$ of a singular inverse, would trivialize the problem. Both are ruled out by the definitions above. A sorry-free sanity file shows that (H1)–(H2) hold for data with $\bar Q=-\tfrac12I$ negative definite, and that the Riccati class is non-empty.

Contributions are welcome on all of the following:

• the Itô product rule for the published Itô processes;
• the existence of continuous versions;
• Gronwall-type uniqueness for linear mean-field SDEs and BSDEs;
• Carathéodory theory for matrix Riccati equations with measurable coefficients;
• the PSD matrix identity, which uses only Mathlib linear algebra.

Selected references

• J. Yong, Linear-quadratic optimal control problems for mean-field stochastic differential equations, SIAM J. Control Optim. 51(4) (2013) 2809–2838. https://doi.org/10.1137/120892477
• J. Yong and X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3
• S. Chen, X. Li and X. Y. Zhou, Stochastic linear quadratic regulators with indefinite control weight costs, SIAM J. Control Optim. 36(5) (1998) 1685–1702. https://doi.org/10.1137/S0363012996310478
• R. Buckdahn, B. Djehiche and J. Li, A general stochastic maximum principle for SDEs of mean-field type, Appl. Math. Optim. 64 (2011) 197–216. https://doi.org/10.1007/s00245-011-9136-y
• H. P. McKean, A class of Markov processes associated with nonlinear parabolic equations, Proc. Natl. Acad. Sci. USA 56 (1966) 1907–1911. https://doi.org/10.1073/pnas.56.6.1907

Motivation

Counting the proper $q$-colorings of a graph, and sampling one uniformly at random, are basic problems of approximate counting with a long history in statistical physics, where proper colorings are the zero-temperature antiferromagnetic Potts model. On bipartite graphs these problems are tied to #BIS, the problem of approximately counting independent sets in a bipartite graph, whose complexity is unresolved. Galanis, Štefankovič, Vigoda and Yang showed that approximately counting proper $q$-colorings is #BIS-hard on bipartite graphs of maximum degree $\Delta$ whenever $q \le \Delta/(2\log\Delta)$ (SIAM J. Comput. 45(6), 2016). A positive result in that regime therefore has to use structure beyond bipartiteness and bounded degree.

Jenssen, Keevash and Perkins (SIAM J. Comput. 49(4) 2020) use expansion. Their Theorem 5 says that for $\Delta \ge Cq^2\log^2 q$ there is an FPTAS and a polynomial-time sampler for proper $q$-colorings on almost every $\Delta$-regular bipartite graph. This answered Conjecture 1 of the authors' SODA 2019 extended abstract. Liao, Lin, Lu and Mao (APPROX/RANDOM 2019) independently proved a similar result under a slightly stronger condition on $\Delta$. The organizing idea, that most colorings of a strongly expanding bipartite graph follow one of a few patterns, comes from the work of Peled and Spinka on rigidity of colorings of $\mathbb Z^d$ (arXiv:1808.03597).

This mission is the fourth of a series formalizing the four main results of that paper; it covers Theorem 5.

Setting

Fix integers $q \ge 3$, $\Delta \ge 3$ and $m \ge 1$. The vertex set is $V = \mathcal O \sqcup \mathcal E$, two sides of $m$ vertices each (so $n = 2m$). $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ is the finite set of labelled simple graphs on $V$ whose edges all join $\mathcal O$ to $\mathcal E$ and in which every vertex has degree $\Delta$. A property holds for almost every $\Delta$-regular bipartite graph if the fraction of graphs in $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ having it tends to $1$ as $m \to \infty$.

For $S \subseteq V$ the vertex boundary $\partial S$ is the set of vertices outside $S$ with a neighbour in $S$, and $S^+ = S \cup \partial S$. The graph is a bipartite $(\sigma,\rho)$-expander if $|\partial S| \ge \rho|S|$ for every $S$ inside one side with $|S| \le \sigma m$.

A proper $q$-coloring is a map $f : V \to [q]$ with $f(u) \ne f(v)$ on every edge; $\mathcal X_q(G)$ is their set and $Z_G(q) = |\mathcal X_q(G)|$. A pattern is a pair $(A,B)$ of disjoint sets with $A \cup B = [q]$; there are $2^q$ of them. A coloring agrees with $(A,B)$ at $v$ if $v \in \mathcal O$ and $f(v) \in A$, or $v \in \mathcal E$ and $f(v) \in B$. For $S \subseteq V$, $\chi_{A,B}(S)$ is the set of proper colorings that disagree with $(A,B)$ at every vertex of $S$ and agree everywhere else.

$G^3$ joins two vertices at $G$-distance at most $3$. A set is little if $|S| \le 4q\frac{\log\Delta}{\Delta}m$. A polymer is a little set that is connected in $G^3$; $\mathcal C(G)$ is the set of polymers, and two polymers are compatible if their $G$-distance exceeds $3$. For a pattern $(A,B)$, the weight and the polymer partition function are

$$w_{A,B}(\gamma) = \frac{|\chi_{A,B}(\gamma)|}{|A|^m|B|^m}, \qquad \Xi_{A,B}(G) = \sum_{\Gamma} \prod_{\gamma\in\Gamma} w_{A,B}(\gamma),$$

the sum over all families $\Gamma \subseteq \mathcal C(G)$ of pairwise compatible polymers, the empty family included. Finally $\hat Z$ is an $\varepsilon$-relative approximation to $Z$ if $e^{-\varepsilon}\hat Z \le Z \le e^{\varepsilon}\hat Z$.

Formalization targets

Goal: the deterministic core of Theorem 5

There is an absolute constant $C > 0$ such that for all $q \ge 3$ and $\Delta \ge Cq^2\log^2 q$, almost every $\Delta$-regular bipartite graph $G$ satisfies

$$e^{-\varepsilon}\tilde Z_G(q) \le Z_G(q) \le e^{\varepsilon}\tilde Z_G(q), \qquad \tilde Z_G(q) = \sum_{(A,B)} |A|^m|B|^m\,\Xi_{A,B}(G), \quad \varepsilon = e^{-m/(4q)},$$

and, for every pattern $(A,B)$ and every polymer $\gamma \in \mathcal C(G)$, the Kotecký–Preiss condition

$$\sum_{\gamma' \in \mathcal C(G):\ d(\gamma',\gamma)\le 3} w_{A,B}(\gamma')\,e^{|\gamma'| + g(\gamma')} \le |\gamma|, \qquad g(\gamma) = \frac{\Delta}{10q^2\log\Delta}|\gamma|.$$

The constant $C$ is left existential, as in the paper.

Milestones

In the order of the proof:

1. Lemma 23, the expansion of almost every regular bipartite graph;
2. Lemma 27, the bound on $|\chi_{A,B}(S)|$;
3. Lemma 28, the covering of $\mathcal X_q(G)$ by $\chi_{A,B}(S)$ with $S$ little;
4. the product formula after (13);
5. Claim 30, the size bound for sparse sets;
6. the binomial estimate, an existing platform theorem;
7. Lemma 29, the reduction;
8. the weight bound of §5.1;
9. the per-vertex estimate (15).

Significance

The goal is the whole mathematical content of Theorem 5. The paper's algorithm (its Theorem 8, adapted from Helmuth, Perkins and Regts, Algorithmic Pirogov–Sinai theory) takes exactly these two facts as input. Given the Kotecký–Preiss condition, the cluster expansion of each $\log\Xi_{A,B}(G)$ converges and truncating it gives the estimator; the reduction transfers the estimate to $Z_G(q)$. With the goal proved, the remaining distance to the FPTAS is algorithmic bookkeeping, not combinatorics.

The result has been proved since 2019 and is not formalized anywhere. A formal proof would add a machine-checked polymer-model reduction for a spin system with exponentially many ground states, a reusable model of uniformly random regular bipartite graphs, and a checked instance of the "expansion implies few ground states" argument used throughout this literature.

Difficulty

The obvious first idea is a one-ground-state expansion, as for the hard-core model, where configurations are close to "all even" or "all odd". For colorings there are $2^q$ patterns. A coloring can lie close to several of them, so the reduction must show that the sets $\chi_{A,B}(S)$ with $S$ little overlap only negligibly. That needs an inclusion–exclusion step whose error is exponentially small in $m/q$. A second difficulty is the size of polymers: little sets are $q$ times larger than the sets of the hard-core analysis. Claim 30 is what keeps the union of compatible polymers from becoming a large set that the expansion no longer controls. Finally, the constants must be uniform in $q$. The single condition $\Delta \ge Cq^2\log^2 q$ has to cover the expansion lemma, the reduction and the Kotecký–Preiss estimate at once.

Formalization scope

The FPTAS and the sampling algorithm are not formalized. Mathlib has no machine model in which "polynomial time" could be stated, and the running times carry unquantified constants. The goal is the mathematics the algorithm rests on: the reduction and the Kotecký–Preiss condition, with the paper's constants $e^{-m/(4q)}$, $4q\log\Delta/\Delta$ and $\Delta/(10q^2\log\Delta)$. Neither half may be dropped. Replacing $e^{-m/(4q)}$ by an existential error, or summing the Kotecký–Preiss condition over compatible rather than incompatible polymers, would make the goal trivial or wrong.

Conventions committed to in Lean:

• Vertices are Fin m ⊕ Fin m, and $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ is the set of labelled $\Delta$-regular graphs with edges only between the two fixed sides. The paper does not fix a bipartition; this fixed-sides model is a disclosed choice, matching §5's $|\mathcal O| = |\mathcal E| = m$.
• Distances are Mathlib's extended distance edist, so vertices in different components are at distance $\infty$ and never incompatible.
• A pattern is encoded by $A \subseteq [q]$ with $B = [q]\setminus A$. Patterns with an empty side are kept: their weights are $0$ under Lean's $x/0 = 0$, so they contribute $0$ to $\tilde Z_G(q)$, as on the page for large $m$.
• log is the natural logarithm; the binomial estimate is used in nats.

Added hypotheses:

• $A, B \ne \emptyset$ in Lemma 27 and in the product formula, which divide by $|A|$ and $|B|$;
• $\Delta \ge 3$ in Lemma 28 and Claim 30, the paper's standing convention (§1.3);
• $m \ge 1$ in Lemma 29, which fails on the empty vertex set.

The goal needs none of these, since its limit is in $m$ and its constant absorbs $\Delta$.

A complete development needs a counting theory of random regular bipartite graphs (for Lemma 23, through Bassalygo's expansion theorem), counts of connected sets in bounded-degree graphs, and inclusion–exclusion over patterns. The random-graph model and the polymer-model definitions are reusable across this series and beyond. Proofs of any milestone, and alternative routes to Lemma 23, are welcome.

Selected references

• M. Jenssen, P. Keevash and W. Perkins, Algorithms for #BIS-hard problems on expander graphs, SIAM J. Comput. 49(4) (2020) 681–710. https://doi.org/10.1137/19M1286669
• A. Galanis, D. Štefankovič, E. Vigoda and L. Yang, Ferromagnetic Potts model: refined #BIS-hardness and related results, SIAM J. Comput. 45(6) (2016) 2004–2065.
• R. Peled and Y. Spinka, Rigidity of proper colorings of $\mathbb Z^d$, arXiv:1808.03597 (2018). https://arxiv.org/abs/1808.03597
• C. Liao, J. Lin, P. Lu and Z. Mao, Counting independent sets and colorings on random regular bipartite graphs, APPROX/RANDOM 2019, Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2019).
• T. Helmuth, W. Perkins and G. Regts, Algorithmic Pirogov–Sinai theory, Probab. Theory Related Fields (2020); extended abstract at STOC 2019.
• R. Kotecký and D. Preiss, Cluster expansion for abstract polymer models, Comm. Math. Phys. 103(3) (1986) 491–498.
• L. A. Bassalygo, Asymptotically optimal switching circuits, Problems Inform. Transmission 17(3) (1981) 206–211.

Motivation

The hard-core model assigns weight to independent vertex sets of a graph. Its partition function counts those sets when the activity is one and weights larger sets more heavily when the activity increases. Counting independent sets on bipartite graphs is a standard benchmark for approximate counting: the general problem is difficult, while random regular graphs have additional expansion that can make approximation possible. Jenssen, Keevash and Perkins prove an approximation and sampling theorem for almost every sufficiently high degree regular bipartite graph when the activity is above an explicit threshold Jenssen–Keevash–Perkins, Theorem 2.

The question is specific to a random graph model. It does not assert the same conclusion for every regular bipartite graph. The authors use a criterion attributed to Bassalygo to show that almost every graph in the model has the expansion needed by their argument Jenssen–Keevash–Perkins, Theorem 22 and Lemma 23. Liao, Lin, Lu and Mao independently obtained related counting results under somewhat stronger parameter conditions Liao–Lin–Lu–Mao, 2019.

Setting

Let $G$ be a simple graph with two labelled sides $\mathcal O$ and $\mathcal E$, each containing $m$ vertices, and let every vertex have degree $\Delta$. An independent set $I$ contains no adjacent pair. For activity $\lambda>0$, the hard-core partition function is

$$Z_G(\lambda)=\sum_{I\text{ independent}}\lambda^{|I|}.$$

For a vertex set $S$, its vertex boundary $\partial S$ consists of vertices outside $S$ with a neighbor in $S$. The graph is a bipartite $(\sigma,\rho)$-expander when every subset of either side with size at most $\sigma m$ has boundary of size at least $\rho$ times its size. The expansion parameters used here are $\sigma=4\log\Delta/\Delta$ and $\rho=\Delta/(4\log\Delta)-1/2$. A set is tiny when its size is at most $\sigma m$ Jenssen–Keevash–Perkins, Definition 21 and §4.4.

The graph $G^2$ joins distinct vertices whose distance in $G$ is at most two. On either side, a polymer is a nonempty, tiny, $G^2$-connected vertex set. Two polymers on the same side are compatible if every pair of their vertices is more than distance two apart in $G$. A polymer $\gamma$ has weight $w_\gamma=\lambda^{|\gamma|}/(1+\lambda)^{|\partial\gamma|}$. Summing products of weights over mutually compatible polymer families gives the partition functions $\Xi^{\mathcal E}(G)$ and $\Xi^{\mathcal O}(G)$ Jenssen–Keevash–Perkins, §§4.1, 4.4.

“Almost every” means that, for fixed $\Delta$, the fraction of labelled $\Delta$-regular bipartite graphs satisfying a property tends to one as $m$ tends to infinity. The random graph is chosen uniformly from graphs on the two fixed sides Jenssen–Keevash–Perkins, p. 3.

Formalization targets

The first target is the authors' expansion premise: for all sufficiently large $\Delta$, almost every graph is a bipartite $(4\log\Delta/\Delta,\Delta/(4\log\Delta)-1/2)$-expander. The main target combines two deterministic claims on almost every such graph. For every $\lambda>50\log^2\Delta/\Delta$, write $n=2m$ and

$$\widehat Z_G(\lambda)=(1+\lambda)^m\bigl(\Xi^{\mathcal E}(G)+\Xi^{\mathcal O}(G)\bigr),\qquad \varepsilon_0=(1+\lambda)^{-n/4}.$$

First, $\widehat Z_G$ is an $\varepsilon_0$-relative approximation in the paper's exponential convention:

$$e^{-\varepsilon_0}\widehat Z_G(\lambda)\le Z_G(\lambda)\le e^{\varepsilon_0}\widehat Z_G(\lambda).$$

Second, each of the two polymer models obeys the Kotecký–Preiss condition with decay $g(\gamma)=|\gamma|\Delta\log(1+\lambda)/(10\log\Delta)$:

$$\sum_{\gamma'\text{ incompatible with }\gamma}w_{\gamma'}e^{|\gamma'|+g(\gamma')}\le |\gamma|.$$

The same graph event must support every activity above the threshold; the activity quantifier is inside the limiting probability. The intermediate targets are Bassalygo's entropy criterion, the high probability expansion lemma, the tiny-side lemma for independent sets, the approximation lemma at its weaker activity threshold, a published binomial-entropy estimate, and the per-vertex polymer sum bound Jenssen–Keevash–Perkins, Theorem 22, Lemmas 23–25 and §4.5.

Significance

The reduction expresses a weighted independent-set count through two finite polymer partition functions whose weights decay under the same expansion condition. The KP bound supplies the convergence condition used by the paper's general polymer approximation theorem. Together these are the mathematical inputs to its algorithmic Theorem 2 Jenssen–Keevash–Perkins, Theorems 2, 8.

A formal proof would make the expansion assumptions, distance convention, graph probability limit, and error normalization explicit. The target is a formalization of a published result, not an open conjecture. The proposal contains statements and definitions; their proofs remain to be supplied. The binomial estimate is already machine checked on Prove2Me and is included by reference.

Difficulty

An independent set can occupy vertices on both sides of a bipartite graph. Merely taking one side as the dominant phase double counts sets that are sparse on both sides. The tiny-side lemma and the polymer decomposition identify and control that overlap. The random graph step also requires an expansion estimate strong enough to apply to every small subset of either side, rather than only to a typical subset Jenssen–Keevash–Perkins, §§4.4–4.5.

Formalization scope

Lean uses finite simple graphs on $\mathrm{Fin}(m)\oplus\mathrm{Fin}(m)$, with the left and right summands serving as the odd and even sides. This fixes a labelled bipartition for the uniform random graph model. Distances use extended natural graph distance, so vertices in different components have infinite distance. Polymer families include the empty family, and graph connectivity excludes the empty polymer. Sizes are natural numbers; thresholds involving logarithms are real inequalities. Binary entropy in the cited expansion theorem is measured in bits, while Mathlib's binary entropy is converted from natural units. The approximation uses exponential relative error exactly as in Definition 10 of the paper.

The FPTAS, sampling algorithm, and running-time assertion are outside this mission because Mathlib has no matching machine and cost model. The goal formalizes both the partition-function reduction and its KP condition, the mathematical inputs consumed by the paper's algorithm theorem. It quantifies over all activities above the threshold within the almost-every event, preventing a separate favorable graph set for each activity. The fixed-sides model and the explicit domain of Bassalygo's entropy formula are disclosed representation choices. The tiny-side milestone (Lemma 24) carries a graph-size threshold depending on the degree: as printed, for every graph size, it fails on small dense graphs (the complete bipartite graph minus disjoint complete blocks), and the main result uses it only as the graph size grows. Reusable contributions include finite graph expansion lemmas, polymer partition-function identities, and bounds on connected vertex sets.

Selected references

• M. Jenssen, P. Keevash and W. Perkins, Algorithms for #BIS-hard problems on expander graphs, SIAM Journal on Computing 49(4), 2020, 681–710. DOI.
• L. Bassalygo, Asymptotically optimal switching circuits, Problems of Information Transmission 17(3), 1981, 206–211. Publisher record.
• C. Liao, J. Lin, P. Lu and Z. Mao, Counting independent sets and colorings on random regular bipartite graphs, APPROX/RANDOM, 2019. DOI.

Motivation

A firm selling a fixed stock of a perishable product over a finite season must set prices without knowing how demand responds to them. Online retail and travel platforms often see a customer's segment before quoting a price, so they can price-discriminate across consumer types. Learning a separate demand curve for each type, however, seems to cost more exploration as the number of types grows. Chen and Gallego (arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022) give a learning algorithm whose regret does not depend on the number of types. Their key step is to learn a single scalar first: the shadow price of inventory.

Earlier work on the single-type problem frames the question. Besbes and Zeevi (Operations Research, 2009) defined the regret against the fluid benchmark and showed that no policy can achieve regret decaying faster than $n^{-1/2}$. Wang, Deng and Ye (Operations Research, 2014) gave a single-product algorithm whose regret matches this rate up to logarithmic factors. Chen and Gallego extend the rate to $M$ types with one inventory constraint.

Setting

There are $M\ge1$ consumer types, a season $[0,T]$ and an inventory $c$. When the firm charges price $p$ to type $m$, type-$m$ consumers arrive at rate $d_m(p)$. Prices range over $[0,p_\infty]$, where $p_\infty$ is a choke price with $d_m(p_\infty)=0$. Assumption 1 asks that each $d_m$ be strictly decreasing, bounded and Lipschitz, and that the revenue rate $r_m(\lambda)=\lambda d_m^{-1}(\lambda)$ be Lipschitz and twice differentiable, with $0<M_3\le-r_m''\le M_4$.

The fluid problem (2) maximizes $\sum_m\int_0^Tp_m(t)d_m(p_m(t))\,dt$ subject to $\sum_m\int_0^Td_m(p_m(t))\,dt\le c$. Its optimal value is $J^D(T,c)$. Its dual is one-dimensional. With

$$\mathcal R_m(z)=\max_{p}d_m(p)(p-z),\qquad \mathcal P_m(z)=\operatorname*{argmax}_pd_m(p)(p-z),\qquad g(z)=cz+T\sum_m\mathcal R_m(z),$$

the dual optimum is $z^*=\operatorname{argmin}_{z\ge0}g(z)$, and the optimal fluid prices are the constants $p^*_m=\mathcal P_m(z^*)$.

In the $n$-th system demand and inventory scale together: type $m$ arrives as a Poisson process with rate $n\,d_m(p)$, and the inventory is $nc$. The firm does not know $d_m$. It knows $T$, $c$, $n$, the constants of Assumption 1 and, by Assumption 2, intervals $[\underline p,\overline p]$ and $[0,\overline z]$ that contain every $p^*_m$ and $z^*$. A policy $\pi$ has expected revenue $J^\pi_n(T,c)$, and its regret is

$$R^\pi_n(T,c)=1-\frac{J^\pi_n(T,c)}{J^D_n(T,c)}.$$

Algorithm 1, the primal-dual learning algorithm, runs phases $k=1,\dots,K$ of shrinking lengths $\tau^{(k)}$. In each learning phase it tests a price grid inside the current interval estimators of every $p^*_m$. It then minimizes an empirical dual function on a grid of $z$ and re-centres the interval estimators of $z^*$ and $p^*_m$. In the last phase it either charges a marked-up price (sufficient capacity), or tests two prices and interpolates between them so that total sales end close to $nc$ (insufficient capacity). Its tuning depends on a constant $\epsilon>0$.

Formalization targets

Goal: Theorem 1 (p. 17)

For every $\delta>0$ one can choose $\epsilon>0$ and a constant $C$, independent of $n$, such that

$$R^\pi_n(T,c)\le C(\log n)^{2+\delta}n^{-1/2}\qquad\text{for all }n\ge3.$$

The two capacity regimes (Propositions 2–3)

$$z^*=0:\ R^\pi_n=O\big((\log n)^{2+16\epsilon}n^{-1/2}\big),\qquad z^*>0:\ R^\pi_n=O\big((\log n)^{2+18\epsilon}n^{-1/2}\big).$$

Milestones

• Proposition 1: the fluid problem is solved by the constant prices $p^*$, with complementary slackness; and the monotonicity, convexity and derivative of $\mathcal P_m$ and $\mathcal R_m$.
• Lemmas 9 and 10: a Poisson tail bound decaying faster than any power, and $\mathbb E|X-\lambda|\le\sqrt\lambda$.
• Lemmas 1 and 2: $K\le3\log n+3$, and the learning phases take at most half the season.
• Lemmas 3–5: the interval estimators contain $z^*$, $p^*_m$ and $\mathcal P_m$ on the dual interval, except with probability $O((\log n)^2/n)$.
• Lemmas 6–7: the sales at the start of the last phase are close to the fluid level.
• Lemma 8: when $z^*>0$, $\mathbb E|S(T)-nc|=O((\log n)^\epsilon n^{1/2})$.

Significance

Theorem 1 states that personalized pricing for $M$ types under a shared inventory constraint is learnable at the single-type rate $n^{-1/2}$, up to logarithms, with a constant independent of $n$. Combined with the Besbes–Zeevi lower bound, the algorithm is rate-optimal. Learning the scalar shadow price $z^*$, instead of the joint optimum of an $M$-dimensional problem, is what avoids the curse of dimensionality.

The result is proved in the paper; no machine-checked version exists. A formalization would add to the platform a multi-type Poisson pricing model with stock-outs, the one-dimensional Lagrangian dual of the fluid revenue-management problem, an exactly specified multi-phase learning algorithm, and reusable Poisson deviation lemmas. Lemmas 1, 2, 9 and 10 and Proposition 1 can be proved independently of the probabilistic analysis.

Difficulty

The obvious argument estimates every $p^*_m$ directly and charges the estimate. With interval estimators of width $n^{-1/4}$ this loses revenue of order $n^{-1/4}$ per unit time when the inventory constraint binds ($z^*>0$), because $p^*_m$ is then not the unconstrained maximizer of $p\,d_m(p)$. The paper's (11) and (19) show the loss. The bound $n^{-1/2}$ requires steering the total sales to within $O(n^{1/2})$ of the inventory, which is Lemma 8, and a second-order expansion of the revenue around $p^*$ that uses the first-order condition $r_m'(d_m(p^*_m))=z^*$.

Formally, a further difficulty is the closed loop: the prices of a phase depend on the counts of earlier phases, and the counts are Poisson only conditionally, through the random time change $N_m(n\int_0^td_m(P_m(s))\,ds)$.

Formalization scope

All declarations live in the namespace PrimalDualPricing.Regret. Printed page numbers equal PDF page numbers in the cited preprint.

• Model. Types are Fin M. Each $d_m:\mathbb R\to\mathbb R$ satisfies Assumption 1 on $[0,p_\infty]$ and is otherwise any extension with $0\le d_m\le M_1$; the last-phase prices $\underline p^{(K)}_m-\alpha$ and $\overline p^{(K)}_m+\alpha$ can leave $[0,p_\infty]$. $d_m(p_\infty)=0$ encodes the choke price. $\mathcal P_m$ and $z^*$ are fields carrying their optimality properties.
• Assumption 2 is read with $z^*\in[0,\overline z)$; the page prints $(0,\overline z)$, which would drop the case $z^*=0$ that Proposition 2 and Theorem 1 cover. The price interval is placed in the domain, $0\le\underline p<\overline p\le p_\infty$.
• Remark 2 assumes $M_3\le g''\le M_4$; this is read on $[0,\overline z]$, because globally it is unsatisfiable. Each $\mathcal P_m$ is $M_2$-Lipschitz.
• The fluid value $J^D$ is the supremum of (2) over measurable price paths. The identity $J^D=T\sum_mp^*_md_m(p^*_m)$ is Proposition 1.4, a milestone, and is not built into the definition.
• The algorithm. The grid sizes $N^{(k)}$, $N_z^{(k)}$ are rounded up. Grid spacing is $\Delta_m/N$ for prices and $\Delta_z/(N_z+1)$ for duals: the text and Table 1, respectively the text and line 15, agree on these, and Algorithm 1 line 7 and Table 1 print the other forms. Ties in (8)–(9) go to the smallest index. $\theta$ in (14) is projected onto $[0,1]$, with $\theta=0$ when (14) is degenerate. An empty $p^l$ period in step 4 follows the pseudo-code. The decision rules never take $d_m$, $\mathcal P_m$ or $z^*$ as arguments.
• The system. $M$ independent unit-rate Poisson processes (the published IsPoissonProcess) with right-continuous, jointly measurable paths. The inventory of the $n$-th system is $\lfloor nc\rfloor$ units, and nothing is sold after the stock-out. Lemmas 6–8 use the uncapped sales of the paper's modified system (§4).
• Asymptotics. "$O(f(n))$" is read as $\exists C$, independent of $n$ and the phase index, for all $n\ge3$. "Sufficiently small $\epsilon$" is read as every $\epsilon\in(0,\epsilon_0)$. The algorithm needs $n\ge3$ for $K$ to exist.
• Corrected misprints. Proposition 1.2 prints $\mathcal R_m'=-\sum_md_m(\mathcal P_m)$ with the index reused; the statement is $-d_m(\mathcal P_m(z))$. Proposition 1.3 and the global form of the bound in 1.1 fail at the kinks of $\mathcal P_m$. Part 1's derivative bound is stated as a Lipschitz bound, and part 3 is omitted. Lemmas 3–4 are stated in product form. Propositions 2–3 are stated through their regret conclusions. The printed comparison $\tilde J^\pi_n\le J^\pi_n$ (pp. 13–14) can fail when a last-phase price exceeds $\overline p$, so it is not used.

A formalization that lets the policy read the true demand, measures regret against anything other than $J^D_n$, ignores the stock-out in $J^\pi_n$, or assumes the high-probability events of Lemma 5 would trivialize the goal; none of these is done here.

Contributions to the reusable parts are welcome: Poisson tails, the envelope theorem for $\mathcal R_m$, and the time-change construction of policy-driven Poisson sales.

Selected references

• N. Chen, G. Gallego, A Primal-dual Learning Algorithm for Personalized Dynamic Pricing with an Inventory Constraint, arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1812.09234
• O. Besbes, A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6), 2009. https://doi.org/10.1287/opre.1080.0640
• Z. Wang, S. Deng, Y. Ye, Close the Gaps: A Learning-While-Doing Algorithm for Single-Product Revenue Management Problems, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2013.1249
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24

Motivation

Training a model by stochastic gradients on a constrained or regularized loss is a stochastic composite problem: a smooth expected loss, observed only through noisy gradients, plus a simple non-smooth term such as a constraint set or an $\ell_1$ penalty. For convex losses, accelerated stochastic approximation methods attain the optimal rates (Lan 2012; Ghadimi & Lan 2012). For nonconvex losses, the available guarantees came from randomized stochastic gradient methods (Ghadimi & Lan 2013) and their mini-batch proximal versions (Ghadimi, Lan & Zhang 2016), which are not optimal when the problem happens to be convex.

Ghadimi and Lan (arXiv:1310.3787v1, 2013; Math. Program. 156, 2016) gave one accelerated scheme covering both cases. This mission formalizes its most general result, Theorem 4 (§3.2): the randomized stochastic accelerated gradient (RSAG) method with mini-batches, on a composite objective whose smooth part may be nonconvex and whose gradients are noisy.

Setting

Work in $\mathbb R^n$ with the Euclidean norm. The problem (1.3) is

$$\min_{x\in\mathbb R^n}\ \Phi(x):=\Psi(x)+\mathcal X(x),\qquad\Psi=f+h,$$

where $f$ is differentiable with $L_f$-Lipschitz gradient and may be nonconvex, $h$ is convex and differentiable with $L_h$-Lipschitz gradient, $L_\Psi=L_f+L_h$, and $\mathcal X$ is a convex, possibly non-smooth function with bounded domain $K$ (for instance the indicator of a convex compact set, or that indicator plus $\|\cdot\|_1$).

The prox map (2.37) is $\mathcal P(x,y,c)=\operatorname{argmin}_u\{\langle y,u\rangle+\frac1{2c}\|u-x\|^2+\mathcal X(u)\}$ for $c>0$, and the gradient mapping (2.38) is $\mathcal G(x,y,c)=\frac1c[x-\mathcal P(x,y,c)]$. With $y=\nabla\Psi(x)$, a small $\|\mathcal G\|$ certifies approximate stationarity. Assumption 2 asks for $M$ with $\|\mathcal P(x,y,c)\|\le M$ for all $x,y$ and $c>0$.

Gradients come from a stochastic oracle: queried at $x$, it returns $G(x,\xi)$ for a random sample $\xi$. Assumption 1 asks that the output be unbiased, $\mathbb E[G(x,\xi)]=\nabla\Psi(x)$, with variance at most $\sigma^2$.

Algorithm 4 takes $\alpha_1=1$, $\alpha_k\in(0,1)$ for $k\ge2$, $\beta_k,\lambda_k>0$, batch sizes $m_k\ge1$, starts from $x_0=x^{ag}_0$, and for $k\ge1$ sets

$$x^{md}_k=(1-\alpha_k)x^{ag}_{k-1}+\alpha_kx_{k-1},\qquad\bar G_k=\frac1{m_k}\sum_{i=1}^{m_k}G(x^{md}_k,\xi_{k,i}),$$ $$x_k=\mathcal P(x_{k-1},\bar G_k,\lambda_k),\qquad x^{ag}_k=\mathcal P(x^{md}_k,\bar G_k,\beta_k).$$

With $\Gamma_1=1$ and $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$ (2.6), the output is $(x^{md}_R,x^{ag}_R)$, where $R\in\{1,\dots,N\}$ is drawn independently of the oracle with

$$\mathrm{Prob}\{R=k\}=\frac{\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)}{\sum_{j=1}^N\Gamma_j^{-1}\beta_j(1-L_\Psi\beta_j)}.\tag{3.7}$$

Formalization targets

Goal: Theorem 4 (pp. 21–22)

Fix $N\ge1$, assume for $k=1,\dots,N$

$$\alpha_k\lambda_k\le\beta_k<\frac1{L_\Psi}\ \ (2.9),\qquad\frac{\alpha_1}{\lambda_1\Gamma_1}\ge\frac{\alpha_2}{\lambda_2\Gamma_2}\ge\cdots\ \ (2.10),$$

let $x^*$ be an optimal solution and $S=\sum_{k=1}^N\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)$. Then

$$\mathbb E\big[\|\mathcal G(x^{md}_R,\nabla\Psi(x^{md}_R),\beta_R)\|^2\big]\le\frac8S\Big[\frac{\|x_0-x^*\|^2}{2\lambda_1}+\frac{L_f}{\Gamma_N}(\|x^*\|^2+2M^2)+\sigma^2\sum_{k=1}^N\frac{\beta_k(4+(1-L_\Psi\beta_k)^2)}{4\Gamma_k(1-L_\Psi\beta_k)m_k}\Big],\tag{3.30}$$

and, if $L_f=0$,

$$\mathbb E\big[\Phi(x^{ag}_R)-\Phi(x^*)\big]\le\frac1S\sum_{k=1}^N\beta_k(1-L_\Psi\beta_k)\Big(\frac{\|x_0-x^*\|^2}{2\lambda_1}+\sigma^2\sum_{j=1}^k\frac{\beta_j(4+(1-L_\Psi\beta_j)^2)}{4\Gamma_j(1-L_\Psi\beta_j)m_j}\Big).\tag{3.31}$$

The expectations are over $R$ and all samples. The goal keeps general step sizes and batch sizes; Corollaries 4 and 5 (explicit policies) are left for follow-up work.

Milestones

In the order of the proof: Lemma 4 ($\mathcal G(x,\cdot,c)$ is 1-Lipschitz); the mini-batch variance bound (3.28) and its consequence (3.29) for the gradient mapping; Lemma 1, (2.16) and Lemma 5, the two-sided bound $-\frac{L_f}2\|y-x\|^2\le\Psi(y)-\Psi(x)-\langle\nabla\Psi(x),y-x\rangle\le\frac{L_\Psi}2\|y-x\|^2$; the three-point inequalities (3.32)–(3.33) and their combination (3.34); the descent bound (2.46) (already proved on the platform) and (2.47); the one-step and summed inequalities of p. 22; the iterate bound (2.52); the summed inequality at $x=x^*$; and the expected bound (3.35).

Significance

The result. Theorem 4 covers stochastic composite problems whether or not $\Psi$ is convex, with one step-size policy. Under Corollary 4's policy and batch sizes it gives a sample complexity for $\mathbb E\|\mathcal G\|^2\le\epsilon$ that improves the dependence on $L_h$ over mini-batch proximal stochastic gradient [Ghadimi, Lan & Zhang 2016], and when $L_f=0$ it recovers the optimal rate for convex stochastic composite optimization. Its proof is a template for later variance-controlled accelerated methods: a weighted Lyapunov argument in which nonconvexity enters only through $L_f$ and noise only through the martingale and variance terms.

Formalizing it. The result has been proved and refereed since 2016. As far as is known, no proof assistant has a formalization of it, and the platform has no accelerated stochastic method with a nonconvex guarantee. A complete development gives machine-checked versions of the mini-batch variance bound for martingale-difference noise, the Lipschitz property of the gradient mapping, the proximal three-point inequality on a convex domain, and the composite accelerated analysis with noise. Each of these can be reused in other stochastic proximal methods.

Difficulty

Copying the deterministic composite proof (Theorem 2) fails in two places. First, the deterministic step bounds $\min_k\|\mathcal G_k\|$ through the decrease $\|x^{ag}_k-x^{md}_k\|^2$, but here $x^{ag}_k$ is computed from $\bar G_k$, so this decrease measures the stochastic gradient mapping. Passing back to the exact one costs an extra variance term, which is why the constant is 8 rather than 2. Second, the noise $\bar\delta_k$ appears in two ways. The linear term $\langle\bar\delta_k,x^*-x_{k-1}\rangle$ vanishes only in expectation, and only because $x_{k-1}$ is fixed before the batch is drawn. The quadratic terms need the variance of an average of dependent samples, which is $\sigma^2/m_k$ only when the samples within a batch are conditionally unbiased given the earlier ones. A pathwise argument cannot remove either term, and an unconditional reading of Assumption 1 does not give the second.

Formalization scope

• Space and smoothness. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E). Smoothness of $f$ and $h$ is the platform's ConvexOptAlg.SmoothGD.IsBetaSmooth. $\Psi$, $\nabla\Psi$ and $L_\Psi$ are given with the identities $\Psi=f+h$, $\nabla\Psi=\nabla f+\nabla h$, $L_\Psi=L_f+L_h$.
• The convex term is its domain K with finite values X and ConvexOn ℝ K X; the prox map is a function P with the minimizer hypothesis IsProxMap K X P. A real-valued $\mathcal X$ on all of $\mathbb R^n$ is excluded: it makes Assumption 2 unsatisfiable and the goal vacuous. So is a free P with no minimizer property.
• The noise. Oracle calls are numbered consecutively; iteration $k$ makes calls $S_{k-1}+1,\dots,S_{k-1}+m_k$ with $S_k=m_1+\dots+m_k$, all at $x^{md}_k$. Assumption 1 is the published GhadimiLan.RSG.AssumptionA1 along these query points: conditional unbiasedness given a filtration of the earlier calls, and conditional variance bound $\sigma^2$. This conditional form is what the paper's proof uses, and the i.i.d. setting satisfies it. The oracle is jointly measurable. The variance bound (3.28) is a milestone and is never assumed.
• The output index $R$ is measurable, takes values in $\{1,\dots,N\}$ with mass function (3.7), and is independent of the whole sample sequence. Algorithm 4 runs pathwise, for every $k$, and is evaluated at $R$, which is the paper's "run $N$ steps, output the $R$-th iterate". Integrability of every expected quantity is part of each conclusion.
• Excluded trivializations: batch size fixed to 1 (general $m_k$ is kept), $\sigma=0$, a fixed $R$, and (3.28) taken as a hypothesis.
• Conventions. Indexing is 1-based, and $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$, so $\Gamma_1=1$. (2.9) and (2.10) are imposed for $k=1,\dots,N$, and $\beta_k<1/L_\Psi$ is written $L_\Psi\beta_k<1$. Two hypotheses are added: an optimal $x^*$ exists (the statement uses it), and $\|x_0\|\le M$ (used silently in (2.52) at $k=1$). The page prints $\Phi(x)$ on the left of (3.35) where $\Phi(x^*)$ is meant; the Lean states $\Phi(x^*)$.

Contributions welcome: proofs of any milestone. Lemma 4, (3.28) and the three-point inequality are self-contained and reusable. Also welcome: the measurability of the iterates, and Corollaries 4–5 as follow-up statements.

Selected references

• S. Ghadimi, G. Lan, Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming, arXiv:1310.3787v1, 2013; Math. Program. 156 (2016) 59–99. https://arxiv.org/abs/1310.3787v1 · https://doi.org/10.1007/s10107-015-0871-8
• S. Ghadimi, G. Lan, H. Zhang, Mini-batch stochastic approximation methods for nonconvex stochastic composite optimization, Math. Program. 155 (2016) 267–305 (reference [13] of the paper: the mini-batch variance bound and Proposition 1, the Lipschitz property of $\mathcal G$). https://doi.org/10.1007/s10107-014-0846-1
• S. Ghadimi, G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23 (2013) 2341–2368 (the randomized stochastic gradient method). https://doi.org/10.1137/120880811
• S. Ghadimi, G. Lan, Optimal stochastic approximation algorithms for strongly convex stochastic composite optimization, I: a generic algorithmic framework, SIAM J. Optim. 22 (2012) 1469–1492 (reference [11] of the paper; its Lemma 2 is the three-point inequality). https://doi.org/10.1137/110848864
• G. Lan, An optimal method for stochastic composite optimization, Math. Program. 133 (2012) 365–397. https://doi.org/10.1007/s10107-010-0434-y