Optimization

Motivation

Duality is the organizing principle of convex optimization: a minimization problem's optimal value equals a maximization problem's optimal value, and this coincidence, rather than being a lucky accident, follows from a separating-hyperplane argument that applies whenever the two problems' feasible regions are shaped compatibly enough. Werner Fenchel formalized this in the 1950s for pairs of convex and concave functions related by the Legendre-Fenchel transform, and the resulting Fenchel duality theorem specializes, for linear objectives over polyhedral feasible regions, to linear programming duality — the fact, central to the entire theory of combinatorial optimization, that a linear program's optimal value can always be certified from above and below by a pair of primal and dual feasible solutions. Murota's Discrete Convex Analysis (SIAM, 2003) collects this classical machinery, together with the integrality theory that lets it produce combinatorial (integer-valued) certificates rather than merely real ones, as the technical foundation the rest of the book builds its discrete theory on top of.

Setting

For $f : \mathbb R^n \to \mathbb R \cup \{+\infty\}$, the epigraph is $\operatorname{epi} f = \{(x,Y) : Y \ge f(x)\}$, and $f$ is convex iff $\operatorname{epi} f$ is a convex set; $f$ is proper if additionally its effective domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ is nonempty, and closed if $\operatorname{epi} f$ is topologically closed. A function $h : \mathbb R^n \to \mathbb R \cup \{-\infty\}$ is concave, proper, closed analogously via its hypograph. The convex conjugate is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$, and the concave conjugate $h^\circ(p) = \inf_x\{\langle p,x\rangle - h(x)\}$. The relative interior $\operatorname{ri} S$ of a set $S$ is the interior of $S$ relative to its affine hull. A function is polyhedral if its epigraph (or hypograph) is a finite intersection of half-spaces. Given an $m \times n$ matrix $A$, $b \in \mathbb R^m$, $c \in \mathbb R^n$, the primal and dual linear programs are $\min\{c^\top x : Ax=b,\ x\ge0\}$ and $\max\{b^\top y : A^\top y \le c\}$, with feasible regions $P$, $D$. A matrix is totally unimodular if every square submatrix has determinant $0$, $1$, or $-1$. A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S = \bar S \cap \mathbb Z^n$, where $\bar S$ is the convex hull of $S$'s real embedding; the discrete Minkowski sum is $S_1+S_2 = \{x_1+x_2 : x_1\in S_1, x_2\in S_2\}$.

Formalization targets

Goal (Theorem 3.6, Fenchel duality). For proper convex $f$ and proper concave $h$ satisfying at least one of four alternative conditions — a relative-interior condition on $\operatorname{dom} f \cap \operatorname{dom} h$, a polyhedrality condition on the same, or the analogous pair of conditions on $\operatorname{dom} f^\bullet \cap \operatorname{dom} h^\circ$ together with closedness of $f$, $h$ —

$$\inf_x\{f(x)-h(x)\} = \sup_p\{h^\circ(p)-f^\bullet(p)\},$$

with the extremum on the appropriate side attained whenever the common value is finite. This is the mission's capstone: the four alternative hypotheses make it the most broadly applicable statement of the four convex-duality results in this mission, each of the other three being either a special case in substance (Theorem 3.5, separation, which 3.6 is proved from) or a literal specialization to linear data (Theorem 3.10, LP duality).

Supporting milestones. Theorem 3.2 (biconjugation: $f^\bullet$ is always closed proper convex, and $g^{\bullet\bullet}=g$ for closed proper convex $g$); Theorem 3.5 (the separation theorem for convex/concave functions, under two of Theorem 3.6's four hypotheses); Theorem 3.9 (the Farkas lemma, equality form); Theorem 3.10 (LP duality: weak duality, strong duality with attainment, and complementary slackness); Theorem 3.13 (total unimodularity of the constraint matrix guarantees an integral optimal solution whenever an optimal solution exists); Proposition 3.14 (an explicit potential function certifying a minimum-weight bipartite perfect matching, via the totally unimodular incidence-matrix LP); and Proposition 3.16 (for a translation-invariant family of hole-free discrete sets, the property that discrete disjointness implies closure disjointness is equivalent to the discrete Minkowski sum matching the integer points of the closures' Minkowski sum).

Significance

Fenchel duality is the single result from which the separation theorem, LP duality, and (via the totally-unimodular incidence matrix of a bipartite graph) the combinatorial duality underlying weighted bipartite matching all descend, in one unbroken chain of specialization; formalizing this chain in one mission exhibits that structure directly, rather than treating each result as an independent fact. Proposition 3.16 plays a different role: it is the chapter's warning that naive discrete analogues of convexity (hole-freeness) do not automatically inherit convexity's good closure properties under Minkowski sums, which is exactly the gap the book's later M-convexity and L-convexity machinery is built to close — this mission's Proposition 3.16 is therefore the motivating negative result for the rest of the book's positive theory, not a loose end. So far as a platform search shows, no existing formalization matches this chunk's specific combination of extended-valued (possibly $\pm\infty$) functions, the four-alternative Fenchel duality hypothesis, or the bipartite-matching-via-total-unimodularity argument; the one related platform result (VectorSpaceOpt.fenchel_duality, from Luenberger) is for real-valued functions on general normed spaces under a single relative-interior-and-solidness hypothesis, a different generality from the extended-valued, four-hypothesis statement here.

Difficulty

The naive approach to Theorem 3.6 tries to prove the duality gap is zero directly from the definitions of the two conjugates, which only gives the easy inequality $\inf \ge \sup$ (a one-line computation, shown in the book's own proof in three lines); the substantive content is the reverse inequality, and it genuinely fails without a constraint-qualification hypothesis like (a1)-(b2) — Example 3.8 in the book exhibits a convex/concave pair with $\inf = 0 \ne -1 = \sup$ when none of the four conditions hold. The book's actual route reduces Theorem 3.6 to the separation theorem (Theorem 3.5) applied to $f$ shifted down by the (assumed finite) infimum, which produces the separating affine function directly; this is why Theorem 3.5, although logically a special case in spirit, earns its own milestone rather than being subsumed silently.

Formalization scope

All convex and concave functions are represented uniformly as (V → ℝ) → EReal-valued (Fintype V), rather than mixing WithTop ℝ for convex and WithBot ℝ for concave functions, so that Theorem 3.2's biconjugate — whose properness is a conclusion, not an assumption — has a well-defined codomain without extra casts. Convexity is defined via the epigraph being a convex subset of the ordinary real vector space $(V\to\mathbb R)\times\mathbb R$ (Mathlib's Convex ℝ), following the book's own equivalent characterization, rather than unfolding the direct inequality definition, which would require a extended-arithmetic scalar-multiplication convention (0\cdot(+\infty)=0) that Mathlib does not provide for EReal. The relative interior is defined directly from the book's own metric-ball-intersected-with-affine-hull description, since Mathlib has no relative-interior primitive at the pinned revision. Polyhedra are finite intersections of explicit half-spaces. A bipartite perfect matching is represented as a bijection between the two vertex sides restricted to the edge set — a faithful, not narrower, representation since every perfect matching between equal-size parts arises this way. The formalization does not trivialize: Theorem 3.6's four hypotheses are carried in full (not reduced to the easiest single case), and no result is stated only for finite-valued (never $\pm\infty$) functions, which would discard the entire point of the extended-value convex-analysis framework this chapter sets up for the rest of the book. Infrastructure needed beyond Mathlib's Convex, Matrix, and EReal API: all epigraph/hypograph, conjugate, relative-interior, and polyhedral apparatus is defined fresh in DiscreteConvex.IntegralConvexityB; a contribution proving any of the seven milestones independently, or supplying Mathlib-quality relative-interior lemmas, would be a natural entry point.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 3.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation

Real investors do not merely accumulate wealth for a single terminal payoff; they consume along the way, and the market they invest in is rarely a single fixed statistical regime for years at a time — bull and bear markets, business cycles, and volatility regimes shift the distribution of returns. Bäuerle and Rieder's §4.3 extends the terminal-wealth theory of chunk 04a by adding a consumption choice at every stage (the Ramsey/Merton consumption-investment problem), and §4.4 extends it again by letting the return distribution itself depend on a hidden, Markov-modulated environment state. Both extensions are shown to be genuine instances of the same abstract finite-horizon Markov Decision Process machinery from Chapter 2 — the joint consumption-investment choice and the extra regime coordinate change the state and action spaces, but not the proof strategy, which is exactly the point.

Setting

The consumption-investment problem: state $E := \mathrm{dom}\,U_p$ (wealth), action $\mathbb{R}_{\ge0}\times\mathbb{R}^d$ (consumption $c$, amounts $a$ invested), transition $T_n(x,c,a,z) = (1+i_{n+1})(x-c+a\cdot z)$, reward $r_n(x,c,a) := U_c(c)$, terminal reward $g_N := U_p$. Value functions $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[\sum_{k=n}^{N-1} U_c(c_k(X_k)) + U_p(X_N)]$. The one-period sub-problem: $D(x) := \{(c,a) : 0\le c\le x,\ (1+i)(x-c+a\cdot R)\in\mathrm{dom}\,U_p \text{ a.s.}\}$, $u(x,c,a) := U_c(c) + \mathbb{E}[U_p((1+i)(x-c+a\cdot R))]$, $v(x) := \sup_{(c,a)\in D(x)} u(x,c,a)$.

The regime-switching extension (§4.4): an environment process $(Y_n)$, a finite-state Markov chain with transition probabilities $p_{jk}$, modulates the risky-asset return law: given $Y_n=j$, the next relative risk $R_{n+1}$ has law $Q_j$, and $(R_{n+1},Y_{n+1})$ has joint law $Q_j(dz)p_{jk}$ given $Y_n=j$, $Y_{n+1}=k$. The augmented state is $(x,j) \in [0,\infty)\times E_Y$; value functions $J_n(x,j)$ are defined analogously, with the recursion incorporating a finite sum over the next regime.

Formalization targets

Goal — Theorem 4.3.3

$$V_N = U_p, \qquad V_n(x) = \sup_{(c,a)\in D_n(x)} \bigl[U_c(c) + \mathbb{E}\,V_{n+1}\bigl((1+ i_{n+1})(x-c+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave, continuous, and an optimal strategy realized by per-stage maximizers. This is chunk 04a's Theorem 4.2.2 with consumption added, and every closed-form corollary below specializes it.

Eight milestones: the one-period existence/regularity theorem (Theorem 4.3.1); the zero-mean special case (Theorem 4.3.5); power- and logarithmic-utility closed forms (Theorems 4.3.6, 4.3.7); the regime-switching generalization of the goal itself (Theorem 4.4.1), its power-utility closed form (Theorem 4.4.2), and two comparative-statics results on how the optimal policy moves across regimes under a stochastic order (Theorems 4.4.4, 4.4.5).

Significance

Theorem 4.3.3's consumption-investment structure theorem is the basis for every result about optimal spending and saving under uncertainty; its power/log closed forms (Theorems 4.3.6/4.3.7) recover the classical facts that a power-utility investor consumes and invests constant fractions of current wealth (myopic, wealth-independent policy fractions) while a log-utility investor's optimal consumption fraction, $1/(N-n+1)$, is the textbook "consume your remaining horizon's worth" rule. The regime-switching extension (§4.4) is the discrete-time analogue of Hamilton's regime-switching models, now standard in empirical finance; Theorems 4.4.4-4.4.5 give a rigorous comparative-statics answer to "does a riskier regime call for more or less stock exposure," using the increasing-concave stochastic order rather than a first- moment heuristic — the mathematically correct notion of "regime $k$'s returns dominate regime $j$'s for every risk-averse (concave, monotone) preference," not merely "regime $k$ has a higher mean."

No result of this chunk was found on the platform (searched "consumption investment", "regime switching", "stochastic order"). The proofs largely mirror chunk 04a's (the book itself says so explicitly for Theorems 4.3.1, 4.3.7, 4.4.2), so this mission's contribution is the precise joint-choice statement of each result and, for the comparative-statics theorems, the correct increasing-concave order (≤_icv, Definition B.3.9c) rather than the plain concave order (≤_cv) chunk 02c already needed for a different theorem — the two are genuinely different relations and must not be conflated.

Difficulty

The naive approach to the goal decouples the consumption and investment choices into two independent optimizations; the book's own proof shows they do separate at the level of the per-stage optimization (Theorem 4.3.6's proof: the transformed problem factors into a consumption fraction $\zeta$ and an investment fraction $\alpha$ optimized independently once the wealth scale is normalized out), but the admissible sets remain jointly constrained ($0\le c\le x$ interacts with the investable amount $x-c$), so treating them as literally independent unconstrained problems would silently solve an easier, different problem. For the regime-switching comparative statics (Theorem 4.4.5), the natural first attempt tries to prove monotonicity of $d_n(j)$ in $j$ directly from $Q_j\le_{\mathrm{icv}}Q_k$ alone; the book's own induction needs both hypotheses simultaneously (the environment chain's own stochastic monotonicity, governing how the regime itself evolves, and the return-distribution order, governing the one-period objective) — Theorem 4.4.4's monotonicity of $\alpha^*(j)$ handles the second factor of the induction's product (Eq. (4.22)) while the chain's stochastic monotonicity handles the first; dropping either hypothesis breaks the induction step.

Formalization scope

The consumption-investment vocabulary (ConsumptionInvestmentMarket, its value function, the one-period sub-problem) mirrors chunk 04a's pure-investment TerminalWealthMarket pattern exactly, extended to a joint $(c,a)$ action. The regime-switching model (RegimeSwitchingMarket) represents the finite regime set $E_Y$ abstractly (a Fintype with a row-stochastic transition matrix p : EY → EY → ℝ, not a PMF/product-measure construction on the joint disturbance): the book's own formula for $J_n^\pi$ is already a finite sum over the next regime of an integral against $Q_j$, so this is the direct, faithful representation and needs no additional measure-theoretic machinery — Jpi/J are built via an accumulator recursing through this finite-sum-of-integrals at each step (the natural generalization of chunk 04a's EFromToAcc pattern to a kernel that depends on an evolving state coordinate, rather than an exogenous process). Theorem 4.4.4/4.4.5 introduce LEIncreasingConcaveOrder (Definition B.3.9c) fresh, since chunk 02c's stochastic-order triple (≤_st/≤_cv/≤_cx) does not include the increasing-concave order this chunk's theorems actually use — reusing one of those three would silently substitute a different hypothesis, exactly the trap the chunk brief warns against. IsStochasticallyMonotoneChain (Definition B.3.13) is likewise restated fresh for a finite chain given by its transition matrix.

No trivializing formalization: D_n(x) is a genuine joint constraint on (c,a) (not two independent unconstrained choices); the six closed-form theorems (4.3.6, 4.3.7, 4.4.2, plus the comparative-statics pair) each state their own explicit recursion for $d_n$ — matching the brief's own note that the index-base convention is not uniform across them (Theorem 4.3.6 gives $d_N$ and recurses backward; Theorem 4.4.2 gives $d_0(j)$ and recurses forward) — encoded exactly as each theorem states it, not standardized to one direction.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• J. D. Hamilton, "A new approach to the economic analysis of nonstationary time series and the business cycle", Econometrica, 1989 (the regime-switching framework §4.4 specializes to a portfolio-choice setting).

Motivation

An investor with a fixed planning horizon, an initial fortune, and a personal attitude toward risk (a utility function) wants to allocate wealth between a riskless bond and several risky assets, rebalancing at each of $N$ periods, to maximize the expected utility of terminal wealth. This is the oldest and most basic problem of mathematical finance's dynamic-programming tradition, going back to Samuelson (1969) and Merton (1969, continuous time). Bäuerle and Rieder's Chapter 4 is where the abstract finite-horizon Markov Decision Process theory built up in Chapter 2 — the Bellman equation, existence of optimal policies under compactness and continuity, propagation of concavity through the value function — is first put to genuine financial work: the multiperiod terminal-wealth problem is shown to be exactly an instance of that general theory, and the reduction pays off immediately in six closed-form solutions for the standard families of utility functions used throughout the literature (power, HARA, logarithmic, exponential).

Setting

An investor with utility function $U : \mathrm{dom}\,U \to \mathbb{R}$ (Definition 3.4.1: strictly increasing, strictly concave, continuous) and wealth $x$ invests in a bond (interest rate $i_{n+1}$ on $[n,n+1)$) and $d$ risky assets with relative risk $R_{n+1}$ (Chapter 3). The one-period problem: admissible investments $D(x) := \{a \in \mathbb{R}^d : (1+i)(x+a\cdot R) \in \mathrm{dom}\,U \text{ a.s.}\}$, $u(x,a) := \mathbb{E}[U((1+i)(x+a\cdot R))]$, $v(x) := \sup_{a \in D(x)} u(x,a)$. The multiperiod problem is the $N$-stage Markov Decision Model with state space $E := \mathrm{dom}\,U$ (wealth), action space $\mathbb{R}^d$, transition $T_n(x,a,z) = (1+i_{n+1})(x+a\cdot z)$, zero one-stage reward, terminal reward $g_N := U$; its value functions are $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[U(X_N)]$ over Markov portfolio strategies $\pi$.

Formalization targets

Goal — Theorem 4.2.2

$$V_N = U, \qquad V_n(x) = \sup_{a \in D_n(x)} \mathbb{E}\bigl[V_{n+1}\bigl((1+i_{n+1})(x+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave and continuous, and an optimal portfolio strategy $(f_0^*,\dots,f_{N-1}^*)$ realized by maximizers of the recursion. This is the structural result every closed-form solution below specializes.

Eight milestones: the one-period existence/regularity theorem the induction step reduces to (Theorem 4.1.1); the upper bounding function that makes Chapter 2's existence machinery apply (Proposition 4.2.1); the zero-mean special case (Theorem 4.2.4); and four utility-specific closed forms plus the binomial-model comparative-statics lemma (Theorems 4.2.6, 4.2.11, 4.2.13, 4.2.15; Lemma 4.2.9).

Significance

Theorem 4.2.2 is the template for every dynamic portfolio problem in the rest of this book (consumption-investment in Chapter 4 §4.3-4.4, mean-variance and index tracking later in Chapter 4, and the partially-observed and jump-market analogues in Chapters 6 and 9): check a handful of structural conditions on the market data, and the existence, regularity, and recursive computability of the optimal policy follow automatically from Chapter 2's general theory rather than needing a bespoke argument each time. The six closed-form corollaries are the results practitioners actually use: the power/HARA/log/exponential-utility feedback rules are the standard textbook portfolio formulas (the logarithmic case is Kelly betting; the exponential case's wealth-independent optimal amount is the CARA-utility hallmark used throughout insurance and reinsurance mathematics), and Lemma 4.2.9's monotonicity result is the discrete-time analogue of the Merton ratio's dependence on the market's risk premium.

No result of this chunk was found on the platform (searched "terminal wealth", "portfolio optimization", "power utility", "HARA utility"). The proofs are complete in the book and mostly short (each utility-specific theorem reduces to checking the Structure Assumption via a transformation to a fraction-of-wealth variable); this mission's contribution is the precise formal statement of each closed form, with its own explicit recursion for $d_n$, since the six theorems share a structure but genuinely differ in which one-period sub-problem and which scaling variable ($x$, $x+bS^0_n/S^0_N$, or a wealth-independent constant) each uses.

Difficulty

The obvious shortcut for the goal is to prove existence of an optimal policy and its concavity/monotonicity properties by separate, ad hoc arguments at each stage; the actual content of Theorem 4.2.2 is that both reduce, via Theorem 4.1.1, to a single one-period fact applied identically at every stage — the induction step is exactly "if $v \in \mathrm{I\!M}_{n+1}$ [strictly increasing/concave/continuous with linear growth], then $v$ is a utility function on $E$ up to the growth bound, so Theorem 4.1.1 applies directly to $T_n v$." Missing this reduction leads to reproving compactness/upper-semicontinuity arguments from Chapter 2 by hand at every stage instead of invoking Theorem 4.1.1 once per stage. For the six closed-form theorems, the shared trap is conflating the different one-period sub-problems: the power- and HARA-utility theorems solve the same sub-problem (4.7) after a wealth-shift transformation, while the exponential-utility theorem's sub-problem (4.13) has a fundamentally different scaling (the optimal amount, not fraction, is wealth-independent) — collapsing these into one "utility-agnostic" statement would hide exactly the distinction the book is making.

Formalization scope

The multiperiod value function V is defined as an explicit supremum over admissible Markov portfolio strategies (not the Bellman recursion itself, and not full history-dependent strategies), following the book's own citation of Theorem 2.2.3 to justify restricting to Markov strategies for this model; this keeps the goal's parts (b)/(c) genuine content rather than restatements of the value function's own definition. The one-period vocabulary (OnePeriodD/OnePeriodU/OnePeriodV, NoArbitrageOnePeriod) is a self-contained restatement matching §4.1's own notation (a single $i$, $R$, no time index), independent of chunk 03's full market/portfolio apparatus, since Theorem 4.1.1's own content is exactly this one-period reduction. Proposition 4.2.1's proof cites two facts as already established elsewhere in the book (a concave function is dominated by an affine function; no-arbitrage bounds admissible actions linearly in wealth) — both are taken as explicit hypotheses of the Lean statement rather than re-derived, since re-deriving them is not this proposition's own content. HARA and power utility share one sub-problem definition (Afrac/vPower, Eq. (4.7)); logarithmic and exponential utility each need their own (AfracLog/vLog, vExp, Eqs. (4.11), (4.13)) since their admissibility sets and objective functions genuinely differ (a strict vs. non-strict inequality; a fraction vs. an absolute amount).

No trivializing formalization: each of the six closed-form theorems states its own explicit recursion for $d_n$ (a finite product or sum over $k=n,\dots,N-1$ of genuinely different per-stage terms) rather than a shared abstract "some sequence $d_n$ exists with $V_n = d_n \cdot (\text{shape})$" — the latter would hide exactly which recursion each utility function produces, the actual content the brief for this chunk flags as the point of having six near-identical theorems rather than one parametrized statement. Optimal strategies are stated in their exact feedback form ($f_n^*(x) = \alpha_n^* x$, or the HARA-specific affine shift, or the wealth-independent exponential-utility amount), not merely asserted to exist.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• R. C. Merton, "Lifetime portfolio selection under uncertainty: the continuous-time case", Review of Economics and Statistics, 1969 (the continuous-time analogue this discrete-time theory approximates, per Chapter 3's binomial-to-Black-Scholes convergence result).

Motivation

The maximum weight matching (MWM) problem asks, for a graph with edge weights, for a set of vertex-disjoint edges of largest total weight. It is a central problem of combinatorial optimization, with applications to transportation, assignment and scheduling, and as a subroutine for shortest paths, planar max cut, Chinese postman tours and metric TSP. Edmonds' blossom algorithm (1965) solves it on general graphs; the fastest implementation, due to Gabow, runs in $O(mn+n^2\log n)$ time, and the scaling algorithm of Gabow and Tarjan (1991) runs in $O(m\sqrt{n\log n}\,\log(nN))$ time on graphs with $n$ vertices, $m$ edges and integer weights of magnitude at most $N$. Applications such as switch scheduling, graph clustering and sparse linear solvers accept a slightly suboptimal matching in exchange for speed. This motivates $(1-\epsilon)$-approximate maximum weight matchings: matchings whose weight is at least a $1-\epsilon$ fraction of the optimum.

Timeline of linear and near-linear time approximation for general graphs (Section 1.3 and Table IV of the paper; the entries below are as the paper attributes them):

• Folklore: the greedy algorithm, which repeatedly takes the heaviest remaining edge, gives a $\tfrac12$-MWM in $O(m\log n)$ time.
• Preis (STACS 1999): a $\tfrac12$-MWM in linear time; Drake and Hougardy (2003) gave a simpler one.
• Drake and Hougardy (2003; journal version Vinkemeier and Hougardy, ACM Trans. Algorithms 2005): a $(\tfrac23-\epsilon)$-MWM in $O(m\epsilon^{-1})$ time; Pettie and Sanders (2004) improved this to $O(m\log\epsilon^{-1})$.
• Duan and Pettie (FOCS 2010) and Hanke and Hougardy (2010): a $(\tfrac34-\epsilon)$-MWM in $O(m\log n\log\epsilon^{-1})$ time.
• Duan and Pettie (2014): a $(1-\epsilon)$-MWM in $O(m\epsilon^{-1}\log\epsilon^{-1})$ time, which is linear for every fixed $\epsilon$.

Setting

Let $G=(V,E)$ be a finite simple graph with integer weights $w:E\to\{1,\dots,N\}$, $N=2^L$. A matching $M$ is a set of vertex-disjoint edges, with weight $w(M)=\sum_{e\in M}w(e)$; a vertex is free if no edge of $M$ touches it. $M$ is a $c$-MWM if $c\cdot w(M')\le w(M)$ for every matching $M'$.

A blossom is built recursively: a single vertex $\{v\}$ is a trivial blossom with $E_{\{v\}}=\emptyset$; an odd number $\ge3$ of disjoint blossoms $A_0,\dots,A_\ell$ joined in a cycle by edges $e_i\in A_i\times A_{i+1}$ form the blossom $B=\bigcup A_i$ with edge set $E_B=\bigcup E_{A_i}\cup\{e_0,\dots,e_\ell\}$. It is full if $|M\cap E_B|=(|B|-1)/2$. The algorithm keeps a laminar set $\Omega$ of full blossoms; a root blossom is a maximal one, and $G/\Omega$ contracts each root blossom to a single vertex.

Dual values $y:V\to\mathbb R$ and $z$ on odd vertex sets give each edge the value

$$yz(u,v)=y(u)+y(v)+\sum_{B\ \text{odd},\ u,v\in B} z(B).$$

The scaling algorithm (Figure 2 of the paper) has parameters $N$ and $\epsilon'=2^{-g}\le\tfrac14$. It runs scales $i=0,\dots,L$ with granularity $\delta_i=\epsilon'N/2^i$ and truncated weights $w_i(e)=\delta_i\lfloor w(e)/\delta_i\rfloor$. Each scale repeats four steps: augment along a maximal set of vertex-disjoint augmenting paths of the eligible graph $G_{\mathrm{elig}}$, shrink a maximal set of new blossoms, adjust the duals by $\pm\delta_i/2$, and dissolve root blossoms whose $z$-value has reached zero. It stops when the free vertices' $y$-values reach a scale-dependent value, which is $0$ at scale $L$. Eligibility is given by Definition 3.2; the linear-time variant keeps the algorithm unchanged and uses Definition 3.10, which additionally ignores an edge $e$ in scales $i>\mathrm{scale}(e)+\log\epsilon'^{-1}$ unless it is a blossom edge.

Formalization targets

Goal: Theorem 3.12, approximation half

For every $\epsilon$ with $\epsilon'\le\epsilon/7$, the algorithm of Figure 2 with Definition 3.10 eligibility has a terminating run, and every terminating run returns a matching $M$ with

$$w(M)\ \ge\ (1-\epsilon)\,w(M')\qquad\text{for every matching } M' \text{ of } G .$$

Milestones, in attack order

• Lemma 2.3: approximate complementary slackness ($yz(e)\ge(1-\epsilon_0)w(e)$ everywhere, $yz(e)\le(1+\epsilon_1)w(e)$ on matched and blossom edges, zero free duals) gives a $(1+\epsilon_1)^{-1}(1-\epsilon_0)$-MWM.
• Section 2 rescaling: rounding real weights to $\lfloor w/\gamma_r\rfloor$, $\gamma_r=\epsilon w_{\max}/n$, loses at most a factor $1-\epsilon/2$.
• Lemma 3.5: with Definition 3.2 the algorithm preserves Property 3.1, which consists of granularity, active blossoms, near domination $yz(e)\ge w_i(e)-\delta_i$, near tightness $yz(e)\le w_i(e)+2(\delta_j-\delta_i)$ for type-$j$ edges, and equal free duals.
• Lemma 3.6: eligible edges searched up to scale $i$ weigh at least $N/2^{i+1}+\delta_i$, and matched edges satisfy $yz(e)\le(1+4\epsilon')w(e)$.
• Lemma 3.7: the output under Definition 3.2 is a $(1-5\epsilon')$-MWM.
• Theorem 3.8: the approximation half of Theorem 3.8, with $\epsilon'\le\epsilon/5$.
• Lemma 3.11: the invariants under Definition 3.10, including $yz(e)>(1-\epsilon')w_i(e)$ and $yz(e)<(1+6\epsilon')w_i(e)$ once $i>\mathrm{scale}(e)+\gamma$.

Significance

The result. Theorem 3.12 gives the first algorithm for $(1-\epsilon)$-approximate maximum weight matching on general graphs that runs in linear time for every fixed $\epsilon$; earlier linear-time algorithms achieved only $\tfrac12$ or $\tfrac23-\epsilon$. Its analysis is a relaxation of Edmonds' complementary slackness conditions that grows weaker over the scales, but not uniformly, and Lemma 2.3 certifies an approximate matching by approximately feasible duals.

Formalizing it. The result is proved in the paper. Mathlib (at the pinned revision) has matchings, alternating walks and Tutte's theorem, but no blossoms, contracted graphs or weighted matching algorithms. A complete development gives a Lean model of blossoms, contraction and augmenting paths through blossoms, a verified primal–dual invariant for a scaling algorithm, and a checked approximate-slackness certificate for matchings. Each of these can be reused to formalize Edmonds' exact algorithm or the Gabow–Tarjan scaling algorithm.

Difficulty

The two halves of the argument pull against each other. Lemma 2.3 needs near domination and near tightness as multiplicative bounds. The algorithm maintains only additive bounds whose slack for an edge of type $j$ is $2(\delta_j-\delta_i)$, and this slack does not shrink as the scales advance. Converting it into a factor $1+O(\epsilon')$ requires a lower bound on the weight of every edge that ever became eligible, which in turn depends on the free vertices' duals following an exact schedule across scales.

For Definition 3.10 the obvious argument breaks down: an edge that is ignored after scale $\mathrm{scale}(e)+\gamma$ may violate near domination and near tightness by an amount that grows with every later dual adjustment. The claim is that the accumulated violation stays within an $O(\epsilon')$ fraction of $w_i(e)$, and establishing this requires tracking every adjustment that can reach an ignored edge.

On the combinatorial side, the Augmentation and Blossom Shrinking steps work in the contracted graph $G/\Omega$. Their correctness uses the classical facts that augmenting paths lift through full blossoms and that blossoms stay full after augmentation (Lemma 2.1), which have to be formalized from scratch.

Formalization scope

Graphs are SimpleGraph V on a Fintype V with decidable equality; edges are Sym2 V; matchings are Finset (Sym2 V) with pairwise vertex-disjoint edges of $G$; weights are $w:\mathrm{Sym2}\,V\to\mathbb N$ with $1\le w(e)\le 2^L$ on edges. Duals, $\delta_i$ and $w_i$ are real numbers. $z$ is a function on all finite vertex sets and $yz$ sums it over the odd sets that contain the edge, as on the page. $N=2^L$ and $\epsilon'=2^{-g}$, $g\ge2$, are given through their exponents. $\mathrm{scale}(e)$ uses the convention $\mu_{-1}=+\infty$. The paper's standing assumption $N\le n^2$ is used only for running time and is omitted.

The algorithm is a nondeterministic relation. A state holds $M$, $\Omega$ with its blossom edge sets, $y$, $z$, a ghost record of the scale in which each edge last entered $M\cup\bigcup_{B\in\Omega}E_B$, and the common free-vertex dual that drives the loop test. The maximal sets of augmenting paths and of new blossoms and the lifts of paths through blossoms are choices. Invariants are stated for states reachable by a run, and the goal asserts both that a terminating run exists and that every terminating run returns a $(1-\epsilon)$-MWM.

The running times $O(m\epsilon^{-1}\log N)$ of Theorem 3.8 and $O(m\epsilon^{-1}\log\epsilon^{-1})$ of Theorem 3.12 are not formalized: the paper fixes no cost model, and its bounds rely on a modified depth-first search and on word-RAM table lookups. The explicit constants $\epsilon'\le\epsilon/5$ (Theorem 3.8) and $\epsilon'\le\epsilon/7$ (Theorem 3.12) are the ones the proofs supply.

The following trivializing formalizations are ruled out: a "matching" that may contain non-edges or repeated edges; a goal about a state only assumed to satisfy Property 3.1 rather than reached by the algorithm; a run relation with no terminating run, which the existence conjunct excludes; eligibility or blossoms chosen freely instead of by the page's rules; and comparison only against matchings of the contracted graph instead of all matchings of $G$.

Welcome contributions include a Lean treatment of blossoms and their contraction (Lemma 2.1, which is not a milestone here), the lift of augmenting paths, Lemmas 3.3 and 3.4 as auxiliary results, and proofs of the milestones in the order listed.

Selected references

• R. Duan and S. Pettie, Linear-Time Approximation for Maximum Weight Matching, Journal of the ACM 61(1), Article 1, 2014. https://doi.org/10.1145/2529989
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• H. N. Gabow and R. E. Tarjan, Faster scaling algorithms for general graph-matching problems, Journal of the ACM 38(4), 815–853, 1991. https://doi.org/10.1145/115234.115366
• R. Preis, Linear time 1/2-approximation algorithm for maximum weighted matching in general graphs, STACS 1999, LNCS 1563, 259–269 (cited from the bibliography of Duan and Pettie 2014).
• D. E. D. Vinkemeier and S. Hougardy, A linear-time approximation algorithm for weighted matchings in graphs, ACM Transactions on Algorithms 1(1), 107–122, 2005 (cited from the bibliography of Duan and Pettie 2014).
• S. Pettie and P. Sanders, A simpler linear time 2/3 − ϵ approximation to maximum weight matching, Information Processing Letters 91(6), 271–276, 2004 (cited from the bibliography of Duan and Pettie 2014).

Motivation

The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system $\dot x = Ax + Bu$ so as to minimize an integrated quadratic cost. When the full state is measured and the gain may be chosen freely, the optimal feedback is given by the algebraic Riccati equation (Kalman, 1960). In many applications only an output $y = Cx$ is measured, and the controller is restricted to a static feedback $u = -Ky$. For this output-feedback problem no Riccati-type characterization exists; the design problem is a non-convex optimization over the gain matrix $K$.

Direct optimization of the gain by gradient descent, known in the control literature since Levine and Athans (1970) and revived in reinforcement learning as policy gradient (Fazel, Ge, Kakade and Mesbahi, 2018, arXiv:1801.05039), is therefore of interest both to control engineers and to the learning community. Fatkhullin and Polyak (arXiv:2004.09875, SIAM J. Control Optim. 2021) give a self-contained analysis of the continuous-time problem: the cost is coercive on the set of stabilizing gains, smooth on sublevel sets, and, for state feedback, satisfies a gradient-domination (Łežanski–Polyak–Łojasiewicz) inequality. From these they derive convergence guarantees for the gradient method.

Setting

Fix real matrices $A\in\mathbb R^{n\times n}$, $B\in\mathbb R^{n\times m}$, $C\in\mathbb R^{r\times n}$ and weights $Q\in\mathbb R^{n\times n}$, $R\in\mathbb R^{m\times m}$, and an initial-state covariance $\Sigma\in\mathbb R^{n\times n}$. A gain is a matrix $K\in\mathbb R^{m\times r}$, and the closed-loop matrix is $A_K = A - BKC$. A square matrix is Hurwitz if all its complex eigenvalues have negative real part. The set of stabilizing gains is

$$\mathcal S = \{K\in\mathbb R^{m\times r} : A_K \text{ is Hurwitz}\}.$$

For $K\in\mathcal S$ let $X(K)$ be the unique solution of the Lyapunov equation

$$A_K^\top X + XA_K + C^\top K^\top RKC + Q = 0,$$

and define the cost $f(K)=\mathrm{Tr}\big(X(K)\Sigma\big)$, the expected integrated quadratic cost of the closed loop from a random initial state with covariance $\Sigma$. With $Y(K)$ the solution of $A_KY+YA_K^\top+\Sigma=0$, the gradient of $f$ in the Frobenius inner product is

$$\nabla f(K)=2\big(RKC-B^\top X(K)\big)Y(K)C^\top .$$

A known stabilizing gain $K_0\in\mathcal S$ is given, and $\mathcal S_0=\{K\in\mathcal S: f(K)\le f(K_0)\}$ is its sublevel set. The standing assumptions are $Q,R,\Sigma\succ0$, $\operatorname{rank}C=r$ and $B\neq0$. State feedback (SLQR) is the case $C=I$.

The gradient method with step sizes $\gamma_j$ is

$$K_{j+1}=K_j-\gamma_j\nabla f(K_j),\qquad j\ge0 .$$

A number $L>0$ is a smoothness constant if $\|\nabla f(K)-\nabla f(K')\|_F\le L\|K-K'\|_F$ for all $K,K'\in\mathcal S_0$.

Formalization targets

Goal: Theorem 4.2 for state feedback

For $C=I$, an optimal gain $K_*\in\mathcal S$, and any smoothness constant $L$:

1. if $0<\gamma_j\le 2/L$ for all $j$, then every $K_j\in\mathcal S_0$ and

$$f(K_{j+1})\le f(K_j)-\gamma_j\Big(1-\frac{L\gamma_j}{2}\Big)\|\nabla f(K_j)\|_F^2 ;$$

2. if $0<\varepsilon_1\le\gamma_j\le 2/L-\varepsilon_2$ with $\varepsilon_2>0$, then $\nabla f(K_j)\to0$,

$$\min_{0\le j\le k}\|\nabla f(K_j)\|_F^2\le\frac{f(K_0)}{c_1k}\quad(k\ge1),\qquad c_1=\frac{\varepsilon_1\varepsilon_2L}{2},$$

and there are $c\ge0$, $0\le q<1$ with $\|K_j-K_*\|_F\le c\,q^j$.

Milestones

In attack order:

• Appendix A lemmas. Trace duality of dual Lyapunov equations (Lemma A.1), the trace sandwich (Lemma A.4), and eigenvalue lower bounds for Lyapunov solutions (Lemma A.5).
• Coercivity and existence. Coercivity of $f$ with the lower bounds (3.1)–(3.2) (Lemma 3.8), boundedness of $\mathcal S_0$ (Corollary 3.9), and existence of a minimizer (Corollary 3.10).
• Smoothness. The gradient formula (Lemma 3.11) and existence of a smoothness constant on $\mathcal S_0$ (Theorem 3.15, qualitative form).
• Gradient domination for state feedback. Lemmas C.2, C.3 and C.1, and the LPL inequality with the explicit constant (3.11):

$$\tfrac12\|\nabla f(K)\|_F^2\ge\mu\big(f(K)-f(K_*)\big),\qquad K\in\mathcal S_0 \qquad\text{(Theorem 3.17)}.$$

• Theorem 4.2 for output feedback. Descent and stationarity, parts 1 and 2 without the linear rate, for general $C$.

Significance

The theorem shows that a plain first-order method, started from any stabilizing gain, never destabilizes the closed loop and decreases the cost monotonically, for output feedback as well as state feedback. For state feedback it converges globally and linearly to the optimal gain. The cost is non-convex, and its domain $\mathcal S$ is open, possibly non-convex and unbounded, so this does not follow from convex optimization theory. It is the continuous-time counterpart of the policy-gradient guarantees of Fazel et al. for discrete-time LQR, and it underlies model-free and data-driven variants of gain tuning.

The result is proved in the paper, but it has not been formalized. The formalization adds three things. It makes the invariance argument (the iterates stay in $\mathcal S_0$) explicit, and the paper describes that argument as the non-trivial part. It corrects the statements where the printed text is wrong (see below). It also produces a reusable library of Lyapunov-equation facts. Mathlib has no Lyapunov equation, no LQR cost and no Hurwitz stability theory, and the platform has no continuous-time LQR material. The nearest platform items treat discrete-time Riccati iteration (BertsekasDP.riccati_convergence_stability) and Polyak–Łojasiewicz rates on a whole normed space (ShiOptRates.pl_rate). Neither applies to a function defined only on a non-convex open subset.

Difficulty

The standard descent-lemma argument assumes $f$ is defined and $L$-smooth on the whole space. Here $f$ is defined only on $\mathcal S$, and it is not smooth on all of $\mathcal S$: it blows up at the boundary. A gradient step from a point of $\mathcal S_0$ could in principle jump out of $\mathcal S$, where the Lyapunov equation has no meaningful solution. The smoothness bound is available only inside $\mathcal S_0$, so the argument must show that the whole segment from $K_j$ to $K_{j+1}$ stays in $\mathcal S_0$ before the descent inequality can be used on it. That requires coercivity, compactness of $\mathcal S_0$ and an exit-time argument. For the linear rate, gradient domination has to be established on $\mathcal S_0$ with constants controlled by $f(K_0)$, and passing from function values to distances to $K_*$ needs that minimizer's structure. Gradient domination fails for output feedback (the paper's Example 3.4 has two disconnected components with different minima), so the linear rate is stated only for $C=I$.

Formalization scope

Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every element of the complex spectrum has negative real part. $X(K)$, $Y(K)$ are "the unique solution of the Lyapunov equation, $0$ if there is none or several"; this junk value is never used, because every statement evaluates $f$ and $\nabla f$ only at gains proved or assumed to lie in $\mathcal S$. The iterates' membership in $\mathcal S_0$ is a conclusion of the goal, never a hypothesis; assuming it would delete the theorem's content. $\nabla f$ is defined by the formula (3.3), and Lemma 3.11 is the theorem that it is the gradient. $\|\cdot\|_F$ is $\sqrt{\sum M_{ij}^2}$, $\|\cdot\|$ is the spectral (operator) norm, and $\lambda_1,\lambda_n$ are the minimum and maximum eigenvalue of a symmetric matrix. State feedback is the instance $r=n$, $C=1$. In (4.6) the Frobenius norm replaces the paper's spectral norm, which is equivalent because $c$ is existential. The minimum over $0\le j\le k$ requires $k\ge1$.

Deviations from the printed text, each recorded in the item's Formalization Note:

• The smoothness constant. The explicit $L$ of (3.8) is false as printed (for $n=m=1$, $A=0$, $B=100$, $Q=100$, $R=10^{-3}$, $\Sigma=0.1$, $K_0=10^{-6}$, one has $f''(K_0)=2L$). The goal therefore takes $L$ as any Lipschitz constant of $\nabla f$ on $\mathcal S_0$, which is the paper's definition of $L$-smoothness (§3.6) and all that its proof uses. Theorem 3.15 enters only as "some such $L>0$ exists".
• Lemma C.1. It is stated with $\lambda_1^2(\Sigma)$ in the denominator, as its proof concludes and as (3.11) requires.
• Lemma A.5. It is stated for $A^\top X+XA+Q=0$; the printed $-Q$ admits no positive definite solution.
• The gain space. $\mathcal S\subseteq\mathbb R^{m\times r}$, where p. 3 prints $\mathbb R^{m\times n}$.

Not stated: Theorem 4.3 and Algorithm 4.1, Lemma 3.6, Lemmas 3.12–3.14, Corollary 3.16 and the explicit constant (3.8). Welcome contributions include a Lyapunov-equation library (existence, uniqueness, integral representation, positivity), continuity of the spectrum, and the exit-time argument, which is reusable for any descent method on a sublevel set of an open domain.

Selected references

• I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, SIAM J. Control Optim. 59(5), 2021; preprint arXiv:2004.09875v2. https://arxiv.org/abs/2004.09875
• M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML 2018. https://arxiv.org/abs/1801.05039
• W. Levine, M. Athans, On the determination of the optimal constant output feedback gains for linear multivariable systems, IEEE Trans. Automat. Control 15(1), 1970. https://doi.org/10.1109/TAC.1970.1099363
• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5, 1960.

Motivation

Stochastic approximation finds a root $x^*$ of an unknown map $R:\mathbb R^N\to\mathbb R^N$ from noisy evaluations $y_t=R(x_{t-1})+\xi_t$, by the Robbins–Monro recursion $x_t=x_{t-1}-\gamma_ty_t$. It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, $\sqrt t(x_t-x^*)\Rightarrow N(0,G^{-1}S(G^{-1})^T)$ with $G=R'(x^*)$ and $S$ the noise covariance, is achieved by the matrix step $\gamma_t=t^{-1}G^{-1}$, which requires knowing $G$.

Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of $G$: run the recursion with scalar steps that decrease more slowly than $1/t$ and output the running average $\bar x_t$ of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.

Timeline:

• 1951, Robbins and Monro: the recursion and its convergence in probability.
• 1958, Sacks: asymptotic normality of $x_t$ for $\gamma_t=\gamma/t$.
• 1988, Ruppert: averaging in one dimension, i.i.d.-type noise.
• 1990–1992, Polyak; Polyak and Juditsky: averaging in $\mathbb R^N$ for linear problems with martingale-difference noise (Theorem 1) and nonlinear problems (Theorem 2).

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $(\xi_t)_{t\ge1}$ an adapted $\mathbb R^N$-valued noise process. Given a nonrandom $x_0\in\mathbb R^N$ and step sizes $\gamma_t>0$, algorithm (7) is

$$x_t=x_{t-1}-\gamma_t\bigl(R(x_{t-1})+\xi_t\bigr),\qquad\bar x_t=\frac1t\sum_{i=0}^{t-1}x_i .$$

The error is $\Delta_t=x_t-x^*$ and the estimation error is $\bar\Delta_t=\bar x_t-x^*$.

The hypotheses are:

• Assumption 3.1: a Lyapunov function $V$ with $V(x)\ge\alpha|x|^2$, Lipschitz gradient, $V(0)=0$, $\nabla V(x-x^*)^TR(x)>0$ for $x\neq x^*$, and $\nabla V(x-x^*)^TR(x)\ge\lambda_1V(x-x^*)$ near $x^*$.
• Assumption 3.2: $|R(x)-G(x-x^*)|\le K_1|x-x^*|^{1+\lambda}$ near $x^*$, with $0<\lambda\le1$ and every eigenvalue of $G$ having positive real part.
• Assumption 3.3: $\xi_t$ is a martingale difference with $E(|\xi_t|^2\mid\mathcal F_{t-1})+|R(x_{t-1})|^2\le K_2(1+|x_{t-1}|^2)$. It splits as $\xi_t=\xi_t(0)+\zeta_t$, where $\xi_t(0)$ is a martingale difference whose conditional covariance tends to $S\succ0$ in probability and whose conditional second moments are uniformly integrable, and $E(|\zeta_t|^2\mid\mathcal F_{t-1})\le\delta(x_{t-1}-x^*)$ with $\delta(x)\to0$ as $x\to0$.
• Assumption 3.4: $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$, $\sum_t\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, $\gamma_t\to0$ and $\sum_t\gamma_t^2<\infty$.

The linear case, algorithm (2), is $R(x)=Ax-b$ with every eigenvalue of $A$ having positive real part.

Formalization targets

Goal: Theorem 2

Under Assumptions 3.1–3.4,

$$\bar x_t\to x^*\ \text{a.s.},\qquad\sqrt t\,(\bar x_t-x^*)\xrightarrow{D}N\bigl(0,\;G^{-1}S(G^{-1})^T\bigr).$$

Milestones

• Lemma 1, Part 2: under condition (4) on the steps, $t\gamma_t\to\infty$.
• Lemma 1: the matrices $\varphi_j^t=A^{-1}-\gamma_j\sum_{i=j}^{t-1}\prod_{k=j}^{i-1}(I-\gamma_kA)$ are uniformly bounded, and $\frac1t\sum_{j<t}\|\varphi_j^t\|\to0$.
• Lemma 2: the representation (A9) of $\sqrt t\,\bar\Delta_t$ for the linear error recursion.
• Theorem 1(a): the linear case, $\sqrt t(\bar x_t-x^*)\Rightarrow N(0,A^{-1}S(A^{-1})^T)$.
• Proof of Theorem 2, Part 1: $V(\Delta_t)$ converges almost surely to a finite limit.
• Proof of Theorem 2, p. 850: $x_t\to x^*$ almost surely.
• Proof of Theorem 2, Part 4: the average of the linearised process $\Delta^1_t=\Delta^1_{t-1}-\gamma_t(G\Delta^1_{t-1}+\xi_t)$ satisfies $\sqrt t(\bar\Delta^1_t-\bar\Delta_t)\to0$ almost surely.

Significance

Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance $G^{-1}S(G^{-1})^T$ is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).

The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.

Difficulty

The obvious approach analyses $x_t$ directly. It fails: with steps decreasing more slowly than $1/t$, $\sqrt t(x_t-x^*)$ diverges, and only the average has the $\sqrt t$ rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ in a quantitative way.

The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the $\sqrt t$ scale, which needs a summability estimate on $|\Delta_i|^{1+\lambda}i^{-1/2}$ obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by $\sqrt t$.

Formalization scope

Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given $\mathcal F_{t-1}$" is written with shifted indices ($\xi_{t+1}$ given $\mathcal F_t$). The algorithm is a recursive definition from $(x_0,\gamma,R,\xi)$, with $\gamma_0,\xi_0$ unused and $\bar x_t$ averaging $x_0,\dots,x_{t-1}$. Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its $\eta$–$\delta$ definition.

Corrections of the printed text, each used by the paper's own proof:

1. Assumption 3.1 prints $V(x^*)=0$ and $\ge\lambda V(x)$. Stated as $V(0)=0$ and $\ge\lambda_1V(x-x^*)$ (as printed they force $x^*=0$). The drift constant is renamed $\lambda_1$, since the paper uses $\lambda$ also in Assumption 3.2.
2. Eq. (10) is garbled as printed. It is stated as $\sum\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, the form of Assumptions 4.7 and 5.6 and of p. 851.
3. Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$.
4. $\gamma_t\to0$ and $\sum\gamma_t^2<\infty$ are added to Assumption 3.4. The proof uses them (p. 849), and they do not follow from it.
5. $R$ is assumed continuous. The paper states no regularity of $R$, but its proof of almost sure convergence (pp. 849–850) needs $\nabla V(x-x^*)^TR(x)$ bounded away from $0$ on annuli around $x^*$, which continuity and Assumption 3.1 provide.
6. Lemma 1 and Theorem 1(a) are stated under condition (4) only. The constant-step condition (3) is false as printed ($A=\mathrm{diag}(1,10)$, $\gamma=1$), and Theorem 2 does not use it.
7. (A3) is stated with the norm inside, as its proof establishes.
8. (A9) and the linearised process of Part 4 are stated with $-\gamma_t\xi_t$ noise signs, and with $\Delta^1_0=\Delta_0$. The printed $+$ signs contradict (A8) at $t=2$.

Several formalizations would make the goal trivial, and all are ruled out:

• conditional expectations of non-integrable functions, which are $0$ in Lean (every noise process is required to be in $L^2$);
• a real supremum for the uniform integrability in Assumption 3.3, which is $0$ on unbounded families;
• an arbitrary process with a property in place of the recursion (7);
• a degenerate Dirac target (the covariance $G^{-1}S(G^{-1})^T$ is positive definite under the hypotheses).

Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.

Selected references

• B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
• H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22, 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• J. Sacks, Asymptotic distribution of stochastic approximation procedures, Ann. Math. Statist. 29, 373–405, 1958. https://doi.org/10.1214/aoms/1177706619
• D. Ruppert, Efficient estimations from a slowly convergent Robbins–Monro process, Cornell University ORIE Technical Report 781, 1988 (no stable online link located).
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

Motivation

A graph records pairs of objects that cannot be chosen together. An independent set is a choice with no conflicting pair. When each vertex has a nonnegative weight, maximum weighted independent set asks for a conflict-free set with the greatest total weight. This model occurs when choices have values and pairwise incompatibilities. On general graphs the optimization problem is difficult; the planar restriction gives a concrete geometric promise under which approximation is possible. Williamson and Shmoys state a polynomial-time approximation scheme for planar maximum independent set as Theorem 10.11 of The Design of Approximation Algorithms, in the author electronic manuscript at PDF/manuscript page 271.

Setting

The instance has vertices labeled by Fin n, an adjacency table edge : Fin n → Fin n → Bool, and a real weight weight i for each vertex. SimpleGraph.fromRel turns the table into an undirected simple graph G. The theorem requires every weight to be nonnegative. A finite set S is feasible when G.IsIndepSet (S : Set (Fin n)) holds. Its value is ∑ i ∈ S, weight i.

Planarity is expressed by HasPlanarDrawing G: vertices are placed at distinct points of the real plane, and every edge is represented by a continuous simple arc. An arc has no vertex in its interior, and distinct edges can meet only at endpoints. This is a concrete local drawing convention for the planar graph promise. The drawing witnesses the hypothesis; it is not passed as part of the algorithm's input.

The computational model is a fixed finite unit-cost RAM program. Its input includes the vertex count, an integer accuracy parameter, a complete adjacency table, and the real weights in named memory cells. Its instructions include natural-number and real addition and subtraction, exact comparisons, random-access loads and stores, branches, jumps, and halt. The machine starts with the instance preloaded and produces a bitmap after the adjacency table. This precise instruction set is a formalization convention: the book states an arithmetic-operation running time but does not specify a machine language.

Formalization targets

For every real $\varepsilon>0$, let $k=\max(1,\lceil1/\varepsilon\rceil)$. The goal asserts that a single finite program and fixed positive natural constants $C,d$ work for every planar instance and every vector of nonnegative real weights. The program must halt after a number $t$ of operations satisfying

$$t+1\le C\,2^{dk}(n+1)^2.$$

Its bitmap must represent an independent set $A$, and for every independent set $S$,

$$(1-\varepsilon)\sum_{i\in S}w_i\le\sum_{i\in A}w_i.$$

Comparison with every feasible $S$ includes an optimal solution. The same program and constants precede all accuracy and instance quantifiers. The $(n+1)^2$ form includes the empty graph without imposing zero running time. The result corresponds to the $O(2^{O(1/\varepsilon)}n^2)$ bound in Theorem 10.11; the formal statement makes the constants and accuracy parameter explicit.

Significance

The result supplies an accuracy-time tradeoff for planar weighted independent set: any fixed positive accuracy has a quadratic dependence on graph size in this operation model, while the accuracy dependence is exponential. It separates the planar setting from the general graph problem. The finite instruction set and input layout make the computational claim inspectable, including what information the program receives and what counts as an operation.

The cited result is known in the textbook. This mission asks for a Lean proof of the packaged statement; the theorem currently has sorry, and no machine construction or correctness proof is claimed. The original local statement was compiled and source reviewed before packaging. That prior result establishes statement validity in its source workspace, while the upload payload is checked separately.

Difficulty

A high-quality independent set in each planar region does not immediately give a high-quality global set: edges across regions can create conflicts, and discarding boundary vertices can lose weight. A proof must coordinate the approximation inequality with a uniform operation bound for one program across all graph sizes, accuracies, and real weight vectors. It must also show the computed bitmap is always independent and that execution reaches an explicit halt instruction within the bound. These requirements rule out treating an optimizer, an embedding, or a best solution as preloaded input.

Formalization scope

The goal uses finite labeled graphs, nonnegative arbitrary real weights, exact real arithmetic, and the concrete drawing predicate above. It does not claim a bit-complexity bound for encoded reals. The RAM starts from a complete adjacency table and weight vector, with no supplied drawing or optimum. Its step function is deterministic; an invalid program counter is stuck, so the theorem explicitly requires a halt instruction. Outputs are bits in designated natural memory cells and are checked for validity before their weighted value is compared.

The packaged definitions are the drawing predicate, instruction type, state, transition, iteration, input layout, and output decoder. They contain no proof axioms or optimization oracle. The rational-input polynomial bit-time fragment in the source workspace is a separate statement and is outside this goal. A complete contribution would construct the finite program and prove its running time and approximation guarantee in the specified model.

Selected references

• David P. Williamson and David B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, author electronic manuscript, Theorem 10.11, PDF/manuscript p. 271; weighted independent-set setting p. 269 and context pp. 270–272. DOI.

Motivation

Digital services are paid for with attention: an ad-financed platform earns more the longer its users stay. Policy reports on digital markets (Crémer, de Montjoye and Schweitzer, 2019; the U.K. Digital Competition Expert Panel, 2019; Scott Morton et al., 2019) worry that such firms degrade their services with features that capture attention at the user's expense, and they usually recommend more competition. Ichihashi and Kim, Addictive Platforms (Bank of Canada Staff Working Paper 2022-16; Management Science, 2023), ask whether competition actually helps. Their answer depends on how scarce attention is. When attention is scarce, platforms compete by making their services more addictive rather than better, and a monopoly serves the consumer better than a duopoly. This mission formalizes that comparison, the paper's headline result, together with the two equilibrium characterizations it rests on.

Setting

There are $K$ platforms and a single consumer. Each platform $k$ chooses an addictiveness $d_k \ge 0$. The consumer observes $d = (d_1, \dots, d_K)$, joins a set $J$ of platforms and allocates attention $a_k \ge 0$ to each $k \in J$. She receives $0$ if $J = \emptyset$, and otherwise

$$\sum_{k\in J} u(a_k, d_k) - C\Big(\sum_{k\in J} a_k\Big),$$

subject to the attention cap $\sum_{k\in J} a_k \le \overline{A}$, where $\overline{A} \in \mathbb{R}_+ \cup \{\infty\}$. Platform $k$ earns the attention $a_k$ if the consumer joins it and $0$ otherwise.

The service utility $u(a, d)$ is twice differentiable, strictly increasing and concave in attention $a$, and strictly decreasing in $d$. The marginal utility $u_1(a, d) = \partial u/\partial a$ is strictly increasing in $d$, so a more addictive service is worse to join but harder to stop using. There is some $d$ at which no amount of attention makes the service worth joining, and $u(0,0) \ge 0$. The attention cost $C : \mathbb{R}_+ \to \mathbb{R}_+$ is strictly increasing, convex and twice differentiable, with $\lim_{a\to0}[u_1(a,0) - C'(a)] > 0$. These are Assumptions 1 and 2 of the paper.

Platforms choose addictiveness simultaneously, and then the consumer chooses $J$ and $a$. The solution concept is pure-strategy subgame perfect equilibrium: the consumer chooses optimally at every profile $d$, and no platform gains by changing its own $d_k$. A monopolist ($K = 1$) breaks ties in the consumer's favour. Consumer surplus is the consumer's payoff in the equilibrium outcome.

The monopoly benchmark uses three quantities. The first is $A(d) = \arg\max_{A\ge0} u(A,d) - C(A)$, the consumer's attention on one platform when there is no cap. The second is $d^A(\overline{A}) = \min\{d \in [0,\infty] : A(d) \ge \overline{A}\}$, the lowest addictiveness at which she exhausts her attention. The third is $d^P(\overline{A})$, the addictiveness at which her best capped payoff from one platform falls to zero. Under competition, $A_K(d) = \arg\max_{A\in[0,\overline{A}]} K\,u(A/K, d) - C(A)$ is the total attention she spends on $K$ platforms of common addictiveness $d$.

Formalization targets

Goal: Proposition 3 (monopoly versus duopoly)

Let $\overline{A}^M$ be the least cap from which on monopoly consumer surplus is zero. For every monopoly equilibrium with addictiveness $d^M$ and every duopoly equilibrium with $(d_1, d_2)$:

$$0 < \overline{A} \le A(0) \;\Longrightarrow\; d^M < d_1,\ d^M < d_2,\ CS^{\mathrm{duo}} < CS^{\mathrm{mono}},$$ $$\overline{A} \ge \overline{A}^M \;\Longrightarrow\; d_1 \le d^M,\ d_2 \le d^M,\ CS^{\mathrm{mono}} \le CS^{\mathrm{duo}}.$$

The proposition is silent about intermediate caps, and so is the goal.

Milestones

1. Proposition 1 (monopoly). The monopolist sets $\min\{d^A(\overline{A}), d^P(\overline{A})\}$, which is increasing in $\overline{A}$. The consumer's payoff rises on $[0, A(0)]$, falls on $[A(0), \overline{A}^M]$ and is zero from some $\overline{A}^M > A(0)$ on.
2. Lemmas B.1–B.4. These are comparative statics of the consumer's problem: the tangent intercept $u(x) - xu'(x)$ is increasing, the value of spreading attention over $y$ platforms is concave in $y$, and the incremental gain from one more platform falls with the addictiveness and the number of the platforms already joined.
3. Step 1 of the proof of Proposition 2. For $K \ge 2$ there is a unique $d^* > 0$ solving the indifference condition (3) between joining $K$ and $K - 1$ platforms.
4. Proposition 2 (competition). For $K \ge 2$, every platform chooses $d^*$ in the unique equilibrium.

Significance

Proposition 3 separates two effects of competition. Business stealing pushes duopolists to raise addictiveness, because a more addictive service captures a larger share of a fixed attention budget. Competition for participation restrains them, because a consumer can drop a platform and spend her time on its rival. When attention is scarce the first effect dominates and the consumer is strictly worse off under duopoly. When it is abundant the monopolist extracts the whole surplus and duopoly cannot be worse. The result is the basis of the paper's policy discussion: digital curfews and the comparison between the equilibrium and the joint-profit outcome (Propositions 4 and 6). Propositions 1 and 2 are used throughout the paper.

The paper proves these results on paper. No machine-checked proof exists. A formal proof would check several delicate points. One is the role of the monopolist's tie-break, without which every $d \in [0, d^P]$ is a monopoly equilibrium when attention is scarce. Another is that the uniqueness argument for the duopoly needs a consumer who best-responds off the equilibrium path. The appendix also asserts a few claims without argument or slightly too strongly, recorded below. Verifying them is part of the work.

Difficulty

The obvious argument for Proposition 3 compares equilibrium payoffs through the closed forms of Figure 3, and closed forms do not exist in general. Every object is defined by an optimization problem whose maximizer has no formula. The value functions are concave but need not be differentiable, so the envelope-theorem steps of Appendix B cannot be applied as written; they have to be replaced by monotone comparative statics or one-sided derivatives. Proposition 2's uniqueness is the hardest part. It rules out asymmetric equilibria by a deviation argument that controls which platforms the consumer joins after a small change in one platform's addictiveness (Lemma B.4). It also needs the consumer's whole strategy, not only her choice on the path.

Formalization scope

Platforms are Fin K; the paper's platform 1 is the index 0. Addictiveness and attention are real numbers restricted to $[0,\infty)$, and only the values of $u$ and $C$ there matter. The cap $\overline{A}$ is an extended nonnegative real (ℝ≥0∞), so $\overline{A} = \infty$ is a genuine case and "$\overline{A} \ge \overline{A}^M$" includes it. Derivatives on $[0,\infty)$ are one-sided at $0$.

The definition file states the paper's Assumptions 1–2 as printed and adds disclosed pins:

• $u(\cdot, d)$ is strictly concave. The page says "concave", but Lemma B.1 needs strict concavity and Lemma B.2 applies Lemma B.1 to $u(\cdot,d)$.
• $C(0) = 0$. Without it $d^P$ need not exist.
• The uncapped consumer problem has an optimal attention profile for every profile and every nonempty $J$. The page (p. 6) assumes this for $\overline{A} = \infty$, and $A(d)$ presupposes it.
• $\overline{A} > 0$ where the result needs it: Proposition 1's characterization, Step 1, Proposition 2 and the first half of Proposition 3. At $\overline{A} = 0$ every profile is an equilibrium.

"Increasing" and "decreasing" are weak unless the page says "strictly". The one exception is "higher addictiveness" in the first half of Proposition 3, which is stated strictly because the proof gives $d^M = 0 < d^*$.

Three statements differ from the printed text. Lemma B.2's "$V^*$ is strictly concave" is false on the paper's own Figure 3 instance and is stated as concavity. The strict clause of Lemma B.4 fails when $C$ is linear and is not posed. The derivative claims of Lemmas B.2–B.4 are stated as decreasing differences of value functions.

Several trivializing formalizations are excluded:

• An equilibrium requires the consumer to best-respond at every profile, not only at the equilibrium one.
• The tie-break is part of the monopoly equilibrium.
• Equilibria exist (Propositions 1 and 2 assert existence), and a sanity file checks the standing hypotheses on $u(a,d) = 1 - e^{-(a-d)}$, $C(a) = a/2$.
• No value function is a real supremum; maxima enter through maximizers.

Not posed: Proposition 4 and later results, and the side models of Remarks 2–3. A complete development needs maximizers of concave problems on intervals and simplices, monotone comparative statics (Topkis, Milgrom–Shannon), and envelope arguments for concave value functions. These pieces are reusable well beyond this paper, and contributions of them as separate lemmas are welcome.

Selected references

• S. Ichihashi and B.-C. Kim, Addictive Platforms, Bank of Canada Staff Working Paper 2022-16, 2022. https://doi.org/10.34989/swp-2022-16. Published in Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4392
• P. Milgrom and I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2), 583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
• J. Crémer, Y.-A. de Montjoye and H. Schweitzer, Competition Policy for the Digital Era, report for the European Commission, 2019. https://doi.org/10.2763/407537