All missions

Motivation

The method of multipliers (augmented Lagrangian method) solves a constrained convex program by alternating an unconstrained minimization in the primal variables with an explicit update of the Lagrange multipliers. Rockafellar showed in 1976 that the classical quadratic version is the proximal point algorithm applied to the dual problem, and that a variant which also adds a proximal term in the primal variables, the proximal method of multipliers, is the proximal point algorithm applied to the saddle operator of the Lagrangian (Rockafellar 1976, Math. Oper. Res.). The primal proximal term makes each subproblem strictly convex, so its minimizer is unique, and the theory gives convergence of the primal and dual iterates together.

Penalty functions other than the quadratic one, such as the exponential multiplier method, were used in practice and studied by Bertsekas, Kort and Tseng, but their convergence theory was separate from the proximal point framework. Eckstein's 1993 paper (Math. Oper. Res. 18(1), 202–226) replaces the squared distance in the proximal point algorithm by the D-function of a Bregman function. Its §5 obtains the first nonquadratic generalization of the proximal method of multipliers and proves that it converges to a saddle point. This mission formalizes that theorem, Theorem 8.

• 1967: Bregman introduces D-functions for convex feasibility (Bregman 1967).
• 1976: Rockafellar proves convergence of the quadratic method of multipliers and the proximal method of multipliers via the proximal point algorithm.
• 1990–1992: Censor and Zenios propose the proximal minimization algorithm with D-functions.
• 1993: Eckstein proves convergence of the Bregman proximal point algorithm for maximal monotone operators (Theorem 1) and derives nonquadratic multiplier methods (Theorems 6–8).

Setting

A convex program of the form (10) is

$$\min f(x)\quad\text{subject to}\quad g_i(x)\le0\ (i=1,\dots,m),\ x\in C,$$

where $C\subseteq\mathbb R^n$ is closed, nonempty and convex, and $f,g_1,\dots,g_m:\mathbb R^n\to(-\infty,+\infty]$ are proper lower semicontinuous convex functions, finite on $C$. Write $g(x)=(g_1(x),\dots,g_m(x))$ and $\overline{\Omega^+}=\{p\in\mathbb R^m:p\ge0\}$. The Lagrangian is $l(x,p)=f(x)+\sum_ip_ig_i(x)$ for $x\in C$, $p\ge0$; $l(x,p)=-\infty$ for $x\in C$, $p\not\ge0$; $l(x,p)=+\infty$ for $x\notin C$. A saddle pair $(x^*,p^*)$ satisfies $l(x^*,p)\le l(x^*,p^*)\le l(x,p^*)$ for all $x,p$; the paper calls these optimal solution–Lagrange multiplier pairs. The saddle operator on $\mathbb R^{n+m}$ is $K(x,p)=\partial_xl(x,p)\times(-\hat\partial_pl(x,p))$, where $\partial_x$ is the subdifferential of the convex function $l(\cdot,p)$ and $\hat\partial_p$ the set of supergradients of the concave function $l(x,\cdot)$.

For a differentiable $h$, the D-function is $D_h(x,y)=h(x)-h(y)-\langle\nabla h(y),x-y\rangle$. A Bregman function with open zone $S$ is a function $h:\overline S\to\mathbb R$, continuously differentiable on $S$, strictly convex and continuous on $\overline S$, whose partial level sets of $D_h$ are bounded, and which satisfies two sequential conditions relating $D_h\to0$ to convergence (Definition 1). For $h:\mathbb R^m\to\mathbb R$, the monotone conjugate is $h^{*+}(z)=\sup_{p\ge0}\{\langle p,z\rangle-h(p)\}$.

Given Bregman functions $h_x$ on $\mathbb R^n$ and $h_p$ on $\mathbb R^m$ and step sizes $c_k>0$, the nonquadratic proximal method of multipliers (12) is

$$x^{k+1}=\arg\min_{x\in C}\Big\{f(x)+\tfrac1{c_k}h_p^{*+}\big(\nabla h_p(p^k)+c_kg(x)\big)+\tfrac1{c_k}D_{h_x}(x,x^k)\Big\},\qquad p^{k+1}=\nabla h_p^{*+}\big(\nabla h_p(p^k)+c_kg(x^{k+1})\big).$$

Formalization targets

Goal: Theorem 8

Assume $c_k$ positive and bounded away from zero, $h_x$ a Bregman function with zone $S_x\supseteq C$, $h_p$ a Bregman function with zone $S_p\supseteq\overline{\Omega^+}$ and $\operatorname{im}\nabla h_p=\mathbb R^m$, and $\{(x^k,p^k)\}$ conforming to (12). Then

$$\exists\text{ saddle pair}\ \Longrightarrow\ (x^k,p^k)\to(x^*,p^*)\ \text{for some saddle pair }(x^*,p^*),$$ $$\nexists\text{ saddle pair}\ \Longrightarrow\ \{x^k\}\text{ or }\{p^k\}\text{ is unbounded}.$$

Existence clause

For the same step-size assumption, if in addition $\operatorname{im}\nabla h_x=\mathbb R^n$, a sequence conforming to (12) exists from every $(x^0,p^0)\in C\times\overline{\Omega^+}$. This is the third sentence of Theorem 8, stated as a separate item.

Milestones

Lemma 2 (four descriptions of $h^{*+}$, monotonicity), Lemma 3 ($h^{*+}$ finite and differentiable), Lemma A4 (a subdifferential chain rule), (14) (the $x$-step is a Bregman proximal step on $\partial_xl$), the formula $\hat\partial_pl(x,p)=\{g(x)\}-\partial\delta^+(p)$, maximal monotonicity of $K$, saddle pairs $=$ zeros of $K$, $h_x\oplus h_p$ is a Bregman function with zone $S_x\times S_p\supseteq\overline{\operatorname{dom}K}$, the identity (13), Theorem 1 restated on $\mathbb R^{n+m}$, Theorem 4 restated, and the existence clause.

Significance

Theorem 8 gives a family of primal–dual methods for convex programs, parametrized by two Bregman functions, each with the convergence guarantee of the quadratic proximal method of multipliers: convergence of both sequences to a saddle point when one exists, and divergence otherwise. Choosing $h_p$ to match the orthant (for instance entropy-like functions) yields exponential-type multiplier updates, and choosing $h_x$ to match $C$ adapts the primal regularization to the feasible set. The uniqueness of the primal minimizer, which the dual method of §4.2 lacks, is what allows convergence of the primal iterates without further assumptions.

The result is proved in the paper, with some steps asserted rather than proved (that $h_x\oplus h_p$ is a Bregman function; the maximality of $K$, cited from Rockafellar). No machine-checked proof of Theorem 8, of Theorem 1, or of the monotone-conjugate lemmas is known. A formalization would check the reduction of (12) to (13) carefully, including the extended-value conventions of the Lagrangian, and would provide reusable statements about Bregman functions on product spaces and about saddle operators of convex programs.

Difficulty

The reduction of Theorem 8 to Theorem 1 is short on the page but uses several nontrivial facts. The $x$-step is a constrained minimization of a composite function; turning its optimality condition into the inclusion (14) in $\partial_xl(x^{k+1},p^{k+1})$ needs a chain rule for a nondecreasing differentiable outer function composed with extended-valued convex functions (Lemma A4), together with properties of the monotone conjugate (Lemmas 2 and 3) that rest on recession arguments in the Appendix. The $p$-step requires identifying $\partial[h_p^{*+}]^*$ with $\nabla h_p+\partial\delta^+$, which uses $S_p\supseteq\overline{\Omega^+}$. Maximal monotonicity of $K$ is a theorem about closed saddle functions, not a consequence of monotonicity alone. Theorem 1 itself is the main theorem of the paper and depends on all six conditions of Definition 1.

A natural first idea, applying Theorem 1 to $K$ directly with an arbitrary Bregman function on $\mathbb R^{n+m}$, does not describe (12): the method is the specific instance $h=h_x\oplus h_p$, and the identification of its steps with $(\nabla h+c_kK)^{-1}$ is the content of (13).

Formalization scope

• $\mathbb R^k$ is EuclideanSpace ℝ (Fin k); $\mathbb R^{n+m}$ is WithLp 2 (E n × E m), which carries the Euclidean inner product. The §2 objects (Bregman function, $D_h$, runs of (3) written through the equivalent inclusion (4)) are defined over any finite-dimensional real inner product space so that Theorem 1 applies on $\mathbb R^{n+m}$.
• Extended-real functions are EReal-valued; properness, convexity (of the epigraph) and subgradients use published definitions. $h_p^{*+}$ is EReal-valued; the recursion (12) uses its real value and the gradient of that real function, which is exact because Lemma 3, a milestone, proves finiteness and differentiability.
• "Optimal solution–Lagrange multiplier pair" is the saddle inequality, as identified on p. 220. "Converges to one" means both sequences converge, to the two components of one saddle pair; "unbounded" means the range is not bounded.
• The $x$-step is a minimality predicate over $C$ rather than $\arg\min$ (equivalent; the minimizer is unique). A run requires $x^0\in S_x$, not $x^0\in C$, and $p^k\in S_p$, so that every gradient in (12) is defined.
• Corrected typos: the page's "$S_p\supset\overline{\Omega^+}$" is read as $\supseteq$; in Lemma A4, "Lemma 5" is Lemma 2 and "$f(x)\in\mathbb R^n$" is $\mathbb R^m$; Theorem 1's "monontone" is monotone; the supergradient formula's "$\delta^+(p)$" denotes $\partial\delta^+(p)$; the existence clause's extra parenthesis is dropped. In Lemma A4 a term $y_i\partial f_i(x^0)$ with $y_i=0$ is $\{0\}$, following the proof.
• The §4.2 assumption that the dual functional is not everywhere $-\infty$ is not assumed; §5 does not use it.
• A trivializing formalization is ruled out: the goal's hypotheses are satisfiable (with $h_x=h_p=\frac12\|\cdot\|^2$, $C=\mathbb R$, $f(x)=x^2$, $g_1(x)=x-1$ there is a saddle pair, checked in Lean), $h^{*+}$ is not replaced by a real supremum with junk values, and the saddle predicate quantifies over all of $\mathbb R^n\times\mathbb R^m$.
• Infrastructure a full development needs: Bregman functions on products, the monotone conjugate and its smoothness, a subdifferential sum and chain rule for extended-valued functions, maximal monotonicity of saddle operators, and Theorem 1. The monotone conjugate lemmas and Theorem 1 are shared with the companion missions of this series. Contributions to any milestone are welcome, including proofs of the restated Theorems 1 and 4 independent of the companion missions.

Selected references

• J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 1993, 202–226. https://doi.org/10.1287/moor.18.1.202
• R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1(2), 1976, 97–116. https://doi.org/10.1287/moor.1.2.97
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3), 1967, 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• Y. Censor and S. A. Zenios, Proximal minimization algorithm with D-functions, Journal of Optimization Theory and Applications 73(3), 1992, 451–464. https://doi.org/10.1007/BF00940051

Motivation

Monotone comparative statics asks when the optimal choice of a decision maker moves in a predictable direction as a parameter of the problem changes: when a firm facing a higher price produces more, when a monopolist facing lower costs sets a lower price, when a player in a game best-responds with a higher strategy to higher strategies of the others. The classical sufficient conditions, due to Topkis (Topkis 1978), are supermodularity of the objective in the choice variable and increasing differences in the choice and the parameter. Both are cardinal conditions: they can be destroyed by a strictly increasing change of the units in which the objective is measured, although such a change does not alter any optimal choice.

Milgrom and Shannon (Econometrica 1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed that the ordinal conditions are necessary and sufficient for the set of maximizers to be monotone in the parameter and the constraint set (their Theorem 4). This mission concerns the relation between the ordinal notion and the cardinal one: in which sense is a quasisupermodular function "a supermodular function up to a change of units"? Section 3 of the paper answers it with Theorem 8. An earlier notion in the same direction, supermodularizable functions, was studied by Li Calzi (1991).

Setting

Let $X$ be a lattice: a partially ordered set in which every two elements $x, y$ have a least upper bound $x \vee y$ (join) and a greatest lower bound $x \wedge y$ (meet). Examples are $\mathbb{R}^n$ and products of finite chains, ordered componentwise.

A function $f : X \to \mathbb{R}$ is supermodular on a set $S \subseteq X$ if

$$f(x) + f(y) \le f(x \vee y) + f(x \wedge y) \qquad \text{for all } x, y \in S.$$

It is quasisupermodular (p. 162) if for all $x, y \in X$

1. $f(x) \ge f(x \wedge y)$ implies $f(x \vee y) \ge f(y)$, and
2. $f(x) > f(x \wedge y)$ implies $f(x \vee y) > f(y)$.

A function $h : \mathbb{R} \to \mathbb{R}$ is strictly increasing if $r < s$ implies $h(r) < h(s)$. A function $f$ is supermodularizable if $h \circ f$ is supermodular on $X$ for some strictly increasing $h$.

For $x_1, x_2 \in X$ the set $\{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}$ is closed under $\vee$ and $\wedge$; it is the sublattice generated by $x_1$ and $x_2$ and has at most four points.

Quasisupermodularity depends only on the order of the values of $f$, so it is preserved by strictly increasing transformations; supermodularity is not. Every supermodular function is quasisupermodular, and so is every supermodularizable function.

Formalization targets

Goal: Theorem 8 (p. 165)

$f : X \to \mathbb{R}$ is quasisupermodular if and only if there is $g : \mathbb{R} \times X \times X \to \mathbb{R}$ such that (i) $r \mapsto g(r, x_1, x_2)$ is strictly increasing for every $(x_1, x_2) \in X^2$, and (ii) for every $x_1, x_2 \in X$,

$$x \mapsto g(f(x), x_1, x_2) \ \text{ is supermodular on } \{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}.$$

Milestones

1. Invariance (p. 164): if $f$ is quasisupermodular and $g$ strictly increasing, $g \circ f$ is quasisupermodular.
2. Supermodularizable implies quasisupermodular (pp. 164–165): if $h$ is strictly increasing and $h \circ f$ is supermodular on $X$, then $f$ is quasisupermodular.
3. Lemma (p. 165): if $f$ is quasisupermodular on $L = \{x, x', x \vee x', x \wedge x'\}$, then $h \circ f$ is supermodular on $L$ for some strictly increasing $h : \mathbb{R} \to \mathbb{R}$.
4. Example 1 (p. 165): the function on $\{0,1\} \times \{0,1,2,3\}$ with rows $(1,2,2,1)$ and $(3,4,5,3)$ is quasisupermodular but not supermodularizable.

The Lemma is the "only if" direction of Theorem 8 on a single sublattice; Example 1 shows why the transformation in Theorem 8 must be allowed to depend on $(x_1, x_2)$.

Significance

Theorem 8 characterizes an ordinal property by a family of cardinal ones: quasisupermodularity is exactly local supermodularizability, on every two-generated sublattice. It explains why quasisupermodularity, and not supermodularity, is the natural hypothesis of ordinal comparative statics, and Example 1 marks the boundary: a single global transformation is not enough, so supermodularizable functions form a strictly smaller class. The paper states an analogous characterization of the single crossing property (Theorem 9, p. 166) without proof.

On the formalization side, none of these results is machine-checked anywhere known to this mission. The platform already holds Topkis's lattice-theoretic definitions and theorems (supermodularity, increasing differences, monotonicity of the argmax under the cardinal conditions); this mission adds the ordinal notion and its characterization on top of the published definition of supermodularity. A formal proof of the Lemma also requires constructing a strictly increasing map of all of $\mathbb{R}$ that moves one prescribed value, which is reusable for other "ordinal versus cardinal" results.

Difficulty

The "if" direction and the invariance and supermodularizability remarks are short unfoldings of the definitions. The work is in the Lemma. On a four-point lattice the values $a, b, c, d$ of $f$ at $x, x \vee x', x \wedge x', x'$ need not satisfy $a + d \le b + c$, and the obvious attempt, applying one transformation fixed in advance (such as an exponential), fails: the needed transformation depends on the four values. A strictly increasing $h$ of the whole real line must be chosen to separate the values while preserving their order, and the degenerate configurations in which some of the four values coincide, or in which $x$ and $x'$ are comparable so that the lattice has fewer than four points, have to be handled separately. A second subtlety is that quasisupermodularity is used for both orders of the pair $(x, x')$.

Formalization scope

• Lattices are Mathlib's Lattice class; joins and meets are ⊔ and ⊓. Functions are real valued.
• Quasisupermodularity is a draft definition QuasiSupermodularOn g S, relativized to a set $S$; the paper's notion on $X$ is QuasiSupermodularOn f Set.univ. It quantifies over all ordered pairs of $S$.
• Supermodularity is the published definition Supermodularity.Monotonicity.SupermodularOn (Topkis series), also relativized to a set; supermodularity "on the sublattice" is SupermodularOn _ {x₁, x₂, x₁ ⊔ x₂, x₁ ⊓ x₂}.
• "Strictly increasing" is StrictMono. With merely monotone transformations the statements trivialize: a constant transformation is supermodular on every set, which would make the "if" direction of Theorem 8 false and the second half of Example 1 false. The formal statements rule this out.
• The transformation $g : \mathbb{R} \times X \times X \to \mathbb{R}$ of Theorem 8 is curried, g : ℝ → X → X → ℝ; it may depend on $(x_1, x_2)$ but not on $x$. Transformations are defined on all of $\mathbb{R}$, as printed, not only on the values of $f$.
• The Lemma's four-point lattice is formalized as the subset $\{x, x', x \vee x', x \wedge x'\}$ of an ambient lattice, with both notions relativized to it; the subset is closed under join and meet, so this is the page's statement, including the degenerate cases.
• Example 1's domain is Fin 2 × Fin 4 with the product order.

Contributions welcome: proofs of the milestones and the goal; a general lemma producing strictly increasing maps $\mathbb{R} \to \mathbb{R}$ with prescribed values on finitely many points.

Selected references

• P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
• D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 305–321, 1978. https://doi.org/10.1287/opre.26.2.305
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• M. Li Calzi, Generalized Symmetric Supermodular Functions, Working Paper, Stanford University, 1990 (listed so in the paper's references; the text on p. 165 cites it as Li Calzi (1991)).

Motivation

The speed at which a finite reversible Markov chain approaches its stationary distribution is controlled by its eigenvalues. For a chain with eigenvalues $1=\beta_0>\beta_1\ge\dots\ge\beta_{m-1}\ge-1$, the distance to stationarity after $n$ steps is governed by $\beta_*^{\,n}$, where $\beta_*=\max(\beta_1,|\beta_{m-1}|)$ (Diaconis and Stroock 1991, Proposition 3). Upper bounds on the second eigenvalue $\beta_1$ are the familiar half of this picture, and they are what Cheeger-type and Poincaré inequalities provide. The other half is the smallest eigenvalue $\beta_{\min}=\beta_{m-1}$: a chain whose smallest eigenvalue is close to $-1$ oscillates almost periodically and mixes slowly whatever $\beta_1$ is. A chain is aperiodic exactly when $\beta_{\min}>-1$, but that qualitative fact gives no rate.

Diaconis and Stroock's paper gives geometric bounds for both ends of the spectrum, expressed through systems of paths in the graph of the chain. Their bound on $\beta_{\min}$ uses closed paths with an odd number of edges, the combinatorial witnesses of aperiodicity. The paper has been a standard reference for path (canonical-path, multicommodity-flow) methods in the analysis of Markov chain Monte Carlo since its publication.

Timeline:

• 1988–1989, Jerrum and Sinclair: conductance (Cheeger-type) bounds on $\beta_1$ for chains on combinatorial structures.
• 1991, Diaconis and Stroock: path bounds for $\beta_1$ (Proposition 1, the Poincaré inequality $\beta_1\le1-1/\kappa$) and for $\beta_{\min}$ (Proposition 2, this mission), with the specializations to random walks on graphs (Corollaries 1 and 2).

Setting

Let $X$ be a finite set and $P(x,y)$ the transition matrix of an irreducible Markov chain on $X$, reversible with respect to a probability distribution $\pi$:

$$Q(x,y)=\pi(x)P(x,y)=\pi(y)P(y,x)\qquad(x,y\in X).$$

The operator $(P\varphi)(x)=\sum_yP(x,y)\varphi(y)$ is self-adjoint on $L^2(\pi)$, with inner product $\langle\varphi,\psi\rangle_{L^2(\pi)}=\sum_x\varphi(x)\psi(x)\pi(x)$, so its eigenvalues are real. Write $E(\varphi^2)=\sum_x\varphi(x)^2\pi(x)$ and let $\beta_{\min}$ be the smallest eigenvalue of $P$.

The graph of the chain has vertex set $X$, an edge from $x$ to $y$ when $Q(x,y)>0$, and a self-loop at $x$ when $Q(x,x)>0$. An odd closed path $\sigma_x$ at $x$ is a sequence of edges from $x$ back to $x$, with an odd number of edges, in which no directed edge is traversed twice. Its length is

$$|\sigma_x|_Q=\sum_{e\in\sigma_x}Q(e)^{-1}.$$

A system of odd paths $\Sigma=(\sigma_x)_{x\in X}$ chooses one such path for every point, and its load is

$$\iota=\iota(\Sigma)=\max_e\sum_{\sigma_x\ni e}|\sigma_x|_Q\,\pi(x),$$

the maximum over directed edges $e$ of the weighted length of the paths through $e$ (display (1.7) of the paper).

For the random walk on a graph $G=(X,E)$, $P(x,y)=1/d(x)$ when $\{x,y\}\in E$, with $d(x)$ the degree, and $\pi(x)=d(x)/2|E|$. There $d_*$ is the maximum degree, $\sigma_*$ the largest number of edges of a path in $\Sigma$, and $b_*=\max_e\sharp\{\sigma\in\Sigma:e\in\sigma\}$.

Formalization targets

Goal: Proposition 2

For an irreducible, aperiodic, reversible chain and every system $\Sigma$ of odd closed paths,

$$\beta_{\min}\ge-1+\frac{2}{\iota(\Sigma)}.$$

Milestones (the steps of the paper's proof)

1. The identity (1.8): $\tfrac12\sum_{x,y}(\varphi(x)+\varphi(y))^2Q(x,y)=E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}$.
2. Along an odd closed path $x,y,w,\dots,z,x$: $\varphi(x)=\tfrac12\{(\varphi(x)+\varphi(y))-(\varphi(y)+\varphi(w))+\dots+(\varphi(z)+\varphi(x))\}$.
3. For every $\varphi$: $E(\varphi^2)\le\frac{\iota}{2}\big(E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}\big)$.
4. Every eigenvalue $\beta$ of $P$ satisfies $\beta\ge-1+2/\iota$.

Companions

• Corollary 2. For the random walk on a connected, non-bipartite graph and any system $\Sigma$ of odd paths, $\beta_{\min}\ge-1+\dfrac{2}{d_*\sigma_*b_*}$.
• Remark 1.3. With odd paths $\sigma_{xy}$ for every ordered pair and $\tilde\iota=\max_e\sum_{\sigma_{xy}\ni e}|\sigma_{xy}|_Q\pi(x)\pi(y)$: $\beta_{\min}\ge-1+1/\tilde\iota$.

Significance

Proposition 2 turns aperiodicity into a number. With Proposition 1, which bounds $\beta_1\le1-1/\kappa$ through paths between pairs of points, it bounds the absolute spectral gap $1-\beta_*$ entirely in terms of path geometry, and so bounds the variation distance to stationarity through Proposition 3. Corollary 2 is the form most often applied: for a random walk on a non-bipartite graph, a choice of short odd cycles that do not crowd any single edge certifies that the walk does not oscillate.

Proposition 2 and its corollary are proved in the paper. As far as a search of the platform shows, no machine-checked proof exists. The platform already has the vocabulary (stochastic matrices, stationarity, reversibility, eigenvalues and the $L^2(\pi)$ inner product, from the published Levin–Peres–Wilmer layer) and the qualitative fact that $-1$ is not an eigenvalue of an irreducible aperiodic chain. This mission adds the quantitative bound, the identity (1.8), and the path inequality, all reusable for other path-based eigenvalue estimates.

Difficulty

Each step is elementary, but the bookkeeping is where a proof can go wrong. The Cauchy–Schwarz step is applied along each path separately, and the resulting double sum over points and over the edges of their paths must be exchanged into a sum over edges. That exchange is exact only if each path traverses each directed edge at most once. A path that crosses an edge twice contributes twice, while $\iota$ counts it once. Self-loops are edges here, and the sum over directed edges in the last step must match the sum over ordered pairs $(x,y)$, including $x=y$, in the identity (1.8). The alternating signs work only because the number of edges is odd; an even closed path cancels $\varphi(x)$ instead of doubling it.

The bound is also only as good as the chosen paths: short odd cycles that spread their load over many edges give a small $\iota$, and the choice of $\Sigma$ is part of every application.

Formalization scope

The chain is a real matrix P : Matrix V V ℝ on a Fintype V, with the published predicates IsStochastic, Irreducible, Aperiodic, IsStationary (which includes that $\pi$ is a probability vector) and DetailedBalance. $Q$ is edgeMeasure, the inner product innerPi, eigenvalues IsEigenvalue (a real eigenvalue with a nonzero real eigenfunction). $\beta_{\min}$ is the infimum of the real eigenvalues of $P$, a minimum for a stochastic matrix on a nonempty set.

Paths are vertex lists. A path traverses the directed edges between consecutive vertices, each with $Q>0$. The paper defines $|\sigma_x|_Q$ "by analogy with (1.4)", whose paths may not repeat an edge. For the directed edges of §1C this rule is read as "no directed edge twice". Under the unordered reading a vertex of degree one would have no odd closed path, contradicting the page's remark that such paths always exist for irreducible aperiodic chains. $\iota$ is a real supremum over the finite set of directed edges with $Q>0$, and it is $0$ only when there is no edge. A system of odd paths on a nonempty set excludes that case, so the bound is never reduced to $\beta_{\min}\ge-1$ by $2/0=0$. The system $\Sigma$ is a universally quantified hypothesis of every statement, never an existential one. No milestone assumes the inequality of milestone 3 or the identity (1.8) as a hypothesis. No assumption $|X|\ge2$ is made.

Milestones 3 and 4 do not assume aperiodicity: the existence of an odd path system implies it. The identity (1.8) assumes only stochasticity and stationarity. Corollary 2 assumes only that the graph is connected and not 2-colorable; the chain properties follow from these. In Corollary 2, $b_*$ counts paths through a directed edge, which is at most the count through the unordered edge, so the stated bound implies the one with the unordered count. Only the first half of Remark 1.3 is stated; its second half needs Proposition 1's quantity, which belongs to another mission of the series.

Contributions welcome: proofs of the milestones in order, a general Cauchy–Schwarz-along-paths lemma shared with the Poincaré inequality, and the existence of odd path systems for irreducible aperiodic chains.

Selected references

• P. Diaconis and D. Stroock, Geometric bounds for eigenvalues of Markov chains, Ann. Appl. Probab. 1(1):36–61, 1991. https://doi.org/10.1214/aoap/1177005980
• A. Sinclair and M. Jerrum, Approximate counting, uniform generation and rapidly mixing Markov chains, Inform. and Comput. 82(1):93–133, 1989. https://doi.org/10.1016/0890-5401(89)90067-9
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (2nd ed. 2017). https://doi.org/10.1090/mbk/107

Motivation

An oracle lets an algorithm ask for the value of a function without giving it a description of that function. An oracle lower bound isolates how many questions are needed, even when computation between questions is unrestricted. Bennett, Bernstein, Brassard and Vazirani used this viewpoint to compare classical and quantum access to randomly chosen functions and permutations. Their Theorem 3.6 states an almost-sure separation: relative to a random permutation oracle, a quantum machine using time $o(2^{n/3})$ cannot capture all of $(\mathrm{NP}\cap\mathrm{coNP})^A$ BBBV, Theorem 3.6. The same paper notes that its exponent $1/3$ may reflect the available argument rather than the true boundary BBBV, p. 12.

The finite statement behind that separation is a quantum query lower bound for a uniformly random permutation. It asks about one bit of the inverse image of a fixed string, rather than inversion of the whole permutation. This gives a sharply defined target with the paper's explicit query and error constants.

Setting

Let $\Sigma^n=\{0,1\}^n$, and let $A$ be a permutation oracle of $\Sigma^n$. Its inverse image of the all-one string $1^n$ exists and is unique. Define the language $\mathcal L_A$ by putting $y$ in $\mathcal L_A$ when the first bit of $A^{-1}(y)$ is $1$. The paper observes that access to $A$ puts this language in both $\mathrm{NP}^A$ and $\mathrm{coNP}^A$: either possible bit of the inverse image can be witnessed by an input to the permutation BBBV, p. 10. This mission tests membership only at $y=1^n$.

A $T$-query quantum algorithm starts in a unit vector of a finite complex Hilbert space. A basis configuration records an optional length-$n$ query string, an answer register, and finite workspace. On a querying configuration $(x,z,w)$, an oracle operation replaces the answer register by $z\oplus A(x)$; it leaves a nonquerying configuration unchanged. Each oracle operation is followed by an algorithm-chosen unitary. The final acceptance probability is the sum of the squared amplitudes of accepting basis configurations. A run decides a yes-or-no question if its acceptance probability is at least $2/3$ on a yes instance and at most $1/3$ on a no instance. These thresholds match the paper's bounded-error convention BBBV, §2 and §3.1.

For a state $\phi$, the query magnitude $q_y(\phi)$ is the total squared amplitude of basis configurations querying string $y$. Thus $0\le q_y(\phi)\le1$ for a unit state, and the magnitudes over all strings sum to at most $1$. This is Definition 3.2 of the paper BBBV, p. 7.

Formalization targets

The goal is the finite claim in the proof of Theorem 3.6. For every $n\ge1$, every finite-workspace algorithm $M$ with $T$ queries, and a uniform permutation $A$ of $\Sigma^n$,

$$T\le\frac{2^{n/3}}{100} \quad\Longrightarrow\quad \Pr_A\!\left[M\text{ fails to decide whether the first bit of }A^{-1}(1^n)\text{ is }1\right]\ge\frac18.$$

The milestones follow the statements used in the paper: Theorem 3.1 relates Euclidean distance between final states to their observed distributions; Theorem 3.3 bounds the effect of changing answers at queried strings; and the proof of Theorem 3.6 establishes the uniform transposition chain, the $1/2$ membership split, the expected query-magnitude estimate, and the $1/50$ expected final-state distance BBBV, pp. 7–11. The source text of each milestone is recorded with its page in the mission's milestone list.

Significance

The result identifies a concrete task that cannot be decided reliably with too few quantum oracle calls for a positive fraction of length-$n$ permutation oracles. The inverse image exists by definition, so the obstruction is the number of queries needed to learn its first bit. This is the quantitative part of the paper's relative separation for $\mathrm{NP}\cap\mathrm{coNP}$; the passage to an almost-sure statement over countably many machines is described in the paper but lies beyond this mission's formal goal BBBV, pp. 10–12.

The theorem is proved on paper and is not claimed here as an open mathematical problem. Formalizing it produces reusable finite-dimensional machinery for quantum queries: an XOR oracle as a unitary basis permutation, query magnitude, a time-dependent hybrid oracle, and counting-based probability over finite permutation spaces. The milestone statements remain open Lean proof obligations in this proposal.

Difficulty

A direct comparison of an algorithm's run under two nearby permutation oracles requires knowing that the algorithm seldom queries the locations where those oracles differ. The distinguished preimage $A^{-1}(1^n)$ cannot simply be declared rarely queried: learning about it is exactly the task under study. The paper therefore studies a chain of random transpositions and a run whose oracle changes by step. The subtle point is that a string used in a later transposition is still uniform when the earlier query state is formed BBBV, pp. 10–11. The expected query-magnitude milestone states that point explicitly.

Formalization scope

The Lean carrier of strings is $\mathrm{Fin}(n)\to\mathbb Z/2\mathbb Z$. Algorithms use finite configuration types and EuclideanSpace ℂ; the query register is optional, and none represents configurations that make no length-$n$ query. An oracle answers with the full length-$n$ value by XOR in the answer register. The paper describes a Boolean oracle, but one full-value query can be simulated with $n$ Boolean queries and one Boolean query with two full-value queries. The latter direction transfers this lower bound to the paper's oracle at a changed constant. Answers at lengths other than $n$ are fixed and absorbed into the inter-query unitaries, as in the paper's finite-length argument. The full oracle quantum Turing machine, complexity classes as Lean objects, and the almost-sure conclusion are outside the model.

Probabilities and expectations are finite counting fractions. The chain samples a uniform $\pi_0$ and independent uniform $x_1,\ldots,x_{T+1}$, with $x_0=\pi_0^{-1}(1^n)$; this has the same joint law as the paper's conditional sampling order. The recurrence $\pi_{i+1}=\pi_i\circ(x_i\ x_{i+1})$ uses the paper's composition direction. The first-bit test requires $n\ge1$, and any comparison to $\pi_{T-1}$ requires $T\ge1$. The goal quantifies over every finite workspace and algorithm before sampling the permutation. A uniform function in place of a permutation, or a predetermined inverse image, would change the task and is excluded.

The paper's Theorem 3.3 prints a final-state bound $\varepsilon$ that fails for a one-query XOR example; the milestone states the valid $2\varepsilon$ bound. Its baseline oracle may vary by step because the proof of Theorem 3.6 uses the hybrid run. The explicit constants $T\le 2^{n/3}/100$, failure probability $1/8$, and expected distance $1/50$ remain as printed. General finite-dimensional unitary and probability lemmas, together with a proof of the time-dependent hybrid bound, are welcome contributions. The finite query model and transposition-chain definitions are reusable in other oracle lower bounds.

Selected references

• C. H. Bennett, E. Bernstein, G. Brassard, and U. Vazirani, Strengths and weaknesses of quantum computing, SIAM Journal on Computing 26(5), 1997; arXiv:quant-ph/9701001v1.

Motivation

How fast a finite Markov chain forgets its starting point is the central quantitative question in the analysis of Monte Carlo algorithms, card shuffling and random walks on groups. The classical tool is the spectral gap $\lambda$, which controls convergence in $\ell^2(\pi)$ but loses a factor $1/\pi(x)$ when converted into a bound for a chain started at a point. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) brought the logarithmic Sobolev constant $\alpha$, introduced by Gross for Gaussian measures (Amer. J. Math. 97 (1975)), into the study of finite chains, and showed that it gives sharper mixing bounds in many examples.

The entropy route to ergodicity is the cleanest consequence of a log-Sobolev inequality: the relative entropy of the chain's law with respect to stationarity decays exponentially at rate $2\alpha$, and at rate $4\alpha$ for reversible chains. The paper notes that the reversible case is contained in Bakry's Saint-Flour lectures (Lecture Notes in Math. 1581, 1994) and Stroock's notes on Gibbs states (Lecture Notes in Math. 1563, 1993), and that Miclo (preprint, 1995) treated the nonreversible case.

Setting

Let $\mathcal X$ be a finite set and $K$ a Markov kernel: $K(x,y)\ge0$ and $\sum_y K(x,y)=1$. Let $\pi$ be an invariant probability, $\sum_x\pi(x)K(x,y)=\pi(y)$, with $\pi(x)>0$ for every $x$. Functions act on the right, $Kf(x)=\sum_yK(x,y)f(y)$, and $\langle f,g\rangle=\sum_xf(x)g(x)\pi(x)$ is the inner product of $\ell^2(\pi)$, with norms $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$. The chain is reversible if $\pi(x)K(x,y)=\pi(y)K(y,x)$ for all $x,y$.

The continuous-time heat semigroup is

$$H_t=e^{-t(I-K)}=e^{-t}\sum_{n\ge0}\frac{t^n}{n!}K^n,$$

acting on functions by $H_tf(x)=\sum_yH_t(x,y)f(y)$ and on probability measures by $\mu H_t(y)=\sum_xH_t(x,y)\mu(x)$. The row $H_t^x=H_t(x,\cdot)$ is the law at time $t$ of the chain started at $x$.

The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$; it is bilinear but not symmetric unless the chain is reversible. With

$$\mathcal L(f)=\sum_x|f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x),$$

the log-Sobolev constant is

$$\alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\ne0\Big\}.$$

The relative entropy of a probability $\mu$ is $\mathrm{Ent}_\pi(\mu)=\sum_x\mu(x)\log\frac{\mu(x)}{\pi(x)}$, and the total variation distance is $\|\mu-\pi\|_{TV}=\sup_{A\subset\mathcal X}|\mu(A)-\pi(A)|$.

Formalization targets

Goal: Theorem 3.6 (p. 722)

For every probability measure $\mu$ on $\mathcal X$,

$$\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-2\alpha t},\qquad t>0,$$

and, if $(K,\pi)$ is reversible,

$$\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-4\alpha t},\qquad t>0.$$

Milestones

1. §2.1, Remarks (ii), p. 702: if $\mu=f\pi$ then $\mu H_t$ has density $H_t^*f$, where $H_t^*$ is the semigroup of the adjoint kernel $K^*(x,y)=K(y,x)\pi(y)/\pi(x)$.
2. Lemma 2.5, second part, p. 707: $\partial_t\,\mathrm{Ent}_\pi(H_tf)|_{t=0}=-\mathcal E(f,\log f)$.
3. Lemma 2.7, p. 708: $\mathcal E(\log f,f)\ge2\,\mathcal E(\sqrt f,\sqrt f)$, and $\ge4\,\mathcal E(\sqrt f,\sqrt f)$ for reversible chains.
4. §3.3, p. 722: for $f\ge0$ with $\|f\|_2=1$ and $\mu=f^2\pi$, $\mathcal L(f)=\mathrm{Ent}_\pi(\mu)$.
5. (2.8), p. 710: $2\|\mu-\pi\|_{TV}^2\le\mathrm{Ent}_\pi(\mu)\le\|\mu-\pi\|_{TV}+\tfrac12\|\mu/\pi-1\|_{\pi,2}^2$.

Companion: (3.3) (p. 723)

For an irreducible chain, every $x$ and $t>0$,

$$2\|H_t^x-\pi\|_{TV}^2\le\Big(\log\frac1{\pi(x)}\Big)e^{-2\alpha t},$$

with $2\alpha$ replaced by $4\alpha$ for reversible chains.

Significance

Theorem 3.6 turns a single functional inequality into a convergence statement valid for every initial law, with no spectral assumption and no reversibility in the first half. Through Pinsker's inequality it gives (3.3), whose prefactor $\log(1/\pi(x))$ replaces the factor $1/\pi(x)$ of the spectral bound $4\|H_t^x-\pi\|_{TV}^2\le\pi(x)^{-1}e^{-2\lambda t}$. When $\pi(x)$ is exponentially small in the size of the problem, as for random walks on large groups or product spaces, $\log(1/\pi(x))$ is polynomial where $1/\pi(x)$ is exponential, and the time needed to make the bound small drops accordingly. This is the mechanism behind the sharp mixing bounds the paper derives from $\alpha$.

The results are proved in the paper and are classical; they are not, to our knowledge, formalized. The platform has measure-theoretic statements of Pinsker's inequality and the published finite Markov chain vocabulary of Levin–Peres–Wilmer (stochastic matrices, stationarity, total variation, the heat kernel), but nothing about log-Sobolev constants of finite chains, the entropy derivative along a Markov semigroup, or entropy decay. A formal development provides the entropy layer of the finite-chain theory: the adjoint semigroup, the dissipation identity, the comparison of $\mathcal E(\log f,f)$ with $\mathcal E(\sqrt f,\sqrt f)$, and Pinsker's inequality in the encoding used by the mixing-time library.

Difficulty

The statement is about measures, while the natural quantities to differentiate are densities with respect to $\pi$, and for a nonreversible chain the density of $\mu H_t$ evolves under the adjoint semigroup, not under $H_t$. The Dirichlet form is not symmetric, so the order of its arguments matters at every step, and the improvement from $2\alpha$ to $4\alpha$ holds only under reversibility.

The obvious first idea, differentiating $\mathrm{Ent}_\pi(\mu H_t)$ term by term, meets $\log 0$ wherever the density vanishes. The initial law may be a point mass, and for a reducible chain the density can stay zero at positive times. The argument must therefore handle the boundary $t=0$ and the degenerate laws separately from the smooth interior. The constant $\alpha$ is defined as an infimum over all functions, with no claim that it is attained or positive.

Formalization scope

The state space is a Fintype with decidable equality, $K$ is a real matrix with the published predicate MarkovMixing.IsStochastic, $\pi$ satisfies MarkovMixing.IsStationary K π and $\pi(x)>0$ for all $x$, and reversibility is MarkovMixing.DetailedBalance K π. $H_t$ is the published MarkovMixing.heatKernel K t (the Poisson series), the adjoint kernel is MarkovMixing.timeReversal K π, and total variation is MarkovMixing.tvDist. Time is real, and the decay statements are for $t>0$.

The local definitions are $\mathcal E(f,g)=\sum_x(f(x)-Kf(x))g(x)\pi(x)$, the norms $\|f\|_p$, $\mathcal L$, $\alpha$ as a real infimum over the ratios with $\mathcal L(f)\ne0$, $\mathrm{Ent}_\pi(\mu)$, and $\mu H_t$ as the row vector $\mu\,H_t$. Lean's Real.log 0 = 0 implements $0\log0=0$. The goal does not assume irreducibility: it is true for every stochastic $K$ with a positive invariant probability, and a reducible chain has $\alpha=0$. The companion (3.3) keeps irreducibility, the standing assumption of Section 3. In Lemmas 2.5 and 2.7 the paper's $f\ge0$ is strengthened to $f>0$, because $\log f$ is $-\infty$ at a zero of $f$ on the page and $0$ in Lean.

Several encodings would make the goal trivially true and are ruled out. $\alpha$ is not assumed positive. $\mu$ is a probability, since for $\mu=2\pi$ the entropy is a positive constant in $t$. $\pi$ is invariant and positive, so $\mu/\pi$ is meaningful. The eigenvalue-based MarkovMixing.spectralGap is not used. Applying $H_t$ to $\mu$ as a function, $H_t\mu$, is not the same as $\mu H_t$ for a nonreversible chain.

A complete development needs: termwise differentiation of the heat-kernel series and the semigroup property $\partial_tH_t=(K-I)H_t$; the adjoint identity for $H_t$; elementary convexity inequalities for $\log$ and $\sqrt{\cdot}$; the symmetric form of $\mathcal E$ for reversible chains; Pinsker's inequality on a finite set; and a scalar Grönwall lemma. The heat-kernel calculus and Pinsker's inequality in the MarkovMixing.tvDist encoding are reusable by the other missions of this series and by any mixing-time development. Proofs of individual milestones are welcome independently of the goal.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6 (1996), 695–750. https://doi.org/10.1214/aoap/1034968224
• L. Gross, Logarithmic Sobolev inequalities, Amer. J. Math. 97 (1975), 1061–1083. https://doi.org/10.2307/2373688
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, 2nd ed., American Mathematical Society, 2017. https://doi.org/10.1090/mbk/107

Prove a deterministic $O(n^{1.999074})$ algorithm for integer 3SUM in the campaign's shared word-RAM model, improving the verified $1.999112$ bound.

A promising parameter choice is $c=22$, $\theta=0.11229$, $D=\lfloor n^{0.054}\rfloor$, and $g=\lceil D^{0.0343}\rceil$. Lean-checked arithmetic certificates give $\gamma>0.0686$, $q\le0.431369<0.4314$, and $0.054<R_c$. The predicted Exact Triangle saving is $\delta=0.0018522$, giving a 3SUM cutoff of $1.9990739$ and a strict margin below the target.

The algorithmic claim remains open. The milestones are to establish the faster inner solver, then verify the integer computations for $D$ and $g$ and prove the total Exact Triangle cost, including preprocessing and scans. The existing verified reductions and foundation definitions can then be reused. The numerical certificates alone do not prove the mission.