Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Operations Research Optimization Probability+1·Captain: mikedeng1

Asymptotic Optimality of Order-up-to Policies in Lost Sales Inventory Systems: Ordering Up to the Newsvendor Level for Penalty b + τh Is Asymptotically Optimal as b → ∞Research Paper

Motivation

Periodic-review inventory systems face a simple choice each period: how much to order before the next demand is known. When unmet demand is lost, the order can affect the stock available several periods later without preserving a backlog that records earlier shortages. This makes the optimal policy difficult to describe when replenishment takes time. An order-up-to policy offers a practical rule: order enough to bring the inventory position to a fixed level. Huh, Janakiraman, Muckstadt and Rusmevichientong ask when that simple rule performs as well as the best admissible lost-sales policy as the penalty for a lost unit grows. Their working paper, pp. 3–4 and 17–18, proves asymptotic optimality for a particular level obtained from a related backorder system.

The motivating costs are concrete. A lost sale may represent an expedited service part or a missed sale whose cost is much larger than one period of holding inventory. The paper's central comparison concerns the high-penalty regime while holding the demand law, lead time and holding rate fixed. The fixed-level policy can be computed from the distribution of demand over the lead time plus the order period; it does not require solving the full lost-sales control problem. The paper also supplies a finite-penalty bound, which this mission retains as a milestone. Huh et al., pp. 3–4, 17–18.

Setting

Let $D_1,D_2,\ldots$ be independent, identically distributed nonnegative demands with finite positive mean. An order takes a fixed integer lead time $\tau\ge1$ to arrive. At the start of period $t$ , the order placed $\tau$ periods earlier arrives; then a new order is placed, and demand $D_t$ is observed. Unmet demand is lost. At period end, each unit remaining on hand incurs holding cost $h>0$ , and each lost unit incurs penalty $b>0$ . The inventory position counts on-hand units and outstanding orders. An order-up-to- $S$ policy raises this position to $S\ge0$ whenever possible.

Write $C^{\mathcal L,S}(h,b)$ for the long-run average cost of that policy and $C^{\mathcal L*}(h,b)$ for the infimum over admissible policies. The corresponding backorder system retains unmet demand as negative net inventory and charges $b$ per backordered unit per period. For an order-up-to level $S$ , its stationary average cost is

C^{\mathcal B,S}(h,b)=h\mathbb E[(S-\mathbf D)^+]+b\mathbb E[(\mathbf D-S)^+],\qquad \mathbf D=\sum_{i=1}^{\tau+1}D_i.

The newsvendor level $S^{\mathcal B*}(h,b)$ is the smallest nonnegative $S$ with $\Pr(\mathbf D\le S)\ge b/(b+h)$ ; it attains the best backorder order-up-to cost $C^{\mathcal B*}(h,b)$ . The paper's Assumption 1 concerns this lead-time demand $\mathbf D$ : if $m_{\mathbf D}(t)=\mathbb E[\mathbf D-t\mid\mathbf D>t]$ when the conditioning event has positive probability and zero otherwise, then $m_{\mathbf D}(t)/t\to0$ as $t\to\infty$ . Huh et al., pp. 3–4, 9, 11–12.

Formalization targets

Asymptotically optimal order-up-to level

Fix $h$ , $\tau$ and the demand law satisfying Assumption 1. Set $S_{b+\tau h}=S^{\mathcal B*}(h,b+\tau h)$ . The goal is the equivalent multiplicative form of Theorem 15(b): for every $\varepsilon>0$ , all sufficiently large $b$ satisfy

\inf_{S\ge0}C^{\mathcal L,S}(h,b)\le C^{\mathcal L,S_{b+\tau h}}(h,b)\le(1+\varepsilon)C^{\mathcal L*}(h,b).

The infimum over order-up-to levels captures the paper's best such policy. The right-hand comparator remains the infimum over all admissible lost-sales policies. The multiplicative form also covers an almost-surely constant demand law, where both costs can be zero and a literal ratio would be undefined. Huh et al., Theorem 15(b), p. 17.

Explicit finite-penalty bound

Theorem 15(a) is a milestone. With $S'=S^{\mathcal B*}(h,b/(\tau+1))$ and $\psi(S';h,q)=q\mathbb E[(\mathbf D-S')^+]/(h\mathbb E[(S'-\mathbf D)^+])$ , its factor is

\frac{1+\nu_b\psi(S';h,b/(\tau+1))}{1+\psi(S';h,b/(\tau+1))},\qquad \nu_b=\frac{(b+\tau h)(\tau+1)}{b}.

The milestone states the bound where the expected holding quantity in $\psi$ is positive. Earlier milestones state the pathwise comparison of the systems, the two-sided average-cost comparison with penalties $b/(\tau+1)$ and $b+\tau h$ , the lower bound on unrestricted lost-sales optimal cost, the newsvendor formula, and the backorder sensitivity results used by the theorem. Huh et al., Lemmas 5, 9, 13 and Theorems 6, 15, pp. 11–18.

Significance

The theorem gives a specific computable stock level whose relative cost loss vanishes in the high-penalty regime. It addresses the gap between a tractable backorder benchmark and the more difficult lost-sales control problem. The finite-penalty factor states how the comparison depends on lead time, holding cost, penalty and the shortage-to-holding ratio; the asymptotic statement alone would not quantify that dependence. The paper establishes these mathematical results; the mission asks for machine-checked proofs of the stated Lean targets. Huh et al., pp. 17–18.

Formalizing the result would also supply reusable infrastructure for coupled inventory systems: measurable demand-path laws, pathwise recursions with delayed delivery, extended nonnegative long-run costs, and a clean comparison between an explicit policy and the infimum over unrestricted policies. The backorder newsvendor and mean-residual-life components can be reused beyond this particular lost-sales model.

Difficulty

The backorder system has a closed stationary cost formula, while a lost-sales order-up-to process generally cannot be replaced directly by that formula. The paper notes that its on-hand inventory distribution need not converge from every starting state, even under a fixed order-up-to policy. One must therefore justify the long-run comparison without assuming stationarity from an arbitrary start. A second difficulty is the benchmark: comparing only against other order-up-to policies is too weak to establish Theorem 15, because the goal uses the optimal cost over all admissible lost-sales policies. Huh et al., pp. 14–16, 18.

Formalization scope

Lean reuses the published CappedBaseStock lost-sales model. Its demands are nonnegative and i.i.d. with finite positive mean; $\tau\ge1$ and $h,b>0$ . Period zero in Lean is period one in the paper. Both coupled processes start with zero on-hand stock and an empty pipeline. Inventory $X_t$ is read immediately after delivery, before current demand. Lost-sales costs lie in $[0,\infty]$ and use the limsup of expected Cesàro averages; the backorder closed form uses real Bochner expectations under finite-mean demand. The paper's stationary lost-sales cost and this Cesàro cost are identified using its long-run results, but those convergence results are outside this proposal. Huh et al., pp. 14–16.

The paper prints nonnegative rates in Theorem 15, while its displayed newsvendor fraction and shortage-to-holding ratios require positive denominators. Theorem 6(a) therefore states the ratio limit for nonconstant demand laws. The main theorem uses a multiplicative limit bound that also covers constant demand, where the printed ratio is undefined.

The quantity $C^{\mathcal L*}$ is an infimum over measurable, history-dependent policies with private randomization; no attaining policy is assumed. The backorder optimum is an infimum over nonnegative order-up-to levels. Assumption 1 is imposed on the sum of $\tau+1$ demands, and the limit $b\to\infty$ is expressed by a positive threshold uniform over all parameter records with the fixed lead time and holding rate. The mission excludes a restricted policy comparator, a fixed penalty, a one-period lead-time specialization, and Assumption 1 on single-period demand. Solvers may contribute proofs of any milestone, along with finite-mean and measurability lemmas needed to connect the model to the backorder benchmarks.

Selected references

W. T. Huh, G. Janakiraman, J. A. Muckstadt and P. Rusmevichientong, Asymptotic Optimality of Order-up-to Policies in Lost Sales Inventory Systems, working paper, December 4, 2006; published in Management Science 55(3), 2009. DOI: 10.1287/mnsc.1080.0945.
G. Janakiraman, S. Seshadri and G. Shanthikumar, A Comparison of the Optimal Costs of Two Canonical Inventory Systems, working paper, Stern School of Business, New York University, 2005; bound quoted in Huh et al., §5, p. 13. Quoted source.

11 thms2 active usersReviewed

Control Theory Dynamic Programming Operations Research+3·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case IX: Imperfect State Information — Reduction to a Perfect-Information Model through a Statistic Sufficient for ControlTextbook

Motivation

In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.

For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.

Setting

The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space $S$ , control space $C$ and observation space $Z$ ; a discount factor $\alpha>0$ ; a lower semianalytic cost $g:SC\to R^*=[-\infty,\infty]$ ; a Borel state transition kernel $t(dx'\mid x,u)$ ; Borel observation kernels $s_0(dz\mid x)$ and $s(dz\mid u,x)$ ; and a horizon $N$ . The initial state $x_0$ has distribution $p\in P(S)$ , $z_0\sim s_0(\cdot\mid x_0)$ , and then $x_{k+1}\sim t(\cdot\mid x_k,u_k)$ , $z_{k+1}\sim s(\cdot\mid u_k,x_{k+1})$ . The controller knows the information vector $i_k=(z_0,u_0,\dots,u_{k-1},z_k)\in I_k$ and must choose $u_k\in U_k(i_k)$ , where the constraint set $\Gamma_k=\{(i_k,u)\mid u\in U_k(i_k)\}$ is analytic.

A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ consists of universally measurable stochastic kernels $\mu_k(du_k\mid p;i_k)$ that respect the constraints (Definition 10.4). Together with $p$ it determines probability measures $P_k(\pi,p)$ on the histories $(x_0,z_0,u_0,\dots,x_k,z_k,u_k)$ , the cost

J_{N,\pi}(p)=\int\Big[\sum_{k=0}^{N-1}\alpha^k g(x_k,u_k)\Big]dP_{N-1}(\pi,p),

and the optimal cost $J^*_N(p)=\inf_\pi J_{N,\pi}(p)$ (Definition 10.5). Assumption $(F^+)$ asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; $(F^-)$ asks the same of the positive part.

A statistic is a sequence of Borel maps $\eta_k:P(S)I_k\to Y_k$ into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, $\Gamma_k=\{(i_k,u)\mid(\eta_k(p;i_k),u)\in\hat\Gamma_k\}$ with $\hat\Gamma_k$ analytic; (b) the conditional law of $\eta_{k+1}$ given $(\eta_k,u_k)$ is a Borel kernel $\hat t_k(dy_{k+1}\mid y_k,u_k)$ , for every $p$ and every policy; and (c) the conditional expectation of $g(x_k,u_k)$ given $(\eta_k,u_k)$ is a lower semianalytic function $\hat g_k(y_k,u_k)$ . The perfect state information model (PSI) of Definition 10.7 has states $y_k\in Y_k$ , constraints $\hat U_k(y_k)=(\hat\Gamma_k)_{y_k}$ , costs $\hat g_k$ and transitions $\hat t_k$ ; its cost and optimal cost at $y\in Y_0$ are $\hat J_{N,\hat\pi}(y)$ and $\hat J^*_N(y)$ . The initial distribution of $y_0$ is

\varphi(p)(\underline Y_0)=\int_S s_0(\{z_0\mid\eta_0(p;z_0)\in\underline Y_0\}\mid x_0)\,p(dx_0).

A Markov (PSI) policy $\hat\mu_k(du\mid y_k)$ acts in (ISI) through $\mu_k(du\mid p;i_k)=\hat\mu_k(du\mid\eta_k(p;i_k))$ .

Formalization targets

Goal: Proposition 10.3

Under $(F^+,\hat F^+)$ or $(F^-,\hat F^-)$ ,

J^*_N(p)=\int_{Y_0}\hat J^*_N(y_0)\,\varphi(p)(dy_0)\qquad\forall p\in P(S),

and a Markov (PSI) policy that is optimal, $\varphi(p)$ -optimal or weakly $\varphi(p)$ - $\varepsilon$ -optimal for (PSI) is respectively optimal, optimal at $p$ , or $\varepsilon$ -optimal at $p$ for (ISI); under $(F^+,\hat F^+)$ an $\varepsilon$ -optimal (PSI) policy is $\varepsilon$ -optimal for (ISI). Here $\hat\pi$ is weakly $q$ - $\varepsilon$ -optimal if $\int\hat J_{N,\hat\pi}\,dq\le\int\hat J^*_N\,dq+\varepsilon$ when $\int\hat J^*_N\,dq>-\infty$ and $\int\hat J_{N,\hat\pi}\,dq\le-1/\varepsilon$ otherwise, and $q$ -optimal if $q(\{y_0\mid\hat J_{N,\hat\pi}(y_0)=\hat J^*_N(y_0)\})=1$ (Definition 10.8).

Milestones

Lemma 10.1: the process $(\eta_0,u_0,\dots,\eta_k,u_k)$ generated in (ISI) by a Markov (PSI) policy has the law $\hat P_k[\hat\pi,\varphi(p)]$ .
Proposition 10.2: $J_{N,\hat\pi}(p)=\int\hat J_{N,\hat\pi}\,d\varphi(p)$ for Markov $\hat\pi$ .
Corollary 10.2.1: $J^*_N(p)\le\int\hat J^*_N\,d\varphi(p)$ .
Lemma 10.2: every (ISI) policy is matched in cost by some Markov (PSI) policy.
Proposition 10.4: $\varepsilon$ -optimal nonrandomized (ISI) policies that depend on $i_k$ only through $\eta_k(p;i_k)$ .
Proposition 10.6: the identity maps on $P(S)I_k$ form a statistic sufficient for control.

Significance

Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the $\varphi(p)$ -average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of $\varepsilon$ -optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.

These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.

Difficulty

The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair $(p,\pi)$ , while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values $\pm\infty$ , so interchanging sums and integrals requires the finiteness assumptions $(F^\pm)$ and $(\hat F^\pm)$ ; and the inequality $J^*_N\ge\int\hat J^*_N\,d\varphi(p)$ requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.

Formalization scope

Horizon. Only finite horizons $N\ge1$ are covered, hence only the cases $(F^+,\hat F^+)$ and $(F^-,\hat F^-)$ of the book's statements; the infinite-horizon cases $(P,\hat P)$ , $(N,\hat N)$ , $(D,\hat D)$ are out of scope.
Extended reals. Costs live in EReal with the book's convention $\infty-\infty=+\infty$ written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction ( $\top-\top=\bot$ ) is never used where both terms can be infinite.
Spaces and measures. $S$ , $C$ , $Z$ , $Y_k$ are Borel spaces in the sense of Definition 7.7 with their Borel $\sigma$ -algebras; $P(S)$ carries the weak topology and the Giry $\sigma$ -algebra. Policies are families of maps into ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of $\mathbb N$ ; only stages $k<N$ are constrained.
Conditional statements. Conditions (22) and (23) are stated through the defining relations of conditional probability and expectation, for every $p$ and every policy, with (23) required when $g(x_k,u_k)$ is quasi-integrable.
Policies in Proposition 10.3. The (PSI) policies in the optimality transfers are Markov, as in Proposition 10.2.
No trivialization. Definition 10.6 is the full definition: analytic $\hat\Gamma_k$ with full projection, Borel kernels $\hat t_k$ satisfying (22) for every $p$ and policy, and lower semianalytic $\hat g_k$ satisfying (23); a weaker notion would make Proposition 10.6 empty.

Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10 (1965) 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
C. Striebel, Sufficient statistics in the optimum control of stochastic systems, Journal of Mathematical Analysis and Applications 12 (1965) 576–592. https://doi.org/10.1016/0022-247X(65)90027-2
N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9

12 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

The Strong Perfect Graph Theorem VI: A Berge Graph Containing a Long Odd Prism Admits a Proper 2-Join, a Balanced Skew Partition or a Proper Homogeneous PairResearch Paper

Motivation

A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Berge conjectured in 1961 that a graph is perfect exactly when it contains no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this strong perfect graph theorem in 2006 (Ann. of Math. 164 (2006), 51–229). Perfect graphs matter beyond graph theory: for them the stable set polytope is described by clique inequalities, so maximum weight stable set and colouring problems become polynomially solvable linear programs (Grötschel, Lovász and Schrijver).

The proof reduces the theorem to a decomposition statement (1.3 of the paper): every Berge graph is basic or admits one of a few decompositions. That statement is in turn proved in twelve steps, listed as 1.8.1–1.8.12. Each step excludes one kind of configuration from a Berge graph without the decompositions. This mission is step 1.8.5, restated as 13.4: it deals with Berge graphs that contain a long odd prism but no appearance of $K_4$ . It is the only step of the proof that needs proper 2-joins in the complement and proper homogeneous pairs.

Setting

All graphs are finite and simple; $\overline{G}$ is the complement of $G$ . A path is an induced subgraph which is a path, and its length is its number of edges. An antipath is a path of $\overline{G}$ . A hole is an induced cycle of length at least $4$ , and an antihole is the complement of a hole of $\overline{G}$ . $G$ is Berge if every hole and antihole of $G$ has even length.

A prism consists of two disjoint triangles $\{a_1,a_2,a_3\}$ , $\{b_1,b_2,b_3\}$ and three paths $P_i$ from $a_i$ to $b_i$ , such that the only edges between different paths are the triangle edges. It is long if some $P_i$ has length $>1$ , even if all three lengths are even, and odd otherwise.

A subdivision $H$ of a graph $J$ replaces every edge of $J$ by a track, these tracks being disjoint except at their ends. $J$ appears in $G$ if $L(H)$ is isomorphic to an induced subgraph of $G$ for some bipartite subdivision $H$ of $J$ , where $L$ is the line graph.

The decompositions in the conclusion (pp. 53–54):

A proper 2-join is a partition $(X_1,X_2)$ of $V(G)$ , with disjoint nonempty $A_i,B_i\subseteq X_i$ , such that the only edges between $X_1$ and $X_2$ are all edges between $A_1$ and $A_2$ and all edges between $B_1$ and $B_2$ . Every component of $G|X_i$ meets $A_i$ and $B_i$ . If $G|X_i$ is a path between single vertices $A_i$ and $B_i$ , it has odd length $\ge 3$ .
A skew partition is a partition $(A,B)$ of $V(G)$ with $A$ not connected and $B$ not anticonnected. It is balanced if no odd path joins two nonadjacent vertices of $B$ through $A$ , and no odd antipath joins two adjacent vertices of $A$ through $B$ .
A proper homogeneous pair is a pair $(A,B)$ of disjoint nonempty sets such that every other vertex is complete or anticomplete to $A$ , and complete or anticomplete to $B$ . All four combinations must occur.

The intermediate objects come from Sections 11–13 of the paper:

A strip $S=(A,C,B)$ : every vertex of $V(S)=A\cup B\cup C$ lies on a rung, a path from $A$ to $B$ with interior in $C$ .
A step: two disjoint rungs joined exactly by an edge at each end.
A step-connected strip: steps cover $V(S)$ and connect $A$ and $B$ .
Left-stars and right-stars: vertices complete to $A$ (resp. $B$ ) and anticomplete to the rest of $V(S)$ .
A banister: a path from a left-star to a right-star whose interior sees nothing of $V(S)$ .
A staircase $K=(S,a_0\text{-}R_0\text{-}b_0)$ : a step-connected strip with a banister of length $\ge 3$ . A staircase can be maximal or strongly maximal.
Three kinds of breaker: sets around a strip or staircase whose presence forces a balanced skew partition.

Formalization targets

Goal: 13.4

Let $G$ be Berge with no appearance of $K_4$ in $G$ or in $\overline{G}$ , and suppose $G$ contains a long odd prism as an induced subgraph. Then

G \text{ or } \overline{G} \text{ admits a proper 2-join, or } G \text{ admits a balanced skew partition, or } G \text{ admits a proper homogeneous pair.}

Milestones

In the order of the paper's argument:

11.3: in a Berge graph with no even prism, every rung of a step-connected strip and every banister has odd length.
11.4: under no appearance of $K_4$ and no even prism, no anticonnected set $Q$ has the six properties listed in the statement.
11.5: a 1-breaker forces a balanced skew partition.
12.1: relative to a maximal staircase, every outside vertex is of exactly one of three types (minor; major; a star with a neighbour on $R_0$ ).
12.3: a connected set containing a left-star and attaching to $B\cup C$ contains a major vertex or a banister.
12.4: a 2-breaker forces a balanced skew partition.
13.3: a 3-breaker forces a balanced skew partition.

Significance

13.4 removes long prisms from the analysis. Combined with 10.6 (the even prism), it shows that a recalcitrant graph contains no long prism in $G$ or $\overline{G}$ , which places it in the class $\mathcal F_5$ (p. 154). The later steps (double diamonds, odd wheels, pseudowheels, wheels) all assume this. The step-connected strip and staircase method developed here is also the paper's model for growing a maximal structure and then classifying how the rest of the graph attaches to it.

The theorem has been proved since 2006; no machine-checked proof of it or of any of its steps is known. The proof of 13.4 also cites these results of the same paper, which are posed in other missions of this series:

10.6 (the even-prism step), posed in mission V;
7.2 (equal parity of the paths of a prism), posed in mission V;
2.1, 2.4, 2.6, 2.7, 4.2, 4.3, 4.5, 4.6 (the Roussel–Rubio lemma and the skew-partition toolkit), posed in mission II.

Difficulty

The difficulty is the volume of case analysis behind every statement. The paper does not prove the exact analogue of the even-prism result 10.6. It warns (p. 127) that it does not know whether that analogue holds, and adds the two extra outcomes instead. The obvious first idea is to take a long odd prism and analyse attachments to it as in Section 10. The paper does not get the result that way (p. 127): it replaces two of the three paths by a maximal step-connected strip. Controlling how every remaining vertex or connected set attaches to such a strip is what the breaker results do. Maximality is also delicate. "Strongly maximal" refers to staircases of the complement, so $G$ and $\overline{G}$ must be handled in one framework.

Formalization scope

Graphs are SimpleGraph V on a Fintype vertex type with decidable equality. $\overline{G}$ is Gᶜ.

Paths, holes, rungs, banisters. Paths are lists of distinct vertices, adjacent exactly when consecutive (induced). Holes are lists adjacent exactly when cyclically consecutive. Rungs are listed from their end in $A$ to their end in $B$ , and banisters from the left-star to the right-star.
Vertex sets. Connectedness of a vertex set is reachability inside G.induce X, so $\emptyset$ is connected. Anticonnectedness is the same notion in Gᶜ.
Prisms. A prism is three paths whose cross adjacencies are exactly the two triangles. Each path has length at least $1$ , so the triangles are disjoint.
Appearances. A subdivision of $J$ is an injection of $V(J)$ together with one track per edge. The tracks are internally disjoint and cover every vertex and edge. An appearance is a graph embedding of $L(H)$ into $G$ , and embeddings reflect adjacency.
Staircases and breakers. A staircase is a quadruple $(A,C,B,R_0)$ . Maximality quantifies over all staircases of $G$ , strong maximality also over staircases of $\overline{G}$ . The breakers are predicates on these data.

Every hypothesis of the paper is kept. "No appearance of $K_4$ " is in $G$ and in $\overline{G}$ for the goal, and in $G$ for the milestones. The goal also keeps "Berge", "no even prism" and "no 1-/2-breaker" where the page has them. 12.1's "exactly one" is an exclusive disjunction. 11.4 is a non-existence statement.

A formalization with non-induced paths, with the complement dropped from "one of $G,\overline{G}$ ", or with a strip, staircase or breaker predicate that no graph satisfies would make the targets empty or false. The definitions here are checked against a concrete graph: the 8-vertex prism with path lengths $1,1,3$ is a long odd prism, and it carries a staircase. Contributions are welcome: proofs of the milestones, and reusable material on induced paths, holes and line graphs of subdivisions.

Selected references

M. Chudnovsky, N. Robertson, P. Seymour, R. Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. https://doi.org/10.4007/annals.2006.164.51
C. Berge, Färbung von Graphen, deren sämtliche bzw. deren ungerade Kreise starr sind, Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg 10 (1961), 114–115.
V. Chvátal, Star-cutsets and perfect graphs, J. Combin. Theory Ser. B 39 (1985), 189–199. https://doi.org/10.1016/0095-8956(85)90049-8
V. Chvátal, N. Sbihi, Bull-free Berge graphs are perfect, Graphs and Combinatorics 3 (1987), 127–139. https://doi.org/10.1007/BF01788536
G. Cornuéjols, W. H. Cunningham, Compositions for perfect graphs, Discrete Mathematics 55 (1985), 245–254. https://doi.org/10.1016/0012-365X(85)90051-7
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

21 thms2 active usersReviewed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

On the Stochastic Matrices Associated with Certain Queuing Processes 2: The GI/M/1 Imbedded Chain Is Ergodic iff ρ < 1 and Recurrent iff ρ ≤ 1Research Paper

Motivation

A single-server queue in which customers arrive according to a renewal process and are served in exponentially distributed times is the system GI/M/1. Observed just before successive arrivals, its queue length is a Markov chain on $\{0, 1, 2, \dots\}$ , the imbedded chain introduced by D. G. Kendall (Kendall 1953, Ann. Math. Statist. 24, pp. 338–354). Whether this chain settles into a statistical equilibrium, keeps returning to the empty state without one, or drifts off to infinity is the first question asked about the queue, and every later quantity (stationary queue lengths, waiting-time distributions) presupposes the answer.

F. G. Foster's 1953 paper (Foster 1953) answers it for GI/M/1 and for M/G/1 by a different route from Kendall's direct analysis: it first proves general criteria, stated in terms of solutions of linear equations and inequalities in the transition matrix, for a countable Markov chain to be ergodic, recurrent or transient, and then checks them on the two queueing matrices. The criteria are of independent use; one of them (Theorem 2 of the paper) is now known as Foster's criterion, the starting point of the drift (Lyapunov-function) method for stability of Markov chains and queueing networks.

Timeline. Kendall (1951, J. Roy. Statist. Soc. B 13) studied queue-length processes directly, including a recurrence argument for M/G/1 that Foster's §3 reproduces; Kendall (1953) introduced the imbedded-chain method and, for GI/M/1, proved by it that $\rho < 1$ is sufficient for ergodicity (Foster 1953, p. 359); Foster (1953) proved the full classification, ergodic iff $\rho < 1$ and recurrent iff $\rho \le 1$ , by the general criteria. This mission treats the GI/M/1 half; a companion mission treats M/G/1.

Setting

A transition matrix on the states $\{0, 1, 2, \dots\}$ is an array $[p_{ij}]$ of nonnegative reals whose rows sum to $1$ . For a state $j$ , $f_{jj}$ is the probability that the chain started at $j$ returns to $j$ at some later step. The chain is recurrent if $f_{jj} = 1$ for every $j$ , transient if $f_{jj} < 1$ for every $j$ , and ergodic (recurrent-nonnull, positive recurrent) if moreover every mean recurrence time $\sum_n n f^{(n)}_{jj}$ is finite. Foster's general theorems concern an irreducible chain (every state reachable from every state), assumed aperiodic for simplicity.

The GI/M/1 chain is described by a sequence $a = (a_n)_{n \ge 0}$ of positive numbers with $\sum_n a_n = 1$ : $a_n$ is the probability that exactly $n$ services are completed between two arrivals. With the tails $\alpha_i = \sum_{j \ge i+1} a_j$ ,

[p_{ij}] = \begin{bmatrix} \alpha_0 & a_0 & 0 & 0 & \cdots \\ \alpha_1 & a_1 & a_0 & 0 & \cdots \\ \alpha_2 & a_2 & a_1 & a_0 & \cdots \\ \vdots & \vdots & \vdots & \vdots & \end{bmatrix},

that is $p_{i0} = \alpha_i$ , $p_{ij} = a_{i+1-j}$ for $1 \le j \le i+1$ , and $p_{ij} = 0$ for $j > i+1$ . In Lean this matrix is gim1Matrix a. The traffic parameter $\rho$ is defined through its inverse,

\rho^{-1} = \sum_{n=1}^{\infty} n\, a_n \in (0, \infty],

the mean number of service completions per interarrival interval (rhoInv a, and rho a $= \rho$ ).

Formalization targets

Goal: the classification of GI/M/1 (§4, p. 359)

\text{the chain is ergodic} \iff \rho < 1, \qquad \text{the chain is recurrent} \iff \rho \le 1 .

Together: ergodic for $\rho < 1$ , recurrent-null for $\rho = 1$ , transient for $\rho > 1$ . The statement carries no constants and leaves the sequence $a$ free apart from positivity and normalization.

Milestones

Theorem 7 (p. 358): for a probability distribution $\{p_n\}$ with $p_0 > 0$ , the equation $\sum_{n \ge 0} z^n p_n = z$ has a root in $(0, 1)$ iff $\sum_{n\ge1} n p_n > 1$ .
Theorem 1, sufficiency (p. 355): a nonnull solution of $\sum_i x_i p_{ij} = x_j$ with $\sum_i |x_i| < \infty$ makes the system ergodic.
Theorem 1, necessity (p. 355): in an ergodic system every nonnegative solution of $\sum_i x_i p_{ij} \le x_j$ has $\sum_i x_i < \infty$ .
Theorem 4 (pp. 356–357): the system is transient iff $\sum_j p_{ij} y_j = y_i$ ( $i \ne 0$ ) has a bounded nonconstant solution.

Milestones 2–4 are stated for a general irreducible aperiodic chain.

Significance

The classification tells exactly when the GI/M/1 queue is stable: the stationary distribution of the imbedded chain, which is geometric, exists precisely in the ergodic case $\rho < 1$ , and for $\rho > 1$ the queue grows without bound. Theorems 1 and 4 are general tools, reusable for any countable chain: Theorem 1 characterizes ergodicity by summable invariant vectors, Theorem 4 characterizes transience by bounded harmonic functions off one state. Theorem 7 is the extinction criterion of branching processes and recurs throughout applied probability.

All of these results are proved in the literature (Foster 1953; Feller's textbook for Theorem 7 and a version of Theorem 4). As far as a search of the platform shows, none of them has a machine-checked proof; the platform holds related special cases for the G/M/1 queue with a specific interarrival law (QueueingFundamentals.GM1.unique_root_unit_interval, open), but not the general lemma or the classification. A formalization would provide the general criteria as reusable library results and the first verified stability classification of a non-Markovian queue's imbedded chain.

Difficulty

The matrix is explicit, but none of the three properties is a finite computation: ergodicity and recurrence are statements about return times over all horizons, so each direction must go through an existence or nonexistence statement about infinite systems of equations. For the converse directions the obvious argument fails: exhibiting a candidate solution such as $x_i \equiv 1$ shows nothing until it is known that ergodicity forces every such solution to be summable, and showing that no bounded nonconstant solution of (7) exists when $\rho < 1$ requires control of all solutions, not of one. The general criteria themselves rest on limit theorems for $p_{ij}^{(n)}$ and on interchanging infinite sums, and the infinite-mean case $\sum n a_n = \infty$ has to be carried along everywhere.

Formalization scope

The Markov-chain vocabulary is the published definition QueueingFundamentals_Foundations_MarkovChain: TransitionMatrix (entries p, nonnegativity, rows summing to $1$ via HasSum), returnProb, meanRecurrenceTime, Irreducible, Aperiodic, PositiveRecurrent. "Ergodic" is PositiveRecurrent. IsRecurrent and IsTransient are defined state by state from returnProb; their complementarity for irreducible chains is a theorem, not a definition.
States are indexed from $0$ , as in the paper. The goal quantifies over every TransitionMatrix whose entries equal gim1Matrix a; such a matrix exists for every admissible $a$ (rows sum to $1$ ), so the statement is not vacuous.
$\rho^{-1}$ and $\rho$ live in $[0, \infty]$ (ℝ≥0∞), with $\infty^{-1} = 0$ : an infinite mean gives $\rho = 0$ , and that chain is ergodic.
The goal does not assume irreducibility or aperiodicity: they follow from $a_n > 0$ . Milestones 2–4 carry them, as the paper's standing assumptions (§1).
Every infinite series appearing in a hypothesis is required to converge (HasSum or Summable), so that a divergent series cannot satisfy an equation or inequality vacuously. In Theorem 1's sufficiency half the $x_i$ may be of either sign. In Theorem 7 the distribution is renamed $q$ to avoid a clash with $p_{ij}$ .
Ruled out as trivializing: defining $\rho$ by a real inverse of a real series, defining "ergodic" as the existence of a summable invariant vector (which is Theorem 1's condition), or stating the goal over a matrix that need not exist.
Not included: the paper's explicit description of the solutions of (7) for $\rho \ge 1$ via the generating function $(1 - z)\{A(z) - z\}^{-1}$ , and the M/G/1 half (Theorems 2, 3, 5), which is the companion mission. Contributions welcome: proofs of the general criteria (reusable for any countable chain), of Theorem 7, and lemmas on the GI/M/1 matrix such as irreducibility and aperiodicity.

Selected references

F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976
D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24 (1953), 338–354 (the paper immediately preceding Foster's in the same issue).
D. G. Kendall, Some problems in the theory of queues, J. Roy. Statist. Soc. B 13 (1951), 151–185.
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950.

8 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

The Strong Perfect Graph Theorem IV: A Berge Graph Whose Appearances of K4 Are All Degenerate Is Double Split, Decomposes, or Has No Appearance of K4Research Paper

Perfect graphs and the decomposition of Berge graphs

A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Perfect graphs are the graphs for which colouring and clique problems behave as linear programs do: the stable-set polytope of a perfect graph is described by its clique inequalities, so maximum weight stable sets and minimum colourings can be computed in polynomial time (Grötschel, Lovász & Schrijver 1988). In 1961 Berge conjectured that a graph is perfect exactly when it has no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006).

The proof is a decomposition theorem: every Berge graph is basic or admits one of a few decompositions. The paper reaches it through twelve steps, 1.8.1–1.8.12 (p. 59), each handling graphs that contain a certain configuration. This mission poses step 1.8.3, Theorem 9.6. It handles Berge graphs that contain the line graph of a bipartite subdivision of $K_4$ , all such line graphs being degenerate.

Setting

All graphs are finite and simple. $\overline{G}$ denotes the complement of $G$ . A hole is an induced cycle of length at least $4$ , an antihole is a hole of $\overline{G}$ , and $G$ is Berge if all its holes and antiholes have even length. A path is always an induced path, and an antipath is a path of $\overline{G}$ . The length of either is its number of edges.

Line graphs and appearances. The line graph $L(H)$ has vertex set $E(H)$ , two edges adjacent when they share an end. $H$ is a subdivision of $J$ if it arises from $J$ by replacing every edge by a track (a path, not necessarily induced), these tracks disjoint except for their ends. $J$ appears in $G$ if, for some bipartite subdivision $H$ of $J$ , $L(H)$ is isomorphic to an induced subgraph of $G$ ; $L(H)$ is then an appearance of $J$ . For $J = K_4$ the appearance is degenerate if some 4-cycle of $H$ contains the four vertices of degree three. A $K_4$ -enlargement is a 3-connected graph with a proper subgraph isomorphic to a subdivision of $K_4$ . An appearance $L(H)$ is overshadowed if some branch of $H$ of odd length $\ge 3$ , with ends $b_1, b_2$ , has a vertex of $G$ nonadjacent to at most one edge at $b_1$ and at most one edge at $b_2$ .

Knots and striations. A knot $(P_1, P_2, Q_1, Q_2)$ is formed by two paths $P_i$ with ends $a_i, b_i$ and two antipaths $Q_j$ with ends $x_j, y_j$ . They are pairwise disjoint and of length $\ge 1$ , $P_1$ is anticomplete to $P_2$ , $Q_1$ is complete to $Q_2$ , and the ends are joined in a prescribed twisted pattern (pp. 107–108). A degenerate appearance of $K_4$ is a knot. A strip $(A, C, B)$ is a family of paths ("rungs") from $A$ to $B$ through $C$ ; an antistrip is a strip of $\overline{G}$ . A striation $L$ is made of $m \ge 2$ strips and $n \ge 2$ antistrips. All rungs and antirungs are odd, the strips are pairwise anticomplete, the antistrips pairwise complete, and every strip is parallel or co-parallel to every antistrip, with enough "twists" between them (p. 112). A striation is maximal if no striation has a strictly larger vertex set. The paper defines when a set of vertices is local for a knot or striation and when it resolves one.

Outcomes. A double split graph has its vertices partitioned into $\{a_i\}, \{b_i\}$ ( $m \ge 2$ ) and $\{c_j\}, \{d_j\}$ ( $n \ge 2$ ). Each $a_ib_i$ is an edge and each $c_jd_j$ a nonedge, distinct pairs $\{a_i,b_i\}$ are anticomplete and distinct pairs $\{c_j,d_j\}$ complete to each other, and every $\{a_i,b_i\}$ and $\{c_j,d_j\}$ are joined by exactly two disjoint edges. A skew partition $(A, B)$ of $V(G)$ has $G|A$ disconnected and $\overline{G}|B$ disconnected. It is balanced if no odd path joins nonadjacent vertices of $B$ through $A$ and no odd antipath joins adjacent vertices of $A$ through $B$ . A proper 2-join is a partition $(X_1, X_2)$ of $V(G)$ whose only cross edges are complete joins $A_1$ – $A_2$ and $B_1$ – $B_2$ , with the side conditions of p. 53.

Formalization targets

Goal: Theorem 9.6 (p. 116)

Let $G$ be Berge, with every appearance of $K_4$ in $G$ and in $\overline{G}$ degenerate and no induced subgraph of $G$ isomorphic to $L(K_{3,3})$ . Then

G \text{ is double split} \ \lor\ G \text{ admits a balanced skew partition} \ \lor\ G \text{ or } \overline{G} \text{ admits a proper 2-join} \ \lor\ K_4 \text{ appears in neither } G \text{ nor } \overline{G}.

Milestones

9.1 (p. 108): in a knot of a Berge graph all four paths and antipaths are odd, and either both paths or both antipaths have length one.
9.3 (p. 109): a connected set $F$ whose attachments to a knot are not local either contains a vertex whose neighbourhood resolves the knot, or attaches in one of three special ways ("up to symmetry").
9.4 (p. 112): the neighbourhood in $V(L)$ of a vertex outside a maximal striation $L$ is local or resolves $L$ .
9.5 (p. 113): if every vertex of a connected set $F$ outside $V(L)$ has a local neighbourhood, then the attachments of $F$ in $V(L)$ are local.

9.3–9.5 assume that no $K_4$ -enlargement appears in $G$ or $\overline{G}$ and that no appearance of $K_4$ in $G$ or $\overline{G}$ is overshadowed. An optional, non-milestone item poses 9.7 (p. 118): a Berge graph with an appearance of $K_4$ is a line graph or the complement of one, a double split graph, or admits a proper 2-join (in $G$ or $\overline{G}$ ) or a balanced skew partition.

Significance

9.6 is the step of the proof that produces double split graphs, one of the five basic classes. In the main argument it follows step 1.8.1 (5.1, nondegenerate appearances of $K_4$ ) and is combined with it in 9.7. Through 9.7 it gives the first half of 13.5: every recalcitrant graph belongs to the class $\mathcal{F}_5$ and so contains no appearance of $K_4$ in $G$ or $\overline{G}$ .

The theorem has been proved since 2006. We know of no machine-checked proof of the strong perfect graph theorem or of any of its steps. Mathlib has line graphs and graph embeddings but no subdivisions, appearances or decompositions of Berge graphs. This mission produces a faithful Lean statement of step 1.8.3 and of the four lemmas its proof rests on, together with Lean definitions of knots, strips and striations.

Difficulty

The obvious approach would take a degenerate appearance of $K_4$ and study how each remaining vertex attaches to it, as §§5–6 do for nondegenerate appearances. This does not close. A degenerate appearance can be read as a line graph or as its complement, so the analysis of a vertex in $G$ and in $\overline{G}$ has to be run at once. Single vertices can also be absorbed into larger structures that the line-graph analysis does not see. The proof grows the appearance to a maximal striation and classifies attachments to it, and the hard steps are 9.4 and 9.5. Their proofs need 9.3 in every case, and they use maximality to refute configurations that would let the striation grow.

Formalization scope

Graphs are SimpleGraph V on a Fintype with decidable equality. Every object is defined as on the page, in the namespace StrongPerfectGraph.DoubleSplit.

Paths and antipaths are induced and given as vertex lists. A list fixes the labelling of the ends: $a_i, b_i$ are the first and last vertices of $P_i$ , and $x_j, y_j$ those of $Q_j$ .
The empty set is connected (p. 54).
Line graphs are Mathlib's SimpleGraph.lineGraph; "isomorphic to an induced subgraph" is an induced embedding ↪g. Subdivisions $H$ and enlargements $J'$ range over graphs on Fin k.
"Every appearance of $K_4$ is degenerate" is the absence of a nondegenerate appearance. The hypothesis on $L(K_{3,3})$ concerns $G$ only. Every other hypothesis concerns both $G$ and $\overline{G}$ , as on the page.
A striation is a structure with $m$ strips and $n$ antistrips indexed by Fin m, Fin n.
"Up to symmetry" in 9.3 is the paper's exchange of $P_1, P_2$ and $Q_1, Q_2$ with the ends renamed so that the result is again a knot. Both compatible renamings are allowed, and so is their composite, the reversal of all four.

Dropping the bars of the complement would make the theorem false or vacuous. So would reading "path" as a non-induced path, or encoding a decomposition so that it always exists. The statements use the complement explicitly, induced paths throughout, and the full definitions of p. 53–54.

The proof of 9.6 also uses results of the same paper that are posed in other missions of this series. These are 2.1, 2.2, 4.1 and 4.2, posed in mission II (skew partitions), and 5.3, 5.8, 6.1 and 7.5, posed in mission III (line graphs). They are not posed again here. The bridge 9.2 between knots and line graphs, whose proof the paper omits as obvious, is not posed either. Proofs of 9.1, of 9.3, and reusable lemmas about knots and striations are welcome.

Selected references

M. Chudnovsky, N. Robertson, P. Seymour, R. Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. https://doi.org/10.4007/annals.2006.164.51
C. Berge, Färbung von Graphen, deren sämtliche bzw. deren ungerade Kreise starr sind, Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe 10 (1961), 114.
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

19 thms2 active usersReviewed

Control Theory Dynamic Programming Operations Research+2·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case VII: The Finite-Horizon Borel Model — over Universally Measurable Policies J*_K = T^K(J_0)Textbook

Motivation

Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.

Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).

Setting

A finite horizon stochastic optimal control model is a nine-tuple $(S,C,U,W,p,f,\alpha,g,N)$ . The state space $S$ , control space $C$ and disturbance space $W$ are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint $U(x)\subseteq C$ is nonempty and $\Gamma=\{(x,u)\mid u\in U(x)\}$ is analytic in $S\times C$ . Disturbances are drawn from a Borel stochastic kernel $p(dw\mid x,u)$ , the system moves by $x_{k+1}=f(x_k,u_k,w_k)$ with $f$ Borel, the discount factor $\alpha$ is a positive real, the one-stage cost $g:\Gamma\to[-\infty,\infty]$ is lower semianalytic ( $\{g<c\}$ is analytic for every real $c$ ), and $N\ge1$ is the horizon. The state transition kernel is $t(B\mid x,u)=p(\{w\mid f(x,u,w)\in B\}\mid x,u)$ .

A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ chooses $u_k$ from a universally measurable stochastic kernel $\mu_k(du_k\mid x_0,u_0,\dots,x_k)$ concentrated on $U(x_k)$ ; it is Markov if $\mu_k$ depends on $x_k$ only, and nonrandomized if every $\mu_k(\cdot\mid\cdot)$ is a point mass. $\Pi'$ denotes all policies and $\Pi$ the Markov ones. A policy and an initial distribution $p$ determine a probability measure $r_N(\pi,p)$ on state–control paths, and the $K$ -stage cost and optimal cost are

J_{K,\pi}(x)=\int\Big[\sum_{k=0}^{K-1}\alpha^k g(x_k,u_k)\Big]dr_N(\pi,p_x),\qquad J^*_K(x)=\inf_{\pi\in\Pi'}J_{K,\pi}(x).

Assumption (F⁺) requires $\int g^-\,dq_k(\pi,p_x)<\infty$ , and (F⁻) requires $\int g^+\,dq_k(\pi,p_x)<\infty$ , for every policy, initial state and stage, where $q_k$ is the marginal of $r_N$ on the $k$ -th pair. The DP operators are

T_\mu(J)(x)=\int_C\Big[g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big]\mu(du\mid x),\qquad T(J)(x)=\inf_{u\in U(x)}\Big\{g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big\}.

Formalization targets

Goal: Proposition 8.2

J^*_K=T^K(J_0),\qquad K=1,\dots,N,

under (F⁺) or (F⁻), where $J_0\equiv0$ . The goal leaves the horizon, the discount factor and the sign of $g$ unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.

Milestones

In attack order: Lemma 8.1 (the cost of a Markov policy equals $T_{\mu_0}\cdots T_{\mu_{K-1}}(J_0)$ ), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of $T$ ), Lemma 8.3 (under (F⁺), $T^K(J_0)>-\infty$ ), Lemma 8.4 (monotone and bounded convergence for $T_\mu$ ). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ( $J^*_K$ is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).

Significance

Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.

All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention $\infty-\infty=\infty$ .

Difficulty

The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on $K$ , choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and $T(J)$ is generally not Borel even when $J$ and $g$ are; Borel policies are too few for $\varepsilon$ -optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.

Formalization scope

Lean conventions:

Spaces carry [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.
Extended reals are EReal. Addition inside costs and integrands uses the book's convention $-\infty+\infty=+\infty$ (badd), not Mathlib's, which gives $\bot+\top=\bot$ . Integrals are $\int f^+-\int f^-$ with $\infty-\infty=\infty$ (extInt).
The universal σ-algebra is the intersection of all completions (universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).
The integral against $r_N(\pi,p)$ is the iterated integral of Eq. (4) of Chapter 8 (pathInt).
Stages are indexed $0,\dots,N-1$ , and a history is $k$ state–control pairs plus the current state.
$g$ is stored on $S\times C$ , but only its values on $\Gamma$ are constrained or used.

A trivializing formalization is excluded by construction. $J^*_K$ is the infimum over all policies in $\Pi'$ , not over Markov or nonrandomized ones. $J_{K,\pi}$ is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.

A complete development needs:

the analytic-set and universal-measurability theory of §7.6–7.7: closure of analytic sets under projections and sections, measurability of integrals against universally measurable kernels (Proposition 7.46), and the selection theorem (Proposition 7.50);
extended-real integration lemmas in the style of Lemma 7.11.

This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Chapter 8. https://web.mit.edu/dimitrib/www/soc.html
D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Ann. Probab. 2 (1974), 926–941. https://doi.org/10.1214/aop/1176996558
S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Math. Oper. Res. 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

14 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

The Strong Perfect Graph Theorem V: A Berge Graph with No Nondegenerate Appearance of K4 Containing an Even Prism Is a Nine-Vertex Even Prism or DecomposesResearch Paper

Motivation

A perfect graph is a finite simple graph in which every induced subgraph has chromatic number equal to its largest clique size. This equality gives a structural reason that a clique lower bound on the number of colours is attainable for every induced part of the graph. Berge proposed a forbidden-subgraph description of perfect graphs: a graph should be perfect exactly when it has neither an odd hole nor an odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved that statement in The strong perfect graph theorem, Annals of Mathematics 164 (2006), Theorem 1.2. Their proof separates possible configurations in a Berge graph and shows that each either belongs to a controlled class or admits a decomposition.

This mission isolates the even-prism step, Theorem 10.6 of that paper. A prism is one of the configurations that can appear in a Berge graph even though odd holes and antiholes do not. The step matters because its conclusion leaves only a specific nine-vertex graph or one of two decompositions that the larger proof handles elsewhere. It is the result identified as step 1.8.4 in the authors’ outline (paper, pp. 59 and 124).

Setting

All graphs here are finite and simple. A path means an induced path; a single vertex is allowed as a path of length zero. A hole is an induced cycle with at least four vertices, and an antihole is a hole in the complementary graph. A graph $G$ is Berge if every hole of $G$ and of its complement $\overline G$ has even length.

A prism has two disjoint triangles, $A=\{a_1,a_2,a_3\}$ and $B=\{b_1,b_2,b_3\}$ , joined by three pairwise vertex-disjoint induced paths $R_i$ from $a_i$ to $b_i$ . Between distinct paths, the only edges are those in $A$ and those in $B$ . The prism is even when all three $R_i$ have even length. “ $G$ contains an even prism” means that such paths exist as an induced configuration in $G$ ; $G$ may have other vertices. “ $G$ is an even prism” means the paths cover every vertex of $G$ (paper, pp. 93 and 119).

An appearance of $K_4$ is an induced copy in $G$ of the line graph of a bipartite subdivision $H$ of the four-vertex complete graph. It is nondegenerate if no four-cycle of $H$ contains all four branch vertices. Only appearances in $G$ are excluded in this mission; appearances in $\overline G$ are allowed by the hypotheses (paper, pp. 72, 74–75).

A proper 2-join partitions the vertices into two sides with specified, nonempty attachment sets. The cross edges are exactly the two complete attachment pairs; every component of either side meets both of its attachment sets. If a side is itself a path between singleton attachment sets, that path has odd length at least three. A balanced skew partition divides the vertices into $A$ and $B$ so that $A$ is disconnected, $B$ is disconnected in the complement, and two path parity conditions hold: no odd path crosses $A$ between nonadjacent vertices of $B$ , and no odd antipath crosses $B$ between adjacent vertices of $A$ (paper, pp. 53–54).

Formalization targets

Prism lemmas

The numbered milestones are Theorems 7.2–7.4 and 10.5. They assert common parity of the three prism paths, common neighbours of an anticonnected set at both end triangles, preservation of two neighbours under replacement of one even prism path, and the balanced skew partition forced by a major vertex. A vertex is major when it is adjacent to at least two vertices of each end triangle. These milestones match the paper’s statements on pp. 93 and 123 (paper).

Goal: Theorem 10.6

For a Berge graph $G$ with no nondegenerate appearance of $K_4$ in $G$ ,

G\text{ contains an even prism} \quad\Longrightarrow\quad \bigl(G\text{ is an even prism and }|V(G)|=9\bigr) \;\lor\; G\text{ admits a proper 2-join} \;\lor\; G\text{ admits a balanced skew partition}.

The first case describes the entire graph, not just an induced nine-vertex subgraph. The statement fixes all outcomes exactly as in Theorem 10.6, p. 124.

Significance

Theorem 10.6 removes even prisms from the unresolved part of the strong perfect graph theorem’s structural argument. If the graph is larger than the exceptional prism and has no nondegenerate $K_4$ appearance, the theorem supplies a proper 2-join or a balanced skew partition. Subsequent results can work with those decompositions instead of treating arbitrary attachments to a prism (paper, §10 and the outline at 1.8.4).

The mathematical result is proved in the 2006 paper. The work here is to give its graph objects and statements machine-checkable meanings, then formalize the known proof. This proposal contains open Lean theorem statements and sorry-free definitions; the proof obligations remain for solvers. The definitions of induced paths, holes, subdivisions, and decomposition predicates can also support other steps of this paper. The Roussel–Rubio lemma and the balanced-skew-partition results of §§2–4 are proved in the same paper and posed in mission II of this series. The prism-attachment result 10.4 is posed in mission VI, where it is used most directly.

Difficulty

An outside connected set can attach to several parts of a prism without containing a single major vertex. Its attachments need not be local to one path or one triangle, so checking vertices one at a time does not decide which decomposition exists. The paper’s §10 distinguishes several attachment patterns; the evenness of the paths and the exclusion of a nondegenerate $K_4$ appearance restrict them, but do not themselves give a 2-join or skew partition by a one-line parity argument. The larger proof must also account for attachments throughout the graph while preserving the full definitions of both decomposition outcomes (paper, pp. 119–127).

Formalization scope

Lean represents a graph as SimpleGraph V with a finite vertex type. The prism is three lists of vertices, each an induced path; the lists are disjoint, and the cross-edge condition admits exactly the two end triangles. Reversing a list changes its orientation but not the underlying graph configuration. A hole uses a cyclic list with the closing edge; Berge checks holes in both $G$ and $\overline G$ . Connectivity is reachability in an induced graph, so the empty vertex set is connected as the paper says. A $K_4$ subdivision uses six tracks on a finite carrier, with all its vertices and edges accounted for; the appearance uses an induced graph embedding of its line graph. The exception checks that the prism covers the whole graph and that $|V(G)|=9$ .

These encodings require genuinely induced paths and the paper’s nondegenerate appearance condition. Dropping either would change the theorem. The proper 2-join includes component reachability and the odd-path special case; the balanced skew partition includes both path parity clauses. The nine-vertex graph formed by two triangles and three two-edge paths has a separate sorry-free Lean witness, so the exceptional outcome is nonvacuous. Useful contributions include the numbered prism lemmas, attachment analysis for 10.6, and reusable results about finite induced paths and graph subdivisions.

Selected references

Maria Chudnovsky, Neil Robertson, Paul Seymour and Robin Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. DOI: 10.4007/annals.2006.164.51.

12 thms2 active usersReviewed

Combinatorics Graph Theory Operations Research+2·Captain: mikedeng1

Maximal Flow Through a Network II: In an ab-Planar Network Some Chain from Source to Sink Meets Every Cut Exactly OnceResearch Paper

Motivation

The maximum flow problem asks how much of a commodity can be shipped from a source to a sink through a network whose arcs have limited capacities. L. R. Ford, Jr. and D. R. Fulkerson's 1956 paper Maximal Flow Through a Network proved the minimal cut theorem: the largest flow value equals the smallest total capacity of a set of arcs that separates source from sink. That theorem is formalized in the companion mission Maximal Flow Through a Network I.

The second section of the same paper treats a special class of networks, those that remain planar after an arc from source to sink is added. For these networks the paper shows that one particular source–sink chain crosses every minimal separating set exactly once. This structural fact turns the minimal cut theorem into a simple computing procedure: repeatedly push as much flow as possible along such a chain and delete the arcs it saturates. The paper notes that G. Dantzig had conjectured, before the minimal cut theorem was proved, that this procedure yields a maximal flow on planar networks. The same "uppermost path" idea underlies later algorithms for maximum flow in planar graphs with source and sink on a common face (Itai and Shiloach, 1979).

The statement is short and purely combinatorial in its conclusion, but its hypothesis is topological. This mission isolates that theorem.

Setting

A network $N$ has a finite set $V$ of vertices and a finite set $E$ of arcs. Each arc $e$ joins two distinct end vertices, written $\mathrm{tail}(e)$ and $\mathrm{head}(e)$ ; arcs carry no direction, and two arcs may join the same pair of vertices. Two distinct vertices are distinguished, the source $a$ and the sink $b$ , and each arc carries a positive capacity (capacities play no role in the target below).

A chain joining $u$ and $w$ is a set $C$ of distinct arcs that can be arranged as $\alpha_1(v_0v_1), \alpha_2(v_1v_2), \dots, \alpha_k(v_{k-1}v_k)$ with $v_0 = u$ , $v_k = w$ , and the vertices $v_0, \dots, v_k$ pairwise distinct; each arc may be traversed in either direction. The empty set is the null chain from $u$ to $u$ .

A set $D$ of arcs is a disconnecting set if every chain joining $a$ and $b$ contains an arc of $D$ . A disconnecting set none of whose proper subsets is disconnecting is a cut.

The network is ab-planar if the graph of $N$ , together with one additional arc joining $a$ and $b$ , can be drawn in the plane without crossings: vertices go to distinct points of $\mathbb R^2$ ; each arc, including the added arc $ab$ , goes to an injective continuous path between the points of its end vertices; no arc passes through a vertex other than its ends; and two distinct arcs meet only at endpoints of both. In Lean the drawing is the structure ABPlaneDrawing N, and $N$ is ab-planar when Nonempty (ABPlaneDrawing N). The section's standing assumption is that no arc of $N$ already joins $a$ and $b$ .

Formalization targets

Goal: Theorem 2 (p. 403)

If $N$ is ab-planar, no arc of $N$ joins $a$ and $b$ , and some chain joins $a$ and $b$ , then

\exists\, T \text{ a chain joining } a \text{ and } b \ \text{ such that }\ |T \cap D| = 1 \ \text{ for every cut } D \text{ of } N.

This is FordFulkerson56.Planar.ab_planar_exists_chain_meeting_each_cut_once. "Precisely once" is exact cardinality one, neither "at least once" (true of every chain) nor "at most once".

Milestone: a chain meeting a cut in one prescribed arc (proof of Theorem 2, p. 403)

For every network $N$ , every cut $D$ and every arc $\alpha \in D$ , there is a chain $C$ joining $a$ and $b$ with $C \cap D = \{\alpha\}$ . No planarity is involved; the statement is what the minimality of a cut provides to the proof.

Further item: the Fig. 2 example (p. 403)

In the "gas, water, electricity" graph $K_{3,3}$ with the arc $ab$ removed, every chain joining $a$ and $b$ meets some cut in three arcs. This network is not ab-planar, so the example shows that the planarity hypothesis of Theorem 2 cannot be dropped.

Significance

Theorem 2 and the minimal cut theorem together give the paper's procedure for planar networks: if $T$ meets every cut once, then imposing a flow $k$ on $T$ lowers the value of every cut by exactly $k$ , so the minimal cut value, and hence the maximal flow value, drops by $k$ . Saturated arcs can then be deleted and the step repeated. Without the "exactly once" property the reduction could overshoot the cut structure, and the greedy step would not be justified. The theorem is also one of the earliest instances of the link between planarity and cut structure that later underlies planar duality arguments for minimum cuts.

The result has been known since 1956 and is not open. No machine-checked version is recorded on the platform, and Mathlib, at the pinned revision, has neither planar graphs nor the Jordan curve theorem. A formal proof would be the first formalized statement about source–sink planar networks in this library, and the counterexample item records, as a checkable fact, that the hypothesis is necessary.

Difficulty

The conclusion is combinatorial while the hypothesis is a drawing in $\mathbb R^2$ . The paper's proof normalises the drawing (the added arc $ab$ on the outer boundary, the graph in a vertical strip with $a$ on the left line and $b$ on the right), selects the "top-most" chain from $a$ to $b$ , and argues that a chain meeting a cut below the top-most chain must cross another such chain. Each of these steps rests on plane topology: the existence of the outer region, the meaning of "top-most", and the fact that two chains with interleaved endpoints on a boundary must intersect, which is a form of the Jordan curve theorem.

The naive purely combinatorial route fails: the analogous statement for arbitrary networks is false (Fig. 2), so any argument has to use the drawing somewhere. Replacing the drawing by a combinatorial embedding (rotation systems, faces) is possible but then requires proving that the two notions agree, which is again Jordan-curve territory.

Formalization scope

Conventions committed to in the Lean statements:

Vertices and arcs are finite types V, E with decidable equality. Arcs are undirected, may be parallel, and have two distinct end vertices. Source and sink are distinct, capacities are positive (structure Network).
A chain is a Finset E that is the arc set of some arrangement as a simple path (IsChainWalk, IsChain); the null chain is allowed.
IsDisconnecting and IsCut quantify over all chains joining source and sink; a cut is a disconnecting set no proper subset of which is disconnecting.
ab-planarity is a plane drawing of the graph with the extra arc indexed by none : Option E, with injective Paths in ℝ × ℝ as arcs.

Hypotheses of the goal: hno_ab, the standing assumption of §2 (no arc joins $a$ and $b$ , p. 403); hconn, that some chain joins $a$ and $b$ . The second is not stated in the paper; its proof starts from "the chain joining a and b which is top-most", which presupposes one, and without it the statement is false (if $a$ and $b$ are disconnected, the empty set is a cut and no chain exists).

The drawing structure is satisfiable (a three-vertex path network has an explicit drawing), so the planarity hypothesis is not vacuous; and it covers the added arc $ab$ and all crossings, so $K_{3,3}$ minus $ab$ is not ab-planar and the goal is not refuted by the paper's own example. A formalization that dropped the arc $ab$ from the drawing, or quantified over disconnecting sets instead of cuts, would state a false theorem and is ruled out.

A complete development needs basic plane topology for paths in $\mathbb R^2$ (a Jordan-curve-type separation lemma for simple closed curves, or an equivalent statement about crossing paths in a strip), together with combinatorial lemmas about chains (concatenation and shortcutting of chains at a common vertex). The topological lemmas are reusable well beyond this mission. Proofs through a combinatorial embedding are welcome, provided the equivalence with ABPlaneDrawing is proved.

Selected references

L. R. Ford, Jr. and D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
A. Itai and Y. Shiloach, Maximum flow in planar networks, SIAM Journal on Computing 8 (1979), 135–150. https://doi.org/10.1137/0208012
H. Whitney, Planar graphs, Fundamenta Mathematicae 21 (1933), 73–84. https://doi.org/10.4064/fm-21-1-73-84

7 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

The Strong Perfect Graph Theorem III: A Berge Graph Containing a Nondegenerate Line Graph of a Bipartite Subdivision of K4 Is a Line Graph or DecomposesResearch Paper

Motivation

A graph is perfect if every induced subgraph has chromatic number equal to its clique number, and Berge if no induced subgraph is an odd cycle of length at least five (an odd hole) or the complement of one (an odd antihole). Berge conjectured in 1961 that the two classes coincide. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006), 51–229. Perfect graphs matter beyond graph theory. A graph is perfect exactly when its stable-set polytope is defined by clique inequalities (Chvátal; Lovász), so the theorem characterizes the graphs on which the stable-set and colouring integer programs are solved by their linear relaxations.

The proof is a structure theorem. Every Berge graph is basic (bipartite, the complement of a bipartite graph, the line graph of a bipartite graph or its complement, or a double split graph), or it admits a proper 2-join, a proper homogeneous pair or a balanced skew partition. The proof splits into twelve steps (1.8.1–1.8.12, p. 59), each about Berge graphs that contain a particular configuration. This mission is the first step, statement 5.1 of the paper. It covers Berge graphs that contain a large line graph, and it takes up Sections 5–8 (pp. 72–107).

Setting

All graphs are finite and simple. For a graph $G$ , $\overline{G}$ is its complement. A path is an induced path, and its length is its number of edges. A track is a path in the conventional, not necessarily induced, sense. A set $X \subseteq V(G)$ is connected if $G|X$ is connected, and anticonnected if $\overline{G}|X$ is connected.

The line graph $L(H)$ of a graph $H$ has vertex set $E(H)$ , and two edges are adjacent when they share an end. $G$ is a line graph if $G \cong L(H)$ for some graph $H$ . A subdivision of a graph $J$ replaces each edge $uv$ of $J$ by a track from $u$ to $v$ , the tracks being disjoint except for their ends. A branch-vertex is a vertex of degree at least $3$ . A branch is a maximal track whose internal vertices are not branch-vertices. $J$ is 3-connected if it has more than three vertices and no set of at most two vertices disconnects it.

For a bipartite subdivision $H$ of $K_4$ , $L(H)$ is degenerate if some 4-cycle of $H$ passes through its four vertices of degree three. A graph $J$ appears in $G$ if $L(H)$ is isomorphic to an induced subgraph of $G$ for some bipartite subdivision $H$ of $J$ .

Two decompositions occur in the conclusion. A skew partition is a partition $(A, B)$ of $V(G)$ with $A$ not connected and $B$ not anticonnected. It is balanced if no odd path joins two nonadjacent vertices of $B$ through $A$ , and no odd antipath joins two adjacent vertices of $A$ through $B$ . A proper 2-join is a partition $(X_1, X_2)$ of $V(G)$ with nonempty disjoint $A_i, B_i \subseteq X_i$ such that:

$A_1$ is complete to $A_2$ and $B_1$ is complete to $B_2$ ;
there are no other edges between $X_1$ and $X_2$ ;
every component of $G|X_i$ meets both $A_i$ and $B_i$ ;
if $|A_i| = |B_i| = 1$ and $G|X_i$ is a path between them, that path has odd length $\ge 3$ .

The development needs further objects, each defined on its page: saturating edge sets and major vertices (pp. 77, 81), overshadowed appearances (p. 85), $J$ -enlargements (p. 75), and $J$ -strip systems with their rungs (p. 98).

Formalization targets

Goal (5.1, p. 72)

Let $G$ be Berge and let $H$ be a bipartite subdivision of $K_4$ such that $L(H)$ is nondegenerate and is an induced subgraph of $G$ . Then

G \text{ is a line graph} \;\lor\; G \text{ admits a proper 2-join} \;\lor\; G \text{ admits a balanced skew partition}.

Milestones

5.7 (pp. 77–78): a classification of edge sets $X$ of a bipartite cyclically 3-connected $H$ with no even track of length $\ge 4$ whose end-edges are the only edges in $X$ .
6.1 (pp. 85–86): the common neighbours of an anticonnected set of major vertices saturate $L(H)$ , apart from listed small exceptions.
7.1 (p. 92): three internally disjoint tracks through prescribed edges in a 3-connected graph.
7.5 (p. 94): an overshadowed appearance gives a $J$ -enlargement with a nondegenerate appearance, or a balanced skew partition.
8.1 (p. 99): all $uv$ -rungs of a strip system have the same parity.
8.2 (p. 99): a rung of length $0$ next to one of positive length gives an overshadowed appearance.
5.4 = 8.6 (pp. 76, 105): the general theorem. If no $J$ -enlargement has a nondegenerate appearance in $G$ , then for an appearance $L(H_0)$ of $J$ (with a side condition in the degenerate case), either $G = L(H_0)$ , or $H_0 \neq K_{3,3}$ and $G$ admits a proper 2-join, or $G$ admits a balanced skew partition.

The proposal also contains 5.2 (p. 73, step 1.8.2: Berge graphs containing $L(K_{3,3})$ ) and 5.3 (p. 74) as theorems without milestones.

Significance

5.1 is the line-graph step of the decomposition theorem. It turns "contains a substantial line graph" into "is a line graph or decomposes". The later steps of the proof start from the complementary case, where no such appearance exists (degenerate appearances in §9, prisms in §§10–13). The strip-system technique of §8 can be reused: it assembles all alternative rungs of a line-graph appearance and analyses how the rest of the graph attaches to it.

The strong perfect graph theorem is proved, but to our knowledge no proof assistant has a machine-checked proof of it. This mission formalizes one of its twelve structural steps. Several results of the same paper that the proof of 5.4 uses are posed in other missions of this series and are not posed here:

the Roussel–Rubio lemma 2.1, and 2.2–2.4, 2.6, 2.7, 4.1–4.3 and 4.5 from §§2–4, including the "loose implies balanced" lemma 4.2 (mission II);
the prism lemmas 7.3 and 7.4 (mission V).

The statements 5.5, 5.6, 5.8, 8.3, 8.4 and 8.5 are also used in the proof. They are open to solvers as further lemmas.

Difficulty

Knowing that $G$ contains some appearance of $K_4$ is not enough to make $G$ a line graph or to decompose it. Vertices outside the appearance can attach to it in many ways. Each such pattern has to be shown to be impossible in a Berge graph, or to yield a larger appearance of a bigger graph $J'$ , or to yield a decomposition. The first idea, analysing one outside vertex at a time, fails for two reasons. Connected sets of "minor" vertices can attach non-locally even when each vertex alone attaches locally (5.8). And anticonnected sets of "major" vertices are what produce the skew partitions (6.1). The small cases make things harder: $L(K_{3,3})$ , $L(K_{3,3}\setminus e)$ and degenerate subdivisions of $K_4$ are basic in several ways at once, so the theorem fails for them without the nondegeneracy hypothesis.

Formalization scope

Graphs are SimpleGraph V on a Fintype. $\overline{G}$ is Gᶜ. $L(H)$ is Mathlib's H.lineGraph on H.edgeSet. " $L(H)$ is an induced subgraph of $G$ " is an induced embedding H.lineGraph ↪g G, and " $G = L(H_0)$ " says that this embedding is surjective. Paths and holes are vertex lists with the induced-adjacency condition. Tracks are vertex lists with consecutive vertices adjacent; their adjacency is not induced. Subdivisions carry an injection of $V(J)$ and one track per edge of $J$ . These tracks are internally disjoint, avoid $V(J)$ internally, and cover every vertex and every edge of $H$ . "3-connected" includes the paper's convention of more than three vertices. " $J = K_4$ ", " $H = K_{3,3}$ " mean isomorphism. Existentially quantified graphs ( $H$ in an appearance, the enlargement $J'$ , the graph of which $G$ is a line graph) live on Fin n.

The standing assumptions are those of each statement: $G$ is Berge and $J$ is 3-connected. In 7.1 the two edges $e, f$ are taken distinct, as the conclusion requires. "Up to symmetry" in 6.1 becomes an existential choice of the labelling of the 4-cycle and of the order of $y, y'$ .

The formalization would be trivial if paths were allowed to be non-induced, if the complement bars in 5.4 and 6.1 were dropped, or if a "subdivision" could share internal track vertices or carry extra vertices or edges. The definitions rule out all three. A sorry-free check shows that $K_4$ is a subdivision of itself and is not bipartite.

Reusable infrastructure: tracks, branches, subdivisions, 3-connectivity, appearances and strip systems. Contributions are welcome on the graph-theoretic lemmas 5.3 and 7.1, which do not need Berge graphs, and on the Berge-specific milestones in the order listed.

Selected references

M. Chudnovsky, N. Robertson, P. Seymour, R. Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. https://doi.org/10.4007/annals.2006.164.51
C. Berge, Färbung von Graphen, deren sämtliche bzw. deren ungerade Kreise starr sind, Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe 10 (1961), 114.
V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975), 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
G. Cornuéjols, W. H. Cunningham, Compositions for perfect graphs, Discrete Math. 55 (1985), 245–254. https://doi.org/10.1016/0012-365X(85)90051-7
V. Chvátal, Star-cutsets and perfect graphs, J. Combin. Theory Ser. B 39 (1985), 189–199. https://doi.org/10.1016/0095-8956(85)90049-8

21 thms2 active usersReviewed

Group Theory Number Theory·Captain: Lucas

The Mathieu group M23 is a Galois group over QResearch Paper

Motivation

The inverse Galois problem asks whether every finite group $G$ occurs as the Galois group of a finite Galois extension of $\mathbb{Q}$ . For finite simple groups, a large part of the problem was settled by the rigidity method (Shih, Fried, Belyi, Matzat, Thompson) and its refinements such as the braid-group method. Between 1984 and 1989 this machinery realized 25 of the 26 sporadic simple groups as Galois groups over $\mathbb{Q}$ , in fact as Galois groups of regular extensions of $\mathbb{Q}(t)$ . The Mathieu group $M_{23}$ was the single exception.

Timeline.

1985–1987: Hoyden-Siedersleben and Häfner obtained regular $M_{23}$ -extensions of $k(t)$ for $k=\mathbb{Q}(\sqrt{-23})$ and $k=\mathbb{Q}(\sqrt{-7})$ , by passing through $M_{24}$ .
1996: Granboulan constructed a regular $M_{23}$ -extension of $k(t)$ for every field $k$ over which a certain conic has a point; that conic has no rational point.
2013: Elkies computed the four complex polynomials $P$ of degree 23 with $\mathrm{Gal}(P(x)-t/\mathbb{C}(t))\cong M_{23}$ ; each is defined over a quartic number field.
2026: Huang, Jackson, Lee, Poonen, Pries and Zhang (arXiv:2608.08538) produced an explicit regular $M_{23}$ -extension of $\mathbb{Q}(t)$ and explicit degree-23 polynomials over $\mathbb{Q}$ with Galois group $M_{23}$ , completing the program for the sporadic groups.

Setting

$S_{23}$ denotes the group of permutations of the 23 points $\{1,\dots,23\}$ , acting on the left, so $(\sigma\tau)(x)=\sigma(\tau(x))$ . The paper fixes three explicit permutations

g_1=(1,11)(2,23)(3,8)(4,16)(5,21)(7,20)(15,19)(18,22),

g_2=(1,2,11,10,16,9,6,3,23,19,20,14,21,17,4,8,22,5,18,15,13,7,12),

g_3=(1,2,3,4,10,11,12,7,19,18,8,6,9,16,17,21,22,5,14,20,13,15,23),

and the Mathieu group $M_{23}$ is the subgroup of $S_{23}$ generated by $g_1$ and $g_2$ . A $G$ -extension of a field $k$ is a Galois extension $L/k$ together with an isomorphism $\mathrm{Gal}(L/k)\cong G$ . A finite extension $L$ of $\mathbb{Q}(t)$ is regular if it contains no nontrivial algebraic extension of $\mathbb{Q}$ .

For a triple of conjugacy classes $(C_1,C_2,C_3)$ of $M_{23}$ , the set $\Sigma_c$ consists of triples $(h_1,h_2,h_3)\in C_1\times C_2\times C_3$ with $h_1h_2h_3=1$ that generate $M_{23}$ , and the Nielsen class $\mathrm{Ni}_c$ is the set of orbits of $\Sigma_c$ under simultaneous conjugation by $M_{23}$ . The paper works with the classes $C_1=2$ , $C_2=23A$ , $C_3=23B$ , represented by $g_1,g_2,g_3$ .

Formalization targets

Goal (Theorem 1.1)

\exists\ K/\mathbb{Q}\ \text{finite Galois with}\ \mathrm{Gal}(K/\mathbb{Q})\cong M_{23}.

Stronger forms

Theorem 1.3: there is a finite Galois extension $L/\mathbb{Q}(t)$ , regular over $\mathbb{Q}$ , with $\mathrm{Gal}(L/\mathbb{Q}(t))\cong M_{23}$ .
Examples 1.2 and 3.7: two explicit monic degree-23 polynomials in $\mathbb{Z}[x]$ whose splitting fields are $M_{23}$ -extensions of $\mathbb{Q}$ , unramified outside $\{2,3,23\}$ and $\{2,7,23\}$ respectively.

Supporting milestones

Facts about $M_{23}$ stated in §3 (order $10{,}200{,}960$ , simplicity, 4-transitivity, 17 conjugacy classes), the membership $(g_1,g_2,g_3)\in\Sigma_c$ , the count $|\mathrm{Ni}_c|=7$ , the Riemann–Hurwitz count of Lemma 3.1, the hyperbolic triangle of Lemma 3.2, and the group-theoretic step of Corollary 3.6 ( $M_{23}$ is not normal in any strictly larger subgroup of $S_{23}$ ).

Significance

Theorem 1.1 removes the last sporadic exception: combined with earlier work, every sporadic simple group is the Galois group of a regular extension of $\mathbb{Q}(t)$ (Corollary 1.4), and hence occurs as a Galois group over every number field, in infinitely many mutually independent ways.

The paper's proof is computer-assisted: Belyi maps were computed numerically and the final claims were certified in Magma and PARI/GP. No machine-checked proof in a proof assistant is known. A formal proof of the explicit-polynomial statements (Examples 1.2 and 3.7) would give an independent, kernel-checked certificate of Theorem 1.1. The group-theoretic milestones (order, simplicity, transitivity, class counts, the Nielsen count) are reusable for any later work on $M_{23}$ or the other Mathieu groups.

Difficulty

The rigidity method fails for $M_{23}$ : for every $G_{\mathbb{Q}}$ -stable triple of conjugacy classes the Nielsen class has size different from $1$ , so no rational point of a Hurwitz space is forced. The smallest positive size, $|\mathrm{Ni}_c|=7$ for $\{2,23A,23B\}$ , leaves seven covers, and the fact that one of them has field of moduli $\mathbb{Q}$ was found by explicit computation, with no conceptual explanation. Certifying that a particular degree-23 polynomial has Galois group exactly $M_{23}$ requires both a lower bound (the group contains $M_{23}$ , for instance via cycle types and the classification of transitive groups of degree 23) and an upper bound (the group is contained in a conjugate of $M_{23}$ , for instance via resolvents or reduction modulo primes). Neither bound is a finite check inside current Mathlib.

Formalization scope

$S_{23}$ is Equiv.Perm (Fin 23). The paper's point $k$ corresponds to k - 1 : Fin 23, and permutations compose as functions, which matches the paper's left-action convention. $M_{23}$ is defined as Subgroup.closure {g₁, g₂}, so it is not described up to isomorphism. Galois groups are groups of field automorphisms, K ≃ₐ[ℚ] K, and a $G$ -extension is recorded as a group isomorphism with $M_{23}$ . $\mathbb{Q}(t)$ is RatFunc ℚ. "Unramified outside $S$ " for a number field is encoded as "every prime dividing the absolute discriminant lies in $S$ ", which is equivalent by Dedekind's discriminant theorem. The Nielsen class is the set of orbits of $\Sigma_c$ under simultaneous conjugation. Hyperbolic angles in the Poincaré disk are defined through the hyperbolic law of cosines.

The geometric statements Lemma 3.3 and Proposition 3.5 concern the numerically computed curve $X_{\mathbb{C}}$ and the polynomial $F(T,V)$ , which the paper does not print, so they are not milestones. Lemma 3.1 enters only through its Riemann–Hurwitz count.

Contributions are welcome on decidable certificates for permutation-group facts in Lean, on Galois-group certification for explicit polynomials, and on Hilbert irreducibility.

Selected references

X. Huang, B. Jackson, K.-H. Lee, B. Poonen, R. Pries, S. Zhang, The Mathieu group $M_{23}$ is a Galois group over $\mathbb{Q}$ , 2026. https://arxiv.org/abs/2608.08538
G. Malle, B. H. Matzat, Inverse Galois Theory, 2nd ed., Springer, 2018.
J.-P. Serre, Topics in Galois Theory, Jones and Bartlett, 1992.
N. D. Elkies, The complex polynomials $P(x)$ with $\mathrm{Gal}(P(x)-t)\cong M_{23}$ , ANTS X, Open Book Series 1, 2013.
M. D. Fried, H. Völklein, The inverse Galois problem and rational points on moduli spaces, Math. Ann. 290 (1991), 771–800.

18 thms2 active usersReviewed

Machine Learning Optimization Probability+1·Captain: mikedeng1

Variance-based Regularization with Convex Objectives II: A Covering-Number Certificate and Oracle Inequality for the Robust MinimizerResearch Paper

Motivation

Empirical risk minimization (ERM) chooses, from a class $\mathcal F$ of loss functions, the one with the smallest average loss on a sample $X_1,\dots,X_n$ . Its standard guarantees bound the excess population risk by a term of order $1/\sqrt n$ , whatever the variance of the losses. When good functions in $\mathcal F$ have small variance, a better trade-off is available in principle: minimize the empirical risk plus a standard-deviation penalty $\sqrt{2\rho\,\mathrm{Var}_{\widehat P_n}(f)/n}$ . Maurer and Pontil (COLT 2009) showed that this sample variance penalization enjoys faster rates, but the penalized objective is non-convex even for convex losses, so it cannot be minimized efficiently in general.

Duchi and Namkoong (arXiv:1610.02581v3, 2017; NIPS 2017) replace the variance penalty by a distributionally robust objective: the worst-case average loss over all reweightings of the sample within a $\chi^2$ -divergence ball of radius $\rho/n$ . This objective is convex whenever the loss is convex, and it equals the empirical risk plus the standard-deviation penalty up to an error of order $1/n$ . Theorem 3 of the paper turns this into a guarantee for the minimizer of the robust objective, using covering numbers of the class. This mission formalizes Theorem 3 and the lemmas its proof rests on.

Setting

Let $\mathcal X$ be a measurable space, $P$ a probability measure on it, and $X_1,\dots,X_n$ ( $n\ge1$ ) an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$ . Let $\mathcal F$ be a nonempty class of measurable functions $f:\mathcal X\to[M_0,M_1]$ , and set $M = M_1-M_0$ . Write $\mathbb E[f]=\int f\,dP$ , $\mathrm{Var}(f)$ for the variance of $f(X)$ , and

\mathbb E_{\widehat P_n}[f] = \frac1n\sum_{i=1}^n f(X_i),\qquad \mathrm{Var}_{\widehat P_n}(f) = \frac1n\sum_{i=1}^n f(X_i)^2 - \big(\mathbb E_{\widehat P_n}[f]\big)^2 .

For $\rho\ge0$ , the $\chi^2$ ball $\mathcal P_n$ is the set of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$ , $\sum_i p_i = 1$ and $\frac12\sum_i (np_i-1)^2\le\rho$ : the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$ . The robust risk of $f$ is

R_n(f) = \sup_{P:\,D_\phi(P\|\widehat P_n)\le \rho/n}\mathbb E_P[f(X)] = \max_{p\in\mathcal P_n}\sum_{i=1}^n p_i f(X_i),

and a robust minimizer is any $\widehat f\in\operatorname{argmin}_{f\in\mathcal F} R_n(f)$ .

Complexity is measured by empirical $\ell_\infty$ covering numbers. For $V\subset\mathbb R^m$ , $N(V,\epsilon,\|\cdot\|_\infty)$ is the least number of points $v_1,\dots,v_N\in V$ such that every $v\in V$ lies within sup-distance $\epsilon$ of some $v_i$ . For $x\in\mathcal X^m$ let $\mathcal F(x)=\{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}$ , and

N_\infty(\mathcal F,\epsilon,m) = \sup_{x\in\mathcal X^m} N\big(\mathcal F(x),\epsilon,\|\cdot\|_\infty\big)\in\mathbb N\cup\{\infty\}.

Formalization targets

Goal: the oracle inequality (16)

Let $n\ge 8M^2/t$ , $t\ge\log 12$ , $\epsilon>0$ and $\rho\ge 9t$ . With probability at least $1-2(3N_\infty(\mathcal F,\epsilon,2n)+1)e^{-t}$ , every robust minimizer $\widehat f$ satisfies

\mathbb E[\widehat f(X)] \le \inf_{f\in\mathcal F}\left\{\mathbb E[f] + 2\sqrt{\frac{2\rho}{n}\mathrm{Var}(f)}\right\} + \frac{19M\rho}{3n} + \left(2+4\sqrt{\frac{2t}{n}}\right)\epsilon .

The certificate (15)

Under the same hypotheses and with the same probability, simultaneously for all $f\in\mathcal F$ ,

\mathbb E[f(X)] \le R_n(f) + \frac{11}{3}\frac{M\rho}{n} + \left(2+4\sqrt{\frac{2t}{n}}\right)\epsilon .

Supporting results (milestones)

Theorem 1, inequality (10): for every vector $z\in[M_0,M_1]^n$ , the robust mean minus the sample mean lies between $\big(\sqrt{2\rho s_n^2/n}-2M\rho/n\big)_+$ and $\sqrt{2\rho s_n^2/n}$ .
Lemma C.1: a uniform empirical Bernstein bound over $\mathcal F$ with probability $1-6N_\infty(\mathcal F,\epsilon,2n)e^{-t}$ .
Lemma A.1, first bound: $\mathbb P(s_n\ge\sqrt{\mathbb E s_n^2}+t)\le\exp(-nt^2/(2M^2))$ .
Bernstein's inequality for one fixed $f$ , as displayed in the proof (p. 38).
The certificate (15).

Significance

Inequality (15) says the robust risk is a uniform upper confidence bound on the population risk, with an $O(1/n)$ slack instead of the $O(1/\sqrt n)$ slack of the empirical risk. Inequality (16) says the robust minimizer competes with the best variance-penalized population risk in the class. When some $f\in\mathcal F$ has small risk and small variance, the excess risk of $\widehat f$ is of order $1/n$ up to the covering term, a rate ERM does not achieve in general (§3.3 of the paper gives an example). For a parametric class with $N_\infty(\mathcal F,\epsilon,2n)$ polynomial in $1/\epsilon$ , choosing $\epsilon=M/n$ gives Corollaries 3.1 and 3.2 of the paper.

The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission's output is a formal proof of Theorem 3 and its ingredients: a deterministic analysis of the $\chi^2$ -constrained linear program (Theorem 1 (10)), a covering-number empirical Bernstein inequality (Lemma C.1, from Maurer and Pontil), concentration of the sample standard deviation (Lemma A.1), and the scalar Bernstein inequality in the form used. Each of these is reusable outside distributionally robust optimization.

Difficulty

The deterministic part, (10), is a short analysis of a quadratically constrained linear program. The main obstacle is Lemma C.1. A union bound over a cover of $\mathcal F$ fails directly: the cover depends on the sample, and a population-level cover of $\mathcal F$ need not be finite. The standard route goes through a ghost sample of size $n$ (hence covering at $2n$ points), a symmetrization that must preserve the sample variance rather than only the mean, and a concentration bound for the sample variance itself. Lemma A.1 needs concentration of $s_n$ , a non-linear and non-smooth function of the sample, at the sub-Gaussian rate $M/\sqrt n$ . Finally, the oracle inequality (16) holds for an infimum over the whole class, while the concentration step for the comparison function is only proved for one fixed $f$ at a time.

Formalization scope

The sample is the coordinate process of the product measure $P^{\otimes n}$ on $\mathcal X^n$ (Measure.pi). Each probability statement bounds the probability of the bad event, the set of samples where the inequality fails for some $f$ (or some minimizer). This set need not be measurable, and its measure is then the outer measure, as is standard in empirical-process theory. Probability bounds are computed in $[0,\infty]$ , and the covering number is valued in $\mathbb N\cup\{\infty\}$ , so an infinite covering number makes the bound trivial rather than collapsing to zero. Covering numbers are internal (centres in $\mathcal F(x)$ ) and use closed sup-norm balls, as on p. 9; this is Mathlib's Metric.coveringNumber. The empirical variance is normalized by $1/n$ . The $\chi^2$ ball is encoded as weight vectors on the sample points; with tied sample values this gives the same supremum as the paper's distributions on the sample. Statement (16) is formalized for every minimizer of the robust risk, and the event is empty if no minimizer exists. The infimum ranges over the nonempty class $\mathcal F$ , on which every term is at least $M_0$ . Population moments are those of bounded measurable functions, hence finite.

Deviations from the printed text:

Lemma A.1 is stated only for its first (upper-tail) bound. The paper derives the second bound from Lemma A.4, which is false as printed; the second bound is not stated. $M>0$ is assumed because $M^2$ is a denominator.
Lemma C.1 is the paper's restatement of Maurer and Pontil's Theorem 6, with a general radius $\epsilon$ . It is formalized as printed, with the implicit assumption $\epsilon>0$ made explicit.
$n\ge1$ is assumed throughout. The hypothesis $n\ge 8M^2/t$ is kept as printed.

A trivializing formalization is ruled out: the bound is not taken over all functions, a probability bound is not formed from the real part of an infinite covering number, and the minimizer is not a hypothesis that can fail to exist for the given sample.

Needed infrastructure: product-measure concentration (Bernstein, and a bounded-difference or convex-Lipschitz inequality for $s_n$ ), symmetrization with a ghost sample, and finite union bounds over a cover. Contributions are welcome on any milestone, in particular a general covering-number empirical Bernstein inequality, which is reusable on its own.

Selected references

J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017 (NIPS 2017; JMLR 20, 2019). https://arxiv.org/abs/1610.02581
A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2

11 thms2 active usersReviewed

Analysis Convex Optimization Operations Research+1·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems II: The Łojasiewicz Inequality for Convex Subanalytic Functions on Bounded SetsResearch Paper

Motivation

The Łojasiewicz inequality states that near a critical point $a$ of a real-analytic function $f$ there are $\theta\in[0,1)$ and $C$ with $|f(x)-f(a)|^{\theta}\le C\,\|\nabla f(x)\|$ . Łojasiewicz used it in the 1960s to prove that every bounded trajectory of the gradient flow $\dot x=-\nabla f(x)$ has finite length and converges to a single critical point, a conclusion that fails for general $C^\infty$ functions. The inequality has since become the standard tool for convergence analysis of descent methods on nonconvex problems.

Optimization problems are, however, rarely smooth: constraints enter through indicator functions, and objectives contain norms, maxima and penalties. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the inequality to nonsmooth subanalytic functions, replacing $\|\nabla f\|$ by a slope built from the limiting subdifferential. Their Section 3.1 treats functions continuous on a closed domain; Section 3.2, the subject of this mission, treats lower semicontinuous convex functions, which may jump to $+\infty$ and whose domain need not be closed. The Kurdyka–Łojasiewicz framework built on this paper (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014) underlies the convergence theory of proximal and splitting algorithms used throughout operations research.

Setting

Work in $\mathbb R^n$ with the Euclidean norm, and let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$ .

A set $A\subseteq\mathbb R^n$ is semianalytic if near every point it is a finite union of finite intersections of sets $\{f_{ij}=0,\ g_{ij}>0\}$ with $f_{ij},g_{ij}$ real-analytic. It is subanalytic if near every point it is the projection of a bounded semianalytic subset of $\mathbb R^n\times\mathbb R^m$ . A function is subanalytic when its graph $\{(x,\lambda): f(x)=\lambda\}$ is. Semialgebraic functions (norms, polynomials, indicators of polyhedra) are subanalytic.

The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\ne x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge 0$ , for $x\in\operatorname{dom} f$ , and is empty otherwise. The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $(x_k,f(x_k))\to(x,f(x))$ . The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|:x^*\in\partial f(x)\}$ , equal to $+\infty$ when $\partial f(x)=\emptyset$ , and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points. For lower semicontinuous convex $f$ , $\partial f$ is the subdifferential of convex analysis and $\operatorname{crit} f$ is the set of minimizers. Write $\min f$ for the minimum value and $d_S(x)$ for the distance from $x$ to $S=\operatorname{crit} f$ . The epigraphical sum $g(x)=\inf_u\{f(u)+\tfrac12\|x-u\|^2\}$ is the Moreau envelope of $f$ .

Ratios follow the paper's conventions $0^0=1$ and $\infty/\infty=0/0=0$ .

Formalization targets

Goal: Theorem 3.3

Let $f$ be lower semicontinuous, convex and subanalytic with $\operatorname{crit} f\ne\emptyset$ . For every bounded set $K$ there is $\theta\in[0,1)$ such that

\frac{|f-\min f|^{\theta}}{m_f}\quad\text{is bounded on }K.

The exponent may depend on $K$ ; neither $\theta$ nor the bound is fixed.

Milestones

Eq. (5): $\partial f=\hat\partial f=$ the convex subdifferential, for lsc convex $f$ .
Section 3.2: $\operatorname{crit} f$ is closed, convex and equal to the set of minimizers.
Inequality (16): $|f(x)-\min f|\le\|x^*\|\,d_S(x)$ for all $x^*\in\partial f(x)$ .
Remark 3.6: $|f-\min f|/m_f$ is bounded around every critical point, without subanalyticity.
Proposition 2.9: the epigraphical sum $g$ is $C^1$ and subanalytic when $\inf f\in\mathbb R$ .
Properties (a)–(c): $g$ is finite and $C^1$ , $g\le f$ , $\operatorname{crit} g=\operatorname{crit} f$ , $\inf g=\inf f$ .
Proposition 2.13(ii): $\operatorname{crit} f$ is subanalytic for subanalytic $f$ that is relatively bounded on its domain.
Section 2.1: the distance to a subanalytic set is subanalytic.
The Łojasiewicz factorization lemma on compact sets (recalled from Bierstone–Milman).
Inequality (15): $d_S(x)\le c^{-1/r}|f(x)-\min f|^{1/r}$ on $K$ , with $r>1$ , $c>0$ .
Remark 3.5: the growth condition $|f-\min f|\ge c\,d_S^{\,r}$ on a compact $K$ alone yields a Łojasiewicz inequality at critical points interior to $K$ .

Significance

Theorem 3.3 gives, for convex subanalytic functions, a Łojasiewicz inequality that is uniform on bounded sets rather than local at one critical point, and it needs neither continuity of $f$ on its domain nor a closed domain. Remark 3.4 of the paper exhibits a convex function covered by Theorem 3.3 but not by the continuous-case Theorem 3.1. Through inequality (20) of Section 4, it yields finite length and convergence rates for the subgradient flow $\dot x\in-\partial f(x)$ of such functions. The intermediate inequality (15) is a Hölderian error bound, $d_S\le C|f-\min f|^{1/r}$ , of the kind that drives linear and sublinear rate analyses of first-order methods.

The result is proved in the paper; no machine-checked version of it, or of the nonsmooth Łojasiewicz inequality in any form, is known. Formalizing it would add to the library: subanalytic sets and functions, the limiting subdifferential of convex functions and its agreement with the classical one, the Moreau envelope with its critical points and infimum, and the passage from a growth condition to a Łojasiewicz inequality. Remarks 3.5 and 3.6 isolate parts that need no subanalytic geometry at all.

Difficulty

The convex-analysis steps (inequality (16), properties of the Moreau envelope) are classical. The obstacle is subanalytic geometry. The natural first idea, applying the Łojasiewicz factorization lemma directly to $f-\min f$ and $d_S$ , fails: $f$ is neither continuous nor finite, and its domain need not be subanalytic even when $f$ is convex and subanalytic (Example 2.5 of the paper). The milestones route through the Moreau envelope, which is continuous and finite, but subanalyticity is not preserved by infima over unbounded sets, so the subanalyticity of the envelope (Proposition 2.9) needs a localization argument. The subanalyticity of $\operatorname{crit} g$ and of $d_S$ rests on the stability theory of subanalytic sets (Gabrielov's complement theorem, the projection theorem for globally subanalytic sets), none of which exists in Mathlib.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "lower semicontinuous, convex, somewhere finite and never $-\infty$ " is the published definition MoreauProx.Characterization.GammaZero, whose convexity is convexity of the epigraph. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the convex subdifferential subgrad appears only in Eq. (5), which proves the agreement and is never assumed. Semianalytic and subanalytic sets are defined from scratch for any finite-dimensional real normed space, so that one definition serves $\mathbb R^n$ and its products; global subanalyticity is not defined. $\min f$ is written $\inf_y f(y)$ in EReal and converted to a real number only where it is finite. The bounded ratio (14) is encoded as " $|f(x)-\min f|^{\theta}\le C\|x^*\|$ for every $x\in K$ and every $x^*\in\partial f(x)$ ", with real powers (Real.rpow, $0^0=1$ ). Inequalities (15) and (17) are imposed only where $f(x)<+\infty$ , since Lean sends $+\infty$ to $0$ under toReal.

Trivializing encodings are ruled out: the goal is stated with the limiting subdifferential rather than an assumed convex subdifferential, the slope is never computed in ℝ≥0∞ where $0\cdot\infty=0$ would make the ratio vacuous, and $\theta$ remains existential in $[0,1)$ with the quantifier order "for every $K$ there is $\theta$ ", so that $\theta=0$ is excluded at critical points in $K$ by $0^0=1$ .

A complete development needs a working theory of subanalytic sets (stability under finite unions, complements, closure, projections of bounded sets, the factorization lemma), the Moreau envelope of a convex function on $\mathbb R^n$ and its $C^1$ property, and the convex-analytic description of the limiting subdifferential. The subanalytic-geometry layer and the Moreau-envelope facts are reusable well beyond this mission; contributions to either, or proofs of the convex-only milestones (Eq. (5), (16), Remarks 3.5–3.6), are welcome independently.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
E. Bierstone, P. D. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, Les Équations aux Dérivées Partielles, Éditions du CNRS, Paris, 1963, 87–89.
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. https://doi.org/10.1007/s10107-011-0484-9
J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146 (2014) 459–494. https://doi.org/10.1007/s10107-013-0701-9

18 thms2 active usersReviewed

Linear Optimization Operations Research Optimization+2·Captain: mikedeng1

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 2: The Two-Phase Shadow-Vertex Simplex Method Has Polynomial Smoothed ComplexityResearch Paper

Motivation

The simplex method solves linear programs by moving between vertices of a feasible polyhedron. Its worst-case number of moves can grow exponentially, yet it often performs well on ordinary inputs. Worst-case examples alone therefore give an incomplete account of the method’s behavior. Spielman and Teng introduced smoothed analysis to measure expected performance after small random perturbations of an arbitrary input. Their result for a two-phase shadow-vertex simplex method gives a polynomial bound in the input dimensions and inverse perturbation scale. The pinned preprint is the source for every theorem number and constant in this mission.

The paper separates a geometric result about the expected size of a polytope’s shadow (Theorem 4.0.1) from the algorithmic result here (Theorem 5.0.1). That separation matters: a plane chosen before perturbation and a plane chosen by a running algorithm have different distributions. This mission addresses the latter. It complements the standard-form simplex theorems already formalized in the Introduction to Linear Optimization series and the worst-case Klee–Minty result in the Smale’s Ninth Problem mission; those results concern different algorithms or input models and are context rather than imported statements.

Setting

A linear program is specified by vectors $a_1,\ldots,a_n\in\mathbb R^d$ , right-hand sides $y_1,\ldots,y_n\in\mathbb R$ , and an objective vector $z\in\mathbb R^d$ :

\max_x\langle z,x\rangle\quad\text{subject to}\quad \langle a_i,x\rangle\le y_i\qquad(1\le i\le n).

The paper’s two-phase shadow-vertex method first draws a collection $\mathcal I$ of $d$ -element subsets of $[n]$ and chooses one whose constraint matrix $A_I$ has the largest smallest singular value. It sets a power-of-two scale $M$ from the input norm and a power-of-two scale $\kappa$ from that singular value. These determine positive relaxed right-hand sides $y'_i$ : $M$ for $i\in I$ and $\sqrt d M^2/(4\kappa)$ otherwise. A coefficient vector $\alpha$ is chosen uniformly from $A_{1/d^2}=\{\alpha:\sum_{i\in I}\alpha_i=1,\ \alpha_i\ge1/d^2\}$ . The first phase solves the relaxed program LP′ from the objective $A_I\alpha$ .

The second phase uses a lifted program LP⁺ in $\mathbb R^{d+1}$ . For each original constraint it forms $a_i^+=((y'_i-y_i)/2,a_i)$ and $y_i^+=(y'_i+y_i)/2$ , together with two artificial constraints at first coordinates $1$ and $-1$ . LP⁺ connects LP′ to the original program and makes infeasibility detectable. Its shadow is taken in the plane of $(0,z)$ and $z^+=(1,0,\ldots,0)$ .

For positive right-hand sides, an optimal polar simplex is a $d$ -subset of constraints whose scaled vectors $a_i/y_i$ form a facet of $\operatorname{ConvHull}(0,a_1/y_1,\ldots,a_n/y_n)$ and whose unscaled cone contains an objective $q$ . The shadow for objectives $t,z$ is the union of these simplices over all $q$ in $\operatorname{Span}(t,z)$ . Its size bounds the number of polar pivots. In Section 5 the paper writes $S'_z$ for the first-phase shadow size and $S_z^+$ for the second-phase shadow size without the two artificial pivots.

The input is perturbed by independent Gaussians: each coordinate of $a_i$ and each $y_i$ has its prescribed center and common standard deviation $\sigma R$ , where $R=\max_i\|(\bar y_i,\bar a_i)\|_2$ . The algorithm has separate random choices of $\mathcal I$ and $\alpha$ .

Formalization targets

The immediate targets bound the two phases: Lemma 5.2.1 gives an explicit expectation bound for $S'_z$ and Lemma 5.3.1 gives one for $S_z^+$ . Lemma 5.1.1 and its corollaries control the chance that the chosen basis has a very small singular value. Corollary 4.3.3 extends the geometric shadow bound to positive, unequal right-hand sides and general Gaussian covariance. These are the mission’s milestone targets.

The goal is the shape of Theorem 5.0.1. With $C(A,y,z)=\mathbb E_{\mathcal I,\alpha}(S'_z+S_z^++2)$ , there are a single polynomial $\mathcal P$ and a positive constant $\sigma_0$ such that, for all $n>d\ge3$ and all centers and objectives,

\mathbb E_{A,y}C(A,y,z)\le \min\left\{\mathcal P\left(d,n,\frac1{\min(\sigma,\sigma_0)}\right), \binom nd+\binom n{d+1}+2\right\}.

The polynomial is uniform over the dimensions and inputs; its coefficients are not prescribed. The bound on $C$ implies the corresponding result for the actual pivot count through the paper’s step-to-shadow comparison. The goal is stated with a positive center scale $R$ , the case in which the paper’s Gaussian rescaling applies.

Significance

The theorem places the number of pivots of a complete simplex method under one explicit perturbation model, including the work needed to find a starting feasible basis and handle an arbitrary right-hand side. The trivial binomial bound is retained because it controls rare events in the proof and is part of the stated result. The polynomial bound says that even when the unperturbed LP is adversarial, Gaussian noise of a controlled scale makes the expected shadow-size cost polynomial.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its statement and the listed milestones; the draft Lean declarations are targets with sorry, not completed proofs. The reusable formal infrastructure is the finite polar simplex and shadow construction, product Gaussian input law, smallest-singular-value events for sampled minors, and the uniform truncated-simplex coefficient law. The two shadow-size lemmas also require explicit handling of measurable finite-valued counts and their expectations.

Difficulty

The basic shadow estimate fixes its projection plane before perturbing the constraints. In LP′, the initial objective $A_I\alpha$ uses a basis selected after the perturbation, so the relevant plane depends on the random LP. The fixed-plane theorem cannot be substituted directly. For LP⁺, the normalized lifted vectors $a_i^+/y_i^+$ are nonlinear functions of Gaussian data; they are generally not Gaussian vectors. Thus the same shadow estimate does not apply directly to their law either. A further issue is that a poor sampled basis can make $y'$ very large. These are distinct obstacles, reflected in the milestone groups from Sections 5.1, 5.2, and 5.3.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), constraints are Fin n → EuclideanSpace ℝ (Fin d), and index families are finite sets of Fin n. The paper’s $[n]$ starts at one; Fin n starts at zero. The Gaussian constructor receives variance $\sigma^2$ , not standard deviation $\sigma$ . The $3nd\ln n$ draws are rounded upward and are independent uniform draws with replacement. Equal singular values are resolved by the first sampled set. The uniform law on $A_\delta$ is represented by normalized independent exponential weights followed by the affine shift that imposes $\alpha_i\ge\delta$ .

The Lean definition of $C$ is exactly the Section 5 shadow-size upper bound $\mathbb E(S'_z+S_z^++2)$ , computed from the sampled LP data. It is not an arbitrary cost variable. The actual algorithmic step bound needs the paper’s polar algorithm and Lemma 3.3.5. The goal explicitly asks for inner and outer integrability so Lean’s default value for a nonintegrable Bochner integral cannot make the result vacuous. The source’s all-zero center scale is excluded because it gives zero perturbation and defeats the rescaling used in Theorem 5.0.1.

For LP⁺ the vectors live in $\mathbb R^{d+1}$ , so the two LP⁺ milestone bounds use $\mathcal D(n,d+1,\cdot)$ . The preprint prints $d$ in those calls even though the preceding extension theorem would be applied in dimension $d+1$ . Lemma 5.2.1 is written as an inequality: its printed equality is stronger than the bound established on page 71. These corrections are visible in the theorem titles and notes. Contributions that prove the exact statements, establish the measurability and Gaussian law facts, or formalize the step-to-shadow comparison are welcome.

Selected references

Daniel A. Spielman and Shang-Hua Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003, preprint. The PDF used here is the 96-page version with printed and PDF page numbers aligned.

22 thms2 active usersReviewed

Calculus of Variations Control Theory Optimization·Captain: mikedeng1

On the Variational Principle III: Every Terminal-Cost Control Problem Has ε-Optimal Measurable Controls Satisfying the Pontryagin Maximum Principle up to εResearch Paper

Motivation

The Pontryagin maximum principle is the basic first-order necessary condition of optimal control: along an optimal control, the control value at almost every time extremizes a Hamiltonian built from the dynamics and an adjoint vector. The classical statement presupposes that an optimal control exists. For many problems none does: the set of trajectories is not closed, or the cost does not attain its infimum, and the classical principle then says nothing.

Ekeland's 1974 paper On the Variational Principle (DOI 10.1016/0022-247X(74)90025-0) proves a general result about lower semicontinuous functions on complete metric spaces (its Theorem 1.1, now called Ekeland's variational principle) and closes with an application to control theory in §7 (pp. 348–351): for every terminal-cost problem satisfying mild regularity and growth conditions, there are ε-optimal controls that satisfy the maximum principle up to ε, whether or not an optimal control exists. The argument equips the measurable controls with the metric "measure of the set where two controls differ", which has since become a standard device in nonsmooth and approximate optimal control. For the classical theory, Ekeland refers to the treatise of Pallu de la Barrière (Optimal Control Theory, Saunders, 1967).

Setting

Fix $n \ge 0$ , a horizon $T > 0$ , an initial state $x_0 \in \mathbb R^n$ , and a nonempty compact metrizable space $K$ of control values, with its Borel σ-algebra. A control is a measurable map $u : [0, T] \to K$ . The dynamics are a map $f : \mathbb R^n \times K \times [0, T] \to \mathbb R^n$ , and the state obeys

\frac{dx}{dt}(t) = f(x(t), u(t), t) \ \text{ a.e.}, \qquad x(0) = x_0. \qquad (7.1)

A trajectory of $u$ (Lean: IsTrajectory f x₀ T u x) is a function $x$ continuous on $[0, T]$ with $x(t) = x_0 + \int_0^t f(x(s), u(s), s)\,ds$ for all $t \in [0, T]$ . The standing hypotheses are:

(a) $f$ and its state Jacobian $f_x' = (\partial f/\partial x_1, \dots, \partial f/\partial x_n)$ (Lean: fx) are continuous on $\mathbb R^n \times K \times [0, T]$ ;
(b) $\langle x, f(x, u, t)\rangle \le c\,(1 + \|x\|^2)$ for some constant $c$ .

The terminal cost is given by a $C^1$ function $g : \mathbb R^n \to \mathbb R$ , and the problem is to minimize $g(x(T))$ over all controls. The adjoint vector $p$ along a pair $(u, x)$ (Lean: IsAdjoint fx g T u x p) solves the linear equation

\frac{dp}{dt}(t) = -{}^t f_x'(x(t), u(t), t)\, p(t), \qquad p(T) = g'(x(T)),

where ${}^t A$ is the transpose. The control distance (Lean: ctrlDist T u₁ u₂) is

\delta(u_1, u_2) = \operatorname{meas}\{t \in [0, T] \mid u_1(t) \neq u_2(t)\},

and the needle variation $v_\tau$ of a control $u_\varepsilon$ at $t_0$ with value $u_0 \in K$ (Lean: needle T uε u₀ t₀ τ) equals $u_0$ on $[0, T] \cap\, ]t_0 - \tau, t_0[$ and $u_\varepsilon$ elsewhere.

Formalization targets

Goal: Theorem 7.1

For every $\varepsilon > 0$ there is a control $u_\varepsilon$ with trajectory $x_\varepsilon$ and adjoint vector $p_\varepsilon$ such that

g(x_\varepsilon(T)) \le \inf_u g(x(T)) + \varepsilon, \qquad \langle f(x_\varepsilon(t), u_\varepsilon(t), t), p_\varepsilon(t)\rangle \le \min_{w \in K} \langle f(x_\varepsilon(t), w, t), p_\varepsilon(t)\rangle + \varepsilon \ \text{ a.e. on } [0, T].

Milestones

(7.2), a priori bound: every trajectory satisfies $\|x(t)\|^2 \le (\|x_0\|^2 + 2cT)e^{2cT}$ .
Well-posedness (p. 348): every control has exactly one trajectory on $[0, T]$ .
Lemma 7.2: $(\mathcal U, \delta)$ is a complete metric space (on almost-everywhere classes).
Lemma 7.3: $u \mapsto g(x(T))$ is continuous on $(\mathcal U, \delta)$ .
(7.15)–(7.16): a control $u_\varepsilon$ with $F(u_\varepsilon) \le \inf F + \varepsilon^2$ and $F(u) \ge F(u_\varepsilon) - \varepsilon\,\delta(u, u_\varepsilon)$ for all $u$ , where $F(u) = g(x(T))$ .
Lemma 7.4: the right derivative of $\tau \mapsto g(x_\tau(T))$ at $\tau = 0$ , for the needle variations $v_\tau$ , equals $\langle f(x_\varepsilon(t_0), u_0, t_0) - f(x_\varepsilon(t_0), u_\varepsilon(t_0), t_0), p_\varepsilon(t_0)\rangle$ .

Significance

The result. Theorem 7.1 decouples the maximum principle from existence of optimal controls. Any minimizing sequence can be replaced by one consisting of controls that satisfy the necessary condition up to a vanishing error, so approximate extremals are available for numerical schemes and for limiting arguments (relaxation, convergence of extremals) in problems without compactness or convexity of the velocity sets. The same scheme, a complete metric on controls plus Ekeland's principle plus needle variations, underlies later proofs of the maximum principle with state constraints and in nonsmooth settings.

Formalizing it. The theorem has a published proof, which the paper sketches in four pages and partly defers to classical results (local existence for measurable controls, differentiability of trajectories with respect to needle variations). Neither Mathlib nor the platform contains this theorem or a maximum principle for measurable controls with time-dependent dynamics; the nearest platform items assume an exact optimum, a running cost and globally Lipschitz autonomous dynamics. A formalization requires a Carathéodory theory of ODEs in Lean, the complete metric space of controls, and a rigorous version of the classical first-variation computation. Each of these is useful well beyond this paper.

Difficulty

The obvious argument fails at its first step: a minimizing sequence of controls has no convergent subsequence in any useful sense, because measurable controls with values in $K$ are not compact in the metric $\delta$ and their weak limits are relaxed controls, which are not controls. Ekeland's principle avoids compactness, but it needs a complete metric space on which the cost is lower semicontinuous. Completeness of $(\mathcal U, \delta)$ (Lemma 7.2) and continuity of the cost (Lemma 7.3) both require care. Continuity must hold for trajectories driven by merely measurable controls, which converge only in measure. The needle derivative (Lemma 7.4) holds only at times where the trajectory satisfies the state equation in the classical sense, which is almost every time but not every time.

Formalization scope

Controls are functions ℝ → K with Measurable u; only values on $[0, T]$ matter. Trajectories and adjoint vectors are functions ℝ → EuclideanSpace ℝ (Fin n), continuous on $[0, T]$ and solving the integral form of their equation. The paper uses the same form in (7.13). A definition that asks for a derivative at every time would be unsatisfiable for discontinuous controls and would make the goal vacuous; the integral form avoids this.
Hypothesis (a) is stated as joint continuity of f and fx on univ ×ˢ univ ×ˢ Icc 0 T together with HasFDerivAt (fun y => f y u t) (fx x u t) x. Hypothesis (b) is ∃ c, … with the order of arguments $f(x, u, t)$ ; the page prints $f(t, x, u)$ in (b), a slip.
The transpose ${}^t f_x'$ is ContinuousLinearMap.adjoint, and $g'(x)$ is gradient g x.
Infima over controls are never taken as real ⨅; (7.4) and (7.15) are stated as "for every control $u$ with trajectory $x$ ".
(7.5) is printed with " $\times\,\varepsilon$ ". The proof's last line (7.21) gives " $+\,\varepsilon$ ", which is what is stated. The minimum over the compact $K$ is replaced by the equivalent "for every $w \in K$ ", with one null set for all $w$ .
Added hypothesis: [Nonempty K] in the goal and milestone 5. With $K$ empty no control exists and the existential statements would be false.
Lemma 7.2 is stated as the triangle inequality, " $\delta = 0$ iff almost-everywhere equality on $[0, T]$ ", and sequential completeness for measurable controls. Lemma 7.3 is sequential continuity. Lemma 7.4 is a one-sided derivative within $[0, t_0]$ at $0$ , stated for an arbitrary measurable $u_\varepsilon$ .
Theorem 1.1 (Ekeland's principle) is a separate mission of this series and still a draft, so milestone 5 states the instance used here directly.
Out of scope: the uniform bound (7.3) and the remark after Theorem 7.1 that one may take $\varepsilon = 0$ in (7.5) when (7.4) holds with $\varepsilon = 0$ .

Welcome contributions include Carathéodory existence and uniqueness for ODEs with measurable time dependence, Gronwall-type estimates for absolutely continuous functions, the complete metric space of measurable maps under the disagreement measure, and differentiability of flows with respect to initial data.

Selected references

I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974), 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
R. Pallu de la Barrière, Optimal Control Theory, Saunders, Philadelphia, 1967.
L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, New York, 1962.

11 thms2 active usersReviewed

Functional Analysis Operations Research Optimization·Captain: mikedeng1

On the Variational Principle II: Under Linearly Independent Active Constraint Gradients, a Bounded-Below Problem Has ε²-Optimal Feasible Points Satisfying the Lagrange Multiplier Rule up to εResearch Paper

Motivation

The classical Lagrange multiplier rule and its inequality-constrained form, the Karush–Kuhn–Tucker (KKT) conditions, are necessary conditions satisfied at a minimizer of a constrained problem. In finite dimensions, a continuous function bounded below on a closed bounded feasible set attains its minimum, so the rule describes an actual point. In an infinite-dimensional Banach space this fails: closed bounded sets are not compact, minimizing sequences need not converge, and a smooth function bounded below on a smooth constraint set can have no minimizer at all. The multiplier rule then has nothing to describe.

Ekeland's 1974 paper On the Variational Principle (DOI) introduced a principle (its Theorem 1.1) that replaces "a minimizer exists" with "near every almost-minimizer there is a point that strictly minimizes a slightly perturbed function". Section 3 of the paper uses this to prove that, for a problem with finitely many smooth equality and inequality constraints satisfying a linear-independence regularity condition, nearly optimal feasible points satisfy the KKT conditions up to a small error, with no compactness and no existence of a minimizer. This is the first appearance of what is now called an approximate or asymptotic KKT condition, a notion central to the convergence theory of nonlinear programming algorithms.

Setting

Let $V$ be a real Banach space with dual $V^*$ (continuous linear functionals) and dual norm $\|x^*\|_*=\sup_{\|h\|\le1}\langle x^*,h\rangle$ . Let $F:V\to\mathbb R$ be Fréchet-differentiable, with derivative $F'(v)\in V^*$ , and let $G_1,\dots,G_m:V\to\mathbb R$ be $C^1$ (continuously Fréchet-differentiable). Fix $0\le p\le m$ and consider

\inf F(v)\quad\text{subject to}\quad G_i(v)=0\ (1\le i\le p),\qquad G_i(v)\ge0\ (p+1\le i\le m). \tag{3.1}

The feasible set is $\mathcal C=\{v\in V : G_i(v)=0 \text{ for } i\le p,\ G_i(v)\ge0 \text{ for } i>p\}$ (3.2). At $v\in\mathcal C$ the saturated constraints are $I(v)=\{i : G_i(v)=0\}$ (3.3). The regularity assumption (3.4) is: for every $v\in\mathcal C$ , the derivatives $G_i'(v)$ , $i\in I(v)$ , are linearly independent in $V^*$ .

In the Lean development these are EkelandVP.Constraints.feasibleSet p G and EkelandVP.Constraints.IsRegular p G, with constraints indexed by Fin m.

Formalization targets

Goal: Theorem 3.1 (p. 330)

Assume (3.4), $\mathcal C\ne\emptyset$ , and that $F$ is bounded below on $\mathcal C$ (3.5). Then for every $\varepsilon>0$ there are $v_\varepsilon\in\mathcal C$ and $\lambda_1,\dots,\lambda_m\in\mathbb R$ with

F(v_\varepsilon)\le\inf_{\mathcal C}F+\varepsilon^2,\qquad \lambda_i\ge0\ (i>p),\qquad \lambda_i=0 \text{ if } G_i(v_\varepsilon)\ne0,

\Big\|F'(v_\varepsilon)-\sum_{i=1}^m\lambda_iG_i'(v_\varepsilon)\Big\|_*\le\varepsilon.

Milestones, in the order of the paper's proof

(3.8)–(3.12): a feasible $v$ with $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ and $F(w)\ge F(v)-\varepsilon\|w-v\|$ for all $w\in\mathcal C$ (the variational principle applied to $F$ restricted to $\mathcal C$ ; no regularity needed).
(3.16): at a regular feasible point $v$ , every $h$ with $\langle G_i'(v),h\rangle=0$ ( $i\le p$ ) and $\langle G_i'(v),h\rangle\ge0$ ( $i>p$ , $i\in I(v)$ ) is the initial velocity of a $C^1$ curve $u:[0,\tau]\to\mathcal C$ with $u(0)=v$ .
Lemma 3.2: at a point with the property of milestone 1, $\langle F'(v),h\rangle\ge-\varepsilon\|h\|$ for every such $h$ .
Lemma 3.3: an $\varepsilon$ -Farkas–Minkowski lemma in $V^*$ : if $\langle w^*,h\rangle\ge-\varepsilon\|h\|$ whenever $\langle u_i^*,h\rangle=0$ and $\langle v_j^*,h\rangle\ge0$ , then $\|w^*-\sum\lambda_iu_i^*-\sum\mu_jv_j^*\|_*\le\varepsilon$ for some $\lambda_i\in\mathbb R$ and $\mu_j\ge0$ .

An additional item states Corollary 3.4 (p. 333), the one-constraint case: if $G(v)=0\Rightarrow G'(v)\ne0$ , $\{G=0\}\neq\emptyset$ and $F$ is bounded below on $\{G=0\}$ , then for every $\varepsilon>0$ there are $v_\varepsilon$ with $G(v_\varepsilon)=0$ and $\lambda_\varepsilon\in\mathbb R$ with $\|F'(v_\varepsilon)-\lambda_\varepsilon G'(v_\varepsilon)\|_*\le\varepsilon$ .

Significance

The result. Theorem 3.1 is an existence theorem for approximate KKT points that needs neither compactness nor attainment of the infimum. It shows that every bounded-below problem with regular constraints has a sequence of feasible points whose objective values converge to the infimum and along which the KKT residual tends to zero. This is the property that later work calls approximate KKT or asymptotic KKT (AKKT) and uses as a stopping criterion and as a sequential optimality condition for nonlinear programming. Corollary 3.4 is the corresponding nonlinear eigenvalue statement: on a regular level set, $F'$ is approximately proportional to $G'$ at almost-minimizing points.

Formalizing it. The result is classical and proved in the paper; to our knowledge no machine-checked version exists. Mathlib has the Fréchet derivative, the implicit function theorem for strictly differentiable maps, Banach–Alaoglu and the Hahn–Banach separation theorems, but no Ekeland principle in this form, no Lyusternik-type tangent-curve theorem for mixed equality–inequality constraints, and no Farkas lemma in a dual Banach space. Each milestone is a reusable piece of nonlinear optimization theory in Banach spaces.

Difficulty

The obvious argument, "take a minimizer and apply the Lagrange multiplier rule", fails at the first step because no minimizer need exist. The variational principle supplies a point $v_\varepsilon$ that minimizes $F+\varepsilon\|\cdot-v_\varepsilon\|$ on $\mathcal C$ , but that function is not differentiable at $v_\varepsilon$ , so the multiplier rule cannot be applied to it directly either. Two further gaps remain. Linearized feasible directions (those satisfying the derivative conditions on the active constraints) need not be directions along which one can actually move inside $\mathcal C$ ; closing this gap requires the regularity assumption and completeness of $V$ , and must keep the active inequality constraints nonnegative, not just the equalities. And the resulting first-order inequality, which holds only up to $\varepsilon\|h\|$ , must be turned into an approximate multiplier representation in $V^*$ , an infinite-dimensional dual space in which the usual finite-dimensional Farkas lemma does not apply as stated.

Formalization scope

$V$ is a real Banach space: [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]. $V^*$ is V →L[ℝ] ℝ with the operator norm; $F'(v)$ is fderiv ℝ F v.
Constraints are one family G : Fin m → V → ℝ, 0-based: the paper's constraint $i$ is Lean index $i-1$ , an equality constraint iff its index is $<p$ . p ≤ m is assumed in the goal.
$C^1$ is ContDiff ℝ 1; $F$ is Differentiable ℝ F (Fréchet-differentiable everywhere).
No infimum over $\mathcal C$ is formed: "bounded below" is BddBelow (F '' 𝒞) and " $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ " is " $F(v)\le F(w)+\varepsilon^2$ for all $w\in\mathcal C$ ". A real infimum over an empty or unbounded set would be a junk value.
Added hypotheses, disclosed in each item: $\mathcal C\ne\emptyset$ (goal and milestone 1) and $\{G=0\}\ne\emptyset$ (Corollary 3.4). Without them the paper's hypotheses hold vacuously ( $\inf\emptyset=+\infty$ ) while the conclusion asks for a feasible point.
Lemma 3.3 is stated with $\le\varepsilon$ . The paper prints $<\varepsilon$ in (3.20), which fails for $V=\mathbb R$ , no constraints and $w^*=\varepsilon\,\mathrm{id}$ ; its proof gives $\le$ , and Theorem 3.1 uses $\le$ .
Lemma 3.2 and milestone 2 assume the linear independence (3.4) only at the point $v$ under consideration, and Lemma 3.2 is stated for any feasible $v$ with property (3.12); this is exactly what the paper's proof uses.
Regularity is a linear independence of the indexed family $(G_i'(v))_{i\in I(v)}$ , so a repeated saturated constraint violates it; the constraint qualification cannot be trivialized by collapsing duplicates.

Contributions welcome: a general Ekeland principle with the strict-minimizer conclusion, a Lyusternik–Graves tangent-curve theorem for $C^1$ maps with surjective derivative onto $\mathbb R^k$ , and a closedness result for finitely generated cones in $V^*$ .

Selected references

I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974) 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979) 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60 (2011) 627–641. https://doi.org/10.1080/02331930903578700

7 thms2 active usersReviewed

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Sensitivity Theorems in Integer Linear Programming: Every Integral m×n Matrix Has Chvátal Rank at Most 2^(n³+1)·n^(5n)·Δ(A)^(n+1)Research Paper

Motivation

An integer linear program $\max\{wx : Ax \le b,\ x \text{ integral}\}$ is usually attacked through its linear programming relaxation $\max\{wx : Ax \le b\}$ , which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.

W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables $n$ and the largest subdeterminant $\Delta(A)$ of the constraint matrix, independently of the right-hand side.

Timeline.

1958–1963: Gomory introduces integer rounding cuts. In 1973 Chvátal (Discrete Math. 4) shows that finitely many rounds reach the integer hull of a bounded polyhedron.
1977–1979: Blair and Jeroslow prove that for a fixed matrix $A$ the distance between LP and IP optima, and the gap between their values, are bounded by constants depending on $A$ .
1980: Schrijver (Ann. Discrete Math. 9) proves that the Chvátal closure of a rational polyhedron is a polyhedron, and that every rational polyhedron, bounded or not, reaches its integer hull after finitely many rounds.
1986: Cook, Gerards, Schrijver and Tardos prove the explicit bounds of this mission, $n\Delta(A)$ for proximity, and show that every integral matrix has finite Chvátal rank.
Later work, for example Eisenbrand and Weismantel (2018), replaces the $\ell_\infty$ proximity bound by $\ell_1$ bounds for programs in standard form.

Setting

All matrices, vectors and polyhedra are rational. Let $A$ be an integral $m\times n$ matrix. A square submatrix of order $k$ , where $1\le k\le\min(m,n)$ , keeps $k$ rows and $k$ columns of $A$ . The quantity $\Delta(A)$ is the largest $|\det B|$ over all such submatrices $B$ . So $\Delta(0)=0$ , and $\Delta(A)\ge 1$ whenever $A\ne 0$ . Norms are $\|x\|_\infty=\max_i|x_i|$ and $\|x\|_1=\sum_i|x_i|$ .

For $b\in\mathbb{Q}^m$ write $P=\{x\in\mathbb{Q}^n : Ax\le b\}$ . An optimal solution of $\max\{wx : Ax\le b\}$ is a point of $P$ maximizing $wx$ . For $\max\{wx : Ax\le b,\ x\text{ integral}\}$ it is an integral point of $P$ maximizing $wx$ among the integral points of $P$ . A rational polyhedron is a set $\{x : Dx\le d\}$ with $D$ , $d$ rational. The integer hull $P_I$ is the convex hull of the integral points of $P$ .

If $ay\le\beta$ for all $y\in P$ , with $a$ integral and $\beta$ rational, then every integral point of $P$ satisfies the Chvátal cut $ax\le\lfloor\beta\rfloor$ . The Chvátal closure $P'$ is the set of points satisfying all Chvátal cuts. Set $P^{(0)}=P$ and $P^{(i)}=(P^{(i-1)})'$ . Then $P_I\subseteq P^{(i)}$ for all $i$ . The Chvátal rank of $P$ is the least $t$ with $P^{(t)}=P_I$ . The Chvátal rank of the matrix $A$ is the supremum of the Chvátal ranks of $\{x : Ax\le b\}$ over all integral vectors $b$ .

Formalization targets

Goal: Theorem 10 (p. 260)

\sup_{b\in\mathbb{Z}^m}\ \operatorname{rank}\{x : Ax\le b\}\ \le\ 2^{n^3+1}\,n^{5n}\,\Delta(A)^{n+1}.

In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on $m$ or on $b$ .

Milestones, in attack order

Theorem 1 (p. 252). Suppose $Ax\le b$ has an integral solution and the LP maximum exists. Then every LP optimum has an IP optimum within $\ell_\infty$ -distance $n\Delta(A)$ , and every IP optimum has an LP optimum within the same distance.
Corollary 2 (p. 253). Under the same hypotheses, $\max\{wx: Ax\le b\}-\max\{wx : Ax\le b,\ x\text{ integral}\}\le n\Delta(A)\|w\|_1$ .
Theorem 5 (p. 255). Changing $b$ to $b'$ moves LP optima by at most $n\Delta(A)\|b-b'\|_\infty$ and IP optima by at most $n\Delta(A)(\|b-b'\|_\infty+2)$ . This result is off the goal's path.
Theorem 6 (p. 256). A non-optimal integral solution can be improved by an integral solution within $\ell_\infty$ -distance $n\Delta(A)$ .
Theorem 7 (p. 257). A single integral matrix $M$ , with entries at most $n^{2n}\Delta(A)^n$ in absolute value, gives $\{x: Ax\le b\}_I=\{x : Mx\le d_b\}$ for every $b$ for which $Ax\le b$ has an integral solution.
Theorem 8, printed "Theorem 9" (p. 259). If a rational polyhedron $P\subseteq\mathbb{Q}^n$ has no integral point, then $P^{(n^{2n}2^{n^3})}=\emptyset$ .
Corollary 9 (p. 260). Let $q=\max\{wx : x\in P_I\}$ with $w$ integral. Then $P^{(r)}\subseteq\{x : wx\le q\}$ for $r=(n^{2n}2^{n^3}+1)(\lfloor\max\{wx : x\in P\}\rfloor-q)+1$ .

Significance

The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for $\{x : Ax\le b\}$ is controlled by $A$ alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with $b$ . They are also the standard starting point for the later proximity literature.

Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the $\ell_1$ bound with $\Delta$ the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over $\mathbb{Q}$ : polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.

Difficulty

The proximity theorems need a conic decomposition $\bar x-\bar z=\sum\lambda_i g^i$ into integral generators with entries bounded by $\Delta(A)$ . That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.

Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.

The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap $\lfloor\max_P wx\rfloor-q$ is not bounded independently of $b$ until Theorem 7 and Corollary 2 bound it by $n^{2n+2}\Delta(A)^{n+1}$ . Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that $P^{(k)}\cap F\subseteq F^{(k)}$ for faces $F$ , and invariance under unimodular affine maps. None of these is in Mathlib.

Formalization scope

Rationality. Everything is over $\mathbb{Q}$ , following the paper's standing assumption on p. 252. Points are Fin n → ℚ, $A$ is Matrix (Fin m) (Fin n) ℤ cast to $\mathbb{Q}$ , and a polyhedron is a finite system of rational inequalities.
$\Delta(A)$ . Only nonempty submatrices count, so $\Delta(0)=0$ .
Optimality. "The maximum exists" means an optimal solution exists. Existence claims that the paper proves are part of the conclusions: the IP optimum in Theorem 1 and Corollary 2, and $\max\{wx : x\in P\}$ in Corollary 9.
Chvátal closure. It is defined for every subset of $\mathbb{Q}^n$ , using all integral $a$ and rational $\beta$ . The rank is valued in $\mathbb{N}\cup\{\infty\}$ , with $\infty$ if no iterate equals $P_I$ . A version with junk value $0$ would make the goal trivial and is not used. The matrix rank is a supremum over integral $b$ , as printed.
Added hypotheses. Theorems 1 and 6 carry the hypothesis $A\ne0$ . For $A=0$ the bound $n\Delta(A)=0$ makes both statements false, and the proof on p. 257 assumes $A\ne0$ as well. In Corollary 9 the value $q$ is taken to be an integer. This loses nothing, because a maximum of an integral $w$ over $P_I$ is attained at an integral point.
Constants. All constants are exactly as printed, written in $\mathbb{N}$ with $0^0=1$ .

A complete development needs the following:

cone generation with Cramer bounds and Carathéodory's theorem;
LP duality and Farkas' lemma over $\mathbb{Q}$ ;
the polyhedrality of $P'$ for rational polyhedra (Schrijver 1980);
Schrijver's face lemma and unimodular invariance;
a flatness theorem.

The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.

Selected references

W. Cook, A.M.H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34 (1986) 251–264. https://doi.org/10.1007/BF01582230
V. Chvátal, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305–337. https://doi.org/10.1016/0012-365X(73)90167-2
A. Schrijver, On cutting planes, Annals of Discrete Mathematics 9 (1980) 291–296. https://doi.org/10.1016/S0167-5060(08)70085-2
W. Cook, C.R. Coullard, Gy. Turán, On the complexity of cutting-plane proofs, Discrete Applied Mathematics 18 (1987) 25–38. https://doi.org/10.1016/0166-218X(87)90039-4
F. Eisenbrand, R. Weismantel, Proximity results and faster algorithms for integer programming using the Steinitz lemma, ACM Transactions on Algorithms 16 (2020), Art. 5. https://doi.org/10.1145/3340322

11 thms2 active usersReviewed

Analysis Operations Research Optimization·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems I: The Łojasiewicz Inequality at Critical Points of Continuous Subanalytic FunctionsResearch Paper

Motivation

For a real-analytic function $f : U \to \mathbb{R}$ on an open set $U \subseteq \mathbb{R}^n$ and a critical point $a$ (so $\nabla f(a) = 0$ ), the Łojasiewicz gradient inequality says that there is an exponent $\theta \in [0,1)$ such that $|f - f(a)|^{\theta} / \|\nabla f\|$ stays bounded near $a$ . It is the standard tool for proving that bounded gradient trajectories $\dot x = -\nabla f(x)$ have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value $+\infty$ and are not differentiable.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.

Timeline.

1963: Łojasiewicz proves the inequality for real-analytic functions (Une propriété topologique des sous-ensembles analytiques réels), and in 1984 derives convergence of bounded analytic gradient trajectories.
1998: Kurdyka (Ann. Inst. Fourier 48) extends it to $C^1$ functions definable in an o-minimal structure, with a desingularizing function in place of the power.
2006: Bolte, Daniilidis and Lewis prove a nonsmooth Sard theorem (J. Math. Anal. Appl. 321): a subanalytic function continuous on its closed domain is constant on each connected component of its critical set.
2007: The present paper proves the nonsmooth inequality for continuous subanalytic functions (Theorem 3.1) and for lower semicontinuous convex ones (Theorem 3.3).
2007: Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18) extend it to lower semicontinuous functions definable in o-minimal structures (the KL property).

Setting

Write $\mathbb{R}^n$ with its Euclidean norm. A function $f : \mathbb{R}^n \to \mathbb{R} \cup \{+\infty\}$ has domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ .

Subanalytic sets (Definition 2.1). A set $A \subseteq \mathbb{R}^n$ is semianalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ on which $A \cap V = \bigcup_{i=1}^{p}\bigcap_{j=1}^{q}\{x \in V : f_{ij}(x) = 0,\ g_{ij}(x) > 0\}$ with $f_{ij}, g_{ij}$ real-analytic on $V$ . It is subanalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ such that $A \cap V$ is the projection onto $\mathbb{R}^n$ of a bounded semianalytic subset of $\mathbb{R}^n \times \mathbb{R}^m$ , $m \ge 1$ . A function $f$ is subanalytic if its graph $\{(x,\lambda) \in \mathbb{R}^n \times \mathbb{R} : f(x) = \lambda\}$ is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.

Subdifferentials (Definition 2.10). The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y \to x,\, y \ne x} \frac{f(y) - f(x) - \langle x^*, y - x\rangle}{\|y - x\|} \ge 0$ (empty off $\operatorname{dom} f$ ). The limiting subdifferential $\partial f(x)$ is the set of limits of $x^*_k \in \hat\partial f(x_k)$ along $x_k \to x$ with $f(x_k) \to f(x)$ .

Slope and critical points. The nonsmooth slope is $m_f(x) = \inf\{\|x^*\| : x^* \in \partial f(x)\}$ , equal to $+\infty$ when $\partial f(x) = \emptyset$ (equation (4)). The critical set is $\operatorname{crit} f = \{x : 0 \in \partial f(x)\}$ (Definition 2.11).

Formalization targets

Goal: Theorem 3.1

Let $f$ be subanalytic with closed domain and $f|_{\operatorname{dom} f}$ continuous, and let $a \in \operatorname{crit} f$ . Then there is $\theta \in [0,1)$ such that

\frac{|f - f(a)|^{\theta}}{m_f} \ \text{ is bounded around } a,

with the conventions $0^0 = 1$ and $\infty/\infty = 0/0 = 0$ . In division-free form: there are $C$ and a neighbourhood $U$ of $a$ with $|f(x) - f(a)|^{\theta} \le C\|x^*\|$ for all $x \in U$ and $x^* \in \partial f(x)$ . The exponent is existential; the goal fixes no value of $\theta$ or $C$ .

Milestones

Remark 2.12, for $f$ continuous on a closed domain: the graph of $\partial f$ is closed; $\operatorname{crit} f$ is closed; $m_f$ is lower semicontinuous; $\operatorname{crit} f = m_f^{-1}(0)$ .
Proposition 2.13(ii), its clause on the critical set: if $f$ is subanalytic and relatively bounded on its domain, then $\operatorname{crit} f$ is subanalytic.
Equation (6), recalled from the nonsmooth Sard theorem: $f$ is constant on the connected component of $\operatorname{crit} f$ containing $a$ .
The curve selection lemma, recalled from Bierstone–Milman: a boundary point of a subanalytic set is the origin of an analytic arc entering the set.

Significance

The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems $\dot x \in -\partial f(x)$ (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.

Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.

Difficulty

The obvious argument restricts $f$ and $m_f$ to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of $m_f$ ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that $f$ is not smooth: the classical proof differentiates $f$ along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of $f$ on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes $f$ real-valued and $C^1$ , proves a different and much weaker statement.

Formalization scope

Space and values. The space is EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.
Subdifferentials. $\hat\partial f$ and $\partial f$ are the published platform definitions NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to $-\infty$ .
Subanalyticity. It is defined on any finite-dimensional real normed space, so that the same definition covers $\mathbb{R}^n$ , $\mathbb{R}^n \times \mathbb{R}$ and $\mathbb{R}^n \times \mathbb{R}^m$ . Analyticity is AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.
Slope. The slope is valued in $[0,+\infty]$ , with $+\infty$ on points without subgradients.
The inequality. It is the predicate LojIneqAt f a θ: one constant $C$ and one neighbourhood of $a$ , quantified over all limiting subgradients. Under $0^0 = 1$ the value $\theta = 0$ never works at a critical point, as under the paper's conventions.
Not assumed. The goal does not assume lower semicontinuity, real values, global subanalyticity, compactness of the critical set, or $f(a) = 0$ . These are reductions inside the paper's proof. Any formalization that adds them, fixes $\theta$ , or replaces the class of $f$ by semialgebraic or $C^1$ functions trivializes the target.
Infrastructure. A complete proof needs: curve selection; the monotonicity lemma and Puiseux expansions for one-variable globally subanalytic functions; the projection theorem or an equivalent definability argument; the nonsmooth Sard theorem (6); and a chain rule for Fréchet subgradients along analytic curves. Each of these is welcome as a separate contribution, and the subanalytic-geometry results are reusable well beyond this mission.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. https://doi.org/10.1137/050644641
J. Bolte, A. Daniilidis, A. Lewis, A Sard theorem for non-differentiable functions, J. Math. Anal. Appl. 321 (2006) 729–740.
E. Bierstone, P. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007) 556–572. https://doi.org/10.1137/060670080
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, 87–89.
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

12 thms2 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network I: Fat-Shattering Margin Bound with d = fat_H(γ/16)Research Paper

Motivation

Classical generalization bounds for classifiers, built on the VC dimension, grow with the number of adjustable parameters. For neural networks this is at odds with practice: networks with many more weights than training examples often generalize well. Bartlett's 1998 paper (IEEE Trans. Inform. Theory 44(2), 525–536) explains part of this by measuring a real-valued classifier's confidence. If a hypothesis classifies most training examples correctly with a margin $\gamma$ , its misclassification probability is controlled by a scale-sensitive dimension of the class at scale proportional to $\gamma$ , not by its VC dimension. Later in the paper this yields bounds for networks with small weights that do not depend on the number of weights.

This mission formalizes the first of the paper's two main technical results, the margin bound of Theorem 2 (p. 527), together with the steps of its proof on pp. 527–528.

The fat-shattering dimension was introduced by Kearns and Schapire (JCSS 1994). Alon, Ben-David, Cesa-Bianchi and Haussler (J. ACM 1997) proved the scale-sensitive Sauer-type covering bound used here (Theorem 5 of the paper). Shawe-Taylor, Bartlett, Williamson and Anthony (IEEE Trans. Inform. Theory 1998) proved the zero-training-error version (Theorem 1 of the paper). Theorem 2 extends it to hypotheses that make margin errors on the training data.

Setting

Let $X$ be a set and $P$ a probability distribution on $X\times\{-1,1\}$ . The threshold function is $\operatorname{sgn}(\alpha)=-1$ for $\alpha<0$ and $\operatorname{sgn}(\alpha)=1$ for $\alpha\ge0$ . For a real-valued hypothesis $h$ on $X$ , the misclassification probability is $\operatorname{er}_P(h)=P\{\operatorname{sgn}(h(x))\ne y\}$ . For a sample $z=((x_1,y_1),\dots,(x_m,y_m))$ drawn independently from $P$ and $\gamma>0$ , the margin error estimate is

\widehat{\operatorname{er}}{}^{\gamma}_z(h)=\tfrac1m\,|\{i : y_ih(x_i)<\gamma\}|.

Let $H$ be a class of real functions on $X$ . Points $x_1,\dots,x_m$ are $\gamma$ -shattered by $H$ if some $r\in\mathbb R^m$ has the following property: for every sign vector $b\in\{-1,1\}^m$ , some $h\in H$ satisfies $(h(x_i)-r_i)b_i\ge\gamma$ for all $i$ . The fat-shattering dimension $\operatorname{fat}_H(\gamma)$ is the largest such $m$ , possibly $\infty$ .

The proof uses the following objects:

the squashing function $\pi_\gamma(\alpha)=\max(-\gamma,\min(\gamma,\alpha))$ and the class $\pi_\gamma(H)=\{\pi_\gamma\circ h:h\in H\}$ ;
the sample $\ell_\infty$ pseudometric $d_{\ell_\infty(x)}(f,g)=\max_i|f(x_i)-g(x_i)|$ ;
the covering number $\mathcal N_\infty(F,\epsilon,m)$ , the largest over $x\in X^m$ of the size of the smallest $\epsilon$ -cover (Definition 3), and the corresponding packing number $\mathcal M_\infty(F,\alpha,m)$ ;
the quantization $Q_\alpha(x)=\lceil (x-\alpha/2)/\alpha\rceil\alpha$ .

Formalization targets

Goal: Theorem 2

Assume $0<\delta<1/2$ , $0<\gamma<1$ , $m\ge1$ , and $d=\operatorname{fat}_H(\gamma/16)$ finite with $d\le 34m$ . With probability at least $1-\delta$ over $z$ , every $h\in H$ satisfies

\operatorname{er}_P(h)<\widehat{\operatorname{er}}{}^{\gamma}_z(h)+\sqrt{\frac2m\Bigl(d\ln\frac{34em}{d}\log_2(578m)+\ln\frac4\delta\Bigr)} .

Milestones, in the order the proof uses them

Lemma 4. $\operatorname{er}_P(h)<\widehat{\operatorname{er}}{}^{\gamma}_z(h)+\sqrt{(2/m)\ln(2\mathcal N_\infty(\pi_\gamma(H),\gamma/2,2m)/\delta)}$ uniformly over $H$ , with probability at least $1-\delta$ .
Theorem 5 (Alon et al.). If $F:\{1,\dots,n\}\to\{1,\dots,b\}$ and $\operatorname{fat}_F(1)\le d$ , then $\log_2\mathcal N_\infty(F,2,n)<1+\log_2(nb^2)\log_2\sum_{i\le d}\binom ni b^i$ , provided $n$ is large enough.
Writing $F=Q_{\gamma/8}(\pi_\gamma(H))$ : $\operatorname{fat}_F(\gamma/8)\le\operatorname{fat}_{\pi_\gamma(H)}(\gamma/16)$ .
$\mathcal M_\infty(\pi_\gamma(H),\gamma/2,2m)\le\mathcal M_\infty(F,\gamma/2,2m)$ .
$\mathcal N_\infty(\pi_\gamma(H),\gamma/2,2m)\le\mathcal N_\infty(F,\gamma/4,2m)$ .
$\log_2\mathcal N_\infty(\pi_\gamma(H),\gamma/2,2m)<1+d\log_2(34em/d)\log_2(578m)$ when $1\le d\le 2m$ and $m\ge d\log_2(34em/d)+1$ .
$\operatorname{fat}_{\pi_\gamma(H)}(\gamma/16)\le\operatorname{fat}_H(\gamma/16)$ .

A further item, Proposition 8 (p. 529), is the probabilistic device the paper uses to make such bounds uniform over $\gamma$ .

Significance

Theorem 2 is the bound behind the paper's main message. Corollary 9 makes it uniform over $\gamma$ , and Theorem 28 combines it with fat-shattering estimates for networks with bounded weights. Together they show that a network classifying the training data with a large margin generalizes at a rate governed by the size of its weights, not by its number of weights. The same template, a margin error plus a capacity term at scale $\gamma$ , underlies later margin analyses of support vector machines and boosting.

All results in this mission are proved in the literature; none is open. None is machine-checked on this platform: the platform has Rademacher-complexity margin bounds, but no statement about fat-shattering dimension or $\ell_\infty$ sample covering numbers of real-valued classes. A complete formalization would provide a reusable library of these objects, with their basic inequalities between squashing, quantization, packing and covering. It would also give a checked version of the explicit constants $34em/d$ and $578m$ , which differ from those in later textbook treatments.

Difficulty

The bound is uniform over a possibly uncountable class $H$ , so a union bound over hypotheses does not apply. The obvious replacement is a union bound over a cover of $H$ . Two steps make it hard:

Lemma 4. It needs a ghost-sample symmetrization and a random-swap argument, carried out with an $\ell_\infty$ cover of the squashed class on the double sample, so the cover depends on the data.
Theorem 5. Bounding that covering number by the fat-shattering dimension is a combinatorial counting argument about strongly shattered pairs. It is the scale-sensitive analogue of the Sauer–Shelah lemma, and here the bookkeeping of constants is exact.

The quantization steps look routine but carry the factor-of-two losses that produce the constants $\gamma/16$ , $17$ and $578$ .

Formalization scope

The model is in the namespace BartlettNN.Margin.

Labels and samples. Labels are Bool, read as $\pm1$ through pm (true is $+1$ ). $\operatorname{sgn}(0)=1$ . Samples are functions Fin m → X × Bool, indexed from $0$ , with law Measure.pi (fun _ => P). The margin estimate uses the strict inequality $y_ih(x_i)<\gamma$ , and shattering uses $\ge\gamma$ .
Fat-shattering dimension. $\operatorname{fat}$ is valued in ℕ∞. A ℕ-valued supremum would be $0$ on an unbounded set, so the goal assumes fat H (γ/16) = d with d : ℕ.
Covering and packing numbers. Covers are finite and external (centres are arbitrary functions), the cover inequality is strict, and covering numbers are ⊤ when no finite cover exists. $\mathcal N_\infty$ and $\mathcal M_\infty$ are suprema over all samples, with repetitions allowed. " $\alpha$ -separated", which the paper leaves undefined, is read as distance $\ge\alpha$ .
Logarithms. $\ln$ is Real.log, $\log_2$ is Real.logb 2, and $e$ is Real.exp 1.
High probability. "With probability at least $1-\delta$ , every $h$ " bounds the measure of the event that some $h\in H$ violates the inequality. It is not a per-hypothesis statement.

Measurability. The paper states "we ignore issues of measurability, and assume that all sets considered are measurable" (p. 526). This is made explicit, not removed, through three hypotheses:

every $h\in H$ is measurable;
the bad events $\{z:\exists h\in H,\ \operatorname{er}_P(h)\ge\widehat{\operatorname{er}}{}^{\gamma}_z(h)+\epsilon\}$ are measurable;
the double-sample events of display (1) are measurable.

Replacing these by countability of $H$ would weaken the theorem.

Corrections of the printed text.

Theorem 2. The goal adds $d\le 34m$ . Beyond $34m$ the term $d\ln(34em/d)$ decreases, vanishes at $d=34em$ and then turns negative, and the printed statement fails for rich classes. Within this range nothing is lost: the proof covers $d\le2m$ , and for $2m<d\le34m$ the bound exceeds $1$ .
Milestone 6. It carries the hypothesis $d\le 2m$ , the range of the binomial estimate behind $34em/d$ .
Milestone 3. Its printed justification $|Q_{\gamma/8}(a)-Q_{\gamma/8}(b)|<|a-b|+\gamma/16$ is false; the correct term is $\gamma/8$ . The milestone's conclusion is true as printed, and only the conclusion is formalized.

Trivializing formalizations, ruled out. The following would each make the statements empty or different, and none is used:

a ℕ-valued fat dimension or covering number;
Real.sign in place of $\operatorname{sgn}$ ;
a per-hypothesis probability bound;
an unrestricted $d$ , which makes $\sqrt{\cdot}$ of a negative number equal to $0$ ;
a covering number that is $0$ on classes without finite covers.

Infrastructure that a complete development needs, and contributions that are welcome:

product measures and Hoeffding's inequality, which Mathlib has;
a symmetrization (ghost-sample) lemma for margin events;
the combinatorics of Theorem 5;
the elementary inequalities between packing and covering numbers.

The covering/packing and fat-shattering lemmas apply beyond this mission. Proofs of individual milestones, or of Theorem 5 in the generality of Alon et al., are useful contributions in their own right.

Selected references

P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Trans. Inform. Theory 44(2), 525–536, 1998. https://doi.org/10.1109/18.661502
N. Alon, S. Ben-David, N. Cesa-Bianchi, D. Haussler, Scale-sensitive dimensions, uniform convergence, and learnability, J. ACM 44(4), 615–631, 1997. https://doi.org/10.1145/263867.263927
J. Shawe-Taylor, P. L. Bartlett, R. C. Williamson, M. Anthony, Structural risk minimization over data-dependent hierarchies, IEEE Trans. Inform. Theory 44(5), 1926–1940, 1998. https://doi.org/10.1109/18.705570
M. J. Kearns, R. E. Schapire, Efficient distribution-free learning of probabilistic concepts, J. Comput. Syst. Sci. 48(3), 464–497, 1994. https://doi.org/10.1016/S0022-0000(05)80062-5
V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory Probab. Appl. 16(2), 264–280, 1971. https://doi.org/10.1137/1116025

12 thms2 active usersReviewed

Mathematical Physics Probability·Captain: mikedeng1

The Intermediate Disorder Regime for Directed Polymers in Dimension 1+1: The Rescaled Partition Function Converges in Law to a Wiener ChaosResearch Paper

Motivation

A directed polymer in a random environment is a simple random walk whose paths are reweighted by a random field of energies. It is a basic model of disordered statistical mechanics, and in dimension $1+1$ it belongs to the Kardar–Parisi–Zhang (KPZ) universality class: at fixed temperature the free energy fluctuates on the scale $n^{1/3}$ and is expected to follow Tracy–Widom laws. Comets and Yoshida (Ann. Probab. 34 (2006)) showed that in dimension $1+1$ every positive inverse temperature $\beta$ lies in the strong disorder regime, where the normalised partition function tends to zero. At $\beta=0$ the polymer is simply the random walk.

Alberts, Khanin and Quastel (arXiv:1202.4398, Ann. Probab. 42 (2014)) identified the regime in between. If the inverse temperature is scaled as $\beta n^{-1/4}$ , the partition function neither concentrates nor vanishes: it converges in law to a universal random variable, a Wiener chaos in a space–time white noise. That variable is the solution at time $1$ , integrated in space, of the stochastic heat equation with multiplicative noise, whose logarithm is the Hopf–Cole solution of the KPZ equation. The theorem therefore connects discrete polymers to the continuum KPZ equation under weak, $n$ -dependent disorder, with no assumption on the environment beyond exponential moments.

Setting

The environment is a family $\omega=(\omega(i,x))_{i\ge1,\,x\in\mathbb Z}$ of i.i.d. real random variables on a probability space $(\Omega,Q)$ , with mean $0$ and variance $1$ . Write $\lambda(\beta)=\log Q\,e^{\beta\omega}$ . The polymer is the symmetric simple random walk $S$ on $\mathbb Z$ started at $0$ , independent of $\omega$ , under the uniform measure $\mathbf P$ on the $2^n$ step sequences. The energy of an $n$ -step path is $H_n^\omega(S)=\sum_{i=1}^n\omega(i,S_i)$ , and the point-to-line partition function is

Z_n^\omega(\beta)=\mathbf P\big[e^{\beta H_n^\omega(S)}\big].

The modified partition function replaces $e^{\beta\omega}$ by $1+\beta\omega$ : $\mathfrak z_n^\omega(\beta)=\mathbf P\big[\prod_{i=1}^n(1+\beta\,\omega(i,S_i))\big]$ .

On the continuum side, a white noise on $[0,1]\times\mathbb R$ is a centred Gaussian family $\{W(A)\}$ , indexed by the Borel sets of finite Lebesgue measure, with $E[W(A)W(B)]=|A\cap B|$ . Its multiple stochastic integrals are continuous linear maps $I_k:L^2([0,1]^k\times\mathbb R^k)\to L^2$ with $I_k(\mathbf 1_{A_1\times\dots\times A_k})=\prod_jW(A_j)$ for pairwise disjoint $A_j$ . Let $\varrho(t,x)=e^{-x^2/2t}/\sqrt{2\pi t}$ be the heat kernel and $\Delta_k=\{0=t_0<t_1<\dots<t_k\le1\}$ . Put $\varrho_k(\mathbf t,\mathbf x)=\prod_{j=1}^k\varrho(t_j-t_{j-1},x_j-x_{j-1})$ on $\Delta_k\times\mathbb R^k$ , with $x_0=0$ , and zero elsewhere. The Wiener chaos (7) is

\mathcal Z_\beta=\sum_{k\ge0}\beta^kI_k(\varrho_k)=1+\sum_{k\ge1}\beta^k\int_{\Delta_k}\int_{\mathbb R^k}\prod_{i=1}^kW(t_i,x_i)\,\varrho(t_i-t_{i-1},x_i-x_{i-1})\,dx_i\,dt_i .

The discrete counterpart of $I_k$ is the weighted U-statistic $\mathcal S_k^n(g)$ of (29): a sum of products $\prod_j\omega(i_j,x_j)$ over distinct times, weighted by averages of $g$ over space–time rectangles of size $\frac1n\times\frac2{\sqrt n}$ .

Formalization targets

Goal: Theorem 2.1 (second bullet), proved as Proposition 5.4

If, in addition, $\lambda(b)<\infty$ for all $0<b<\beta_0$ for some $\beta_0>0$ , then for every $\beta>0$

e^{-n\lambda(\beta n^{-1/4})}\,Z_n^\omega(\beta n^{-1/4})\xrightarrow{(d)}\mathcal Z_{\sqrt2\beta}\qquad(n\to\infty).

Modified partition function: Proposition 5.3 (Theorem 2.1, first bullet)

Under mean zero and variance one alone, $\mathfrak z_n^\omega(\beta n^{-1/4})\xrightarrow{(d)}\mathcal Z_{\sqrt2\beta}$ .

Milestones

In the order the proof uses them:

the norm $\|\varrho_k\|^2_{L^2}=1/(2^k\Gamma(k/2+1))$ and the convergence of the chaos series (§3.4, Lemma 3.1);
the $L^2$ structure of $\mathcal S_k^n$ (Lemma 4.1);
an approximation lemma for convergence in law (Lemma 4.2);
convergence of $n^{-3k/4}\mathcal S_k^n(g)$ to $I_k(g)$ , jointly over finitely many orders (Theorem 4.3);
convergence of whole discrete chaos expansions (Lemma 4.4);
the exact expansion $\mathfrak z_n^\omega(\beta)=\sum_{k\le n}2^{k/2}\beta^k\mathcal S_k^n(p_k^n)$ (Lemma 5.2);
a uniform $L^2$ bound on the discretised random walk kernels $n^{k/2}p_k^n$ (Lemma A.1);
Proposition 5.3.

Significance

The theorem gives a universal scaling limit for the partition function in a regime where the polymer still moves diffusively but feels the disorder. As a corollary, $\log Z_n^\omega(\beta n^{-1/4})-n\lambda(\beta n^{-1/4})$ converges in law, so the fluctuation exponent of the free energy is $0$ in this regime. The companion results (point-to-point partition functions, Theorem 2.2) show that the rescaled polymer path measure converges to a continuum directed random polymer. Letting $\beta$ grow then interpolates between Gaussian behaviour and the Tracy–Widom GUE fluctuations of the KPZ class. The U-statistic machinery of Section 4 (discrete chaos expansions in an i.i.d. space–time field converging to multiple Wiener–Itô integrals) applies to other discrete models with polynomial chaos expansions.

The theorem is proved in the paper. To our knowledge it has no machine-checked proof, and Mathlib has no space–time white noise, no multiple Wiener integrals, no Wiener chaos, no Lindeberg–Feller theorem for triangular arrays and no local limit theorem for the simple random walk. A complete formalization would build each of these and check the paper's argument, including two statements that are false as printed (see Formalization scope).

Difficulty

The obvious route is to expand $Z_n^\omega(\beta n^{-1/4})$ in powers of $\beta$ and pass to the limit term by term. Two steps of that route do not go through as stated. First, the $k$ -th term is a degenerate U-statistic of order $k$ in the environment. Its convergence to $I_k$ is not a classical central limit theorem: it needs joint control of all orders and a density argument in $L^2([0,1]^k\times\mathbb R^k)$ , and the space–time discretisation must respect the parity of the walk, which is why the rectangles have spatial length $2/\sqrt n$ . Second, exchanging the limit with the infinite sum over $k$ needs bounds on the discrete kernels $n^{k/2}p_k^n$ that are uniform in $n$ and summable in $k$ . Pointwise convergence from the local limit theorem is not enough. Passing from $\mathfrak z_n$ to $Z_n$ also requires a central limit theorem for a triangular array whose law depends on $n$ .

Formalization scope

The environment is ω : ℕ × ℤ → Ω → ℝ, independent and identically distributed, square integrable, with mean $0$ and variance $1$ . Times $i\ge1$ are read. $Z_n$ and $\mathfrak z_n$ are explicit averages over the $2^n$ step sequences. The white noise lives on $[0,1]\times\mathbb R$ , since only $t\le1$ enters (7). $I_k$ is a family of continuous linear maps on $L^2$ characterised by its values on indicators of products of disjoint sets. Every limit theorem quantifies over all white noises and all such families, and a separate item asserts that one exists. $\mathcal Z_\beta$ and $\mathcal S_k^n$ are sums in $L^2$ ; real powers $n^{-1/4}$ , $n^{-3k/4}$ are Real.rpow; $\lambda$ is Mathlib's cgf; convergence in law is TendstoInDistribution.

Normalisation of $I_k$ . The paper's normalisation of multiple integrals is not consistent (§3.2 and the remark on p. 19 differ by $k!$ ). The formalization follows (7) and the variance computation on p. 6: for $g$ supported on $\Delta_k\times\mathbb R^k$ , $E[I_k(g)^2]=\|g\|^2$ .

Corrected statements. Two milestones are stated in the corrected form that the paper's proof establishes:

Lemma 4.1. The bound $Q[\mathcal S_k^n(g)^2]\le n^{3k/2}\|g\|^2$ is false for general $g$ when $k\ge2$ , because permuted index vectors give the same product of environment variables. It is stated for $g$ vanishing outside $\Delta_k\times\mathbb R^k$ , the only case Section 5 uses. "Mean zero" is stated for $k\ge1$ , since $\mathcal S_0^n(g_0)=g_0$ .
Lemma 4.4. It is stated for Fock vectors whose components vanish outside the simplices, with square-summable norms, so that $\sum_kI_k(g_k)$ converges.

Theorem 4.5 and Lemma 4.6 (perturbed environments) are not part of the milestone list. Theorem 4.5 is false as printed: mean zero and a variance tending to $1$ do not give a central limit theorem for a triangular array, and the Lindeberg condition named in its proof must be added. Lemma A.1 is stated for the point-to-line kernels only.

Trivializations ruled out. The limit is the chaos (7) built from a genuine white noise and its multiple integrals, not any random variable with a prescribed property. $I$ is pinned down by $W$ . Every infinite sum comes with a milestone proving its summability, and the partition function averages over all $2^n$ walk paths.

Infrastructure that would be reusable beyond this mission: space–time white noise and multiple Wiener–Itô integrals with their isometry, a Lindeberg–Feller central limit theorem, the local limit theorem for the simple random walk, and the Cramér–Wold device. Contributions of any of these, or of proofs of the milestones in any order, are welcome.

Selected references

T. Alberts, K. Khanin, J. Quastel, The intermediate disorder regime for directed polymers in dimension 1+1, Ann. Probab. 42 (2014), 1212–1256. arXiv:1202.4398
T. Alberts, K. Khanin, J. Quastel, The continuum directed random polymer, J. Stat. Phys. 154 (2014), 305–326. MR3162542
F. Comets, N. Yoshida, Directed polymers in random environment are diffusive at weak disorder, Ann. Probab. 34 (2006), 1746–1770. MR2271480
S. Janson, Gaussian Hilbert Spaces, Cambridge Tracts in Mathematics 129, Cambridge University Press, 1997. MR1474726
P. Billingsley, Convergence of Probability Measures, Wiley, 1968. MR0233396

12 thms2 active usersReviewed

Control Theory Mechanism Design Operations Research+1·Captain: mikedeng1

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 2: The Producer's First-Best Value in Closed FormResearch Paper

Motivation

Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.

The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.

The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.

Setting

Fix integers $N,d\ge0$ (usages for the mean effort and for the volatility effort), cost parameters $\mu\in(0,\infty)^N$ , $\lambda\in(0,\infty)^d$ , nominal volatilities $\sigma\in(0,\infty)^d$ , effort bounds $A_{\max}>0$ and $0<\varepsilon\le1$ , risk aversions $r,p>0$ , a marginal volatility cost $h>0$ , slopes $\kappa,\theta\in\mathbb R$ , a horizon $T>0$ , an initial consumption $X_0\in\mathbb R$ and a reservation utility $R_0<0$ .

The consumer chooses a mean effort $\alpha$ with values in $A=\prod_i[0,\mu_iA_{\max}]$ and a responsiveness effort $\beta$ with values in $B=[\varepsilon,1]^d$ , at cost

c(\alpha,\beta)=c_1(\alpha)+\tfrac12c_2(\beta),\qquad c_1(a)=\tfrac12\sum_i\frac{a_i^2}{\mu_i},\qquad c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}\big(b_j^{-1}-1\big).

The consumption $X$ follows $X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s$ with $\sigma(b)=(\sigma_1\sqrt{b_1},\dots,\sigma_d\sqrt{b_d})$ , in the weak sense: $X$ is the canonical process on $C([0,T],\mathbb R)$ , and an admissible pair $(\nu,\mathbb P)$ is a progressively measurable control $\nu=(\alpha,\beta)$ with a probability measure under which $X$ starts at $X_0$ and solves the associated martingale problem.

The consumer values consumption by $f(x)=\kappa x$ and the producer bears the generation cost $g(x)=\theta x$ ; write $\delta=\kappa-\theta$ . For a payment $\xi$ made at time $T$ , the consumer's and the producer's criteria are

J_A=\mathbb E^{\mathbb P}\Big[-e^{-r\left(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds\right)}\Big],\qquad J_P=\mathbb E^{\mathbb P}\Big[-e^{-p\left(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T\right)}\Big].

A contract is an $\mathcal F_T$ -measurable $\xi$ with uniform exponential moments (2.5). The first-best value is

V^{FB}=\sup\big\{J_P(\xi,\nu,\mathbb P):\ \xi\text{ a contract},\ (\nu,\mathbb P)\text{ admissible},\ J_A(\xi,\nu,\mathbb P)\ge R_0\big\}.

The consumer's Hamiltonians are $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$ . Finally $\rho=\frac{rp}{r+p}$ , $L_0=-\frac1r\log(-R_0)$ , $U(x)=-e^{-px}$ , $\bar\mu=\sum_i\mu_i$ and $x^-=\max(0,-x)$ .

Formalization targets

Goal: Proposition 3.1 (i)

Assume $\delta^-T\le A_{\max}$ . Then

V^{FB}=U\big(\bar v(0,X_0)-L_0\big),\quad \bar v(0,X_0)=\delta TX_0+\int_0^T\Big(\tfrac12\bar\mu(\delta^-)^2(T-t)^2+H_v\big(-h-\rho\delta^2(T-t)^2\big)\Big)dt.

Milestones

Proposition 2.1. The best responses $\hat a(z)$ , $\hat b(\gamma)$ attain the infima defining $H_m$ , $H_v$ , and these Hamiltonians have explicit closed forms.
(A.5). The auxiliary value $\bar V=\sup_{(\nu,\mathbb P)}\mathbb E^{\mathbb P}\big[-e^{-\rho(\int_0^T(\delta X_t-c(\nu_t))dt-\frac h2\langle X\rangle_T)}\big]$ is finite and negative, and $V^{FB}=R_0(\bar V/R_0)^{1+p/r}$ .
Proposition A.3 (i), with the explicit solution of p. 28.

\bar V=-e^{-\rho\left(\delta TX_0+\int_0^T\bar m(t)dt\right)},\qquad \bar m(t)=H_m(\delta(T-t))+H_v\big(-h-\rho\delta^2(T-t)^2\big).

Significance

The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy $\delta$ through the mean-effort term, on the volatility cost $h$ and the effective risk aversion $\rho$ through the volatility Hamiltonian, and on the reservation utility only through the shift by $L_0$ . It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.

The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.

Difficulty

The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of $\bar V$ into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on $\langle X\rangle_T$ ; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on $\bar V$ must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.

Formalization scope

The canonical space is $C([0,T],\mathbb R)$ with the coordinate σ-algebra and the canonical filtration; processes are indexed by $[0,T]$ . Admissible pairs are given by a martingale problem: $X_0=X_0$ almost surely, and both $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are martingales. In the criteria, $\langle X\rangle_T$ is replaced by its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$ ; a contract remains any $\mathcal F_T$ -measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in $[-\infty,0]$ , and every value is an extended-real supremum with $\sup\emptyset=-\infty$ . $B$ is read as $[\varepsilon,1]^d$ , with indices in Fin N and Fin d.

The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: $\varepsilon\le1$ (so $B\ne\emptyset$ ), $R_0<0$ (so $L_0$ is defined), and, for the goal only, $\delta^-T\le A_{\max}$ , without which the printed $\frac12\bar\mu(\delta^-)^2(T-t)^2$ exceeds $H_m(\delta(T-t))$ and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of $H_m$ in Proposition 2.1 is false for $z^->A_{\max}$ and is replaced by $\bar\mu(m z^--m^2/2)$ with $m=z^-\wedge A_{\max}$ ; the index range of $\hat b$ is $j=1,\dots,d$ ; on p. 28, $\int_0^t\bar m$ is $\int_t^T\bar m$ and "(A.11)" is (A.6).

The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.

Selected references

R. Aïd, D. Possamaï, N. Touzi, Optimal electricity demand response contracting with responsiveness incentives, arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022. https://arxiv.org/abs/1810.09063
J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance Stoch. 22, 2018. https://arxiv.org/abs/1510.07111
B. Holmström, P. Milgrom, Aggregation and linearity in the provision of intertemporal incentives, Econometrica 55, 1987. https://doi.org/10.2307/1913238
Y. Sannikov, A continuous-time version of the principal–agent problem, Rev. Econ. Stud. 75, 2008. https://doi.org/10.1111/j.1467-937X.2007.00463.x
I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991, §5.4 (martingale problems and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Mathematical Physics Optimization Partial Differential Equations+1·Captain: mikedeng1

Optimization of Mean-field Spin Glasses I: Every Minimizer of the Extended Parisi Functional Has Full SupportResearch Paper

Motivation

The Ising mixed $p$ -spin model assigns to each configuration $\sigma \in \{-1,+1\}^N$ the energy of a random polynomial whose covariance is $\mathbb E\{H_N(\sigma)H_N(\sigma')\} = N\xi(\langle\sigma,\sigma'\rangle/N)$ . Its ground-state energy $\max_\sigma H_N(\sigma)/N$ converges to the value of a variational problem, the zero-temperature Parisi formula (Auffinger–Chen 2017), in which a functional $\mathsf P$ is minimized over non-decreasing order parameters $\gamma$ . El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) ask how close a polynomial-time algorithm can get to this maximum. Their answer is an extended variational principle: the best value reachable by incremental approximate message passing is $\inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$ , where the space $\mathscr L$ drops the monotonicity constraint.

The algorithm that reaches this value is built from a minimizer $\gamma_*$ of $\mathsf P$ over $\mathscr L$ , and it runs along the set of times where $\gamma_*$ is positive. Theorem 5 of the paper (p. 30) shows that this set is dense: a minimizer has full support. This mission formalizes that theorem and the first- and second-order optimality conditions it rests on (Section 6.1, pp. 22–31).

Timeline. Parisi proposed the variational formula in 1979. Talagrand (2006) and Panchenko (2013) proved it at positive temperature. Auffinger and Chen (2017) established the zero-temperature version with $\Phi(1,x)=|x|$ and proved that a minimizer over the monotone space exists. Jagannath and Tobasco (2016) developed the PDE and SDE tools for the Parisi functional that Section 6.1 of the present paper adapts to non-monotone order parameters. Montanari (2019) gave the first message passing algorithm for the Sherrington–Kirkpatrick case; the present paper (2020) extended it to general mixtures and introduced $\mathscr L$ .

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$ ; its derivatives $\xi'$ , $\xi''$ are the termwise differentiated power series, non-negative and non-decreasing on $[0,1]$ .

An order parameter is a function $\gamma : [0,1) \to \mathbb R_{\ge0}$ . The extended space is

\mathscr L = \Bigl\{\gamma : [0,1)\to\mathbb R_{\ge0} : \|\xi''\gamma\|_{\mathrm{TV}[0,t]}<\infty\ \forall t\in[0,1),\ \int_0^1\xi''(t)\gamma(t)\,dt<\infty\Bigr\},

with the weighted distance $\|\gamma_1-\gamma_2\|_{1,\xi''} = \int_0^1\xi''(t)|\gamma_1(t)-\gamma_2(t)|\,dt$ . The non-negative step functions $\mathsf{SF}_+$ are the finite sums $\sum_i a_i\mathbb I_{[t_{i-1},t_i)}$ with $0=t_0<\dots<t_m=1$ and $a_i\ge0$ .

For a terminal condition $f_0$ (convex, continuous, even, non-negative, differentiable off $0$ with $0\le f_0'\le1$ on $(0,\infty)$ ) and $\gamma\in\mathsf{SF}_+$ , the Parisi PDE

\partial_t\Phi + \tfrac12\xi''(t)\bigl(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\bigr) = 0,\qquad \Phi(1,x) = f_0(x),

has the explicit Cole–Hopf solution $\Phi^\gamma$ : on $[t_{i-1},t_i)$ , $\Phi(t,x) = \gamma_i^{-1}\log\mathbb E\exp\{\gamma_i\Phi(t_i, x+\sqrt{\xi'(t_i)-\xi'(t)}\,G)\}$ with $G\sim\mathsf N(0,1)$ . For $\gamma\in\mathscr L$ , $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n\to\gamma$ in the weighted distance. The Parisi functional is

\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .

Given a Brownian motion $B$ , the process $X$ solves $dX_t = \xi''(t)\gamma(t)\,\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$ , $X_0 = 0$ . The support of $\gamma$ is $S(\gamma) = \{t\in[0,1):\gamma(t)>0\}$ , and $\overline S(\gamma)$ is its closure in $[0,1)$ .

Formalization targets

Goal: Theorem 5

With $f_0(x) = |x|$ , if $\gamma_*\in\mathscr L$ satisfies $\mathsf P(\gamma_*) = \inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$ , then

\overline S(\gamma_*) = [0,1).

Milestones

The path to the goal, in attack order:

Proposition 6.1(b),(c): on step functions, $\partial_x\Phi$ is non-decreasing with $|\partial_x\Phi|\le1$ , and $\|\Phi^{\gamma_1}-\Phi^{\gamma_2}\|_\infty\le\|\xi''(\gamma_1-\gamma_2)\|_1$ .
Lemma 6.2: these properties pass to $\gamma\in\mathscr L$ .
Lemma 6.5: the SDE has a unique strong solution on $[0,1]$ .
Corollary 6.6: $\mathbb E\{\partial_x\Phi(t_2,X_{t_2})^2\}-\mathbb E\{\partial_x\Phi(t_1,X_{t_1})^2\}=\int_{t_1}^{t_2}\xi''(s)\,\mathbb E\{(\partial_x^2\Phi(s,X_s))^2\}\,ds$ .
Lemma 6.7: the map $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$ .
Proposition 6.8: the first variation $\frac{d}{ds}\mathsf P(\gamma+s\delta)|_{s=0+}=\frac12\int_0^1\xi''\delta\,(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t)\,dt$ .
Lemma 6.9: $S(\gamma)$ is a countable disjoint union of intervals.
Corollary 6.10: $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\}=t$ on $\overline S(\gamma_*)$ and $\ge t$ off it.
Corollary 6.11: $\xi''(t)\,\mathbb E\{\partial_x^2\Phi^{\gamma_*}(t,X_t)^2\}=1$ on $\overline S(\gamma_*)$ .
Lemma 6.12: the law of $X_t$ has a density, bounded below on compact sets, once $\gamma$ vanishes.

Significance

The result. Full support identifies the extended variational principle as one whose minimizers are "nowhere flat". The algorithm of Theorem 3 in the paper follows $\gamma_*$ through incremental steps whose size is set by $\gamma_*$ , and it needs no special treatment of gaps where $\gamma_* = 0$ . The stationarity conditions (Corollaries 6.10–6.11) also characterize minimizers over $\mathscr L$ the way the Auffinger–Chen conditions characterize minimizers over the monotone space. They are the starting point for comparing $\inf_{\mathscr L}\mathsf P$ with the Parisi value.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The paper's proofs rely on cited PDE regularity (Jagannath–Tobasco 2016) and on standard SDE theory, often in one line. The mission produces a machine-checked chain from the explicit Cole–Hopf formula to the support theorem. Along the way it builds the Parisi PDE solution on a non-monotone class, a first-variation formula, and stationarity conditions, none of which have a formal counterpart. No formal statement of the Parisi functional or the Parisi PDE exists on Prove2Me (index search, 2026-10-03).

Difficulty

Two steps resist a direct argument. The first is the first variation (Proposition 6.8): differentiating $\Phi^\gamma(0,0)$ in $\gamma$ requires comparing the SDE for $\gamma$ with the SDE for the perturbed parameter and controlling their difference uniformly, which needs bounds on $\partial_x^2\Phi$ that degenerate as $t\to1$ . The second is the exclusion of gaps: on an interval where $\gamma_*=0$ the PDE is a time-changed heat equation, and the contradiction comes from a strict inequality, which requires the law of $X_t$ to charge every interval (Lemma 6.12). The obvious idea of perturbing $\gamma_*$ upward on a gap only yields the inequality (6.14), which is consistent with a gap; the second-order identity at the gap's endpoints is what closes the argument.

Formalization scope

Conventions committed to in Lean:

The mixture is a coefficient sequence $c$ with $c_0=c_1=0$ ; $\xi,\xi',\xi''$ are explicit series.
Order parameters are functions $\mathbb R\to\mathbb R$ read only on $[0,1)$ . Membership in $\mathscr L$ uses eVariationOn for the total variation and IntegrableOn for the integral; the latter includes the a.e.-measurability that the paper takes for granted.
$\Phi^\gamma$ for step functions is the Cole–Hopf recursion (7.3). For a piece with $\gamma_i = 0$ the formula's limit, the heat semigroup, is used instead of a division by zero. $\mathbb E$ over $G$ is integration against gaussianReal 0 1. For $\gamma\in\mathscr L$ , $\Phi^\gamma$ is a limit along the filter of step functions converging in the weighted $L^1$ distance; it is never "some solution of the PDE".
$\partial_x\Phi$ and $\partial_x^2\Phi$ are iterated derivs in $x$ . Lemma 6.2's weak-derivative claim is stated as "convex and 1-Lipschitz", its equivalent.
The SDE uses the published strong-solution concept EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by zero after time $1$ . The driver is assumed to be a standard Brownian motion (IsBrownianReal). Statements about $X$ hold for every strong solution, which by Lemma 6.5 is unique.
Section 6.1's results are stated for every admissible $f_0$ ; $\mathsf P$ is parametrized by $f_0$ , and Theorem 5 fixes $f_0=|\cdot|$ .
Minimality is " $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma\in\mathscr L$ ", never a real infimum. $\overline S(\gamma)$ is closure (S γ) ∩ Ico 0 1. Right-continuity of $\gamma_*$ , the paper's convention from p. 28, is a hypothesis.
Disclosed hypothesis $\xi\not\equiv0$ (some $c_k\neq0$ ) on Theorem 5, Corollaries 6.10–6.11 and Lemma 6.12. For $\xi\equiv0$ every $\gamma$ minimizes $\mathsf P$ and $X\equiv0$ , so $\gamma_*\equiv0$ has empty support and each of those statements fails. When $c_2=0$ no minimizer exists (Corollary 6.11 at $t=0$ ), and Theorem 5 is vacuous, as in the paper.
Lemma 6.12's density bound is stated without choosing density versions: $\varepsilon\,\mathrm{Leb}(A)\le\mathbb P(X_t\in A)$ for measurable $A\subseteq[-M,M]$ .

A trivializing formalization is excluded: $\Phi^\gamma$ and $X$ are the paper's objects, built from the data, so the goal cannot be met by choosing a convenient solution, and minimality over $\mathscr L$ cannot be satisfied by a junk infimum.

Not formalized: the weak formulation (6.4) of Lemma 6.2, printed with a wrong boundary term; the stochastic-integral identity (6.7) of Lemma 6.5; the regularity Lemmas 6.3–6.4; Proposition 6.1(a). The paper's algorithmic Theorems 2–4 are out of scope, because they concern algorithms in an informal model of computation and an AMP state-evolution theory that is not part of this mission.

Useful infrastructure beyond this mission: the Cole–Hopf solution and its Lipschitz dependence on $\gamma$ , the Parisi functional on $\mathscr L$ , and the SDE (6.3). Contributions that formalize Itô's formula for these processes or the regularity of $\Phi^\gamma$ are welcome as supporting lemmas.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Annals of Probability, 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proceedings of the AMS, 2016. https://arxiv.org/abs/1502.04398
A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
M. Talagrand, The Parisi formula, Annals of Mathematics 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
D. Panchenko, The Parisi ultrametricity conjecture, Annals of Mathematics 177(1), 2013. https://doi.org/10.4007/annals.2013.177.1.8

22 thms2 active usersReviewed

Control Theory Mechanism Design Operations Research+1·Captain: mikedeng1

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 1: The Producer's Second-Best Value in Closed FormResearch Paper

Motivation

Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.

Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.

Setting

Fix integers $N,d\ge0$ , cost parameters $\mu\in(0,\infty)^N$ and $\lambda\in(0,\infty)^d$ , nominal volatilities $\sigma\in(0,\infty)^d$ , effort bounds $A_{\max}>0$ and $\varepsilon\in(0,1]$ , risk aversions $r,p>0$ , a marginal cost of volatility $h>0$ , marginal energy value $\kappa$ and cost $\theta$ with $\delta:=\kappa-\theta$ , a horizon $T>0$ , an initial consumption $X_0$ and a reservation utility $R_0<0$ . Write $\bar\mu:=\sum_i\mu_i$ and $x^-:=\max(0,-x)$ .

Consumption. $X$ is the canonical process on $\Omega=C([0,T],\mathbb R)$ with its natural filtration $\mathbb F$ . A control $\nu=(\alpha,\beta)$ is progressively measurable, with $\alpha_t\in A:=\prod_i[0,\mu_iA_{\max}]$ (effort to reduce consumption) and $\beta_t\in B:=[\varepsilon,1]^d$ (effort to reduce volatility). Under $\nu$ the consumption follows, in the weak sense,

X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s,\qquad |\sigma(b)|^2=\sum_j\sigma_j^2b_j .

Effort costs $c(\nu)=c_1(\alpha)+\frac12c_2(\beta)$ per unit time, with $c_1(a)=\frac12\sum_ia_i^2/\mu_i$ and $c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}(b_j^{-1}-1)$ .

Criteria. For a payment $\xi$ at time $T$ , the consumer's criterion is $J_A=\mathbb E[-e^{-r(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds)}]$ and the producer's is $J_P=\mathbb E[U(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T)]$ with $U(x)=-e^{-px}$ . Contracts $\mathcal C$ are the $\mathcal F_T$ -measurable $\xi$ with exponential moments of order $m>1$ uniformly over the consumer's responses (2.5). The consumer's value is $V_A(\xi)=\sup J_A$ , and $\mathcal P^\star(\xi)$ is the set of his optimal responses.

Second best. The producer offers $\xi$ , the consumer responds optimally, ties are broken in the producer's favour, and participation requires $V_A(\xi)\ge R_0$ :

V^{SB}:=\sup_{\xi\in\mathcal C,\ V_A(\xi)\ge R_0}\ \sup_{\mathcal P^\star(\xi)}J_P(\xi,\cdot),\qquad\sup\emptyset=-\infty .

Hamiltonians. $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$ .

Formalization targets

Goal: Proposition 3.2 (i)

Assume $\delta^-T\le A_{\max}$ . With $q_t(z)=h+rz^2+p(z-\delta(T-t))^2$ , $L_0=-\frac1r\log(-R_0)$ ,

m_{SB}(t)=\frac12\bar\mu\delta^2(T-t)^2-\frac12\inf_{z\in\mathbb R}\Big\{\bar\mu\big(z^-+\delta(T-t)\big)^2-2H_v\big(-q_t(z)\big)\Big\},

V^{SB}=U\big(v(0,X_0)-L_0\big),\qquad v(0,X_0)=\delta TX_0+\int_0^Tm_{SB}(s)\,ds .

Milestones

Proposition 2.1. The consumer's best responses $\hat a_i(z)=\mu_i(z^-\wedge A_{\max})$ and $\hat b_j(\gamma)=(1\wedge(\lambda_j\gamma^-)^{-1/2})\vee\varepsilon$ attain the infima defining $H_m$ and $H_v$ , and

H_m(z)=\bar\mu\big(m z^--\tfrac{m^2}2\big),\ m=z^-\wedge A_{\max};\qquad H_v(\gamma)=-\tfrac12\big(\hat c_2(\gamma)-\gamma|\hat\sigma(\gamma)|^2\big).

Lemma A.1. With $f_0(q,\gamma)=q|\hat\sigma(\gamma)|^2+\hat c_2(\gamma)$ , $F_0(q):=\inf_{\gamma\le0}f_0(q,\gamma)=f_0(q,-q)=-2H_v(-q)$ , and $F_0$ is non-decreasing.
Proposition A.4 (ii). A minimiser of $z\mapsto F_0(h-k+rz^2+p(z-y)^2)+\bar\mu(z^-+y)^2$ is $\frac p{r+p}y$ when $y\ge0$ , and lies in $[y,\frac p{r+p}y]$ when $y\le0$ .

A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates $z_{SB}(t)=\frac p{r+p}\delta(T-t)$ and $\gamma_{SB}(t)=-h-\frac{rp}{r+p}\delta^2(T-t)^2$ when $\delta\ge0$ .

Significance

The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.

The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.

Difficulty

The deterministic milestones are calculus on boxes. The goal is not. The upper bound $V^{SB}\le U(v(0,X_0)-L_0)$ must hold for every $\mathcal F_T$ -measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every $\xi\in\mathcal C$ inducing an optimal response can be written as $Y_T^{y_0,Z,\Gamma}$ , an integral against $dX$ and $d\langle X\rangle$ driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.

Formalization scope

All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:

Weak formulation. An admissible pair $(\nu,\mathbb P)$ is a control and a probability measure on $C([0,T],\mathbb R)$ with $X_0=X_0$ a.s., under which $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are $\mathbb F$ -martingales. This is the martingale problem equivalent to weak solutions of (2.1); the paper deliberately leaves weak solutions informal (footnote 2). The pair, not the law alone, is the admissible object, because the cost depends on $\nu$ .
Quadratic variation. $\langle X\rangle_T$ in $J_P$ is its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$ .
Values. Expected utilities are negated lower Lebesgue integrals, in $[-\infty,0]$ ; all suprema are in the extended reals, so the empty supremum is $-\infty$ , as on p. 9.
Hamiltonians are defined by their infima, not by the closed forms of Proposition 2.1.
Indices are Fin N, Fin d; $N=0$ , $d=0$ are allowed. $\hat b_j(\gamma)=1$ when $\lambda_j\gamma^-\le1$ (the paper's $0^{-1/2}=+\infty$ ).
Added hypotheses. $\varepsilon\le1$ ( $B\neq\emptyset$ ), $R_0<0$ ( $\log(-R_0)$ defined), and for the goal $\delta^-T\le A_{\max}$ . The paper's closed form is computed with the effort cap removed (" $\eta_A\to0$ as $A\nearrow\infty$ ", p. 30), and with the capped effort of the model it is correct exactly under this hypothesis.
Corrected misprints. $-2H_m(-q(z))$ in $m_{SB}$ is read as $-2H_v(-q(z))$ ; with $H_m$ the infimum is $-\infty$ . The printed $H_m(z)=\frac12\bar\mu(z^-\wedge A_{\max})^2$ is false for $z^->A_{\max}$ and is corrected. " $j=1,\dots,N$ " for $\hat b$ means $j=1,\dots,d$ . In Proposition A.4 (ii) the open interval becomes closed, and "for large $A$ " is read as $\eta_A\equiv0$ .

The goal is an equality of extended reals between $V^{SB}$ , defined from the model, and an explicit real number. A formalization that defines $V^{SB}$ over a restricted class of contracts, or with a real-valued supremum that returns $0$ on unbounded sets, would trivialize or change it and is not the goal.

Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.

Selected references

R. Aïd, D. Possamaï, N. Touzi, Optimal Electricity Demand Response Contracting with Responsiveness Incentives, arXiv:1810.09063v3, 2019; Mathematics of Operations Research 47 (2022). https://arxiv.org/abs/1810.09063v3
J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance and Stochastics 22 (2018) 1–37. https://doi.org/10.1007/s00780-017-0344-4
B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987) 303–328. https://doi.org/10.2307/1913238
Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008) 957–984. https://doi.org/10.1111/j.1467-937X.2008.00486.x
I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer 1991, §5.4 (martingale problem and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Machine Learning Quantum Information Theoretical Computer Science·Captain: mikedeng1

Shadow Tomography of Quantum States 1: Polylogarithmically Many Copies Suffice to Estimate Every Acceptance Probability to Within εResearch Paper

Motivation

Learning an unknown quantum state is expensive. Full quantum state tomography of a $D$ -dimensional mixed state $\rho$ to accuracy $\varepsilon$ in trace distance needs on the order of $D^2/\varepsilon^2$ copies of $\rho$ (O'Donnell–Wright 2016; Haah et al. 2017), and this is optimal. For a system of $n$ qubits, $D = 2^n$ , so full tomography is out of reach beyond a few dozen qubits.

Often one does not need the whole density matrix, only the behaviour of $\rho$ on a fixed list of tests: acceptance probabilities of verification circuits, expectation values of observables, or the answers a piece of quantum advice gives to a set of questions. Aaronson (arXiv:1711.01053, STOC 2018) named this task shadow tomography and asked whether the number of copies can be polylogarithmic in both the dimension and the number of tests. Measuring each test on separate copies costs $\tilde O(M/\varepsilon^2)$ copies, which is linear in $M$ .

Timeline.

2016: the question was posed at a mini-course without a name (Aaronson, The Complexity of Quantum States and Transformations, §8.3.1).
2016: Harrow, Lin and Montanaro gave a correct "quantum OR" test, repairing an earlier flawed claim (arXiv:1607.03236, Corollary 11).
2017–2018: Aaronson proved the first polylogarithmic bound, the theorem of this mission.
Later work improved the exponents, notably Bădescu–O'Donnell 2021, and introduced the related "classical shadows" of Huang–Kueng–Preskill 2020.

Setting

A mixed state of dimension $D$ is a $D\times D$ Hermitian positive semidefinite matrix $\rho$ with $\mathrm{Tr}\,\rho = 1$ . A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with all eigenvalues in $[0,1]$ . Equivalently, $0 \preceq E \preceq \mathbb 1$ . It accepts $\rho$ with probability $\mathrm{Tr}(E\rho)$ .

The state $\rho^{\otimes k}$ consists of $k$ independent copies of $\rho$ . A measurement of $\rho^{\otimes k}$ with classical output is a POVM: a finite family of positive semidefinite matrices $P_\omega$ on the $k$ -register space with $\sum_\omega P_\omega = \mathbb 1$ . Outcome $\omega$ occurs with probability $\mathrm{Tr}(P_\omega\rho^{\otimes k})$ . An adaptive procedure that measures the copies one after another is described by one such POVM.

Problem 1 (shadow tomography). Given an unknown $\rho$ and known two-outcome measurements $E_1,\dots,E_M$ , output numbers $b_1,\dots,b_M\in[0,1]$ with $|b_i-\mathrm{Tr}(E_i\rho)|\le\varepsilon$ for all $i$ , with success probability at least $1-\delta$ . The output must come from a measurement of $\rho^{\otimes k}$ , with $k=k(D,M,\varepsilon,\delta)$ as small as possible. The measurement may depend on the $E_i$ , but not on $\rho$ .

Formalization targets

Goal: Theorem 2, in the explicit form proved in §5

There is a universal constant $C$ such that, for $M\ge2$ and $0<\varepsilon,\delta\le 1/2$ , Problem 1 is solvable with

k \le C\,\frac{\log D}{\varepsilon}\Big(\frac{\log\log D+\log\frac1\varepsilon}{\varepsilon^{2}}\Big)^{2}\log^4 M\Big(\log\log M+\log\log D+\log\frac1\varepsilon+\log\frac1\delta\Big) = \tilde O\Big(\frac{\log 1/\delta}{\varepsilon^5}\log^4 M\log D\Big)

copies. This is the last display of the proof (p. 19). The goal fixes no constant, so any improvement of $C$ remains consistent with it.

Milestones

Theorem 13 (Harrow–Lin–Montanaro). A one-copy test that accepts with probability at least $(1-\epsilon)^2/7$ if some $\mathrm{Tr}(E_i\rho)\ge1-\epsilon$ , and at most $4\Delta M$ if $\sum_i\mathrm{Tr}(E_i\rho)\le\Delta M$ .
Lemma 14 (Quantum OR Bound). Deciding whether $\max_i\mathrm{Tr}(E_i\rho)\ge c$ or $\le c-\varepsilon$ with $O(\log(1/\delta)\log M/\varepsilon^2)$ copies, independent of $D$ .
Lemma 15 (Gentle Search). Finding $j$ with $\mathrm{Tr}(E_j\rho)\ge c-\varepsilon$ with $O(\frac{\log^4M}{\varepsilon^2}(\log\log M+\log\frac1\delta))$ copies.
Amplification claims (p. 16). The threshold tests $E^*_{i,t,\pm}$ on $\rho^{\otimes q}$ accept with probability at least $5/6$ when the hypothesis is off by $\varepsilon$ , and at most $1/3$ when it is within $\varepsilon/2$ .
Markov claim (p. 17). The postselection test $F_t$ on an arbitrary, possibly entangled, $q$ -register state accepts with probability at most $\frac{a q}{(a+\varepsilon/4)q}$ .
Lemma 12 (Quantum Union Bound, probability part). Measurements each accepting with probability at least $1-\varepsilon$ all accept in succession with probability at least $1-2M\sqrt\varepsilon$ .
Chernoff claim (p. 18). $1-\mathrm{Tr}(F_t\rho^{\otimes q})\le\varepsilon^4/\log^2D$ .
Proposition 20. Promise-gap thresholds for all $i$ at once can be decided with $O(\log(M/\delta)/\varepsilon^2)$ copies.

Significance

The result. Theorem 2 shows that a state of exponential dimension can be learned "for all practical purposes" on exponentially many tests from polynomially many copies. Applications in the paper include a bound on quantum advice and one-way communication, and implications for quantum money and copy-protection. It also shows that the information needed to predict many measurement outcomes is far smaller than the description of $\rho$ .

Formalizing it. The theorem is proved in the paper, and later work improves its exponents. As far as is known it has not been machine-checked. A complete development formalizes the gentle-measurement toolkit (Lemma 12, Lemma 14, Lemma 15), the amplification of two-outcome measurements on tensor powers, and the postselection argument. These are standard tools of quantum learning theory and quantum complexity with no formal counterpart yet. Lemma 14 and Lemma 15 are reusable beyond this mission.

Difficulty

The naive approach measures the $E_i$ directly on shared copies. A measurement that is likely to reject disturbs the state, so later measurements see a damaged state, and separate copies per measurement cost $M$ copies.

The proof needs three ingredients:

a gentle search that finds a measurement on which the current hypothesis is wrong while damaging the copies only slightly;
a potential argument showing that postselection cannot happen too often;
a uniform control of the damage.

The potential argument has to hold for the state after postselection, which is correlated or entangled across registers. Independence-based concentration fails there, which is why the Markov claim, not a Chernoff bound, governs that step. Theorem 13 itself rests on a delicate ancilla-based procedure of Harrow, Lin and Montanaro, and the mission cites it as a milestone without its proof.

Formalization scope

Representation.
- Operators are complex matrices over a finite index type, and states use the published WildeQIT.IsDensityOperator (positive semidefinite, trace one).
- A two-outcome measurement is IsEffect E: both $E$ and $\mathbb 1-E$ are positive semidefinite.
- $\rho^{\otimes k}$ is a matrix indexed by $k$ -tuples Fin k → n.
- A measurement with output is a POVM structure with a finite outcome type. Probabilities are real parts of traces.
Quantifier order of the goal. $\exists C$ , then for all $D,M,\varepsilon,\delta$ there is $k$ ; then for all $E_i$ there are a POVM and outputs $b$ ; then for all $\rho$ . Choosing the measurement after $\rho$ would make the goal trivial (output the true values with $k=0$ ), and this order rules that out.
Disclosed hypotheses.
- Theorem 2 assumes $M\ge2$ , $\varepsilon\le1/2$ and $\delta\le1/2$ . These keep the logarithmic factors positive; at $M=1$ the bound would force $k=0$ .
- Lemma 14 assumes $M\ge2$ , and Lemmas 14 and 15 bound $\delta$ .
- Theorem 13 assumes $\epsilon\le1/2$ , as in Harrow–Lin–Montanaro's Corollary 11.
- The Chernoff claim assumes $D\ge2$ .
Conventions.
- All logarithms are natural, including inside $\log\log$ .
- Amplified tests use real thresholds.
- "Applied in succession" in Lemma 12 uses Lüders instruments ( $\sqrt{E}$ Kraus operators), in the order $E_1,E_2,\dots$ .
- The hypothesis $\rho_t$ enters the amplification claims only as the number $a=\mathrm{Tr}(E\rho_t)$ .
Printed steps not drafted.
- The printed $\varepsilon^{-4}$ form of Theorem 2 relies on an external online-learning algorithm that is only sketched.
- The halting rule of §5 is unspecified, because Lemma 15 always returns an index.
- The asymptotic claims $p_t\ge0.9/D^q$ for $t=o(\log^2D/\varepsilon^4)$ and $t=O(q\log D/\varepsilon)$ use a circular $o(\cdot)$ .
- The trace-distance part of Lemma 12 has an unquantified $O(\cdot)$ .
- Lemma 12's printed bound $1-2M\sqrt\varepsilon$ is weaker than its use on p. 18. It is stated as printed. The proof of the goal must retune constants or use Wilde's stronger $1-2\sqrt{M\varepsilon}$ -type bound.
Contributions welcome. Proofs of any milestone; a formal Hoeffding bound for binomial counts of product effects; the gentle measurement lemma for Lüders instruments; Naimark dilation for effects.

Selected references

S. Aaronson, Shadow Tomography of Quantum States, STOC 2018; arXiv:1711.01053v2, 2018. https://arxiv.org/abs/1711.01053
A. W. Harrow, C. Y.-Y. Lin, A. Montanaro, Sequential measurements, disturbance and property testing, SODA 2017. https://arxiv.org/abs/1607.03236
M. M. Wilde, Sequential decoding of a general classical-quantum channel, Proc. R. Soc. A, 2013. https://arxiv.org/abs/1303.0808
R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory, 2017. https://arxiv.org/abs/1508.01797
C. Bădescu, R. O'Donnell, Improved quantum data analysis, STOC 2021. https://arxiv.org/abs/2011.10908
H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics, 2020. https://arxiv.org/abs/2002.08953

16 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research+2·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design XI: Optimal Sequential Screening by Option ContractsTextbook

Motivation

Many sales are contracted before the buyer knows what the good is worth to her. An airline sells a ticket months before the trip, a hotel sells a refundable or non-refundable room before the traveller's plans are settled, and a supplier signs a capacity contract before demand is realised. At the time of contracting the buyer holds some private information about her future valuation (how likely she is to travel), and after contracting she learns more (whether she actually travels). Sequential screening is the mechanism design problem of a seller facing such a buyer.

The chapter formalized here, Daniel Krähmer and Roland Strausz's Dynamic Mechanism Design (Chapter 11 of Börgers' textbook), develops the problem along two lines. The first is dynamic private information: one sale, two rounds of private information. The second is dynamic allocations: repeated sales, one fixed valuation.

Timeline:

Baron and Besanko (1984) show that dynamic allocations with static information produce no real dynamics in the optimal mechanism.
Courty and Li (2000, Review of Economic Studies) solve the sequential screening problem and show that the optimal mechanism is a menu of option contracts.
Esö and Szentes (2007) decompose the buyer's information into initial and additional information, show that the seller can extract the additional information at no cost, and derive the optimal multi-buyer mechanism, the handicap auction.
Krähmer and Strausz (2011, 2014), cited in the chapter's problems (notes 2–3, p.237), show that the conclusions depend on the model's assumptions; with discrete ex ante types the privacy of the additional information can cost the seller (Problem 11.5(c), p.233).

Setting

A seller sells one indivisible good. Before contracting, the buyer privately observes her ex ante type $\tau\in[\underline\tau,\bar\tau]$ , with distribution function $G$ and density $g>0$ . After accepting the mechanism she privately observes her ex post type $\theta\in[\underline\theta,\bar\theta]$ , $0\le\underline\theta<\bar\theta$ , which is her valuation. Conditionally on $\tau$ it has distribution function $F(\theta\mid\tau)$ and density $f(\theta\mid\tau)>0$ . Both $F$ and $f$ are continuously differentiable in $\tau$ , $|\partial F/\partial\tau|<K$ , and higher $\tau$ is good news in the sense of first-order stochastic dominance: $\partial F(\theta\mid\tau)/\partial\tau<0$ for $\theta\in(\underline\theta,\bar\theta)$ .

A direct mechanism is a pair $q(\tau,\theta)\in[0,1]$ , $t(\tau,\theta)\in\mathbb R$ . The buyer first reports $\tau$ , then $\theta$ . Write $u(\tau,\theta)=\theta q(\tau,\theta)-t(\tau,\theta)$ , $\hat U(\tau'\mid\tau)=\int u(\tau',\hat\theta)f(\hat\theta\mid\tau)\,d\hat\theta$ and $U(\tau)=\hat U(\tau\mid\tau)$ . The mechanism is incentive-compatible if truth about $\theta$ is optimal after every report of $\tau$ , and truth about $\tau$ is optimal against every subsequent reporting function $\theta_r$ . It is individually rational if $U(\tau)\ge0$ for all $\tau$ . The seller maximizes expected revenue $\int\!\!\int t\,f\,g$ . The virtual valuation is

\psi(\tau,\theta)=\theta+\frac{1-G(\tau)}{g(\tau)}\,\frac{\partial F(\theta\mid\tau)/\partial\tau}{f(\theta\mid\tau)} ,

and Assumption 11.1 requires $\psi$ to be increasing in $\tau$ and $\theta$ . The exercise price is $p(\tau)=\min\{\hat\theta\mid\psi(\tau,\hat\theta)\ge0\}$ .

Formalization targets

Goal: Proposition 11.8 (optimal sequential screening)

Under Assumption 11.1 the optimal mechanism is

q^*(\tau,\theta)=\mathbf 1[\theta\ge p(\tau)],\qquad t^*(\tau,\theta)=t_0(\tau)+p(\tau)\,\mathbf 1[\theta\ge p(\tau)],

where $t_0$ is the expression of Proposition 11.5 for $q^*$ , and the lowest type pays

t(\underline\tau,\underline\theta)=\int_{p(\underline\tau)}^{\bar\theta}\hat\theta f(\hat\theta\mid\underline\tau)\,d\hat\theta-p(\underline\tau)\bigl[1-F(p(\underline\tau)\mid\underline\tau)\bigr]+\underline\theta q^*(\underline\tau,\underline\theta).

The goal asserts that this mechanism is incentive-compatible, individually rational and optimal. It also characterizes all optimal mechanisms: an incentive-compatible, individually rational mechanism is optimal if and only if $q=q^*$ almost everywhere off $\{\psi=0\}$ and $U(\underline\tau)=0$ . When $\{\psi=0\}$ is null, this becomes $q=q^*$ and $t=t^*$ almost everywhere.

Milestones

The path to the goal, in the book's order:

the dynamic revelation principle (Proposition 11.1);
the reduction of incentive compatibility to two families of inequalities (Proposition 11.2);
the ex post characterization (Proposition 11.3);
monotonicity and absolute continuity of $U$ (Lemma 11.1);
the envelope formula $U'(\tau)=-\int q(\tau,\hat\theta)\,\partial F(\hat\theta\mid\tau)/\partial\tau\,d\hat\theta$ (Proposition 11.4);
the transfer formula (Proposition 11.5);
sufficiency of monotone allocation rules (Proposition 11.6);
individual rationality at $\underline\tau$ (Proposition 11.7).

Three extensions follow. Propositions 11.9 and 11.10 show that the privacy of the additional information $\gamma=F(\theta\mid\tau)$ costs the seller nothing. Proposition 11.11 gives the optimal mechanism with several buyers. Proposition 11.12 shows that with dynamic allocations and a fixed valuation, repeating the static posted price is optimal.

Significance

The result gives a practical rule: sell an option. Ex ante type $\tau$ pays a fee $t_0(\tau)$ for the right to buy later at the exercise price $p(\tau)$ , and $p$ decreases in $\tau$ . This explains refund and cancellation menus in advance-purchase markets. Proposition 11.10 adds that information the buyer receives after contracting generates no rents under Assumption 11.1. A seller therefore gains from contracting early and from disclosing information after contracting. Proposition 11.12 shows that, under full commitment, a monopolist gains nothing from responding to past purchases.

On the formal side, the results are proved in the literature and in the book, but none of them is machine-checked. The mission produces a verified envelope theorem in a two-dimensional type space where incentive compatibility does not imply monotonicity. It also produces a verified revenue-equivalence formula for sequential mechanisms, and the first verified optimal-mechanism results with dynamic information.

Difficulty

The static argument of Chapter 2 does not carry over directly. Incentive compatibility with respect to $\tau$ does not make $q$ increasing in $\tau$ . The buyer's first-period utility is an expectation over a whole schedule $q(\tau',\cdot)$ , so single crossing has no bite. The characterization therefore splits into necessary conditions (the envelope formula in $\tau$ , which needs Lipschitz continuity of $U$ from the bound $K$ ) and a sufficient condition (monotonicity in both arguments, via first-order stochastic dominance), and the two meet only under Assumption 11.1.

Definition 11.2(ii) quantifies over all off-path reporting functions. The revelation principle does not remove them, so Proposition 11.2 is needed before any envelope argument applies.

Pointwise maximization of the virtual surplus pins down $q$ only where $\psi\ne0$ and only almost everywhere. The optimal mechanism is therefore not unique in the pointwise sense the page states.

Formalization scope

Representation. $F(\theta\mid\tau)$ is F θ τ and $q(\tau,\theta)$ is q τ θ. Functions are total on $\mathbb R$ or $\mathbb R^2$ , and conditions quantify over the type intervals only. $\partial F/\partial\tau$ and $\partial f/\partial\tau$ are fields pinned by HasDerivWithinAt on $[\underline\tau,\bar\tau]$ .
Measurability. The book omits all measurability. Here the densities are jointly measurable, mechanisms are admissible (measurable on the type rectangle, $q\in[0,1]$ ), and reporting functions are measurable. In the observable- $\gamma$ model each $\tilde t(\tau,\cdot)$ is integrable on $[0,1]$ , and in the several-buyer model each payment $t_i$ is integrable against the distribution of the type profile, so that expected utilities and expected revenue are genuine integrals.
Revenue and a.e. Revenue is the integral of $t$ against the joint law with density $g(\tau)f(\theta\mid\tau)$ , and "almost everywhere" refers to that law.
Corrected necessity. The page's pointwise "if and only if" in Propositions 11.8 and 11.11 is corrected. The explicit optimal mechanism is kept, with the formulas (11.10), (11.11), (11.12) and $t_0$ of Proposition 11.5. Necessity is stated almost everywhere and off $\{\psi=0\}$ , and, for several buyers, off ties between virtual valuations.
Regularity. Propositions 11.9 and 11.10 assume $f$ and $\partial F/\partial\tau$ continuous in $(\tau,\theta)$ , the regularity the book invokes on p.217 to differentiate $F^{-1}(\gamma\mid\tau)$ .
Exercise price. $p(\tau)$ is the infimum of $\{\hat\theta\mid\psi(\tau,\hat\theta)\ge0\}$ .

Ruled out. Stating only that the cutoff mechanism is incentive-compatible and individually rational, or only that it beats posted prices, would trivialize the goal. The goal asserts optimality among all admissible incentive-compatible, individually rational sequential mechanisms with randomized allocations, together with the explicit fee $t_0$ and (11.12).

Infrastructure. A complete development needs envelope theorems for suprema of equi-differentiable families, integration by parts with absolutely continuous functions, differentiation under the integral sign, and change of variables $\gamma=F(\theta\mid\tau)$ . The single-buyer lemmas (Propositions 11.2–11.7) are reusable for the multi-buyer case through the interim mechanism $(Q_i,T_i)$ . Proofs of any milestone, and sorry-free lemmas on the definitions, are welcome.

Selected references

D. Krähmer and R. Strausz, Dynamic Mechanism Design, Chapter 11 in T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
P. Courty and H. Li, Sequential Screening, Review of Economic Studies 67 (2000) 697–717. https://doi.org/10.1111/1467-937X.00150
P. Eső and B. Szentes, Optimal Information Disclosure in Auctions and the Handicap Auction, Review of Economic Studies 74 (2007) 705–731. https://doi.org/10.1111/j.1467-937X.2007.00438.x
D. P. Baron and D. Besanko, Regulation and Information in a Continuing Relationship, Information Economics and Policy 1 (1984) 267–302.

18 thms2 active usersReviewed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

Real-Time Optimization of Personalized Assortments: Inventory Balancing Is α_cmin(Ψ)-CompetitiveResearch Paper

Motivation

Online retailers choose, customer by customer, which products to display. The customer's type (location, history, device) is revealed on arrival. Inventories are finite and are not replenished during the selling season. A seller who shows every customer the currently most profitable products can sell out a product early and leave nothing for later customers who would have bought only that product. Golrezaei, Nazerzadeh and Rusmevichientong (Management Science 60(6), 2014) studied this online personalized assortment problem with no assumption on how customer types arrive. They showed that a simple family of index policies, inventory balancing, earns a guaranteed fraction of a clairvoyant benchmark on every arrival sequence.

The result belongs to a line of worst-case guarantees for online allocation with budgets. The $1-1/e$ guarantee for online $b$ -matching of Kalyanasundaram and Pruhs (TCS 2000) was extended to the AdWords problem by Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007), whose guarantee holds as the budgets grow large. Buchbinder, Jain and Naor (ESA 2007) recast that analysis in primal–dual form. Golrezaei et al. extend the setting from "assign one item" to "offer a set, and let the customer choose according to a general choice model".

Setting

A firm sells $n\ge1$ products. Product $i$ earns revenue $r_i>0$ per unit and has initial inventory $c_i\in\{1,2,\dots\}$ . Write $c_{\min}=\min_i c_i$ . The firm may offer any assortment in a family $\mathcal S$ of feasible assortments, and offering nothing is always allowed ( $\emptyset\in\mathcal S$ ). A customer of type $z$ who is offered $S$ buys product $i\in S$ with probability $\varphi^z_i(S)$ and buys nothing otherwise. Each customer buys at most one product. The choice models satisfy substitutability (Assumption 1): adding a product $j$ to a feasible assortment never raises the purchase probability $\varphi^z_i$ of another product $i\ne j$ .

A penalty function is an increasing $\Psi:[0,1]\to[0,1]$ with $\Psi(0)=0$ and $\Psi(1)=1$ . Let $I^{t-1}_i$ be the remaining inventory of product $i$ when the customer of period $t$ , of type $z_t$ , arrives. The inventory-balancing algorithm offers

S^t\in\arg\max_{S\in\mathcal S}\ \sum_{i\in S}\Psi\!\left(I^{t-1}_i/c_i\right) r_i\,\varphi^{z_t}_i(S),

breaking ties by the fewest products. A sale decrements the inventory by one, and $I^t_i=\max\{I^{t-1}_i-Q^t_i,0\}$ , where $Q^t_i$ indicates a purchase of $i$ . The expected revenue over the horizon is $\mathrm{Rev}$ .

The benchmark is the linear program $\mathrm{Primal}(\{z_t\}_{t=1}^T)$ . It maximizes $\sum_t\sum_{S\in\mathcal S}\sum_i r_i\varphi^{z_t}_i(S)\,y^t(S)$ subject to the expected capacity constraints $\sum_t\sum_S\varphi^{z_t}_i(S)y^t(S)\le c_i$ , with $y^t(\cdot)$ a probability vector on $\mathcal S$ in every period. Its value upper-bounds the expected revenue of every online algorithm, including one that knows the whole sequence in advance.

Formalization targets

Goal: Theorem 1

For every horizon $T$ , every sequence of types $z_1,\dots,z_T$ and every feasible solution $y$ of $\mathrm{Primal}(\{z_t\})$ , if $\Psi$ is in addition concave and twice differentiable, then

\mathrm{Rev}\;\ge\;\alpha_{c_{\min}}(\Psi)\sum_{t=1}^T\sum_{S\in\mathcal S}\sum_{i=1}^n r_i\,\varphi^{z_t}_i(S)\,y^t(S),\qquad \alpha_{c_{\min}}(\Psi)=\min_{x\in[0,1-1/c_{\min}]}\frac{1-x}{\frac1{c_{\min}}+1-\Psi(x)+\int_{x+1/c_{\min}}^{1}\Psi(y)\,dy}.

The constant is the paper's, exactly as printed. It depends only on $c_{\min}$ and $\Psi$ .

Milestones

Lemma 5. Both parts are milestones. First, $x\mapsto(1-x)/(2-x-\Psi(x))$ is increasing on $[0,1)$ . Second, $C\mapsto1/C+\int_{a+1/C}^1\Psi$ is decreasing on $[1/(1-a),\infty)$ for $a\in[0,1)$ .
Riemann-sum bound. $\frac1c\sum_{k=I+1}^{c}\Psi(k/c)\le\frac1c+\int_{(I+1)/c}^1\Psi$ for integers $0\le I<c$ .
Telescoping. For an inventory path that starts at $c$ and falls by $0$ or $1$ per step, $\sum_t\Psi(I^{t-1}/c)(I^{t-1}-I^t)=\sum_{k=I^T+1}^{c}\Psi(k/c)$ .
Dual feasibility. Along every non-increasing inventory path, the pair $\theta_i=r_i(1-\Psi(I^T_i/c_i))$ , $\lambda^t=\sum_{i\in S^t}r_i\Psi(I^{t-1}_i/c_i)\varphi^{z_t}_i(S^t)$ is feasible for the dual LP.
Expected dual value. $\mathbb E[\sum_t\lambda^t]=\mathbb E[\sum_i r_i\sum_{k=I^T_i+1}^{c_i}\Psi(k/c_i)]$ .
Expected revenue. $\mathrm{Rev}=\mathbb E[\sum_i r_i(c_i-I^T_i)]$ .
Weak-duality bound. $\mathrm{Primal}\le\mathbb E[\sum_i r_i(\sum_{k=I^T_i+1}^{c_i}\Psi(k/c_i)+c_i(1-\Psi(I^T_i/c_i)))]$ .
Lemma 2. Inventory balancing never offers a product with zero inventory, when $\mathcal S$ is closed under removing a product.

Three further statements are included as plain items. The first is the reduction to $\alpha_{c_{\min}}$ : for $C\ge c_{\min}$ and $x\in[0,1-1/C]$ , the ratio with $C$ in place of $c_{\min}$ is at least $\alpha_{c_{\min}}(\Psi)$ (the two-case argument that closes §A.3). The second is weak duality for the Primal/Dual pair. The third is a pair of evaluations of the formula. The evaluations are $\alpha_{c_{\min}}(x)=1/2$ (Corollary 1) and $\alpha_{c_{\min}}\big(\tfrac{e}{e-1}(1-e^{-x})\big)\to1-1/e$ (Theorem 2, first sentence).

Significance

Theorem 1 separates the guarantee from the horizon, the arrival process and the choice model. The only inputs are the smallest initial inventory and the penalty function. With the linear penalty $\Psi(x)=x$ the guarantee is $1/2$ . With the exponential penalty it approaches $1-1/e$ as $c_{\min}\to\infty$ . The paper shows that no online algorithm does better in that limit, so the exponential penalty is optimal. A myopic seller that ignores inventory can do no better than $1/2$ (Example 1 of the paper). Because the guarantee holds for every choice model satisfying substitutability, it covers the multinomial logit, nested logit and any random-utility model at once.

The theorem is proved on paper, with a complete argument in the published article. It is not formalized anywhere to our knowledge. A formalization would check an argument that combines three strands: linear-programming duality, a stochastic inventory process, and a real-analysis optimization over $x$ . It would also supply a reusable, finite-sum model of online assortment under general choice models, together with a machine-checked form of the competitive-ratio formula that later results (e.g. the $1-1/e$ limit) can build on.

Difficulty

The algorithm is online: it chooses without knowing future types. The benchmark is clairvoyant and respects inventory only in expectation. On a single arrival sequence the two can allocate the same product to entirely different customers, as Example 1 of the paper shows. So the natural first idea, comparing the algorithm with the LP period by period, fails: the LP may sell a product early that the algorithm correctly saves, and the reverse. A valid comparison has to hold across the whole horizon for an adversarial sequence, with the algorithm's revenue an expectation over a random, history-dependent inventory path. The constant adds a second, analytic difficulty. The formula $\alpha_{c_{\min}}(\Psi)$ has an integral where the process has a discrete sum, and a minimum whose range depends on $c_{\min}$ . Yet every product, with its own inventory $c_i\ge c_{\min}$ , has to be accounted for by that single constant.

Formalization scope

Finite, discrete model. Products are Fin n with 0 < n. Assortments are finsets and $\mathcal S$ is a finite family containing $\emptyset$ . Inventories are natural numbers, and truncated subtraction implements $\max\{I-1,0\}$ . Customer types form an arbitrary type, and the arrival sequence is a function Fin T → Z.
Expectations are finite sums. The inventory law is not a parameter. The expectation $\mathbb E[f(I^t)]$ is defined by recursion from the point mass at $c$ , conditioning on the previous period. No measure theory is involved.
Revenue counts actual sales only. A pick of a stocked-out product earns nothing.
The algorithm is any selection rule meeting the specification. In every state it offers a maximizer of the index in $\mathcal S$ with the fewest products among maximizers. The goal holds for every such rule.
Penalty function. Every penalty function satisfies the standing assumptions of §3 ( $\Psi$ maps $[0,1]$ to $[0,1]$ , is non-strictly increasing, and has $\Psi(0)=0$ , $\Psi(1)=1$ ). Theorem 1 adds concavity on $[0,1]$ and twice differentiability, encoded as differentiability of $\Psi$ and of its derivative within $[0,1]$ .
$\alpha_{c_{\min}}(\Psi)$ is the infimum of the ratio over $[0,1-1/c_{\min}]$ , a nonempty set bounded below by $0$ . It equals the paper's minimum.
Ruling out the trivial reading. The competitive ratio is stated in multiplied form, $\alpha\cdot\mathrm{Primal}(y)\le\mathrm{Rev}$ for every feasible $y$ , rather than as a ratio: with $0/0=0$ in Lean the ratio form would be false whenever the LP value is $0$ . The goal is not vacuous: $\Psi(x)=x$ meets every hypothesis, offering $\emptyset$ is always primal feasible, and a selection rule always exists.
Additions relative to the page. Lemma 5 is stated on $[0,1)$ and for $a<1$ , because the paper's closed endpoints are $0/0$ and $1/0$ . The reduction step states $C\ge c_{\min}$ , which the paper leaves implicit. Lemma 2 assumes $\mathcal S$ closed under removing a product, without which it is false; the goal does not assume this. The dual feasibility milestone asserts every dual constraint, not only the one at $S=S^t$ that the paper displays.
Infrastructure. A complete development needs finite-sum Markov-chain expectations, interval integrals of monotone functions, and elementary calculus for concave functions. The model definitions (choice model, Primal/Dual, selection rule, inventory process) are reusable for other online assortment and revenue-management results. Contributions of general lemmas on the recursive expectation operator are welcome.

Selected references

N. Golrezaei, H. Nazerzadeh, P. Rusmevichientong, Real-Time Optimization of Personalized Assortments, Management Science 60(6):1532–1551, 2014. https://doi.org/10.1287/mnsc.2014.1939
B. Kalyanasundaram, K. Pruhs, An optimal deterministic algorithm for online b-matching, Theoretical Computer Science 233:319–325, 2000. https://doi.org/10.1016/S0304-3975(99)00140-1
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
N. Buchbinder, K. Jain, J. Naor, Online primal-dual algorithms for maximizing ad-auctions revenue, ESA 2007, LNCS 4698. https://doi.org/10.1007/978-3-540-75520-3_24
K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147

14 thms2 active usersReviewed