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

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case 2: General Demand: Sym-k-Concave Profit-to-Go, Optimal (s, S, A, p) PolicyResearch Paper

Motivation

A seller with replenishable inventory must decide how much to order and what price to charge before demand is known. A price that increases current revenue can also change the inventory left for later periods; a fixed charge for placing any positive order adds a discontinuity to the decision. Chen and Simchi-Levi study this coordination problem over a finite horizon with backlogging and random, price-dependent demand. Their general-demand result characterizes an optimal order-and-price policy even when a conventional two-threshold ordering rule can fail. The paper gives explicit counterexamples to ordinary $k$ -concavity and to optimality of a standard $(s,S,p)$ policy in this setting (Chen and Simchi-Levi, 2004, §4, Lemmas 3–4).

Setting

There are periods $t=1,\ldots,T$ . At the start of period $t$ , the firm has inventory $x$ , which may be negative because unmet demand is backlogged. It may order to any level $y\ge x$ . If $y>x$ , it pays a fixed ordering cost $k$ as well as a variable cost $c_t(y-x)$ . After ordering it chooses an expected demand level $d$ in a closed interval $[\underline d_t,\overline d_t]$ . The corresponding price is $P_t(d)$ , the inverse of the period's decreasing demand curve, and expected revenue is $R_t(d)=dP_t(d)$ .

Actual demand is $\alpha_t d+\beta_t$ . The random pair $(\alpha_t,\beta_t)$ has a period-dependent law $\mu_t$ , with $\mathbb E[\alpha_t]=1$ and $\mathbb E[\beta_t]=0$ . No sign restriction is placed on $\alpha_t$ in the paper's general model. The inventory after demand is $y-\alpha_t d-\beta_t$ , incurring a convex holding or backlog cost $h_t$ and entering the next period. The paper assumes the random perturbations are independent across periods. Its Bellman equation uses their individual period laws (Chen and Simchi-Levi, 2004, §2, Assumptions 1–5).

The profit-to-go $v_t(x)$ starts with $v_{T+1}(x)=0$ . For a post-order inventory $y$ and expected demand $d$ , write

g_t(y,d)=R_t(d)-c_ty+\mathbb E[-h_t(y-\alpha_t d-\beta_t)+v_{t+1}(y-\alpha_t d-\beta_t)].

The firm maximizes $g_t(y,d)$ over admissible $d$ and then maximizes the resulting value, less the fixed ordering charge, over $y\ge x$ . This defines $v_t(x)$ by equation (2) of the paper. A symmetrically $k$ -convex real function $f$ satisfies

f((1-\lambda)x_0+\lambda x_1)\le(1-\lambda)f(x_0)+\lambda f(x_1)+\max\{\lambda,1-\lambda\}k

for every $x_0,x_1\in\mathbb R$ and $\lambda\in[0,1]$ . A function is symmetrically $k$ -concave when its negative is symmetrically $k$ -convex. This is Definition 4.1, equation (8), and preserves the symmetry between the two endpoint inventories (Chen and Simchi-Levi, 2004, p. 891).

Formalization targets

The goal is Theorem 4.1(c)–(d). If $G_t(y)=\max_{d\in[\underline d_t,\overline d_t]}g_t(y,d)$ , then for every period

G_t\text{ and }v_t\text{ are symmetrically }k\text{-concave}.

There are thresholds $s_t\le S_t$ and a possibly empty set $A_t\subseteq[s_t,(s_t+S_t)/2]$ . An optimal policy orders to $S_t$ if $x<s_t$ or $x\in A_t$ , and places no order otherwise. It chooses the maximizing expected demand for the resulting post-order level. In particular, all states that order to $S_t$ can use the same demand level $d_t(S_t)$ and hence the same price $P_t(d_t(S_t))$ .

The milestones state the preceding polynomial growth and continuity assertions from Theorem 4.1(a)–(b), the threshold structure of Lemma 5(d), and the named steps in the proof on p. 892. The link from the paper's earlier $k$ -convexity to symmetric $k$ -convexity is also included. These targets preserve the paper's general demand law rather than restricting it to the additive case.

Significance

The theorem describes an optimal decision at every inventory level under random price-dependent demand. The exceptional set $A_t$ records states where ordering to $S_t$ is optimal inside the interval where a single reorder threshold need not describe all optimal actions. Thus the result retains a concise policy description while allowing the behavior exhibited by the paper's counterexamples (Chen and Simchi-Levi, 2004, §4).

Formalizing the result requires a reusable account of symmetric $k$ -convexity, a fixed-cost ordering envelope, and a finite-horizon Bellman recursion with real-valued expectations. The source proves Theorem 4.1 on paper. This mission poses its statements as Lean goals; the theorem files currently contain sorry and therefore are not machine-checked proofs. The published platform definition BertsekasKConvex supplies the earlier notion from Definition 2.1, so the bridge to Definition 4.1 can be stated without duplicating it.

Difficulty

In the additive-demand case, a maximizing expected-demand choice can be selected so that post-demand inventory changes monotonically with the initial inventory. For general demand $\alpha_t d+\beta_t$ , that monotonicity can fail: the random multiplier changes how a pricing choice moves the next inventory state. The earlier ordered-chord $k$ -concavity argument therefore does not carry over unchanged. A second issue is the fixed ordering charge. It creates ties between ordering and not ordering, so the policy region can include isolated or noninterval states within $[s_t,(s_t+S_t)/2]$ . The statement must assert Bellman optimality at every $x$ , including those ties, rather than only the geometry of $A_t$ (Chen and Simchi-Levi, 2004, pp. 891–892).

Formalization scope

The Lean model uses expected demand $d$ as the decision variable and obtains price from $P_t(d)$ , matching the paper's reformulation after Assumption 5. The admissible demand interval is nonempty. Periods are natural numbers $1,\ldots,T$ , with $T>0$ and terminal value $v_{T+1}=0$ . Random demand is integrated against a probability measure on $\mathbb R\times\mathbb R$ . The first moments and the paper's demand moment condition are explicit; holding-cost and continuation integrability prevent a nonintegrable real integral from acquiring Lean's default zero value. The paper's $O(|y|^\rho)$ statements are encoded by constants multiplying $1+|y|^\rho$ .

The formal assumptions include $k\ge0$ and $c_t\ge0$ , and set $c_{T+1}=0$ where the paper's Assumption 3 uses that otherwise undefined terminal coefficient. The latter two restrictions make the printed finite-horizon claim valid under its cost interpretation; they are stated rather than silently supplied. The paper assumes temporal independence, while the formal Bellman recursion starts from the marginal laws and so needs no separate joint process. The paper's $(y,p)$ in Theorem 4.1(b) is expressed as $(y,d)$ through the continuous one-to-one price–expected-demand correspondence. The model places no positivity condition on $\alpha_t$ .

The optimized demand value and ordering value are real suprema. The statements include maximizing choices and Bellman attainment; a proof cannot rely on a default value for an empty or unbounded supremum. The goal requires an actual optimal action for every inventory state. Contributions that establish integrability, continuity, coercivity, symmetric convexity preservation, or the ordering-envelope structure are useful beyond this mission.

Selected references

Xin Chen and David Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. DOI: 10.1287/opre.1040.0127.

12 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs: Fully-Supported Problems Attain the Binomial Violation Tail ExactlyResearch Paper

Motivation

Many design problems in control, finance and engineering are convex programs whose constraints depend on an uncertain parameter $\delta$ : a solution must satisfy $x\in\mathcal X_\delta$ for every $\delta$ in a possibly infinite set $\Delta$ . Enforcing all constraints (robust optimization) is often intractable or overly conservative. The scenario approach draws $N$ independent samples of $\delta$ , solves the convex program with those $N$ constraints only, and asks how likely it is that the resulting solution violates a fresh constraint. The question matters wherever a randomized design is certified by a confidence statement, from robust control to chance-constrained portfolio selection.

Timeline.

Calafiore and Campi (Math. Program. 2005; IEEE TAC 2006) introduced the method and bounded the probability that the violation exceeds $\varepsilon$ by a quantity of order $\binom Nd(1-\varepsilon)^{N-d}$ . The bound is valid but loose.
Campi and Garatti (SIAM J. Optim. 2008, this mission's source) proved the bound $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for every convex problem satisfying existence and uniqueness of solutions. They showed it is attained with equality by every fully-supported problem, so it cannot be improved without further assumptions.
Later work extended the result to non-unique solutions, constraint removal, and non-convex decisions (Campi and Garatti, Introduction to the Scenario Approach, SIAM 2018).

Setting

Let $(\Delta,\mathcal D,\mathbb P)$ be a probability space, $c\in\mathbb R^d$ with $d\ge1$ , and let $\mathcal X\subseteq\mathbb R^d$ and $\mathcal X_\delta\subseteq\mathbb R^d$ ( $\delta\in\Delta$ ) be convex closed sets. The violation probability of a point $x$ is

V(x)=\mathbb P\{\delta\in\Delta:\ x\notin\mathcal X_\delta\}.

For a multi-extraction $(\delta^{(1)},\dots,\delta^{(m)})\in\Delta^m$ , the program $P_m$ minimises $c^\top x$ over $x\in\mathcal X\cap\bigcap_{i=1}^m\mathcal X_{\delta^{(i)}}$ . It is assumed that every $P_m$ has a unique solution $x^*_m$ . A constraint $\delta^{(r)}$ is a support constraint of $P_m$ if its removal changes the solution. A convex $P_m$ has at most $d$ support constraints (Proposition 2.2). The problem is fully-supported if, for every $m\ge d$ , the program $P_m$ built from $m$ independent samples has exactly $d$ support constraints with $\mathbb P^m$ -probability one.

Two further objects carry the argument. For $\mathcal I\subseteq\{1,\dots,m\}$ of cardinality $d$ , $S_{\mathcal I}$ is the set of multi-extractions whose support constraints have exactly the indexes in $\mathcal I$ . The violation law is

F(\alpha)=\mathbb P^d\{V(x^*_d)\le\alpha\},

the distribution of the violation of the solution built from $d$ samples.

Formalization targets

Goal: Theorem 2.4, equation (2.3)

For a fully-supported problem, every $N\ge d$ and every $\varepsilon\in[0,1]$ ,

\mathbb P^N\{V(x^*_N)>\varepsilon\}=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.

Milestones (PART 1 of §3)

Proposition 2.2: at most $d$ support constraints.
$S_{\bar{\mathcal I}}\subseteq\widetilde S_{\bar{\mathcal I}}$ for $\bar{\mathcal I}=\{1,\dots,d\}$ , where $\widetilde S_{\bar{\mathcal I}}$ is the set where $\delta^{(d+1)},\dots,\delta^{(m)}$ are not violated by the solution generated by $\delta^{(1)},\dots,\delta^{(d)}$ ; and $\widetilde S_{\bar{\mathcal I}}\subseteq S_{\bar{\mathcal I}}$ up to a probability-zero set.
(3.3): $\mathbb P^m\{S_{\mathcal I}\}=\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)$ for every $\mathcal I$ of cardinality $d$ .
(3.4): $\binom md\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)=1$ for all $m\ge d$ .
Moment uniqueness: $F(\alpha)=\alpha^d$ is the only distribution on $[0,1]$ satisfying (3.4).
(3.2): $F(\alpha)=\alpha^d$ .
Partition chain: $\mathbb P^N\{V(x^*_N)>\varepsilon\}=\binom Nd\int_{(\varepsilon,1]}(1-\alpha)^{N-d}F(\mathrm d\alpha)$ .
Integration by parts: $\binom Nd\int_\varepsilon^1(1-\alpha)^{N-d}\,d\,\alpha^{d-1}\,\mathrm d\alpha=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ .

Significance

The result. Equation (2.3) shows that the scenario bound (2.2) is tight: no bound that depends only on $N$ , $d$ and $\varepsilon$ can be smaller, because a fully-supported problem attains it. The distribution of $V(x^*_N)$ is then a Beta law, $\mathbb P^N\{V(x^*_N)\le\varepsilon\}$ being the probability that a $\mathrm{Binomial}(N,\varepsilon)$ variable is at least $d$ , the same for every fully-supported problem. This is what fixes the sample sizes used in practice: $N$ is chosen so that the binomial tail is below a confidence level $\beta$ . Fact (3.2), that $V(x^*_d)$ has distribution function $\alpha^d$ whatever the problem, is a distribution-free statement of independent interest.

Formalizing it. The result is proved in the source. As far as is known it has no machine-checked proof. The goal statement is already posed on the platform, and this mission supplies the paper's proof structure as milestones. Two milestones are reusable outside the scenario approach: the uniqueness of a distribution on $[0,1]$ given the moments $\int(1-\alpha)^k\,\mathrm dF=1/\binom{d+k}d$ , and the incomplete-beta identity for binomial tails.

Difficulty

The obvious route would compute the law of $V(x^*_N)$ directly, but it depends on the geometry of the constraints. The paper never computes it. It obtains the law of $V(x^*_d)$ only implicitly, through the infinite family of identities (3.4), and recovers it by a uniqueness theorem for moment problems. Two points need care. First, full support holds only almost surely: duplicated samples, for instance, produce programs with fewer than $d$ support constraints, so every set identity holds only up to null sets. Second, the claim that removing a non-support constraint keeps the first $d$ constraints as the only support constraints uses Proposition 2.2. Two identical non-support constraints show that a constraint can become a support constraint after another is removed, unless the count is bounded by $d$ .

Formalization scope

Goal. The goal is the already-posed platform statement ScenarioApproach.Generalization.violation_tail_eq_binomial_sum_of_fullySupported (theorem id cffaa932-832c-42ca-9e81-1848ffab7e34), referenced as it stands and not restated. Proposition 2.2 is the platform statement card_support_constraints_le_dim (f70e8aa3-…). This mission adds the PART 1 steps as milestones under ScenarioExact.PartOne.

Representation. Decisions are vectors in EuclideanSpace ℝ (Fin d). A multi-extraction is ω : Fin m → Δ, with 0-based indexes, so $\bar{\mathcal I}$ is $\{i : i<d\}$ and " $\delta^{(d+1)},\dots,\delta^{(m)}$ " are the indexes $j\ge d$ . $\mathbb P^m$ is Measure.pi (fun _ : Fin m => P). $V$ , the feasible set, solutions, support constraints and full support are the published definitions violation, feasibleSet, IsSolution, IsSupportConstraint and FullySupported. A support constraint is one whose removal admits a feasible point of strictly smaller cost, which under uniqueness is the paper's "its removal changes the solution". Full support is almost sure, not pointwise.

Hypotheses made explicit. Assumption 1 is entered as existence and uniqueness of the solution for every number of constraints and every sample, together with a family of solution maps θs k, each assumed to solve $P_k$ and to be measurable. Under uniqueness, θs N is the goal's solution map. The paper's "measurability ... is assumed for granted" (p. 4) is replaced by joint measurability of $\{(x,\delta):x\in\mathcal X_\delta\}$ and measurability of the solution maps, the same two hypotheses as the goal. No set $S_{\mathcal I}$ is assumed measurable. The nonempty-interior clause of Assumption 1 is unused in PART 1 and is not assumed, so the milestones compose with the goal.

Conventions. $F$ is the push-forward measure violationLaw on $\mathbb R$ , with $F(\alpha)$ = violationLaw … (Set.Iic α). Integrals against $F$ are lower Lebesgue integrals of nonnegative integrands, as extended nonnegative reals: over $[0,1]$ for $\int_0^1$ , and over $(\varepsilon,1]$ for $\int_\varepsilon^1$ in the partition chain, since that integral comes from the event $V>\varepsilon$ . The integration-by-parts identity is a real interval integral. Ranges are $1\le d$ , $d\le m$ , $d\le N$ and $0\le\varepsilon\le1$ .

Ruled out. A pointwise "exactly $d$ support constraints for every sample" would be unsatisfiable for many problems (repeated samples) and would trivialise the probabilistic content, so it is not used. Assuming measurability of the event $\{V(x^*_N)>\varepsilon\}$ or of $S_{\mathcal I}$ , or the identity $\mathbb P^m\{S_{\mathcal I}\}=\mathbb P^m\{\widetilde S_{\mathcal I}\}$ , as a hypothesis would assume part of the conclusion, so none of these is a hypothesis.

Infrastructure. A complete development needs: the support-constraint count (Proposition 2.2, a Helly-type argument), invariance of product measures under coordinate permutations, the change-of-variables formula for push-forward measures, the Hausdorff moment uniqueness theorem on $[0,1]$ , and the binomial–incomplete-beta identity. The last two are general results, and contributions of them are welcome independently.

Selected references

M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19(3) (2008) 1211–1230. https://doi.org/10.1137/07069821X
G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Math. Program. 102 (2005) 25–46. https://doi.org/10.1007/s10107-003-0499-y
G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Trans. Automat. Control 51(5) (2006) 742–753. https://doi.org/10.1109/TAC.2006.875041
M. C. Campi, S. Garatti, Introduction to the Scenario Approach, SIAM, 2018. https://doi.org/10.1137/1.9781611975444
A. N. Shiryaev, Probability, 2nd ed., Springer, 1996, Chapter II, §12. https://doi.org/10.1007/978-1-4757-2539-1

14 thms3 active usersReviewed

Completed

Combinatorics Convex Optimization Optimization+1·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVII: Goemans–Williamson Rounding of the MAXCUT SDP Relaxation Has Expected Value at Least 0.878 Times the Maximum CutTextbook

Motivation

MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor $1/2$ was essentially the best known.

Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least $0.878$ times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant $2/\pi$ .

This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.

Setting

Let $n\ge 0$ and let $A\in\mathbb R^{n\times n}$ be a symmetric matrix with non-negative entries; $A_{i,j}$ is the weight between points $i$ and $j$ . The graph Laplacian is $L=D-A$ , where $D$ is the diagonal matrix with entries $\sum_{j=1}^n A_{i,j}$ . For $x\in\{-1,1\}^n$ the vector $x$ encodes a partition, and MAXCUT is (6.7)

\max_{x\in\{-1,1\}^n} x^\top L x .

Write $\langle M,X\rangle=\operatorname{Tr}(M^\top X)$ for the Frobenius inner product and $\mathbb S^n_+$ for the symmetric positive semidefinite matrices. Since $x^\top Lx=\langle L,xx^\top\rangle$ and $xx^\top\in\mathbb S^n_+$ has unit diagonal, MAXCUT is bounded above by the SDP relaxation

\max\bigl\{\langle L,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1,\ i\in[n]\bigr\}.

A solution $\Sigma$ of the relaxation is any feasible matrix attaining this maximum. The rounding draws $\xi\sim\mathcal N(0,\Sigma)$ , a centered Gaussian vector with covariance $\Sigma$ , and outputs $\zeta=\operatorname{sign}(\xi)\in\{-1,1\}^n$ coordinatewise.

Formalization targets

Goal: Theorem 6.11 (Goemans–Williamson)

For $A$ symmetric with non-negative entries, $L=D-A$ , $\Sigma$ any solution of the relaxation, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$ :

\mathbb E\,\zeta^\top L\zeta\ \ge\ 0.878\max_{x\in\{-1,1\}^n}x^\top Lx.

Milestones

Bounded entries. If $\Sigma\in\mathbb S^n_+$ and $\Sigma_{i,i}=1$ , then $|\Sigma_{i,j}|\le 1$ (remark in the proof of Lemma 6.12).
Lemma 6.12 (Sheppard's formula). If $\xi\sim\mathcal N(0,\Sigma)$ with $\Sigma_{i,i}=1$ and $\zeta=\operatorname{sign}(\xi)$ , then $\mathbb E\,\zeta_i\zeta_j=\frac{2}{\pi}\arcsin(\Sigma_{i,j})$ .
Inequality (6.8). $1-\frac{2}{\pi}\arcsin(t)\ge 0.878(1-t)$ for all $t\in[-1,1]$ .
Relaxation inequality. $\max_{x}x^\top Lx=\max_x\langle L,xx^\top\rangle\le\langle L,\Sigma\rangle$ for every solution $\Sigma$ .

The separately stated Laplacian identity on p. 346 is also included as a theorem item: if $X_{i,i}=1$ for all $i$ , then $\langle L,X\rangle=\sum_{i,j}A_{i,j}(1-X_{i,j})$ ; for $x\in\{-1,1\}^n$ , $x^\top Lx=\sum_{i,j}A_{i,j}(1-x_ix_j)$ .

Companion: Theorem 6.13 (Nesterov)

For $B\in\mathbb S^n_+$ , $\Sigma$ a solution of $\max\{\langle B,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1\}$ , $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$ :

\mathbb E\,\zeta^\top B\zeta\ \ge\ \frac{2}{\pi}\max_{x\in\{-1,1\}^n}x^\top Bx.

Significance

The result. Theorem 6.11 is a polynomial-time randomized $0.878$ -approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to $0.878$ times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.

Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of $\Sigma$ . All three are reusable.

Difficulty

The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair $(\xi_i,\xi_j)$ has the law of $(\langle V_i,\varepsilon\rangle,\langle V_j,\varepsilon\rangle)$ for a standard Gaussian $\varepsilon$ , and then computing an angular measure in the plane, including the degenerate cases $\Sigma_{i,j}=\pm1$ , where the pair is supported on a line. A density-based argument fails there, because $\mathcal N(0,\Sigma)$ has no density when $\Sigma$ is singular, and singular solutions of the relaxation occur (for instance $\Sigma=xx^\top$ ). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ( $0.878$ against the true minimum $\approx0.87856$ ), so crude estimates do not suffice near the minimizer $t\approx-0.689$ .

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. $\mathbb S^n_+$ is Matrix.PosSemidef, which includes symmetry, and $\langle M,X\rangle$ is trace (Mᵀ * X).
$\mathcal N(0,\Sigma)$ is Mathlib's ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite $\Sigma$ , singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.
The sign is $\{-1,1\}$ -valued: $\operatorname{sign}(r)=1$ for $r\ge0$ and $-1$ for $r<0$ . Mathlib's Real.sign would give $\operatorname{sign}(0)=0$ , which takes $\zeta$ out of $\{-1,1\}^n$ ; the two agree almost surely because $\Sigma_{i,i}=1$ .
The maximum over the hypercube is a finite maximum (Finset.sup') over the $2^n$ Boolean vectors read as $\pm1$ vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.
Standing hypotheses: in Theorem 6.11, $A$ symmetric with non-negative entries (the book's MAXCUT setting); in Lemma 6.12, $\Sigma$ positive semidefinite (implicit in " $\xi\sim\mathcal N(0,\Sigma)$ "); in Theorem 6.13, $B$ positive semidefinite. The identities of milestones 4 and 5 hold for every real matrix $A$ and are stated without hypotheses on $A$ .
Ruled out: tying $\xi$ 's law to anything other than $\Sigma$ , or dropping optimality of $\Sigma$ , would make the goal false or vacuous; here the law is exactly $\mathcal N(0,\Sigma)$ and $\Sigma$ is a maximizer.
Welcome contributions: Sheppard's formula in Mathlib's multivariate Gaussian language, a proof of (6.8), and the Schur product theorem ( $A,B\succeq0\Rightarrow A\circ B\succeq0$ ) used in Theorem 6.13.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6):1115–1145, 1995. doi:10.1145/227683.227684
Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optim. Methods Softw. 9(1–3):141–160, 1998. doi:10.1080/10556789808805690
S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37(1):319–357, 2007. doi:10.1137/S0097539705447372
W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation, Phil. Trans. R. Soc. A 192:101–167, 1899. doi:10.1098/rsta.1899.0003

6 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization+1·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVI: Random Coordinate Descent RCD(γ) on a Strongly Convex Coordinate-Smooth Function Has Rate (1 − 1/κ_γ)^tTextbook

Motivation

When a problem has millions of variables, even one full gradient can be too expensive to compute, while a single partial derivative $\partial f/\partial x_i$ is often cheap: in regularized regression, support vector machines and many structured problems, updating one coordinate costs a small fraction of a full gradient step. Coordinate descent methods exploit this by moving along one coordinate at a time. They are among the oldest optimization schemes and were for a long time analysed only for cyclic orders and only asymptotically.

Nesterov (2012) showed that choosing the coordinate at random, with probabilities depending on the coordinate-wise smoothness constants, gives global, non-asymptotic rates that can beat full gradient descent in total work. This mission formalizes that analysis as presented in §6.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 338–342, and in particular its linear rate for strongly convex functions (Theorem 6.8).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be differentiable, write $\nabla_i f(x)=\frac{\partial f}{\partial x_i}(x)$ and let $e_i$ be the $i$ -th standard basis vector. The function is directionally smooth with constants $\beta_1,\dots,\beta_n>0$ if

|\nabla_i f(x+ue_i)-\nabla_i f(x)|\le\beta_i|u|\qquad\text{for all } i\in[n],\ x\in\mathbb R^n,\ u\in\mathbb R,

equivalently, each one-variable restriction $u\mapsto f(x+ue_i)$ is $\beta_i$ -smooth.

For a real exponent $c$ , the weighted norms are

\|x\|_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{c}x_i^2},\qquad \|x\|^*_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{-c}x_i^2}.

For $\alpha>0$ , $f$ is $\alpha$ -strongly convex w.r.t. a norm $\|\cdot\|$ if $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y$ . The point $x^*$ is a minimizer of $f$ .

For $\gamma\ge0$ , RCD( $\gamma$ ) starts at $x_1\in\mathbb R^n$ and iterates

x_{s+1}=x_s-\frac{1}{\beta_{i_s}}\nabla_{i_s}f(x_s)\,e_{i_s},

where $i_1,i_2,\dots$ are drawn independently from $p_\gamma(i)=\beta_i^\gamma/\sum_{j}\beta_j^\gamma$ . The case $\gamma=0$ is uniform sampling; $\gamma=1$ samples proportionally to $\beta_i$ .

Formalization targets

Goal: Theorem 6.8 (p. 341)

Let $\gamma\ge0$ , let $f$ be $\alpha$ -strongly convex w.r.t. $\|\cdot\|_{[1-\gamma]}$ and directionally smooth with constants $\beta_i$ , and let $\kappa_\gamma=\sum_i\beta_i^\gamma/\alpha$ . Then for every $t\ge0$

\mathbb E f(x_{t+1})-f(x^*)\le\Big(1-\frac{1}{\kappa_\gamma}\Big)^t\big(f(x_1)-f(x^*)\big).

Milestones

Lemma 6.9 (p. 341): for $f$ $\alpha$ -strongly convex w.r.t. any norm, $f(x)-f(x^*)\le\frac{1}{2\alpha}\|\nabla f(x)\|_*^2$ .
One coordinate step (p. 340): $f\big(x-\frac{1}{\beta_i}\nabla_i f(x)e_i\big)-f(x)\le-\frac{1}{2\beta_i}(\nabla_i f(x))^2$ .
Expected decrease (p. 340): $\mathbb E_{i_s}f(x_{s+1})-f(x_s)\le-\frac{1}{2\sum_i\beta_i^\gamma}\big(\|\nabla f(x_s)\|^*_{[1-\gamma]}\big)^2$ .
Lemma 6.9 in the weighted norm (p. 342): $\big(\|\nabla f(x)\|^*_{[1-\gamma]}\big)^2\ge2\alpha(f(x)-f(x^*))$ .
Contraction (pp. 341–342): one step multiplies the expected gap by at most $1-1/\kappa_\gamma$ .

Companion: Theorem 6.7 (pp. 339–340)

For $f$ convex and directionally smooth, and $t\ge2$ ,

\mathbb E f(x_t)-f(x^*)\le\frac{2R_{1-\gamma}^2(x_1)\sum_i\beta_i^\gamma}{t-1},\qquad R_{1-\gamma}(x_1)=\sup_{f(x)\le f(x_1)}\|x-x^*\|_{[1-\gamma]}.

Significance

Theorem 6.8 says random coordinate descent converges linearly, with a rate governed by $\sum_i\beta_i^\gamma/\alpha$ instead of the global smoothness constant. For $\gamma=1$ , directional smoothness implies $f$ is $\beta$ -smooth with $\beta\le\sum_i\beta_i$ , so for functions whose global smoothness constant is of the order of $\sum_i\beta_i$ , RCD(1) attains the accuracy of gradient descent after the same number of iterations (book, p. 340, comparing Theorem 6.7 with Theorem 3.3), while each iteration touches a single coordinate. The same per-step inequalities underlie later accelerated and parallel coordinate methods.

These results are proved in the literature (Nesterov 2012; Bubeck 2015). Their contribution here is a machine-checked version. As far as a search of the Prove2Me catalogue shows, no coordinate descent rate of this kind has been formalized there; a Euclidean-norm special case of Lemma 6.9 exists on the platform as a separate result, but not the arbitrary-norm lemma or the weighted-norm instance used here.

Difficulty

The main obstacle is bookkeeping of the randomness: the per-step inequality holds for each fixed iterate, while the theorem is about the expectation over the whole sequence of draws $i_1,\dots,i_t$ , so the pointwise contraction has to be passed through the tower of conditional expectations. In the strongly convex case this is linear and exact; for Theorem 6.7 the recursion on $\delta_s=\mathbb Ef(x_s)-f(x^*)$ is quadratic, and since $\delta_s$ is an expectation while the gradient norm at $x_s$ is random, the pointwise inequality does not transfer to $\delta_s$ verbatim. A second point is geometric: strong convexity, the dual norm and the sampling distribution must use matching weights ( $\beta_i^{1-\gamma}$ against $\beta_i^{\gamma}$ ), and a mismatch silently changes the constant.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient is an explicit map $g$ with HasGradientAt f (g x) x, so $\nabla_i f(x)=g(x)_i$ . Lemma 6.9 is stated for a finite-dimensional real normed space with the Fréchet derivative and the operator norm as the dual norm.
Powers $\beta_i^c$ are real powers. The theorems assume $n\ge1$ , $\alpha>0$ and $\beta_i>0$ , which the book uses implicitly; $\gamma\ge0$ is the book's.
RCD(γ) is a deterministic function of the drawn coordinates, and the expectation over $t$ independent draws from $p_\gamma$ is the finite sum $\sum_{(i_1,\dots,i_t)\in[n]^t}\prod_s p_\gamma(i_s)\,F(i_1,\dots,i_t)$ . No measure theory or integrability conventions are involved.
The minimizer $x^*$ is assumed to exist, as the book does throughout; its uniqueness, which the book assumes "only for sake of notation", is not used.
In Theorem 6.7 the supremum $R_{1-\gamma}(x_1)$ is passed as any real upper bound $R$ on the sublevel set, which is equivalent when the supremum is finite and avoids Lean's value $0$ for an unbounded supremum.
Directional smoothness is required at every $x$ and $u$ , and $p_\gamma$ is fixed by the $\beta_i$ ; neither is weakened to hold only along the iterates, which would change the theorem.

A complete development needs the one-dimensional descent lemma (3.5), weighted Cauchy–Schwarz for the dual pair $\|\cdot\|_{[c]},\|\cdot\|^*_{[c]}$ , and a decomposition of the finite expectation over $[n]^{t+1}$ into the last draw and the first $t$ . The weighted-norm and finite-expectation lemmas are reusable for other randomized coordinate and sampling methods. Proofs of the milestones and of either theorem are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §6.4, pp. 338–342.
Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2):341–362, 2012. doi:10.1137/100802001
P. Richtárik and M. Takáč, Parallel coordinate descent methods for big data optimization, Mathematical Programming 156:433–484, 2016. arXiv:1212.0873

7 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization+1·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XV: SVRG with η = 1/(10β) and k = 20κ Contracts the Expected Optimality Gap by 0.9 per EpochTextbook

Motivation

Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.

Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order $(m+\kappa)\log(1/\varepsilon)$ for the same regime, where $m$ is the number of components and $\kappa$ is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.

Setting

Let $f_1,\ldots,f_m:\mathbb R^n\to\mathbb R$ be differentiable convex functions, with $m\ge1$ , and define the finite-sum objective and its gradient by

f(x)=\frac1m\sum_{i=1}^m f_i(x),\qquad G(x)=\frac1m\sum_{i=1}^m \nabla f_i(x).

Each component is $\beta$ -smooth when its gradient is $\beta$ -Lipschitz in the Euclidean norm: $\|\nabla f_i(x)-\nabla f_i(z)\|_2\le\beta\|x-z\|_2$ for all $x,z$ . The average $f$ is $\alpha$ -strongly convex, meaning that for all $x,z$ it lies at least $\frac\alpha2\|z-x\|_2^2$ above its first-order affine approximation at $x$ . The constants $\alpha$ and $\beta$ are positive, $x^*$ minimizes $f$ over $\mathbb R^n$ , and $\kappa=\beta/\alpha$ .

An epoch begins at an anchor $y$ . Its first inner iterate is $x_1=y$ . For $t=1,\ldots,k$ , draw $i_t$ uniformly from $\{1,\ldots,m\}$ , independently across steps and epochs, and update

x_{t+1}=x_t-\eta\bigl(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)+G(y)\bigr).

The next anchor is the average $y^+=k^{-1}\sum_{t=1}^k x_t$ . In particular, this average uses $x_1$ through $x_k$ , while the last updated point $x_{k+1}$ is excluded. Starting from an arbitrary $y^{(1)}$ and repeating the epoch produces $y^{(s+1)}$ . The expectation of $f(y^{(s+1)})$ is over all $sk$ sampled indices in the first $s$ epochs.

Formalization targets

Goal: geometric contraction across epochs

Theorem 6.5 sets $\eta=1/(10\beta)$ and $k=20\kappa$ and asserts, for every $s\ge1$ ,

\mathbb E f(y^{(s+1)})-f(x^*) \le 0.9^s\bigl(f(y^{(1)})-f(x^*)\bigr).

The epoch length is a count, so the statement takes $k\in\mathbb N$ and explicitly requires $k=20\beta/\alpha$ . The goal uses exactly the book's step size, epoch length, and contraction factor.

Milestones: second moments and a single epoch

Lemma 6.4 bounds $\mathbb E_i\|\nabla f_i(x)-\nabla f_i(x^*)\|_2^2$ by $2\beta(f(x)-f(x^*))$ . Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to $x^*$ . The later display on p. 338 bounds one epoch for any positive step size with $2\beta\eta<1$ . Finally, equation (6.1) substitutes the stated constants to obtain the factor $0.9$ for one epoch. These seven source claims form the milestone list in reading order.

Significance

The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap $D$ falls below $0.9^sD$ in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.

The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.

Difficulty

The sampled component gradient $\nabla f_{i_t}(x_t)$ need not be small when $x_t$ is near $x^*$ , so a bound using only its norm does not yield the desired fixed-step contraction. The correction $-\nabla f_{i_t}(y)+G(y)$ has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both $x_t$ and $y$ . The proof must control those two gaps while respecting the fact that $x_t$ depends on earlier samples. A single-index estimate with $x_t$ held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and $m\ge1$ and $k\ge1$ prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.

The component assumptions include differentiability with an explicit gradient map, convexity on all of $\mathbb R^n$ , and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing $x^*$ exists; this is explicit. Positivity of $\alpha$ and $\beta$ , and integrality of $20\beta/\alpha$ , make the displayed divisions and epoch length meaningful. The general epoch bound also requires $0<\eta$ and $2\beta\eta<1$ . Dimension zero is allowed: the theorem remains a statement about the unique point of $\mathbb R^0$ and its zero objective gap.

The direction always contains the sampled difference $\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)$ and the full anchor gradient $G(y)$ . Replacing that direction with $G(x_t)$ would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.

Selected references

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015, pp. 231–358. arXiv:1405.4980v2
Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, Advances in Neural Information Processing Systems 26 (NIPS), 2013 (the origin of SVRG, cited by Bubeck on p. 335). https://proceedings.neurips.cc/paper/2013/hash/ac1dd209cbcc5e5d1c6e28598e8cbbe8-Abstract.html

10 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization+1·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XIV: Stochastic Mirror Descent on a β-Smooth Function with Noise σ Has Rate Rσ√(2/t) + βR²/tTextbook

Motivation

Many optimization problems in statistics and machine learning ask to minimize an expected loss $f(x)=\mathbb E_\xi\,\ell(x,\xi)$ , or an average $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ over a large data set. Exact gradients of such an $f$ are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.

Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order $1/\sqrt t$ and a smoothness term of order $1/t$ . The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ . Gradients are linear forms $g$ on $E$ , the value of $g$ at $v$ is written $g^\top v$ , and the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ . Let $\mathcal X\subseteq E$ be compact and convex.

A mirror map is a function $\Phi$ on an open convex set $\mathcal D$ with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$ . It is strictly convex and differentiable on $\mathcal D$ , its gradient $\nabla\Phi$ takes every value, and $\|\nabla\Phi(x)\|_*\to\infty$ as $x$ approaches the boundary of $\mathcal D$ . Its Bregman divergence is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$ . The map is 1-strongly convex on $\mathcal X\cap\mathcal D$ if $D_\Phi(y,x)\ge\frac12\|x-y\|^2$ there. A function $f$ is $\beta$ -smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$ .

A stochastic oracle returns, at a query point $x$ , a random linear form $\tilde g(x)$ . When the query point is itself random, the book requires the conditional expectation given the query point, $\mathbb E(\tilde g(x)\mid x)$ , to be a subgradient of $f$ at $x$ . In the smooth case it requires $\mathbb E(\tilde g(x)\mid x)=\nabla f(x)$ together with the variance bound $\mathbb E(\|\tilde g(x)-\nabla f(x)\|_*^2\mid x)\le\sigma^2$ .

S-MD with step $\gamma$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, writing $\tilde g_s=\tilde g(x_s)$ , iterates

x_{s+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}\ \gamma\,\tilde g_s^\top x+D_\Phi(x,x_s).

Let $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$ , and let $x^*$ minimize $f$ on $\mathcal X$ .

Formalization targets

Goal: Theorem 6.3

Let $f$ be convex and $\beta$ -smooth, and let the oracle have variance at most $\sigma^2$ . Then for every $t\ge1$ , S-MD with step $1/(\beta+1/\eta)$ and $\eta=\frac R\sigma\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^t x_{s+1}\Big)-f(x^*)\le R\sigma\sqrt{\frac2t}+\frac{\beta R^2}{t}.

Milestones (the proof's four displays)

For points $x_s,x_{s+1}\in\mathcal X\cap\mathcal D$ and $\eta>0$ , the smoothness step is

f(x_{s+1})-f(x_s)\le\tilde g_s^\top(x_{s+1}-x_s)+\tfrac\eta2\|\nabla f(x_s)-\tilde g_s\|_*^2+(\beta+1/\eta)D_\Phi(x_{s+1},x_s).

If $x_{s+1}$ is the S-MD step, the mirror step is

\tfrac{1}{\beta+1/\eta}\tilde g_s^\top(x_{s+1}-x^*)\le D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})-D_\Phi(x_{s+1},x_s).

Combining the two gives a pathwise bound on $f(x_{s+1})$ with the cross term $(\tilde g_s-\nabla f(x_s))^\top(x^*-x_s)$ . Taking expectations gives the expected one-step bound

\mathbb Ef(x_{s+1})-f(x^*)\le(\beta+1/\eta)\,\mathbb E\big(D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})\big)+\frac{\eta\sigma^2}{2}.

Companion: Theorem 6.1 and (4.10)

For a convex $f$ with $\mathbb E(\|\tilde g(x)\|_*^2\mid x)\le B^2$ , S-MD with $\eta=\frac RB\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^tx_s\Big)-\min_{\mathcal X}f\le RB\sqrt{2/t}.

This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors $g_s$ :

\sum_{s\le t}g_s^\top(x_s-x)\le\frac{R^2}{\eta}+\frac{\eta}{2\rho}\sum_{s\le t}\|g_s\|_*^2.

Significance

Theorem 6.3 says exactly how much smoothness helps under noise. As $\sigma\to0$ it recovers the $\beta R^2/t$ rate of deterministic smooth optimization. For large $t$ the noise term $R\sigma\sqrt{2/t}$ dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging $m$ independent oracle answers divides the variance by $m$ , so the theorem quantifies the benefit of mini-batches: the noise term shrinks by $\sqrt m$ while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.

These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.

Difficulty

The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point $x_s$ is random, so unbiasedness enters only through the conditional expectation given $x_s$ . Making the cross term vanish requires pulling the $\sigma(x_s)$ -measurable vector $x^*-x_s$ out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When $\nabla\Phi$ blows up at the boundary of $\mathcal D$ , the Bregman terms $D_\Phi(x^*,x_s)$ are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer $x^*$ may lie on the boundary of $\mathcal D$ , where $\Phi$ is not part of the book's data. Treating $\mathbb E$ informally, or assuming $x^*\in\mathcal D$ , skips exactly these points.

Formalization scope

Spaces and gradients. $E$ is a finite-dimensional real normed space. Gradients are explicit maps Φ' f' : E → (E →L[ℝ] ℝ), $g^\top v$ is g v, and $\|\cdot\|_*$ is the operator norm. $\beta$ -smoothness is stated with derivatives relative to $\mathcal X$ . $\Phi$ is a total function, constrained only by the mirror-map axioms on $\mathcal D$ .
Runs and oracle. S-MD is a run predicate. For every outcome, $x_1$ minimizes $\Phi$ on $\mathcal X\cap\mathcal D$ , and $x_{s+1}$ is some minimizer of the step objective. The oracle is a predicate on the random sequences $(x_s,\tilde g_s)$ : each $x_s$ is measurable, and the conditional expectations are taken given $\sigma(x_s)$ . Every conditioned quantity is integrable.
Conclusions. Every bound on an expectation also asserts integrability. Without it, the Lean integral of a non-integrable function is $0$ and the bound could hold trivially.
Standing assumptions. The book's $R^2=\sup(\Phi-\Phi(x_1))$ is replaced by any upper bound $R^2$ . The minimizer $x^*\in\mathcal X$ exists (p. 242). $\mathcal X$ is compact and convex (Chapter 4), and convex functions are closed (p. 236).
Positivity side conditions. $R,\sigma,B>0$ and $t\ge1$ make the step sizes and bounds defined, and $\beta\ge0$ .

A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let $x_{s+1}$ be an arbitrary point of $\mathcal X\cap\mathcal D$ would make the theorems false, and are not used either.

A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, https://arxiv.org/abs/1405.4980 (Chapter 6, pp. 329–333; Chapter 4, pp. 297–307).
O. Dekel, R. Gilad-Bachrach, O. Shamir, L. Xiao, Optimal distributed online prediction using mini-batches, Journal of Machine Learning Research 13:165–202, 2012. https://jmlr.org/papers/v13/dekel12a.html
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277

6 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XII: Mirror Prox on a Convex β-Smooth Function Has Rate βR²/(ρt)Textbook

Motivation

First-order methods for constrained convex optimization are usually analysed in the Euclidean norm, where gradient descent and its projected and accelerated variants have well-understood rates. Many constraint sets of practical interest, such as the probability simplex, the $\ell_1$ ball and the spectrahedron, are poorly adapted to the Euclidean geometry: the Euclidean diameter and the Euclidean Lipschitz or smoothness constants grow with the dimension. Mirror descent, due to Nemirovski and Yudin, replaces the Euclidean step by a step taken in the dual space through a mirror map $\Phi$ , so that the rate depends on constants measured in a norm matched to the set. For non-smooth Lipschitz functions it attains the rate $1/\sqrt t$ (Theorem 4.2 of the source, the subject of the previous mission of this series).

For smooth functions, a rate of order $1/t$ is available in any geometry by an extragradient-type modification. Mirror prox was introduced by Nemirovski in 2004 (Prox-method with rate of convergence O(1/t)) for variational inequalities with Lipschitz monotone operators and convex–concave saddle-point problems. It is the basis of smoothing approaches to non-smooth optimization and of stochastic saddle-point methods. This mission formalizes the version for minimizing a single smooth convex function, Theorem 4.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), §4.5.

Setting

Fix an arbitrary norm $\|\cdot\|$ on a finite-dimensional real space $E$ . Gradients are linear functionals on $E$ ; for a functional $g$ write $g^\top v$ for its value at $v$ , and $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ for the dual norm. Let $\mathcal X\subseteq E$ be compact and convex.

The Bregman divergence of a differentiable $\Phi$ is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$ .
Let $\mathcal D$ be a convex open set with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$ . A mirror map on $\mathcal D$ is a function $\Phi$ that is strictly convex and differentiable on $\mathcal D$ , whose gradient takes every value ( $\nabla\Phi(\mathcal D)$ is the whole dual space), and whose gradient norm tends to $+\infty$ at the boundary of $\mathcal D$ .
The Bregman projection of $y\in\mathcal D$ is $\Pi^\Phi_{\mathcal X}(y)=\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y)$ .
$\Phi$ is $\rho$ -strongly convex on $\mathcal X\cap\mathcal D$ if $\Phi(x)-\Phi(y)\le\nabla\Phi(x)^\top(x-y)-\frac\rho2\|x-y\|^2$ there; $f$ is $\beta$ -smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$ .

Mirror prox with step size $\eta$ generates, from $x_t$ ,

\nabla\Phi(y'_{t+1})=\nabla\Phi(x_t)-\eta\nabla f(x_t),\qquad y_{t+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y'_{t+1}),

\nabla\Phi(x'_{t+1})=\nabla\Phi(x_t)-\eta\nabla f(y_{t+1}),\qquad x_{t+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,x'_{t+1}).

The first half is a mirror descent step from $x_t$ to $y_{t+1}$ ; the second restarts from $x_t$ with the gradient evaluated at $y_{t+1}$ .

Formalization targets

Goal: Theorem 4.4

With $\eta=\rho/\beta$ , $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ , $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$ , $f$ convex and $\beta$ -smooth and $x^*$ a minimizer of $f$ on $\mathcal X$ , for every $t\ge1$

f\Bigl(\frac1t\sum_{s=1}^t y_{s+1}\Bigr)-f(x^*)\le\frac{\beta R^2}{\rho t}.

Milestones

Lemma 4.1 (Bregman projections): $(\nabla\Phi(\Pi^\Phi_{\mathcal X}(y))-\nabla\Phi(y))^\top(\Pi^\Phi_{\mathcal X}(y)-x)\le0$ and $D_\Phi(x,\Pi^\Phi_{\mathcal X}(y))+D_\Phi(\Pi^\Phi_{\mathcal X}(y),y)\le D_\Phi(x,y)$ for $x\in\mathcal X\cap\mathcal D$ , $y\in\mathcal D$ .
First term: $\eta\nabla f(y_{t+1})^\top(x_{t+1}-x)\le D_\Phi(x,x_t)-D_\Phi(x,x_{t+1})-D_\Phi(x_{t+1},x_t)$ .
Second term, (4.9): $\eta\nabla f(x_t)^\top(y_{t+1}-x_{t+1})\le D_\Phi(x_{t+1},x_t)-\frac\rho2\|x_{t+1}-y_{t+1}\|^2-\frac\rho2\|y_{t+1}-x_t\|^2$ .
Third term: $(\nabla f(y_{t+1})-\nabla f(x_t))^\top(y_{t+1}-x_{t+1})\le\frac\beta2\|y_{t+1}-x_t\|^2+\frac\beta2\|y_{t+1}-x_{t+1}\|^2$ .
Per-step bound: $f(y_{t+1})-f(x)\le\bigl(D_\Phi(x,x_t)-D_\Phi(x,x_{t+1})\bigr)/\eta$ for $x\in\mathcal X\cap\mathcal D$ .

The three-point identity (4.1), $(\nabla f(x)-\nabla f(y))^\top(x-z)=D_f(x,y)+D_f(z,x)-D_f(z,y)$ , is already posed on the platform as BeckTeboulleMD.EMDA.lemma_4_1 and is included by reference.

Significance

Theorem 4.4 shows that the $1/t$ rate of gradient descent on smooth functions survives in non-Euclidean geometries, with the dimension entering only through $R^2/\rho$ . With the negative entropy on the simplex, $R^2/\rho$ is of order $\log n$ for the $\ell_1$ norm, against a polynomial dependence for Euclidean methods. Beyond this single-function version, the same three-term argument is the core of the analysis of mirror prox for monotone variational inequalities and saddle-point problems (§4.6 and §5.2 of the source), where it gives the $1/t$ rate for smooth convex–concave games.

The result is proved in the source and in Nemirovski's paper. As far as this mission is aware it has no machine-checked proof; Mathlib has no Bregman divergences, mirror maps or mirror-descent-type algorithms. A formal proof would supply reusable infrastructure: the Bregman projection lemma (Lemma 4.1) and the three-point identity are used by every mirror-descent analysis, including the stochastic and online variants later in the source.

Difficulty

The obvious argument for mirror descent bounds $f(x_t)-f(x)$ by $\nabla f(x_t)^\top(x_t-x)$ and leaves a stability term of size $\eta^2\|\nabla f\|_*^2$ , which yields only $1/\sqrt t$ . Smoothness has to be used to cancel that term, and a single gradient step does not do so in a general norm. Mirror prox evaluates the gradient at the extrapolated point $y_{t+1}$ ; the analysis must show that the error created by using $\nabla f(x_t)$ for the first step is paid for by the strong convexity of $\Phi$ , which requires splitting $\nabla f(y_{t+1})^\top(y_{t+1}-x)$ into three terms and bounding each with matching constants.

In Lean the difficulty is in the infrastructure: first-order optimality of a Bregman projection over $\mathcal X\cap\mathcal D$ , which need not be closed; the passage from $x\in\mathcal X\cap\mathcal D$ to a minimizer $x^*$ that may lie on the boundary of $\mathcal D$ ; and Jensen's inequality for the average of the $y_{s+1}$ .

Formalization scope

$E$ is a finite-dimensional real normed space. Gradients are continuous linear functionals E →L[ℝ] ℝ given by explicit maps Φ' and f'; the dual norm is the operator norm. Φ' is the Fréchet derivative of $\Phi$ at each point of $\mathcal D$ ; f' is the derivative of $f$ relative to $\mathcal X$ at each point of $\mathcal X$ .
The mirror map definition keeps all three properties of §4.1, including surjectivity of the gradient and divergence at each frontier point of $\mathcal D$ .
Projections and runs are relations: every admissible argmin choice is covered; no choice function is used. The run is indexed from $t=1$ ; index $0$ is unused.
Standing and implicit hypotheses: $\mathcal X$ compact convex; a minimizer $x^*\in\mathcal X$ exists (the source's standing assumption); $\rho>0$ and $\beta>0$ (so that $\eta=\rho/\beta$ and the division by $\rho t$ are meaningful); $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ (unspecified in §4.5, taken as in mirror descent, §4.2).
$R$ is any real with $\Phi-\Phi(x_1)\le R^2$ on $\mathcal X\cap\mathcal D$ . The source's $R^2=\sup$ is the case where the supremum is finite; when it is infinite, the source's bound is void.
A run in which the second step started from $y_{t+1}$ , or projected $y'_{t+1}$ again, would be mirror descent, for which the claimed rate is false; the formal run follows the four equations of the source exactly. The average is over the extrapolated points $y_{s+1}$ , $s=1,\dots,t$ .

Contributions welcome: proofs of Lemma 4.1 and the three-term bounds, which are reusable for the stochastic mirror descent and saddle-point missions of this series, and the final telescoping and limit argument.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980v2
A. Nemirovski, Prox-method with rate of convergence O(1/t) for variational inequalities with Lipschitz continuous monotone operators and smooth convex-concave saddle point problems, SIAM Journal on Optimization 15(1):229–251, 2004. https://doi.org/10.1137/S1052623403425629
A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

8 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Theoretical Computer Science·Captain: mikedeng1

Online Primal-Dual Algorithms for Covering and Packing 1: The Online Fractional Packing Scheme Is B-Competitive and Violates Each Packing Constraint by at Most 2 log(1 + n·a_i(max)/a_i(min))/BResearch Paper

Motivation

Many resource-allocation problems arrive one request at a time and must be answered immediately: a bandwidth request is admitted or refused when it appears, an advertiser's budget is charged when a query arrives, a job is accepted before later jobs are seen. Their linear-programming relaxations are packing problems: maximize a total profit subject to capacity constraints, where the variables are revealed online and each must be set irrevocably when it is revealed. A standard yardstick for such an online algorithm is its competitive ratio, the worst-case ratio between the offline optimum and the algorithm's value.

Buchbinder and Naor (Math. Oper. Res. 2009) gave a single online primal-dual scheme for the general online fractional packing problem, together with a matching scheme for covering. The scheme raises the newly revealed packing variable while increasing the dual covering variables along an exponential curve, and its analysis is a short primal-dual argument. Earlier online algorithms for throughput-competitive routing and for set cover (Alon et al. 2009) can be read as instances of it, and the same template later became the basis of a monograph on the primal-dual approach to online algorithms (Buchbinder, Naor 2009).

This mission formalizes the paper's headline result, Theorem 3.1, for the scheme exactly as the paper defines it.

Setting

Fix a finite set $I$ of $n\ge1$ packing constraints (equivalently, primal covering variables), with known capacities $c(i)>0$ . Packing variables $y(1),\dots,y(m)$ arrive one per round; in round $j$ the variable $y(j)$ is revealed together with its non-negative column $a(i,j)$ , $i\in I$ . The offline problems form the primal-dual pair of Figure 1 of the paper:

\text{(P)}\ \min\sum_i c(i)x(i)\ \text{ s.t. } \sum_i a(i,j)x(i)\ge1\ \forall j,\ x\ge0;\qquad \text{(D)}\ \max\sum_j y(j)\ \text{ s.t. } \sum_j a(i,j)y(j)\le c(i)\ \forall i,\ y\ge0.

The profit of every $y(j)$ is normalized to $1$ . Every column is assumed to have a positive entry; otherwise the packing problem is unbounded. An online algorithm may set $y(j)$ only in round $j$ and never changes it later.

The scheme with parameter $B>0$ keeps a primal vector $x$ (initially $0$ ) and the dual vector $y$ . In round $j$ it computes the prefix maximum $a_i(\max)=\max_{k\le j}a(i,k)$ . If the new covering constraint $\sum_i a(i,j)x(i)\ge1$ already holds, it sets $y(j)=0$ . Otherwise it sets $y(j)$ to the least $t\ge0$ at which the constraint holds after every $x(i)$ is replaced by

\max\Big\{x(i),\ \frac{1}{n\,a_i(\max)}\Big[\exp\Big(\frac{B}{2c(i)}\sum_{k=1}^{j}a(i,k)y(k)\Big)-1\Big]\Big\},\qquad y(j)=t.

After $r$ rounds, $X(r)=\sum_i c(i)x(i)$ is the primal value and $Y(r)=\sum_{k\le r}y(k)$ the dual value. For the analysis, $a_i(\max)$ and $a_i(\min)$ also denote the largest and the smallest non-zero coefficient of row $i$ over all $m$ columns.

Formalization targets

Goal: Theorem 3.1

For every $B>0$ , the scheme's dual solution is non-negative; after every round $r$ , every non-negative $y'$ that satisfies the packing constraints restricted to the first $r$ columns has $\sum_{k\le r}y'(k)\le B\,Y(r)$ (the scheme is $B$ -competitive); and after all $m$ rounds, for every $i$ ,

\sum_{k=1}^{m}a(i,k)\,y(k)\ \le\ c(i)\cdot\frac{2\log\big(1+n\,a_i(\max)/a_i(\min)\big)}{B}.

The paper states the second part as $c(i)\cdot O\big((\log n+\log(a_i(\max)/a_i(\min)))/B\big)$ ; the bound above is the one its proof establishes.

Milestones: the three claims of the proof

Claim (i): $X(r)\le B\cdot Y(r)$ after every round $r$ .
Claim (ii): after every round, $x\ge0$ and $x$ satisfies every covering constraint revealed so far; no $x(i)$ ever decreases.
Claim (iii): the violation bound of the goal.

Significance

Theorem 3.1 says that a solution within factor $B$ of the optimum can be maintained online at the price of overloading each packing constraint by a factor of order $(\log n+\log(a_{\max}/a_{\min}))/B$ . Scaling the output down by the overload gives a feasible online packing solution with competitive ratio $O(\log n+\log(a_{\max}/a_{\min}))$ , and Lemma 3.1 of the paper shows that no online algorithm does better up to constant factors. The same trade-off underlies the paper's online rounding results for routing (§5.2) and, through the covering counterpart, for set cover (§5.1).

The result is proved in the paper. As far as the platform's record shows, it is not formalized: the published OnlinePrimalDual.GeneralPacking.theorem14_1 (a restatement of the monograph's version) takes the inequality $X\le BY$ and primal feasibility as hypotheses on arbitrary vectors $x,y$ and derives competitiveness by weak duality; it does not mention the scheme and has no violation bound. The published OnlinePrimalDual.GeneralPacking.lemma14_2 is the matching lower bound (Lemma 3.1) and is not part of this mission. A formalization here would give the first machine-checked guarantee for the scheme itself and a reusable analysis pattern (a potential bound integrated along a monotone path) for the other schemes of the paper.

Difficulty

The paper's argument is a derivative comparison along a continuous process: while $y(j)$ rises, $\partial X/\partial y(j)\le B$ . In the discrete formulation each round jumps directly to the least admissible $y(j)$ , and each $x(i)$ is a maximum of its old value and an exponential, so it is continuous but not differentiable where the maximum switches; the comparison must be turned into an integral inequality over $[0,y(j)]$ for such functions. The prefix maximum $a_i(\max)$ changes between rounds, and the claim that this never lowers or raises the primal value needs an invariant ( $x(i)$ is always at least the current increment value). The violation bound rests on a second invariant, $x(i)\le1/a_i(\min)$ , which holds because $y(j)$ is the least admissible value; any formalization that loses minimality (for example by taking an arbitrary admissible $t$ ) loses claim (iii).

Formalization scope

The instance is the published OnlinePrimalDual.GeneralPacking.GeneralInstance I (Fin m) (costs $c>0$ , coefficients $a\ge0$ ); $n=|I|$ with [Nonempty I]; columns are Fin m, arrive in index order, and are 0-based in Lean, so "the first $r$ columns" is (k : ℕ) < r. $m\ge1$ is [NeZero m].
$a_i(\max)$ , $a_i(\min)$ over all columns are the published aMax and aMin. For a row with no non-zero coefficient aMin is $0$ and both sides of the violation bound are $0$ .
The scheme is a function, stateAfter inst B r. The continuous loop of the paper is replaced by its discrete implementation, which the paper itself prescribes (p. 4): $y(j)$ is the least $t\ge0$ restoring the new covering constraint, written as sInf. Every theorem assumes that every column has a positive entry (the paper's standing assumption, p. 4); this makes the infimum attained. If the prefix maximum is $0$ , Lean's $1/0=0$ gives increment $0$ , which agrees with the paper's bracket being $0$ .
Explicit constant. The paper's $c(i)\cdot O((\log n+\log(a_i(\max)/a_i(\min)))/B)$ is instantiated as $c(i)\cdot 2\log(1+n\,a_i(\max)/a_i(\min))/B$ , from claim (iii) of the proof. Logarithms are natural (Real.log), since they invert Real.exp.
$B$ -competitiveness is stated against every non-negative feasible packing solution of every prefix of the input, not only at the end.
A formalization in which the inequality $X\le BY$ , primal feasibility, or the bound $x(i)\le1/a_i(\min)$ is assumed rather than derived from the scheme is ruled out: every statement here is about the vectors the scheme computes from the instance.
Needed infrastructure: monotonicity and continuity of the per-round primal path, attainment of the infimum, an integral (or mean-value) form of the derivative comparison for maxima of exponentials, and weak duality for finite LPs. The weak-duality step and the per-round integration lemma are reusable for missions 2–4 of this series. Proofs of the milestones, and of helper lemmas such as the invariant $x(i)\le1/a_i(\min)$ , are welcome.

Selected references

N. Buchbinder, J. Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research, 2009. https://doi.org/10.1287/moor.1080.0363
N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024
N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2), 2009. https://doi.org/10.1137/060661946

8 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XI: Mirror Descent with a ρ-Strongly Convex Mirror Map Has Rate RL√(2/(ρt))Textbook

Motivation

The projected subgradient method of Chapter 3 measures distances in the Euclidean norm, and its rate $RL/\sqrt t$ depends on the geometry only through a Euclidean radius $R$ and a Euclidean bound $L$ on the subgradients. For many constraint sets that occur in practice this is the wrong geometry. On the probability simplex $\Delta_n$ with subgradients bounded in $\ell_\infty$ , as for linear losses with bounded coefficients, the Euclidean constants make $RL$ grow like $\sqrt n$ , while the problem itself is nearly dimension-free.

Mirror descent, introduced by Nemirovski and Yudin (1983), repairs this. The gradient step is taken in the dual space, after mapping the current point through the gradient of a strictly convex mirror map $\Phi$ , and feasibility is restored by a projection in the Bregman divergence of $\Phi$ rather than in the Euclidean distance. Beck and Teboulle (2003, doi:10.1016/S0167-6377(02)00231-6) recast it as a nonlinear projected subgradient method and showed that with the negative entropy on the simplex its rate is $O(L\sqrt{\log n/t})$ . Nesterov (2009, doi:10.1007/s10107-007-0149-x) introduced dual averaging, a lazy variant that averages the subgradients in the dual space and maps back only when a primal point is needed. Both methods underlie online learning (exponential weights is mirror descent with the entropy), stochastic optimization, and saddle-point methods such as mirror prox.

This mission is the eleventh of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015, arXiv:1405.4980). It covers the preamble of Chapter 4, Sections 4.1 and 4.2, and Section 4.4.

Setting

Let $E$ be a finite-dimensional real vector space (the book's $\mathbb R^n$ ) with an arbitrary norm $\|\cdot\|$ . A linear functional $g$ on $E$ acts on $x$ by $g^\top x$ and has dual norm $\|g\|_*=\sup_{\|x\|\le1}g^\top x$ . Let $\mathcal X\subseteq E$ be compact and convex.

Let $\mathcal D\subseteq E$ be a convex open set with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\neq\emptyset$ . A function $\Phi:\mathcal D\to\mathbb R$ is a mirror map if it is strictly convex and differentiable, its gradient takes every value in the dual space, and $\|\nabla\Phi(x)\|\to+\infty$ as $x$ tends to the boundary of $\mathcal D$ . Its Bregman divergence is

D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y),

and the Bregman projection of $y\in\mathcal D$ is $\Pi^\Phi_{\mathcal X}(y)=\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y)$ . The mirror map is $\rho$ -strongly convex on $\mathcal X\cap\mathcal D$ if $\Phi(x)-\Phi(y)\le\nabla\Phi(x)^\top(x-y)-\frac\rho2\|x-y\|^2$ for all $x,y\in\mathcal X\cap\mathcal D$ .

Let $f$ be convex on $\mathcal X$ with a minimizer $x^*\in\mathcal X$ . A linear functional $g$ is a subgradient of $f$ at $x$ if $f(x)-f(y)\le g^\top(x-y)$ for all $y\in\mathcal X$ , and $f$ is $L$ -Lipschitz if the subgradients satisfy $\|g\|_*\le L$ .

Mirror descent with step $\eta$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, for $t\ge1$ , picks $g_t\in\partial f(x_t)$ and

\nabla\Phi(y_{t+1})=\nabla\Phi(x_t)-\eta g_t,\quad y_{t+1}\in\mathcal D,\qquad x_{t+1}=\Pi^\Phi_{\mathcal X}(y_{t+1}).\tag{4.2–4.3}

Dual averaging instead sets $x_t\in\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}\eta\sum_{s=1}^{t-1}g_s^\top x+\Phi(x)$ (4.6). Let $R^2$ bound $\Phi(x)-\Phi(x_1)$ over $\mathcal X\cap\mathcal D$ .

Formalization targets

Goal: Theorem 4.2

With $\eta=\frac RL\sqrt{\frac{2\rho}{t}}$ , every run of mirror descent satisfies

f\Big(\frac1t\sum_{s=1}^t x_s\Big)-f(x^*)\le RL\sqrt{\frac{2}{\rho t}}.

Milestones

The three-point identity (4.1): $(\nabla f(x)-\nabla f(y))^\top(x-z)=D_f(x,y)+D_f(z,x)-D_f(z,y)$ .
Lemma 4.1: for $x\in\mathcal X\cap\mathcal D$ and $y\in\mathcal D$ , $D_\Phi(x,\Pi^\Phi_{\mathcal X}(y))+D_\Phi(\Pi^\Phi_{\mathcal X}(y),y)\le D_\Phi(x,y)$ , together with the first-order inequality that implies it.
The per-step inequality: $f(x_s)-f(x)\le\frac1\eta\big(D_\Phi(x,x_s)+D_\Phi(x_s,y_{s+1})-D_\Phi(x,x_{s+1})-D_\Phi(x_{s+1},y_{s+1})\big)$ .
The stability term: $D_\Phi(x_s,y_{s+1})-D_\Phi(x_{s+1},y_{s+1})\le(\eta L)^2/(2\rho)$ .
The summed bound: $\sum_{s=1}^t(f(x_s)-f(x))\le D_\Phi(x,x_1)/\eta+\eta L^2t/(2\rho)$ .

Companion: Theorem 4.3

With $\eta=\frac RL\sqrt{\frac{\rho}{2t}}$ , dual averaging satisfies $f\big(\frac1t\sum_{s=1}^tx_s\big)-f(x^*)\le2RL\sqrt{\frac2{\rho t}}$ , with the two displays (4.7) and (4.8) of its proof as supporting items.

Significance

Theorem 4.2 is the basic rate of non-Euclidean first-order optimization. With the Euclidean mirror map $\Phi=\frac12\|\cdot\|_2^2$ it recovers the projected subgradient rate of Chapter 3; with the negative entropy on the simplex, which is $1$ -strongly convex for $\ell_1$ by Pinsker's inequality and has $R^2=\log n$ , it gives $L_\infty\sqrt{2\log n/t}$ , so the dependence on the dimension becomes logarithmic. The same analysis, with $f$ replaced by a sequence of losses, is the regret bound of online mirror descent, and its per-step and stability inequalities are reused for stochastic mirror descent and mirror prox in later chapters of the book.

The results are classical and fully proved in the book. What this mission adds is a machine-checked version in a general finite-dimensional normed space, with gradients as linear functionals and the dual norm as the operator norm, for an arbitrary mirror map on an arbitrary open domain. On Prove2Me the three-point identity (4.1) is already posed, as Lemma 4.1 of the Beck–Teboulle formalization, and is reused here; a regret bound for online mirror descent with Legendre functions is proved in another library, but it is not this theorem and does not cover a domain $\mathcal D$ distinct from the whole space or a Bregman projection onto $\mathcal X\cap\mathcal D$ .

Difficulty

The algebra of the proof is short. The difficulty lies at the boundary of $\mathcal D$ . The minimizer $x^*$ may lie on $\partial\mathcal D$ , where $\Phi$ and $\nabla\Phi$ are not defined; this is the typical case for the entropy on the simplex, where $x^*$ is often a vertex. The per-step bound holds only for comparison points $x\in\mathcal X\cap\mathcal D$ , so the bound at $x^*$ has to be recovered from points of $\mathcal X\cap\mathcal D$ , where no regularity of $f$ beyond convexity on $\mathcal X$ is available. Lemma 4.1 needs the first-order optimality condition of the Bregman projection over the convex set $\mathcal X\cap\mathcal D$ , which is not closed. In the non-Euclidean setting the gradient step cannot be written in the primal space at all: the update (4.2) is an equation between linear functionals, and the norm and dual norm must be kept apart throughout.

Formalization scope

The space is a finite-dimensional real normed space E with an arbitrary norm; gradients and subgradients are elements of E →L[ℝ] ℝ, the dual norm is the operator norm, and $\nabla\Phi$ is an explicit map Φ' with HasFDerivAt Φ (Φ' x) x on $\mathcal D$ .
The mirror map carries all three properties (i)–(iii) of the book; the standing setting ( $\mathcal X$ compact convex, $\mathcal X\subseteq\overline{\mathcal D}$ , $\mathcal X\cap\mathcal D\neq\emptyset$ ) is a single predicate.
Runs are predicates over the first $t$ steps, quantified universally: any subgradient, any $y_{t+1}$ solving (4.2), any minimizer. A run whose next iterate were an arbitrary point of $\mathcal X\cap\mathcal D$ , rather than the Bregman projection, would make the theorem false; the projection is part of the run.
Sequences are indexed from $1$ ; $t\ge1$ , $\rho>0$ , $L>0$ , $R>0$ and $\eta>0$ are explicit, since the step and the bound divide by them.
$R^2$ is any upper bound of $\sup_{\mathcal X\cap\mathcal D}\Phi-\Phi(x_1)$ (the book's $R$ is the least one); when the supremum is infinite the hypotheses cannot be met, as on the page.
" $f$ is $L$ -Lipschitz" is assumed for the subgradients the run uses. Subgradients relative to $\mathcal X$ are unbounded at boundary points of $\mathcal X$ , so the literal "every subgradient at every point" would make the hypothesis unsatisfiable.
The definitions (Bregman divergence, mirror map, Bregman projection, the two runs) are reusable by the later chapters on mirror prox and stochastic mirror descent. Proofs of any milestone, and of the general facts they need (nonnegativity of Bregman divergences, first-order optimality over a convex set that is not closed), are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983 (book; no DOI).
A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. doi:10.1016/S0167-6377(02)00231-6
Y. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120(1):221–259, 2009. doi:10.1007/s10107-007-0149-x

7 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity IX: Nesterov's Accelerated Gradient Descent on a Convex β-Smooth Function Has Rate 2β‖x₁ − x*‖²/t²Textbook

Motivation

Minimizing a convex function $f:\mathbb R^n\to\mathbb R$ whose gradient is Lipschitz is the basic problem of first-order optimization, and it is the regime in which most large-scale methods of machine learning, signal processing and operations research are analysed. The natural method, gradient descent, reaches accuracy $\varepsilon$ after $O(1/\varepsilon)$ gradient evaluations. In 1983 Nesterov showed that a method using the same oracle, but combining the current and the previous iterate, reaches accuracy $\varepsilon$ after only $O(1/\sqrt\varepsilon)$ evaluations, and that no method using only gradient information can do better by more than a constant factor. This accelerated gradient descent and its proximal variants (FISTA) are now the default fast first-order methods for smooth and composite convex problems.

This mission formalizes the accelerated rate as presented in S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §3.7.2, Theorem 3.19, whose proof follows Beck and Teboulle (2009).

Timeline.

1983: Nesterov introduces the accelerated method with rate $O(1/t^2)$ for convex functions with Lipschitz gradient (Soviet Math. Dokl. 27).
1983: Nemirovski and Yudin's black-box lower bounds show that $\Omega(1/t^2)$ is the best possible rate for this class (Theorem 3.14 of the book gives $3\beta\|x_1-x^*\|^2/(32(t+1)^2)$ ).
2009: Beck and Teboulle's FISTA extends the method, with the same step sequence $\lambda_t$ , to composite problems with a simple nonsmooth term (SIAM J. Imaging Sci. 2(1)).
2008: Tseng gives a unified treatment with simpler step sizes (manuscript).

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$ . A differentiable function $f:\mathbb R^n\to\mathbb R$ is β-smooth if its gradient is $\beta$ -Lipschitz:

\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad(x,y\in\mathbb R^n).

Assume $f$ is convex and $\beta$ -smooth with $\beta>0$ , and let $x^*$ be a minimizer of $f$ .

Define the step sequences $\lambda_0=0$ ,

\lambda_t=\frac{1+\sqrt{1+4\lambda_{t-1}^2}}{2}\quad(t\ge1),\qquad\gamma_t=\frac{1-\lambda_t}{\lambda_{t+1}}.

Then $\lambda_1=1$ , $\lambda_t\ge1$ for $t\ge1$ , and $\gamma_t\le0$ . Nesterov's accelerated gradient descent for the smooth case starts from an arbitrary point $x_1=y_1$ and sets, for $t\ge1$ ,

y_{t+1}=x_t-\frac1\beta\nabla f(x_t),\qquad x_{t+1}=(1-\gamma_t)\,y_{t+1}+\gamma_t\,y_t.

The primary sequence $(y_t)$ consists of gradient steps of length $1/\beta$ ; the sequence $(x_t)$ , at which the gradient is queried, moves past $y_{t+1}$ away from $y_t$ (since $\gamma_t\le0$ ). Write $\delta_t=f(y_t)-f(x^*)$ for the optimality gap.

Formalization targets

Goal: Theorem 3.19

For every run of the method and every $t\ge1$ ,

f(y_t)-f(x^*)\le\frac{2\beta\|x_1-x^*\|^2}{t^2}.

The constant $2$ and the exponent $2$ are those printed in the book.

Milestones

In the order of the book's proof (pp. 294–295):

Lemma 3.6, unconstrained (p. 270): $f(x-\tfrac1\beta\nabla f(x))-f(y)\le\nabla f(x)^\top(x-y)-\tfrac1{2\beta}\|\nabla f(x)\|^2$ for all $x,y$ .
(3.23): $f(y_{s+1})-f(y_s)\le\beta(x_s-y_{s+1})^\top(x_s-y_s)-\tfrac\beta2\|x_s-y_{s+1}\|^2$ .
(3.24): $f(y_{s+1})-f(x^*)\le\beta(x_s-y_{s+1})^\top(x_s-x^*)-\tfrac\beta2\|x_s-y_{s+1}\|^2$ .
The λ identity: $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ for $s\ge1$ .
(3.25): $\lambda_s^2\delta_{s+1}-\lambda_{s-1}^2\delta_s\le\tfrac\beta2\bigl(\|\lambda_sx_s-(\lambda_s-1)y_s-x^*\|^2-\|\lambda_sy_{s+1}-(\lambda_s-1)y_s-x^*\|^2\bigr)$ .
(3.26): $\lambda_{s+1}x_{s+1}-(\lambda_{s+1}-1)y_{s+1}=\lambda_sy_{s+1}-(\lambda_s-1)y_s$ .
Telescoped bound: $\delta_t\le\frac{\beta}{2\lambda_{t-1}^2}\|u_1\|^2$ for $t\ge2$ , with $u_1=\lambda_1x_1-(\lambda_1-1)y_1-x^*$ .
Growth of λ: $\lambda_{t-1}\ge t/2$ for $t\ge2$ .

Significance

The result. Theorem 3.19 is the upper half of the statement that first-order methods on smooth convex functions have complexity $\Theta(\sqrt{\beta\|x_1-x^*\|^2/\varepsilon})$ : together with the black-box lower bound of Theorem 3.14 it shows that the accelerated method is optimal up to a constant factor, while plain gradient descent (Theorem 3.3, rate $2\beta\|x_1-x^*\|^2/(t-1)$ ) is not. The same potential-function argument, with the gradient step replaced by a proximal step, yields the rate of FISTA for composite objectives, and the identity $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ is the algebraic core of most later analyses of accelerated and momentum methods.

Formalizing it. The theorem is classical and fully proved on paper. What this mission adds is a machine-checked proof of the $O(1/t^2)$ rate for the exact step sequence of the book, with every intermediate inequality of the proof stated separately so that each can be closed and reused. A Lean development of accelerated gradient descent with this rate is not, to our knowledge, in Mathlib.

Difficulty

The rate does not follow from monotone decrease of $f(y_t)$ , which is the engine of the analysis of plain gradient descent: the accelerated iterates are not monotone, and no single-step inequality on $\delta_t$ alone gives $1/t^2$ . The proof instead tracks a weighted potential $\lambda_{s-1}^2\delta_s+\frac\beta2\|u_s\|^2$ and needs three exact algebraic coincidences: the identity $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ , the completion of a square $2a^\top b-\|a\|^2=\|b\|^2-\|b-a\|^2$ , and the rewriting (3.26) of the update rule, which makes consecutive potentials match exactly. In Lean the work is in this bookkeeping (vector identities in an inner-product space, a real recursion with square roots, and a telescoping sum indexed from $1$ ), not in any deep analytic fact.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $x^\top y$ is ⟪x, y⟫_ℝ.
The gradient is an explicit map $g$ with HasGradientAt f (g x) x for every $x$ ; β-smoothness is the Lipschitz bound on $g$ (not the quadratic upper bound (3.4), which is a consequence). Convexity is ConvexOn ℝ Set.univ f.
$\lambda$ is a real sequence defined by recursion on $\mathbb N$ with $\lambda_0=0$ ; $\gamma_t=(1-\lambda_t)/\lambda_{t+1}$ never divides by zero because $\lambda_{t+1}\ge1$ .
A run is a predicate on two sequences $x,y:\mathbb N\to\mathbb R^n$ , indexed from $1$ as in the book; index $0$ is unconstrained. Every theorem quantifies over all runs.
Standing assumptions: $x^*$ is a minimizer of $f$ (book, p. 242); $\beta>0$ (implicit in the step $1/\beta$ ) is a stated hypothesis.
The page prints the update as $x_{t+1}=(1-\gamma_s)y_{t+1}+\gamma_ty_t$ ; the formalization uses $\gamma_t$ in both places, as the proof's (3.26) requires. A run predicate with a fixed coefficient $\gamma_s$ would describe a different (non-accelerated) method and is ruled out.
The goal is stated for all $t\ge1$ , including $t=1$ , which the printed proof does not cover but which follows from (3.4). The growth bound $\lambda_{t-1}\ge t/2$ is stated for $t\ge2$ , since $\lambda_0=0$ . The telescoping display prints $\delta_s^2$ for $\delta_s$ ; the formalization uses $\delta_s$ .

Contributions of every kind are welcome: proofs of the λ facts and of (3.26) are pure algebra; (3.23)–(3.25) need the descent lemma for β-smooth functions and first-order convexity, both of which are reusable well beyond this mission.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983. mathnet
A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sciences 2(1):183–202, 2009. doi:10.1137/080716542
P. Tseng, On accelerated proximal gradient methods for convex-concave optimization, manuscript, 2008. pdf
A. Nemirovski, D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

10 thms3 active usersReviewed

Completed

Operations Research Optimal Transport Optimization+1·Captain: mikedeng1

Quantifying Distributional Model Risk via Optimal Transport 1: Strong Duality — the Worst-Case Expectation over an Optimal-Transport Ball on a Polish Space Equals Its Dual over (λ, φ)Research Paper

Motivation

A probability model $\mu$ for a random element $X$ is rarely known exactly. Distributionally robust performance analysis replaces the single expectation $E_\mu[f(X)]$ by its worst case over all models within a prescribed distance of $\mu$ . When the distance is an optimal-transport cost, the neighbourhood contains models whose support differs from that of $\mu$ . That matters in stochastic-process applications such as ruin probabilities for insurance reserves, where the natural alternatives (a compensated Poisson process against a Brownian motion) are mutually singular and likelihood-based divergences such as Kullback–Leibler are infinite.

Blanchet and Murthy (arXiv:1604.01446, Math. Oper. Res. 2019) prove that the worst-case expectation over an optimal-transport ball equals a one-dimensional dual problem. They assume only that the underlying space is Polish, the cost lower semicontinuous and the performance function upper semicontinuous and integrable.

Timeline. Esfahani and Kuhn (arXiv:1505.05116, 2015/2018) obtained a dual reformulation for Wasserstein balls around empirical measures on $\mathbb R^d$ . Gao and Kleywegt (arXiv:1604.02199, 2016) proved a general duality whose proof, as Blanchet and Murthy note, uses the local compactness of the space. Blanchet and Murthy (2016, v2 2017) removed local compactness and continuity of the cost. This covers path spaces such as $C[0,T]$ and $D[0,T]$ .

Setting

Let $S$ be a Polish space with Borel σ-algebra $\mathcal B(S)$ , and let $\mu$ be a probability measure on $S$ (the baseline model).

Cost (A1). $c : S\times S\to[0,\infty)$ is lower semicontinuous, and $c(x,y)=0$ if and only if $x=y$ .
Performance function (A2). $f : S\to\mathbb R$ is upper semicontinuous and $\mu$ -integrable.
Budget. $\delta>0$ .

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ whose first marginal is $\mu$ and whose transport cost satisfies $\int c\,d\pi\le\delta$ . The second marginal of $\pi$ is the alternative model. The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$ , and the primal value is

I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}.

The universal σ-algebra $\mathcal U(S)$ is the intersection of the completions of $\mathcal B(S)$ under all probability measures. Write $m\mathcal U(S;\bar{\mathbb R})$ for the $\mathcal U(S)$ -measurable functions $S\to[-\infty,\infty]$ . The dual feasible set $\Lambda_{c,f}$ consists of the pairs $(\lambda,\varphi)$ with $\lambda\ge0$ , $\varphi\in m\mathcal U(S;\bar{\mathbb R})$ and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$ . The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$ , and the dual value is $J=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\}$ . Finally,

\varphi_\lambda(x)=\sup_{y\in S}\{f(y)-\lambda c(x,y)\}\in\mathbb R\cup\{\infty\}.

Formalization targets

Goal: Theorem 1

Under (A1) and (A2):

strong duality,

\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\};

there is $\lambda^*\ge0$ such that $(\lambda^*,\varphi_{\lambda^*})$ is a dual optimizer;
a feasible $\pi^*$ and a feasible $(\lambda^*,\varphi_{\lambda^*})$ with finite $J(\lambda^*,\varphi_{\lambda^*})$ are optimal with $I(\pi^*)=J(\lambda^*,\varphi_{\lambda^*})$ if and only if the complementary slackness conditions hold:

f(y)-\lambda^*c(x,y)=\varphi_{\lambda^*}(x)\ \ \pi^*\text{-a.s.},\qquad \lambda^*\Big(\int c\,d\pi^*-\delta\Big)=0.

The "if" direction is stated without the finiteness assumption.

Milestones

Weak duality $I\le J$ (5). Lemma 15. Strong duality with a primal optimizer on compact $S$ , first for continuous costs (Proposition 5), then for lower semicontinuous ones (Proposition 6). Universal measurability of $\varphi_\lambda$ (§4.2). Lemma 16. The restricted dual bound of Proposition 7. Lemma 8. The univariate formula (9):

I=\inf_{\lambda\ge0}\Big\{\lambda\delta+E_\mu\Big[\sup_{y\in S}\{f(y)-\lambda c(X,y)\}\Big]\Big\}.

Significance

The result. Formula (9) turns an infinite-dimensional optimization over probability measures into a one-dimensional convex minimization that involves only the baseline $\mu$ . A modeller can therefore evaluate it by sampling from $\mu$ . Theorem 1 is the input for the worst-case probability formula for closed sets (Theorem 3 of the paper) and for the existence of worst-case transport plans (Corollary 1). Its complementary slackness conditions describe the structure of every worst-case plan: mass is moved from $x$ to maximizers of $f(z)-\lambda^*c(x,z)$ , and the budget is exhausted whenever $\lambda^*>0$ .

Formalizing it. The result is proved on paper. To our knowledge it has no machine-checked proof. The only related statement on Prove2Me is a special case (empirical baseline, bounded continuous loss, power-of-norm cost on $\mathbb R^m$ ). A complete development would contain duality on compact spaces via Fenchel duality, the extension to σ-compact supports, and measurable-selection arguments for universally measurable functions. The measurable-selection part reuses Bertsekas–Shreve's analytic-set theory, which is already posed on the platform.

Difficulty

The obvious route copies Kantorovich duality. That route fails here because the feasible set $\Phi_{\mu,\delta}$ fixes only one marginal, so it is not tight on a non-compact space. Prokhorov compactness is available only on compact pieces $S_n\times S_n$ . The duality must then be transported to the whole space by a limiting argument that keeps control of the dual multipliers.

A second obstacle is measurability. For a merely lower semicontinuous cost on a non-locally-compact space, $\varphi_\lambda$ need not be Borel measurable, so the dual must range over universally measurable functions. Removing the restriction $y\in S_\pi$ from the envelope (Lemma 8) needs a measurable selection theorem. Arguments that assume closed balls are compact do not apply in the target spaces $C[0,T]$ and $D[0,T]$ .

Formalization scope

Space and costs. S carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]. The cost is a real-valued curried function c : S → S → ℝ; (A1) is the structure AssumptionA1; (A2) is UpperSemicontinuous f together with Integrable f μ; and 0 < δ is assumed throughout.
Extended reals. $I$ , $J$ , $I(\pi)$ , $J(\lambda,\varphi)$ and $\varphi_\lambda$ live in EReal. The integral of an extended-real function is $\int\varphi^+-\int\varphi^-$ with lower Lebesgue integrals, and $\infty-\infty$ evaluates to $-\infty$ . A coupling with $\int f^-\,d\pi=\infty$ therefore never raises $I$ , which is the paper's reading in footnote 2.
Measurability and integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. For such $\varphi$ the lower integral equals the integral against the completion of $\mu$ .
Variants. The dual feasible set takes a set $K$ : with $K=S$ it is (6b), and with $K=S_\pi$ it is (29).
Hidden hypothesis. The "only if" part of Theorem 1(b) carries the hypothesis $J(\lambda^*,\varphi_{\lambda^*})<\infty$ . Without it the equivalence fails when $I=J=\infty$ .
Ruled-out trivializations. A primal that fixes both marginals (or neither), a dual over Borel-measurable $\varphi$ , and a Bochner integral for $\int f\,d\pi$ (which is $0$ off $L^1(\pi)$ ) all describe different problems and are ruled out by the definitions.
Infrastructure and contributions. Needed: Fenchel duality on $C_b(S\times S)$ and its dual $M(S\times S)$ (Riesz–Markov–Kakutani), Prokhorov's theorem, Sion's minimax theorem, and Jankov–von Neumann selection. Several are on the platform or in Mathlib, and all are reusable beyond this mission. Proofs of the milestones in any order, and of the posed Bertsekas–Shreve tools, are welcome.

Selected references

J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
D. Bertsekas and S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 7. MIT open copy
C. Villani, Optimal Transport: Old and New, Springer, 2008. doi:10.1007/978-3-540-71050-9

19 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Airline Seat Allocation with Multiple Nested Fare Classes 2: With Integer-Valued Demands an Optimal Integer Protection-Level Policy ExistsResearch Paper

Motivation

Airlines sell the seats of one flight leg at several prices. Cheaper fare classes tend to book earlier, so the seller must decide, as low-fare requests arrive, how many seats to hold back for later and more valuable passengers. The standard control is nested protection levels: a number $p_k$ of seats is reserved for the $k$ most expensive classes together, and a request of class $k+1$ is accepted only while more than $p_k$ seats remain. Littlewood (1972) gave the optimal rule for two classes; Belobaba's EMSR heuristic (1987, 1989) extended it to many classes without an optimality guarantee.

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes (Operations Research 41(1), 1993) treat any number of classes with independent random demands and characterize optimal protection levels by first-order conditions on the expected revenue: Theorem 1 states that a policy with $f_{k+1}$ in the subdifferential of the expected revenue of the $k$ highest classes at $p_k$ , for every $k$ , is optimal. Their Theorem 2 addresses the question practitioners face first: seats and bookings are whole numbers. If demand is integer valued, is an optimal policy available among integer protection levels? The theorem answers yes. This mission formalizes that theorem and the chain of results in its proof.

Timeline.

Littlewood (1972): two fare classes, rule $f_2 = f_1 \Pr[X_1 > p_1]$ .
Belobaba (1987, 1989): EMSR heuristic for many classes.
Curry (1990) and Wollmer (1992): multiple nested classes, continuous and discrete demand respectively.
Brumelle and McGill (1993): subdifferential optimality conditions for any number of classes (Theorem 1), existence of an optimal integer policy for integer demand (Theorem 2), and the probability conditions (31) (Theorem 3).

Setting

Classes are numbered $k = 1, 2, \dots$ , class $1$ paying the highest fare. Class $k$ has a random demand $X_k \ge 0$ and fare $f_k$ , with $f_1 > f_2 > \cdots$ . The demands are mutually independent on a probability space $(\Omega, \mathcal F, P)$ . A protection-level policy is a sequence $p = (p_1, p_2, \dots)$ with $p_k \ge 0$ ; the dummy level $p_0 = 0$ is never used.

For a demand vector $x$ and $s$ available seats, the revenue of the $k$ highest classes is defined recursively (Eqs. (8)–(9), p. 130):

R_1[s; p; x] = \begin{cases} f_1 s & 0 \le s < x_1,\\ f_1 x_1 & x_1 \le s,\end{cases}

R_{k+1}[s; p; x] = \begin{cases} R_k[s; p; x] & 0 \le s < p_k,\\ (s - p_k) f_{k+1} + R_k[p_k; p; x] & p_k \le s < p_k + x_{k+1},\\ x_{k+1} f_{k+1} + R_k[s - x_{k+1}; p; x] & p_k + x_{k+1} \le s.\end{cases}

The expected revenue is $ER_k[s; p; X] = E\,R_k[s; p; X]$ . A policy is optimal if it maximizes $ER_k[s; \cdot\,; X]$ for every $k$ and every $s \ge 0$ (p. 130).

For a function $g$ and $t \ge 0$ , $\delta_+ g(t)$ and $\delta_- g(t)$ are the right and left derivatives, with $\delta_- g(0) = +\infty$ , and the subdifferential is $\delta g(t) = [\delta_+ g(t), \delta_- g(t)]$ (p. 131). Condition (20) is

f_{k+1} \in \delta ER_k[p_k; (p_0, \dots, p_{k-1}); X], \qquad k = 1, 2, \dots

A function is CLBI (Concave and Linear Between Integers, p. 132) if it is concave on $s \ge 0$ and linear on each interval $[m, m+1]$ , $m = 0, 1, 2, \dots$

Formalization targets

Goal: Theorem 2 (p. 132)

If every $X_k$ is integer valued and the fares are positive, there is a policy $p^*$ with $p^*_k \in \{0, 1, 2, \dots\}$ such that

ER_k[s; q; X] \le ER_k[s; p^*; X] \qquad \text{for every policy } q,\ k \ge 1,\ s \ge 0,

and $p^*$ satisfies (20). The competitor $q$ ranges over all real protection levels.

Milestones (in proof order)

(27): $\delta ER_1[s; p; X] = [f_1 \Pr[X_1 > s], f_1 \Pr[X_1 \ge s]]$ , and $ER_1$ is CLBI.
Covering property (p. 132): if $g$ is CLBI and $\delta_+ g(s_2) < c < \delta_- g(s_1)$ with $s_1 < s_2$ , then $c \in \delta g(n)$ for an integer $n \in [s_1, s_2]$ .
(28)–(29): for $s \ge p_k$ ,

\delta_+ ER_{k+1}[s] = f_{k+1}\Pr[X_{k+1} > s - p_k] + \sum_{i=0}^{\lfloor s - p_k\rfloor} \delta_+ ER_k[s - i]\Pr[X_{k+1} = i],

and the analogous formula for $\delta_-$ at $s > p_k$ . 4. Corollary 1 (p. 131): concavity of $ER_k$ and $f_{k+1} \in \delta ER_k[p_k]$ give concavity of $ER_{k+1}$ . 5. CLBI propagation (p. 133): if $ER_k[\cdot; p^*; X]$ is CLBI and integer $p^*_1, \dots, p^*_k$ satisfy (20), then $ER_{k+1}[\cdot; p^*; X]$ is CLBI. 6. (30): for $s$ large enough, $\delta_+ ER_{k+1}[s; p; X] < f_{k+2}$ . 7. Theorem 1 (p. 131): a policy satisfying (20) is optimal.

Significance

The result. Theorem 2 justifies computing protection levels in whole seats: with integer demand, restricting to integer policies loses nothing against arbitrary real protection levels. The construction also shows that (20) is solvable at every level, so the sufficient condition of Theorem 1 is never empty for integer demand. Many later revenue-management models assume an optimal nested policy exists and rely on this result or its dynamic-programming analogues.

Formalizing it. The theorem is proved on the page by an induction on the class index, but several steps are compressed: (28)–(29) are printed without the range of $s$ on which they hold, and (30) is asserted "by recursive application". To our knowledge none of these statements has a machine-checked proof. A formal development gives a verified account of one-sided derivatives of expectations of piecewise-linear random functions and of the integer covering property. These pieces are reusable for other newsvendor-type and nested-inventory models. The probability-condition characterization (Theorem 3) is the subject of a companion mission in the same series.

Difficulty

Concavity of the expected revenue does not hold for arbitrary policies. It is only guaranteed level by level, when the protection level already chosen at level $k$ satisfies (20). Existence of an integer optimum therefore cannot be obtained by rounding a real optimum: the integer levels must be chosen one at a time, and each choice must preserve both concavity and the CLBI shape needed for the next. A second obstacle is analytic. The one-sided derivatives of $ER_{k+1}$ are expectations of derivatives of a random piecewise-linear function. Exchanging differentiation and expectation, and computing the sums in (28)–(29) exactly at integer and non-integer $s$ , is where informal arguments and formal ones diverge. Finally there are infinitely many classes, so the policy $p^*$ is an infinite sequence built by recursion.

Formalization scope

Model. Classes are indexed by $\mathbb N$ from $1$ ; fares, demands and protection levels are sequences $\mathbb N \to \mathbb R$ . Seats, demands and protection levels are real; an integer policy is a sequence of natural numbers read as reals. Integer-valued demand means each $X_k(\omega)$ is a natural number. Expectations are Bochner integrals.
Standing assumptions (§1). $P$ is a probability measure. The demands are measurable, nonnegative and mutually independent, and the fares are strictly decreasing.
Added hypotheses. The goal assumes positive fares, $f_k > 0$ for $k \ge 1$ . The page leaves this implicit (fares are average revenues), and without it the theorem is false. The same assumption appears in (30), and (27) assumes $f_1 \ge 0$ , without which $ER_1$ is convex rather than concave.
Derivatives. One-sided derivatives are required to exist, with their value asserted; no default value of an undefined derivative is used. The convention $\delta_- g(0) = +\infty$ is built into the subdifferential.
Optimality. Optimality is global: against every real protection-level policy, at every level $k \ge 1$ and every $s \ge 0$ .
Paper's slips corrected. (28)–(29) are stated on their range $s \ge p_k$ (resp. $s > p_k$ ). (30) is stated for every $k \ge 1$ , as the induction uses it, rather than the printed $k = 2, 3, \dots$
Not a trivialization. The goal assumes only the model, integer demand and positive fares. It does not assume concavity, CLBI, (20) or any derivative formula, and optimality is not restricted to integer competitors or to one $k$ .
Duplication. Corollary 1 and Theorem 1 are restated from the companion mission in this series.
Contributions. Proofs of the measure-theoretic derivative lemmas, of the covering property (a statement about real functions), and of the induction are all welcome.

Selected references

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1):127–137, 1993. https://doi.org/10.1287/opre.41.1.127
K. Littlewood, Forecasting and Control of Passenger Bookings, AGIFORS Symposium Proceedings 12:95–117, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, 1987. http://hdl.handle.net/1721.1/68077
P. P. Belobaba, Application of a Probabilistic Decision Model to Airline Seat Inventory Control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
R. E. Curry, Optimal Airline Seat Allocation with Fare Classes Nested by Origins and Destinations, Transportation Science 24(3):193–203, 1990. https://doi.org/10.1287/trsc.24.3.193
R. D. Wollmer, An Airline Seat Management Model for a Single Leg Route When Lower Fare Classes Book First, Operations Research 40(1):26–37, 1992. https://doi.org/10.1287/opre.40.1.26

Related work on the platform. The two-class, integer-capacity EMSR rule of Belobaba (1987) is formalized as SeatInventory.Nested.emsr_protection_level_optimal. It is a relative of the $k = 1$ case of Theorem 2, but it lives in a different model: two classes, a fixed integer capacity, and only integer competitors.

70 thms3 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Rademacher and Gaussian Complexities: Risk Bounds and Structural Results 6: The Expected Maximum Discrepancy Lies Between R_n(F)/2 − 2√(2/n) and R_n(F) + 4√(2/n)Research Paper

Motivation

Data-dependent risk bounds in statistical learning theory control the gap between the expected loss of a learned function and its empirical loss by a complexity penalty that is computed from the training data. The first such penalties were the maximum discrepancy of a function class (Bartlett, Boucheron and Lugosi, Model selection and error estimation, Machine Learning 48, 2002) and its Rademacher complexity (Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Trans. Inf. Theory 47, 2001; Koltchinskii and Panchenko 2000). The maximum discrepancy compares the behaviour of the class on two fixed halves of the sample; the Rademacher complexity compares it on two random halves. Bartlett and Mendelson (JMLR 3, 2002), Lemma 3, show that these two quantities are equivalent up to a factor 2 and an additive $O(1/\sqrt n)$ . This mission formalizes that lemma from the published JMLR article (pp. 463–482); the proof is its Appendix A.

Setting

Let $\mu$ be a probability measure on a measurable space $\mathcal X$ and let $X_1,\dots,X_n$ be independent samples from $\mu$ . Let $F$ be a class of measurable functions $f:\mathcal X\to[-1,1]$ . Let $\sigma_1,\dots,\sigma_n$ be independent uniform $\{\pm1\}$ -valued random variables, independent of the sample.

The Rademacher complexity of $F$ is

R_n(F) = \mathbf E\sup_{f\in F}\left|\frac2n\sum_{i=1}^n\sigma_i f(X_i)\right|.

For even $n$ , the maximum discrepancy of $F$ is the random variable

\hat D_n(F) = \sup_{f\in F}\left(\frac2n\sum_{i=1}^{n/2}f(X_i) - \frac2n\sum_{i=n/2+1}^n f(X_i)\right),

with no absolute value, and the expected maximum discrepancy is $D_n(F)=\mathbf E\hat D_n(F)$ . The class is closed under negation if $f\in F$ implies $-f\in F$ , and $-F=\{-f:f\in F\}$ .

The proof works with the conditional supremum function

s(N) = \frac2n\,\mathbf E\left[\sup_{f\in F}\sum_{i=1}^n\sigma_i f(X_i)\;\middle|\;\sum_{i=1}^n\sigma_i=N\right],

defined for the values $N$ that $\sum_i\sigma_i$ can take.

Formalization targets

Goal: Lemma 3, first and second displays

For every even $n\ge2$ ,

\frac{R_n(F)}{2} - 2\sqrt{\frac2n} \le D_n(F) \le R_n(F) + 4\sqrt{\frac2n},

and if $F$ is closed under negation,

R_n(F) - 4\sqrt{\frac2n} \le D_n(F).

Milestones (Appendix A, pp. 479–480)

$R_n(F)\ge\mathbf E\,s(\sum_i\sigma_i)$ , with equality when $F$ is closed under negation.
$D_n(F) = s(0)$ .
$|s(N_1)-s(N_2)|\le 4|N_2-N_1|/n$ .
$|\mathbf E s(N)-s(\mathbf EN)|\le\mathbf E|s(N)-s(\mathbf EN)|\le4\sqrt{2/n}$ for $N=\sum_i\sigma_i$ .
$R_n(F)=R_n(F\cup-F)\le D_n(F\cup-F)+4\sqrt{2/n}$ .
$D_n(F\cup-F)\le 2D_n(F)+D_n(\{f_0,-f_0\})$ for any $f_0\in F$ (a corrected form of the printed step, see below).

Significance

Lemma 3 makes the maximum discrepancy and the Rademacher complexity interchangeable in risk bounds: a bound in terms of one gives a bound in terms of the other with an explicit additive loss. The maximum discrepancy can be computed by a single empirical risk minimization on a relabelled sample, while the Rademacher complexity has the structural properties (monotonicity, convex-hull invariance, contraction) that make it easy to bound for concrete classes; the lemma transfers the second kind of estimate to the first quantity.

The lemma is proved in the paper; no machine-checked proof of it, or of the comparison between fixed and random half-sample splits, is known to exist. Formalizing it requires the exchangeability argument for i.i.d. samples, the conditioning of a uniform sign vector on its sum, and a moment bound for the Rademacher sum $\sum_i\sigma_i$ , all with explicit constants.

Difficulty

The heart of the proof is that, conditioned on the number of positive signs, a uniform sign vector splits the i.i.d. sample into two random subsets of fixed sizes, and every split of the same sizes has the same law as the fixed split. Making this precise requires a permutation-invariance argument for product measures applied to a supremum over an arbitrary class, where measurability is not automatic. The step from classes closed under negation to general classes is where the printed argument is loose: since $\hat D_n$ has no absolute value, $\hat D_n(F\cup-F)$ is a maximum of two suprema that may be negative, and the naive bound $D_n(F\cup-F)\le2D_n(F)$ fails.

Formalization scope

The Lean development lives in the namespace RadGauss.Discrepancy. Sign vectors are Fin n → Bool (true ↦ 1, false ↦ -1) and expectations over signs are finite averages over all $2^n$ sign vectors; $s(N)$ is the average over the sign vectors with sum $N$ . $R_n$ takes values in $[0,\infty]$ (a lower Lebesgue integral of an $[0,\infty]$ -valued supremum), while $\hat D_n$ , $D_n$ and $s$ are real, because the maximum discrepancy is signed. Inequalities of the form $a-c\le D$ are written $a\le D+c$ with real terms embedded by ENNReal.ofReal; this is equivalent to the printed form since $D_n(F)\ge0$ for nonempty $F$ .

Hypotheses added to the page, all disclosed in each item:

the sample size is even, $n=2m$ with $m\ge1$ , since $\hat D_n$ needs half sums;
$F$ is nonempty (the supremum over the empty class is $-\infty$ in the paper and $0$ in Lean);
every $f\in F$ is measurable, and for every sign vector $\sigma$ the map $x\mapsto\sup_{f\in F}\sum_i\sigma_if(x_i)$ is measurable. This is the measurability guard: without it the Bochner integrals defining $D_n$ and $s$ would silently be $0$ .

Corrections of printed statements:

The Lipschitz bound on $s$ is printed for $0\le n_2<n_1\le n$ but used for negative values of $\sum_i\sigma_i$ ; it is stated for every pair of attainable values.
The printed step $D_n(F\cup-F)\le2D_n(F)$ is false for the signed $\hat D_n$ of p. 464 ( $F=\{f\}$ , $f(X)$ uniform on $\{\pm1\}$ , $n=2$ gives $1\le0$ ); the milestone states it with the additional term $D_n(\{f_0,-f_0\})\le2/\sqrt n$ . The goal itself remains true.
The third display of Lemma 3, $P\{|\hat D_n(F)-D_n(F)|\ge\epsilon\}\le2\exp(-\epsilon^2n/2)$ , is false as printed ( $F=\{f\}$ as above, $n=2$ , $\epsilon=2$ : the probability is $1/2>2e^{-4}$ ) and is not part of the mission.

A formalization in which $D_n$ or $s$ is a junk value (non-integrable or non-measurable suprema, an empty class, an odd sample size with truncated $n/2$ ) would make the goal trivial or meaningless; the hypotheses above rule that out, and the class $F=\{0\}$ satisfies all of them.

Welcome contributions include general lemmas on the invariance of $\mathbf E\sup_{f\in F}\Phi_f(X_{\pi(1)},\dots,X_{\pi(n)})$ under permutations $\pi$ of an i.i.d. sample, conditioning of uniform sign vectors on their sum, and the bound $\mathbf E|\sum_i\sigma_i|\le\sqrt n$ . These are reusable well beyond this mission.

Selected references

P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002) 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48 (2002) 85–113. https://doi.org/10.1023/A:1013999503812
V. Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Transactions on Information Theory 47 (2001) 1902–1914. https://doi.org/10.1109/18.930926
L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5

10 thms3 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Rademacher and Gaussian Complexities: Risk Bounds and Structural Results 5: Kernel Expansions with α′Kα ≤ B² Have Rademacher and Gaussian Complexity at Most 2B√(E k(X,X)/n)Research Paper

Motivation

Kernel methods, such as support vector machines, predict with functions of the form $x \mapsto \sum_i \alpha_i k(x, x_i)$ : finite expansions of a fixed similarity function $k$ centred at data points. Their statistical behaviour is governed by the size of the class of such expansions that the method searches. Bartlett and Mendelson, in Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002), develop risk bounds in terms of the Rademacher and Gaussian complexities of a class, and in §4.3 (pp. 476–478) compute these complexities for the class of kernel expansions whose coefficient vector has quadratic form $\alpha' K \alpha \le B^2$ . The resulting bound depends on the kernel only through its diagonal $k(x,x)$ , which is what makes margin bounds for support vector machines dimension-free. This mission formalizes that computation. The source is the published JMLR article (pages cited by the journal's printed numbers).

Setting

Let $\mathcal X$ be a compact topological space. A kernel is a continuous function $k : \mathcal X \times \mathcal X \to \mathbb R$ such that for every $m$ and all $x_1, \dots, x_m \in \mathcal X$ the Gram matrix $K_{ij} = k(x_i, x_j)$ is symmetric and positive semidefinite. For $B \ge 0$ the class of kernel expansions is

F = \Big\{x \mapsto \sum_{i=1}^m \alpha_i k(x, x_i) : m \in \mathbb N,\ x_i \in \mathcal X,\ \alpha_i \in \mathbb R,\ \sum_{i,j}\alpha_i\alpha_j k(x_i, x_j) \le B^2\Big\},

with centres anywhere in $\mathcal X$ (Lean: kernelClass k B).

For a class $F$ of real functions on $\mathcal X$ and a sample $x_1, \dots, x_n$ , let $\sigma_1, \dots, \sigma_n$ be independent uniform signs and $g_1, \dots, g_n$ independent standard Gaussians. The empirical Rademacher complexity and empirical Gaussian complexity (Definition 2, p. 464) are

\hat R_n(F) = \mathbb E_\sigma \sup_{f\in F}\Big|\frac2n\sum_{i=1}^n \sigma_i f(x_i)\Big|, \qquad \hat G_n(F) = \mathbb E_g \sup_{f\in F}\Big|\frac2n\sum_{i=1}^n g_i f(x_i)\Big|.

For a probability measure $\mu$ on $\mathcal X$ and an i.i.d. sample $X_1, \dots, X_n \sim \mu$ , the Rademacher complexity is $R_n(F) = \mathbb E \hat R_n(F)$ and the Gaussian complexity is $G_n(F) = \mathbb E \hat G_n(F)$ (Lean: empiricalRademacher, empiricalGaussian, rademacherComplexity, gaussianComplexity).

A feature map of $k$ is a map $\Phi : \mathcal X \to \mathcal H$ into a real Hilbert space with $k(x_1, x_2) = \langle \Phi(x_1), \Phi(x_2) \rangle$ .

Formalization targets

Goal: the expected complexity bound (§4.3, p. 478, display after the proof of Lemma 22)

With $X \sim \mu$ ,

R_n(F) \le 2B\sqrt{\frac{\mathbb E\, k(X,X)}{n}}, \qquad G_n(F) \le 2B\sqrt{\frac{\mathbb E\, k(X,X)}{n}}.

Milestone 1: feature-map inclusion (p. 477)

For any feature map $\Phi$ of $k$ , $\|\sum_i \alpha_i \Phi(x_i)\|^2 = \sum_{i,j}\alpha_i\alpha_j k(x_i,x_j)$ , and hence $F \subseteq \{x \mapsto \langle w, \Phi(x)\rangle : \|w\| \le B\}$ .

Milestone 2: Lemma 22 (p. 477)

For every sample $X_1, \dots, X_n$ ,

\hat G_n(F) \le \frac{2B}{n}\sqrt{\sum_{i=1}^n k(X_i, X_i)}, \qquad \hat R_n(F) \le \frac{2B}{n}\sqrt{\sum_{i=1}^n k(X_i, X_i)}.

Significance

The goal shows that the kernel class has complexity of order $n^{-1/2}$ , with a constant given by $B$ and the quantity $\mathbb E\, k(X,X)$ , which is the trace of the integral operator $T_k f = \int k(\cdot, y) f(y)\, d\mu(y)$ on $L_2(\mu)$ . No dimension of the feature space enters. Fed into the paper's margin-cost risk bound (Theorem 21, p. 476), the sample-wise Lemma 22 gives a data-dependent misclassification bound for support vector machines in terms of the trace of the Gram matrix of the training sample. Bounds of this form are the standard complexity estimate for kernel classes in learning theory textbooks.

The result is proved in the paper; nothing in this mission is open mathematics. What the mission adds is a machine-checked version with the paper's normalization (factor $2/n$ , absolute value inside the supremum), covering both the Rademacher and the Gaussian complexity, for expansions with centres anywhere in $\mathcal X$ . Related statements on the platform (Mohri et al.'s Theorem 5.10 and Proposition 9.3) use the $1/n$ normalization without absolute value, assume a uniform bound $\sup_x k(x,x) \le r^2$ , and treat only the Rademacher case, so they do not imply the targets here.

Difficulty

The class $F$ is defined through the kernel, not through a feature map, and its expansions have arbitrarily many centres anywhere in $\mathcal X$ . The supremum over $F$ is therefore a supremum over an infinite-dimensional family, and must be controlled without assuming a separate numerical upper bound on $k(x,x)$ or that the feature space is finite dimensional. For the Gaussian complexity the supremum sits inside an expectation over a continuous random vector, and the passage from the sample-wise bound to the expected bound must move an expectation inside a square root in the right direction. A bound with $\sup_x k(x,x)$ in place of $\mathbb E\, k(X,X)$ is weaker and is not the target.

Formalization scope

Conventions committed to in Lean:

Complexities take values in $[0, \infty]$ (ℝ≥0∞); expectations over the Gaussian vector and over the sample are lower Lebesgue integrals against product measures, and the Rademacher expectation is the exact average over the $2^n$ sign vectors $\sigma : \mathrm{Fin}\,n \to \mathbb Z^\times$ . An unbounded class has complexity $+\infty$ , so a junk value of $0$ for a real supremum or a non-integrable expectation cannot make the bounds trivial.
A kernel (IsKernel k) carries compactness of $\mathcal X$ , joint continuity, and positive semidefiniteness (with symmetry) of every Gram matrix, as in the paper's definition. The goal puts the Borel $\sigma$ -algebra on $\mathcal X$ and assumes $\mu$ is a probability measure; $\mathbb E\, k(X,X)$ is the Bochner integral of the continuous function $x \mapsto k(x,x)$ .
$B \ge 0$ is assumed in every statement (the paper fixes $B > 0$ ). For $B < 0$ the right-hand sides are negative while the left-hand sides are not, and the inclusion of milestone 1 fails.
No $n \ge 1$ hypothesis: at $n = 0$ both sides of every bound are $0$ in Lean.
The feature map in milestone 1 is a hypothesis (any real Hilbert space and any $\Phi$ with $k = \langle \Phi(\cdot), \Phi(\cdot)\rangle$ ); its existence is the RKHS theorem, referenced as the supporting platform item FoundationsML.Kernels.RKHS_exists.
No measurability or integrability hypotheses on $\hat R_n(F)$ or $\hat G_n(F)$ are assumed, and none is needed.

A trivializing formalization is ruled out: the goal is stated for the kernel class $F$ itself, not for the larger ball of linear functionals of a feature map, and not for the subclass with centres at the sample points.

Infrastructure a complete development needs: Gaussian integration over $\mathbb R^n$ (second moments of a standard Gaussian vector), Jensen's inequality for the square root under a lower Lebesgue integral, and Cauchy–Schwarz for positive semidefinite bilinear forms (or the RKHS feature map). The Definition 2 complexities are shared with the paper's other missions and reusable. Contributions of any of these milestones, and of proofs of the goal that avoid the feature map, are welcome.

Selected references

P. L. Bartlett and S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
N. Cristianini and J. Shawe-Taylor, An Introduction to Support Vector Machines, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511801389
N. Aronszajn, Theory of Reproducing Kernels, Transactions of the American Mathematical Society 68 (1950), 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
M. Mohri, A. Rostamizadeh and A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/

8 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

On the Graph Structure of Convex Polyhedra in n-Space II: Whitney's Theorem, a Graph Is n-Tuply Connected iff Any Two Points Are Joined by n Disjoint PathsResearch Paper

Motivation

Vertex connectivity measures how robust a network is against the failure of nodes. It can be measured in two ways that look different. One way counts the fewest nodes whose removal disconnects the network. The other counts the routes between two nodes that share no intermediate node. Whitney's theorem (1932) says that the two measures agree for every pair of nodes. It is the vertex form of Menger's theorem, and it underlies reliability analysis of communication and transportation networks, the design of fault-tolerant routing, and much of structural graph theory.

M. L. Balinski's 1961 paper On the graph structure of convex polyhedra in n-space proves that the graph of a bounded full-dimensional polyhedron in $n$ -space is $n$ -tuply connected (the subject of Mission I of this series). It then invokes Whitney's theorem to conclude that any two vertices of such a polyhedron are joined by $n$ disjoint paths. Balinski gives a short new proof of Whitney's theorem through the max-flow min-cut theorem of Ford and Fulkerson and of Dantzig and Fulkerson. That makes the theorem a consequence of linear programming duality. This mission formalizes that part of the paper: the network vocabulary, the max-flow min-cut theorem with capacities on both points and lines, the integrality of maximum flows, and Whitney's theorem itself.

Timeline.

1927: Menger states the disjoint-paths theorem for separating sets.
1932: Whitney proves the characterization of $n$ -connected graphs by $n$ disjoint paths between every pair of points.
1956: Ford and Fulkerson and Dantzig and Fulkerson prove the max-flow min-cut theorem.
1961: Balinski derives Whitney's theorem from it with a unit-capacity network.

Setting

A graph $G$ consists of a finite set $V$ of points and a set of lines, each line being a pair of distinct points. A path from $p_s$ to $p_k$ is a sequence of lines $(p_1,p_2),(p_2,p_3),\dots,(p_m,p_{m+1})$ with $p_1 = p_s$ , $p_{m+1} = p_k$ and $m \ge 1$ . Paths are disjoint if they have no point in common except possibly their first and last points.

$G$ is $n$ -tuply connected if it has at least $n+1$ points and, for every set $X$ of fewer than $n$ points, the graph $G - X$ remaining after deleting $X$ is connected. $G$ has $n$ disjoint paths from $p_s$ to $p_k$ if there are $n$ pairwise distinct paths from $p_s$ to $p_k$ , none of which repeats a point, and no two of which share a point other than $p_s$ and $p_k$ .

A network is a connected graph with a capacity $c(x) \ge 0$ on every point and $c(e) \ge 0$ on every line, and with a distinguished source $p_s$ and sink $p_k$ . A flow assigns a number $f(C) \ge 0$ to every path $C$ from $p_s$ to $p_k$ , such that for every point $x$ and every line $e$

\sum_{C \ni x} f(C) \le c(x), \qquad \sum_{C \ni e} f(C) \le c(e).

Its value is $\operatorname{val}(f) = \sum_C f(C)$ . A disconnecting set is a pair $(X,F)$ of points and lines that meets every walk from $p_s$ to $p_k$ . Its value is $\sum_{x\in X} c(x) + \sum_{e \in F} c(e)$ .

The unit network of the proof has capacity $1$ on every point except $p_s$ and $p_k$ , and capacity $n+1$ on every line except the line $p_sp_k$ (if present), which has capacity $1$ . In Lean these are IsNTuplyConnected, HasNDisjointPaths, IsFlow, flowValue, IsDisconnecting, cutValue, unitCapV and unitCapE, all in the namespace Balinski61.Whitney.

Formalization targets

Goal: Whitney's theorem (p. 434)

For a finite graph $G$ with at least two points and any $n \ge 0$ :

G \text{ is } n\text{-tuply connected} \iff \text{for all } p_s \ne p_k,\ G \text{ has } n \text{ disjoint paths from } p_s \text{ to } p_k.

Both directions are part of the goal.

Milestones, in the order of the proof

Max-flow min-cut (p. 433). In every network there is a number $M$ that is the value of some flow and of some disconnecting set, with every flow of value at most $M$ and every disconnecting set of value at least $M$ .
Integrality (p. 434). If all capacities are integers, some maximum flow has only integer path flows.
Min-cut in the unit network (p. 434). If $G$ is $n$ -tuply connected and $p_s \ne p_k$ , every disconnecting set of the unit network has value at least $n$ .
Paths from unit flows (p. 434). An integral flow of value at least $n$ in the unit network yields $n$ disjoint paths from $p_s$ to $p_k$ .
Sufficiency (p. 434). If every pair of distinct points is joined by $n$ disjoint paths, $G$ is $n$ -tuply connected.

Significance

Whitney's theorem turns a statement about all small deletion sets into the existence of explicit, verifiable path systems, and back again. In applications it certifies connectivity by exhibiting paths, and it certifies that connectivity is no larger by exhibiting a separating set. It is the base of the theory of $k$ -connected graphs: ear decompositions, the fan lemma, and the structure of minimally $k$ -connected graphs all use it. Inside this paper it supplies the COROLLARY that any two vertices of a bounded full-dimensional polyhedron in $n$ -space are joined by $n$ disjoint edge paths.

None of these results is formalized for vertex connectivity at this Mathlib revision. Mathlib has edge connectivity and connected components but no vertex Menger theorem. The Prove2Me library has max-flow min-cut statements for arc capacities only and integrality results for basic solutions of network LPs, but no flow model with capacities on points. A completed development gives a reusable vertex-capacitated max-flow min-cut theorem for undirected graphs and the first machine-checked Whitney theorem in this library. The results are classical and proved; the remaining work is the formalization.

Difficulty

The sufficiency direction is elementary. The necessity direction needs a global object (a flow, or a family of paths) to exist from purely local hypotheses about deletions. The obvious induction on $n$ , which deletes a point and applies the hypothesis to a smaller graph, does not keep the path systems disjoint. In Balinski's route the weight falls on max-flow min-cut and integrality for path flows with capacities on points, neither of which exists in the library. A second difficulty sits in a case the paper's proof skips: a disconnecting set of the unit network may use the line $p_sp_k$ (capacity $1$ ) together with up to $n-2$ points, and the deletion hypothesis of $n$ -tuple connectedness speaks only about points.

Formalization scope

Graphs are Mathlib SimpleGraphs on a Fintype with decidable equality and adjacency. Paths are walks with IsPath. A flow is a real function on the finite type G.Path ps pk of simple paths; "through a point" and "through a line" mean membership in the walk's support and edge list. Capacities are functions V → ℝ and Sym2 V → ℝ. Nonnegativity, connectivity of $G$ and $p_s \ne p_k$ are hypotheses of the network theorems.

The following readings of loose phrases are explicit in the statements:

"dropping out $n-1$ or fewer points" is $|X| < n$ ;
" $n$ disjoint paths" means $n$ pairwise distinct simple paths. The printed path syntax permits repeated vertices; in a graph with lines $p_s a$ , $p_s b$ , and $p_s p_k$ , the distinct walks $p_s,a,p_s,p_k$ and $p_s,b,p_s,p_k$ share only their endpoints even though the graph is not $2$ -tuply connected. The theorem therefore uses its conventional simple-path reading;
path flows live on simple paths (merging and shortcutting changes no maximum value);
the paper leaves the capacities of $p_s$ and $p_k$ in the unit network unassigned, and here they are $n+1$ ;
"the condition is sufficient is obvious" is the full statement that $n$ -tuple connectedness follows;
the hypothesis $|V| \ge 2$ is added to the goal and to sufficiency, because the paper's "any pair of points" presupposes it and the equivalence fails for a one-point graph.

The max-flow min-cut milestone states that the maximum and the minimum are attained. A statement that only bounds some flow by every cut is satisfied by the zero flow. A connectivity notion without the $n+1$ point count would make every complete graph $n$ -connected for all $n$ . Both trivializations are excluded.

Contributions welcome: a vertex-capacitated augmenting-path or LP-duality proof of max-flow min-cut for path flows, integrality by an augmenting-path argument, the unit-network lemmas, and direct combinatorial proofs of Whitney's theorem that bypass flows.

Selected references

M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian J. Math. 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
G. B. Dantzig and D. R. Fulkerson, On the max-flow min-cut theorem of networks, in Linear Inequalities and Related Systems, Ann. of Math. Stud. 38, Princeton Univ. Press, 1956, 215–221. https://doi.org/10.1515/9781400881987
K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115

9 thms3 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability+1·Captain: mikedeng1

Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms I: The Nonparametric Learn-then-Price Policy Has Regret at Most C(log n)^{1/2}/n^{1/4}Research Paper

Why price without knowing demand

A seller with a fixed stock of a single product and a finite selling season has to set prices without knowing how demand responds to them. This is the standard situation in revenue management: airline seats, hotel rooms, fashion goods and event tickets. The classical theory of dynamic pricing (Gallego and van Ryzin, 1994) assumes that the demand function $\lambda(p)$ , the rate of purchase requests at price $p$ , is known. In practice it has to be learned from sales, while the season runs and the stock is consumed.

Besbes and Zeevi (2009) asked how much revenue is lost for not knowing $\lambda$ . They answered it with explicit policies and matching-order bounds. Their setting differs from the multi-armed bandit literature it borrows from in three ways:

the problem is constrained by an initial inventory;
the set of prices is a continuum;
the set of possible demand functions is a nonparametric class.

This mission formalizes their first main result, Proposition 1: a simple learn-then-price policy has worst-case relative regret of order $(\log n)^{1/2}n^{-1/4}$ in a market of size $n$ .

Setting

Prices. Fix $0<\underline p<\overline p<\infty$ and an off price $p_\infty>0$ outside $[\underline p,\overline p]$ . The seller may charge any price in $[\underline p,\overline p]\cup\{p_\infty\}$ ; charging $p_\infty$ stops demand.

Demand. Requests arrive as a Poisson process whose intensity at time $t$ is $\lambda(p(t))$ . Let $N$ be a unit-rate Poisson process. By the time change (1), the cumulative requests up to time $t$ under a price path $p(\cdot)$ are $N\big(\int_0^t\lambda(p(s))\,ds\big)$ . The seller starts with inventory $x$ and sells until either the horizon $T$ ends or the stock runs out. The expected revenue of a policy $\pi$ is $J^\pi(x,T;\lambda)$ .

Demand class. $\mathcal L=\mathcal L(M,\underline K,\overline K,m)$ is the set of regular demand functions satisfying Assumption 1. Regular means:

$\lambda\ge0$ and $\lambda(p_\infty)=0$ ;
$\lambda$ is non-increasing on $[\underline p,\overline p]$ , with inverse $\gamma$ ;
the revenue rate $r(l)=l\gamma(l)$ is concave.

Assumption 1 requires:

(i) $\lambda\le M$ on $[\underline p,\overline p]$ ;
(ii) $\lambda$ is $\overline K$ -Lipschitz and $\gamma$ is $\underline K^{-1}$ -Lipschitz;
(iii) $\max_p p\lambda(p)\ge m$ .

Benchmark. The deterministic relaxation (5) replaces the random demand by its mean:

J^D(x,T\mid\lambda)=\sup\Big\{\int_0^T p(s)\lambda(p(s))\,ds:\int_0^T\lambda(p(s))\,ds\le x\Big\}.

The regret of a policy is $\mathcal R^\pi=1-J^\pi/J^D$ .

Scaling. In a market of size $n$ the inventory is $nx$ and the demand function is $n\lambda$ , as in (11). The corresponding quantities are $J^\pi_n$ , $J^D_n=nJ^D$ and $\mathcal R^\pi_n$ .

Algorithm 1, $\pi(\tau,\kappa)$ . The policy has three phases.

Learning. On $[0,\tau]$ it tests $\kappa$ equally spaced prices $p_i=\underline p+(i-1)(\overline p-\underline p)/\kappa$ , each for $\Delta=\tau/\kappa$ time units. It estimates $\lambda(p_i)$ by the normalized request counts $\hat\lambda(p_i)$ .
Optimization. It chooses $\hat p^u=\arg\max_i p_i\hat\lambda(p_i)$ and $\hat p^c=\arg\min_i|\hat\lambda(p_i)-x/T|$ , and sets $\hat p=\max\{\hat p^u,\hat p^c\}$ .
Pricing. It charges $\hat p$ on $(\tau,T]$ until the stock runs out.

Formalization targets

Goal: Proposition 1

Let $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$ , and let $\pi_n=\pi(\tau_n,\kappa_n)$ . Then there is a finite constant $C$ , independent of $\lambda$ and $n$ , such that

\sup_{\lambda\in\mathcal L}\mathcal R^{\pi}_n(x,T;\lambda)\le\frac{C(\log n)^{1/2}}{n^{1/4}}\qquad(n\ge2).

The constant is left unspecified, as in the paper. Its dependence on the class parameters, $x$ and $T$ is "somewhat complex" (p. 12), and the order $(\log n)^{1/2}n^{-1/4}$ is the content of the result.

Milestones

The milestones follow the proof in the appendix, in order:

the scaling $J^D_n=nJ^D$ (p. 12);
Fact 1, $J^D\ge m\min\{T,x/M\}$ on $\mathcal L$ ;
Lemma 1, the solution of (5): charge $p^D=\max\{p^u,p^c\}$ until the stock runs out;
Lemma 2, a Poisson deviation bound;
the revenue lower bound (A-2);
Lemma 3, the learned price is near $p^D$ with high probability;
Lemma 4 and the Case 1 bound (A-11), for $\lambda(\overline p)\le x/T$ ;
Lemma 5 and the Case 2 bound (A-15), for $\lambda(\overline p)>x/T$ ;
the Step 4 bound $\mathcal R^\pi_n\le C_{12}(u_n+\tau_n)$ , where $u_n=(\log n)^{1/2}\max\{1/\kappa_n,(n\Delta_n)^{-1/2}\}$ .

Significance

Proposition 1 shows that a seller who knows only a nonparametric class of demand functions can approach the full-information revenue uniformly over the class. Learning costs a vanishing fraction of revenue, and the policy needs no parametric model. Together with the paper's lower bound of order $n^{-1/2}$ for every admissible policy (Proposition 2, not in this mission), it brackets the minimax regret of nonparametric pricing under an inventory constraint. The result is a reference point for the learning-and-earning literature in operations management that followed it.

The result is proved in the paper; to our knowledge, it has no machine-checked proof. Formalizing it requires:

a working theory of policies driven by a time-changed Poisson process, with sales capped by an inventory;
the deterministic relaxation of Gallego and van Ryzin for a continuum of prices with an off price;
uniform (over the class) Poisson concentration bounds.

The mission produces Lean statements of all of these. A proof would also check every constant chain of the appendix, where the argument uses some displays in a form slightly different from their printed statement (see the scope section).

Difficulty

The obvious argument controls the estimation error at the tested prices and concludes that $\hat p$ is close to the optimal price. It breaks in two places.

First, $p^D$ is the larger of two prices, the revenue maximizer and the price that sells the inventory exactly. Near the boundary between these regimes, the revenue rate at $\hat p$ is not controlled by the error in $\hat p$ alone: it needs the concavity of the revenue rate and the inverse Lipschitz bound on $\gamma$ .

Second, when demand at the highest price exceeds the inventory rate ( $\lambda(\overline p)>x/T$ ), the revenue is limited by stock-outs rather than by the price. The bound must then show that nearly all of the inventory is sold during the pricing phase, uniformly over the class.

Throughout, every constant must be independent of the demand function, so the estimates have to hold uniformly over an infinite-dimensional class.

Formalization scope

Poisson process. The demand is driven by IsPoissonProcess N 1 on a probability space $(\Omega,\mathbb P)$ , a published platform definition: ℕ-valued, $N(0)=0$ , monotone paths, independent Poisson increments. The time change (1) is rendered by evaluating $N$ at cumulative intensities.
Inventory. The inventory of the market of size $n$ is $\lfloor nx\rfloor$ units, and sales are $\min\{N(\cdot),\lfloor nx\rfloor\}$ . The cap is never dropped.
Revenue. $J^\pi_n$ is the Bochner expectation of a bounded, finitely-valued revenue, so it is a genuine integral.
Demand functions. A demand function is a map $\mathbb R\to\mathbb R$ , nonnegative, with $\lambda(p_\infty)=0$ . Regularity and Assumption 1 are imposed on $[\underline p,\overline p]$ , and the inverse $\gamma$ is Function.invFunOn.
Benchmark. $J^D$ is a supremum over measurable price paths with integrable demand rate. The supremum is genuine: the set of path revenues is nonempty and bounded.
Algorithm. The grid excludes $\overline p$ , as in the paper. Ties in the grid argmax and argmin go to the smallest index. The estimates compare $\hat\lambda(p_i)$ with $x/T$ .
Tuning. $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$ are encoded with explicit constants $0<c\le c'$ , with $\tau_n\in(0,T]$ and $\kappa_n\ge1$ . Constants may depend on $c,c'$ , the class parameters, the prices, $x$ and $T$ , but never on $\lambda$ or $n$ .
Range of $n$ . Bounds whose right side vanishes at $n=1$ because $\log1=0$ are stated for $n\ge2$ : the goal and (A-15).
Typo correction. Lemma 5's event uses $nx-C_9nu_n$ , as in its proof, not the printed $nx-C_9u_n$ .
Ruled out. A specific demand curve, a fixed $n$ , deterministic demand, a finite price set, a known $\lambda$ , constants depending on $\lambda$ , or dropping the inventory cap would each make the statement a different and easier theorem. None is used.
Not included. The lower bound of Proposition 2 and the second assertion of Lemma 1 ( $J^\pi\le J^D$ for all admissible policies) are not included.

Contributions are welcome at any level: proofs of the milestones (Fact 1, Lemma 1 and Lemma 2 are self-contained), measurability and integrability lemmas for the revenue functional, and a reusable Poisson concentration library built on Mathlib's poissonMeasure.

Selected references

O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000

15 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 1: A k-Fold Realizer of Size t Yields a Vertex Cover of Expected Weight at Most (2 − 2/(t/k)) Times OptimalResearch Paper

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$ -approximations for orders of fractional dimension at most $f$ . This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$ .

Two jobs $x,y$ are incomparable, $x\parallel y$ , when neither $(x,y)$ nor $(y,x)$ lies in $P$ . The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$ ; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$ . A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$ -realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$ -realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$ , or $j=k$ and $(i,\ell)\in P$ , or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$ , and $w(C)=\sum_{u\in C}w_u$ . $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$ . The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$ . For a solution $x$ write $V_a=\{u: x_u=a\}$ , and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$ .

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$ , a $k:t$ -realizer $L_1,\dots,L_t$ of $P$ , and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$ . Then every $C_i$ is a vertex cover of $G^S_P$ , and

\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.

Milestones

Proposition 3.2 (p. 657): $G^S_P=G_P$ .
Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$ .
Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$ .
Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$ .
Hochbaum's observation (§5, p. 659): for half-integral feasible $x$ , $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$ .
Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$ -approximate vertex cover of $G^S_P$ into an $\alpha$ -approximate schedule, Theorem 5.1 gives a $(2-2/f)$ -approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$ . The paper applies it to interval orders ( $3/2$ ), convex bipartite orders and semiorders ( $4/3$ ), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$ -fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$ .

Formalization scope

Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
$\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$ -realizer is a family Fin t → LinearExtension P with $t>0$ . Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's " $y>x$ " in Eq. (4) and " $\mathrm{Prob}[j>i]$ " in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
$G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
[CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$ , taken over a finite nonempty family.
Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$ , which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$ . The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$ .
Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$ , and equals $2$ when $k=0$ .
The paper assumes $\operatorname{fdim}(P)\ge2$ , i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$ .
Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

10 thms3 active usersReviewed

Completed

Algebraic Geometry Complexity Theory Linear Optimization+2·Captain: mikedeng1

Log-Barrier Interior Point Methods Are Not Strongly Polynomial 1: Every Polygonal Curve in the Wide Neighborhood of the Central Path of LW_r(t) from μ̄ ≤ 1 to μ̄ ≥ t² Has at Least 2^(r−1) SegmentsResearch Paper

Motivation

Interior point methods solve linear programs in a number of arithmetic operations polynomial in the bit length of the input (Karmarkar 1984). Whether linear programming admits a strongly polynomial algorithm, one whose number of arithmetic operations is bounded by a polynomial in the number of variables and constraints alone, is open; it is the ninth of Smale's problems for the next century (Smale 1998/2000, see the references). A natural question is whether some interior point method is strongly polynomial. Primal-dual path-following methods follow the central path of a log-barrier problem and are the methods used in practice.

Allamigeon, Benchimol, Gaubert and Joswig (arXiv:1708.01544, SIAM J. Appl. Algebra Geom. 2018) gave such a family. For linear programs $\mathbf{LW}_r(t)$ with $2r$ variables and $3r+1$ constraints, every path-following method that stays in the wide neighborhood of the central path needs at least $2^{r-1}$ iterations once $t$ is large enough. The same family disproves the "continuous Hirsch conjecture" of Deza, Terlaky and Zinchenko (DTZ09, see the references) on the total curvature of the central path. That curvature result is the subject of a separate mission. This mission formalizes the iteration bound.

Setting

For a real $m\times n$ matrix $A$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ and $N:=n+m$ , the paper considers the linear program in slack form and its dual,

\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. }\ Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .

A primal-dual point is $z=(x,w,s,y)\in\mathbb R^{2N}$ . The set $\mathcal F^\circ$ of strictly feasible points consists of the $z$ with all $2N$ coordinates positive that satisfy both equality systems. The duality measure is

\bar\mu(z)=\frac1N\big(\langle x,s\rangle+\langle w,y\rangle\big),

and for $0<\theta<1$ the wide neighborhood of the central path is

\mathcal N^{-\infty}_\theta=\Big\{z\in\mathcal F^\circ:\ x_js_j\ge(1-\theta)\bar\mu(z)\ \forall j,\ \ w_iy_i\ge(1-\theta)\bar\mu(z)\ \forall i\Big\}.

The central path itself is the set of points where all products $x_js_j$ , $w_iy_i$ are equal. The neighborhood bounds the products only from below. It contains the $\ell_2$ and $\ell_\infty$ neighborhoods used by short-step, long-step and predictor-corrector methods.

The instance is $\mathbf{LW}_r(t)$ , for $r\ge1$ and $t>0$ :

\min\ x_1\ \text{ s.t. }\ x_1\le t^2,\ x_2\le t,\ x_{2j+1}\le t\,x_{2j-1},\ x_{2j+1}\le t\,x_{2j},\ x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ (1\le j<r),\ x_{2r-1},x_{2r}\ge0 .

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$ , $m=3r-1$ , $N=5r-1$ . Its wide neighborhood is written $\mathcal N^{-\infty}_{\theta,t}$ . A polygonal curve is a union $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ of $p$ segments, and it is contained in the neighborhood when every point of every segment is.

The milestones use the tropical semifield $\mathbb T=\mathbb R\cup\{-\infty\}$ with $a\oplus b=\max(a,b)$ and $a\odot b=a+b$ . The tropical segment $\mathsf{tsegm}(u,v)$ is the set of points $\lambda\odot u\oplus\mu\odot v$ with $\lambda\oplus\mu=0$ . The Funk metric is $\delta_F(x,y)=\max(0,\max_k(y_k-x_k))$ , with $d_\infty(x,y)=\max(\delta_F(x,y),\delta_F(y,x))$ and the directed Hausdorff distance $d_\infty(X,Y)=\sup_{x\in X}\inf_{y\in Y}d_\infty(x,y)$ . Finally, $\log_t$ is applied coordinatewise, with $\log_t0=-\infty$ .

Formalization targets

Goal: Theorem 30 (p. 27)

Let $r\ge1$ and $0<\theta<1$ , and suppose that

t>\Big(\max\Big((10r-2)!,\ \frac{((10r-1)!)^{24}}{(1-\theta)^3}\Big)\Big)^{2^{r-1}} .\tag{36}

If a polygonal curve $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ is contained in $\mathcal N^{-\infty}_{\theta,t}$ with $\bar\mu(z^0)\le1$ and $\bar\mu(z^p)\ge t^2$ , then

p\ge2^{r-1}.

The threshold (36) is the paper's own explicit constant. Corollary 31 (Theorem B of the introduction) restates the result for algorithms. Any method whose iterates and the segments joining them stay in the wide neighborhood performs at least $2^{r-1}$ iterations to reduce the duality measure from $t^2$ to $1$ .

Milestones

Proposition 1 (p. 5). On the primal-dual feasible set, $\bar\mu((1-\alpha)z+\alpha z')=(1-\alpha)\bar\mu(z)+\alpha\bar\mu(z')$ for all $\alpha\in\mathbb R$ .
Lemma 5 (p. 10). For $u\le v$ in $\mathbb T^d$ , $\mathsf{tsegm}(u,v)$ is a polygonal curve whose segments, oriented from $u$ to $v$ , have directions $e^{K_1},\dots,e^{K_\ell}$ with $K_1\subsetneq\dots\subsetneq K_\ell$ and $\ell\le d$ .
Lemma 8 (p. 11). For a segment $S=[u,v]$ in $\mathbb R^d_+$ and $t>1$ ,

d_\infty\big(\mathsf{tsegm}(\log_tu,\log_tv),\ \log_tS\big)\le\log_t2 .

Lemma 11 (p. 13). For a $d\times d$ matrix $\mathbf M$ with monomial entries $\pm t^{\alpha_{ij}}$ and $t>1$ , $\log_t|\det\mathbf M(t)|$ and $\operatorname{val}(\det\mathbf M)$ differ by at most $\log_td!$ ; the lower bound holds once $t\ge(d!)^{1/\eta(\mathbf M)}$ .
Proposition 20 (p. 19). The explicit recursion for $x^\lambda$ gives the greatest point of the tropical polyhedron $\{x\in\mathcal P':x_1\le\lambda\}$ , where $\mathcal P'\subseteq\mathbb T^{2r}$ is cut out by the tropicalized constraints (26) of $\mathbf{LW}_r$ .

Significance

The theorem shows that the iteration count of a large class of primal-dual log-barrier interior point methods cannot be bounded by any function of $r$ that grows more slowly than $2^{r-1}$ , uniformly in the data. The class includes the methods of Kojima–Mizuno–Yoshise, Monteiro–Adler and Mizuno–Todd–Ye. No such method is strongly polynomial. The constraint matrix of $\mathbf{LW}_r(t)$ is fixed by $r$ and $t$ alone, so the bound concerns the combinatorial dimension, not the bit length. The only property of the method used is that its trajectory stays in $\mathcal N^{-\infty}_{\theta,t}$ . The lower bound therefore applies to every method with that property, whatever rule chooses its steps.

The result is proved in the paper; no machine-checked proof of it or of its tropical ingredients is known. A formalization would check the explicit threshold (36), which the paper derives in a few lines from bounds on Puiseux polyhedra. It would also produce reusable statements about tropical segments, the Funk and Hilbert metrics on $\mathbb T^d$ , and determinants of monomial matrices.

Difficulty

Following the central path is not hard in principle: the obvious argument tracks the duality measure, which decreases by a constant factor per iteration in a neighborhood of the path. That argument gives only upper bounds. The lower bound requires showing that the neighborhood itself, for large $t$ , is too thin to be crossed in a few straight steps, uniformly over every possible trajectory. The paper does this by passing to the limit $t\to\infty$ on logarithmic scale. The image of $\mathcal N^{-\infty}_{\theta,t}$ under $\log_t$ collapses onto a piecewise-linear tropical central path, and a segment of $\mathbb R^{2N}$ becomes, up to $\log_t2$ , a tropical segment. The tropical central path of $\mathbf{LW}_r$ then has to be shown to need $2^{r-1}$ tropical segments. The limit argument has to be made quantitative at a finite, explicit $t$ . That is where the Puiseux-series machinery (Theorems 12, 15 and 19 of the paper) and the explicit constant enter.

Formalization scope

Everything is stated over $\mathbb R$ and $\mathbb T$ ; the goal typechecks without the field of Puiseux series. A primal-dual point is an element of $\mathbb R^n\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$ . The dual equation is $s-A^\top y=c$ with Mathlib's transpose, $\bar\mu$ divides by $N=n+m$ (equal to $5r-1$ for $\mathbf{LW}^=_r$ ), and the wide neighborhood is one-sided. The instance matrix is generated from the paper's 1-based row and column numbers; Lean indices are 0-based. A polygonal curve is a map $z:\{0,\dots,p\}\to\mathbb R^{2N}$ with segment ℝ (z i) (z (i+1)) ⊆ N. The power $2^{r-1}$ in (36) is a natural-number power and the factorials are natural-number factorials. $\mathbb T$ is WithBot ℝ, and distances that can be infinite take values in EReal, with the convention $-\infty+(+\infty)=-\infty$ encoded explicitly.

Two statements are repaired or restated. Lemma 11 is printed for all $t>0$ , but its first inequality fails for $0<t<1$ (for $\mathbf M=\begin{pmatrix}t&1\\1&1\end{pmatrix}$ at $t=1/2$ ), so it is stated for $t>1$ . Lemma 8 makes explicit its implicit hypotheses $t>1$ and $u,v\ge0$ . Proposition 20 is stated in the form its proof establishes, as the greatest point of a tropical polyhedron. Its identification with the valuation of the Puiseux central path is not part of the item. Monomial matrices are given by sign and exponent matrices, and the valuation of the determinant is computed from the permutation expansion.

A trivializing formalization is ruled out: $\mathcal N^{-\infty}_{\theta,t}$ is not empty, since the build includes a sorry-free proof that it contains an explicit point for $r=1$ , $t=2$ , $\theta=1/2$ . A curve with $p=0$ cannot satisfy both duality-measure conditions, since $t^2>1$ .

The paper's Puiseux-series results are not posed: Theorems 12, 15, 19 and 29, Propositions 14, 16, 21 and 28, Corollary 17, and the count $\gamma([0,2])\ge2^{r-1}$ of §6.2. They need a faithful model of the field of absolutely convergent generalized Puiseux series and of the tropical central path. Contributions of that infrastructure, and of these statements as further milestones, are welcome. So are proofs of the five milestones, which need no Puiseux series. Proposition 1, Lemma 5 and Proposition 20 are elementary, and Lemma 8 and Lemma 11 are estimates with explicit constants.

Selected references

X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; arXiv:1708.01544v2. https://arxiv.org/abs/1708.01544
A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Adv. Mech. Math. 17, Springer, 2009, pp. 223–256. https://doi.org/10.1007/978-0-387-75714-8
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2), 1998, 7–15; reprinted in Mathematics: Frontiers and Perspectives, AMS, 2000. https://doi.org/10.1007/BF03025291
M. Develin, B. Sturmfels, Tropical convexity, Doc. Math. 9, 2004. https://arxiv.org/abs/math/0308254
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453
X. Allamigeon, S. Gaubert, M. Skomra, Tropical spectrahedra, Discrete Comput. Geom. 63, 2020; arXiv:1610.06746. https://arxiv.org/abs/1610.06746

12 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Probability+1·Captain: mikedeng1

Data-Driven Robust Optimization V: The Order-Statistic Box U^M Built from Marginal Samples Dominates Value at Risk with Probability at Least 1 − αResearch Paper

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$ by the requirement that it hold for every $\mathbf u$ in an uncertainty set $\mathcal U\subseteq\mathbb R^d$ . The resulting problems are tractable for many sets, but the choice of $\mathcal U$ decides whether the solution means anything probabilistically. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167:235–292, 2018) propose to build $\mathcal U$ from data so that, with high probability over the sample, every robust-feasible decision is also feasible with probability at least $1-\epsilon$ under the unknown distribution $\mathbb P^*$ .

This mission covers §6 of that paper, the case where the data are samples of the marginals of $\mathbb P^*$ , observed separately, with no assumption that the marginals are independent. This is the situation of asynchronous measurements or records with many missing entries: the joint law cannot be learned, yet a valid uncertainty set can still be built. The set is a box whose sides are order statistics, and its guarantee rests on an elementary binomial test (David and Nagaraja, Order Statistics, §7.1) and a Value-at-Risk bound of Embrechts, Höing and Juri (Finance Stoch. 7, 2003).

Setting

Let $\mathbb P^*$ be a probability measure on $\mathbb R^d$ whose support lies in a known box $[\hat{\mathbf u}^{(0)},\hat{\mathbf u}^{(N+1)}]=\{\mathbf u:\hat u^{(0)}_i\le u_i\le\hat u^{(N+1)}_i\}$ . Fix a violation level $0<\epsilon<1$ and a significance level $0<\alpha<1$ .

The Value at Risk of $\tilde{\mathbf u}^T\mathbf v$ under a probability measure $\mathbb P$ is

\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge1-\epsilon\},

and the support function of a set $\mathcal U$ is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u$ . A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$ if for every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ and every $\mathbf x^*$ , $f(\mathbf u,\mathbf x^*)\le0$ for all $\mathbf u\in\mathcal U$ implies $\mathbb P^*(f(\tilde{\mathbf u},\mathbf x^*)\le0)\ge1-\epsilon$ .

From a sample $\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N$ let $\hat u^{(j)}_i$ , $1\le j\le N$ , be the $j$ -th order statistic (the $j$ -th smallest value) of coordinate $i$ , and let $\hat u^{(0)}_i,\hat u^{(N+1)}_i$ be the box ends. The index $s$ is

s=\min\Big\{k\in\mathbb N:\sum_{j=k}^N\binom Nj(\epsilon/d)^{N-j}(1-\epsilon/d)^j\le\frac{\alpha}{2d}\Big\},\qquad s=N+1\text{ if the set is empty}, \tag{26}

and the uncertainty set is the box

\mathcal U^M_\epsilon=\{\mathbf u\in\mathbb R^d:\hat u^{(N-s+1)}_i\le u_i\le\hat u^{(s)}_i,\ i=1,\dots,d\}. \tag{28}

The confidence region $\mathcal P^M$ is the set of probability measures on the box with $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(\mathbf e_i)\le\hat u^{(s)}_i$ and $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ for every $i$ .

Formalization targets

Goal: Theorem 7

If $N-s+1<s$ , then with probability at least $1-\alpha$ over the sample ( $N$ samples of each marginal of $\mathbb P^*$ , each marginal's samples i.i.d., arbitrary dependence across marginals),

\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)\qquad\text{for all }\mathbf v\in\mathbb R^d,

and, for every sample, $\mathcal U^M_\epsilon$ is nonempty, convex and compact with

\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)=\sum_{i=1}^d\max\big(v_i\hat u^{(N-s+1)}_i,\,v_i\hat u^{(s)}_i\big). \tag{29}

Milestones

Positive homogeneity: $\mathrm{VaR}^{\mathbb P}_\delta(c\mathbf w)=c\,\mathrm{VaR}^{\mathbb P}_\delta(\mathbf w)$ for $c>0$ (p. 10).
Each one-sided order-statistic test is valid at level $\alpha/(2d)$ : $\mathbb P^*_{\mathcal S}(\hat u^{(s)}_i<\mathrm{VaR}^{\mathbb P^*}_{\epsilon/d}(\mathbf e_i))\le\alpha/(2d)$ , and the mirror bound for $-\mathbf e_i$ with $\hat u^{(N-s+1)}_i$ (pp. 20–21).
Union bound: $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P^M)\ge1-\alpha$ (p. 21).
The weak Embrechts bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_i\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(v_i\mathbf e_i)$ for every probability measure $\mathbb P$ (p. 21).
If $N-s+1<s$ then $\hat u^{(N-s+1)}_i\le\hat u^{(s)}_i$ (p. 21).
(EC.8): for $\mathbb P\in\mathcal P^M$ , $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_{v_i>0}v_i\hat u^{(s)}_i+\sum_{v_i\le0}v_i\hat u^{(N-s+1)}_i$ (p. ec5).
(29) as a standalone statement (p. 21).

Significance

Theorem 7 gives an uncertainty set with a finite-sample guarantee from data that carry no information on the dependence between coordinates. The set is a box, so the robust counterpart of a linear constraint is again linear, and Remark 12 of the paper notes that separation over $\{(\mathbf v,t):\delta^*(\mathbf v\mid\mathcal U^M)\le t\}$ is in closed form. Unlike the other confidence regions of the paper (χ², G-test, Kolmogorov–Smirnov, bootstrap), whose coverage is asymptotic, tabulated or approximate, the test here is exact and distribution-free, so the probability statement itself is in scope.

The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a complete formal statement of Theorem 7 including the sampling probability, the binomial order-statistic test for a quantile, and the marginal Value-at-Risk bound, all of which are standard tools in nonparametric statistics and risk management that are absent from Mathlib.

Difficulty

The deterministic half, (EC.8) and (29), is short once the weak Embrechts bound is available. The work is in the probabilistic half, which the paper delegates to a textbook citation. Validity of the order-statistic test ties together facts that no library currently connects: the combinatorics of sorted tuples, the binomial law of the number of i.i.d. sample points below a threshold, the behaviour of a quantile at its left limit (the distribution function at the quantile can exceed $1-\epsilon/d$ , so the obvious bound uses the wrong probability), and the comparison of binomial tails across success probabilities. The lower-tail test must be handled with the index $N-s+1$ and the quantile of $-\tilde u_i$ , where a sign or off-by-one slip produces a false statement that still looks plausible. The boundary regime $s=N+1$ , where $\mathcal U^M_\epsilon$ is the a priori box, is valid only because $\mathbb P^*$ lives in that box and needs separate treatment.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with 0-based coordinates; vectors pair by ⬝ᵥ. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ applied to $\mathbf u\mapsto\mathbf u^T\mathbf v$ , and the support function is the published RobustMDP.Shared.supportFunction; both are real infima/suprema, genuine under $0<\epsilon<1$ , a probability measure, and a nonempty bounded set (the goal proves the latter). The order statistics use Mathlib's Tuple.sort; the index $N-s+1$ is N + 1 - s in natural numbers, which is the paper's value since $1\le s\le N+1$ .

The data are an array S : Fin N → Fin d → ℝ, S k i the $k$ -th sample of marginal $i$ , under any probability law Q such that, for each $i$ , the samples S 0 i, …, S (N-1) i are i.i.d. from the $i$ -th marginal of $\mathbb P^*$ (IsMarginalSampleLaw). The dependence between samples of different marginals is left arbitrary, as the paper's asynchronous setting requires; i.i.d. draws of whole vectors are one admissible law. Probabilities of possibly non-measurable events are outer measures. The level $\epsilon$ is fixed: by Remark 11 the family $\{\mathcal U^M_\epsilon\}$ need not work for all $\epsilon$ simultaneously.

The guarantee is stated in the criterion form of Theorem 1(a) of the paper: $\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)$ for all $\mathbf v$ , together with nonemptiness, convexity and compactness of $\mathcal U^M_\epsilon$ . Theorem 1 (mission I of this series) shows that for such sets this criterion is equivalent to implying a probabilistic guarantee. The coverage of the test is proved, not assumed: there is no hypothesis that $\mathbb P^*\in\mathcal P^M$ . A formalization in which the support function is evaluated on an empty or unbounded set, where the library value is 0, would make the criterion trivial; the nonemptiness and compactness conjunct of the goal rules it out.

Standing assumptions: $d\ge1$ , $0<\epsilon<1$ , $0<\alpha<1$ , $\hat{\mathbf u}^{(0)}\le\hat{\mathbf u}^{(N+1)}$ , $\mathbb P^*$ a probability measure with $\mathbb P^*$ -null complement of the box, and Theorem 7's hypothesis $N-s+1<s$ . The page prints the second condition of $\mathcal P^M$ as " $\mathrm{VaR}^{\mathbb P_i}_{\epsilon/d}\ge\hat u^{(N-s+1)}_i$ "; the formal region uses the lower-tail condition $\mathrm{VaR}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ that the hypothesis, its rejection rule and the proof use. (EC.8) is stated with " $\le$ " for each $\mathbb P\in\mathcal P^M$ ; the page's middle equality is not claimed.

Reusable infrastructure welcome beyond this mission: order statistics of tuples and the binomial law of threshold counts for i.i.d. samples; monotonicity of binomial tails in the success probability; the left-limit property of quantiles; the Embrechts-type subadditivity bound for Value at Risk.

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
H. A. David, H. N. Nagaraja, Order Statistics, Wiley (cited by the paper as 1970; third edition 2003), §7.1, distribution-free confidence intervals for quantiles. https://doi.org/10.1002/0471722162
P. Embrechts, A. Höing, A. Juri, Using copulae to bound the Value-at-Risk for functions of dependent risks, Finance and Stochastics 7:145–167, 2003. https://doi.org/10.1007/s007800200085

11 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Probability+1·Captain: mikedeng1

Data-Driven Robust Optimization III: For Independent Marginals, the Kolmogorov–Smirnov Set U^I Has Support Function (19) and Bounds the Worst-Case Value at RiskResearch Paper

Motivation

A robust linear constraint $f(\mathbf u,\mathbf x)\le 0$ for all $\mathbf u\in\mathcal U$ replaces an uncertain parameter $\tilde{\mathbf u}$ by a deterministic uncertainty set $\mathcal U\subseteq\mathbb R^d$ . Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets directly from data. Their requirement is a probabilistic guarantee: every robust-feasible decision should satisfy the constraint with probability at least $1-\epsilon$ under the true distribution $\mathbb P^*$ , and this should hold with probability at least $1-\alpha$ over the sample. The construction runs a statistical hypothesis test, takes its confidence region of distributions, and turns the worst-case Value at Risk over that region into a set.

This mission covers the case where $\mathbb P^*$ may be continuous but its $d$ coordinates are known to be independent and supported in a known box (§5.1 of the paper). The test is the classical Kolmogorov–Smirnov (KS) goodness-of-fit test, applied separately to each marginal. The result is a convex set $\mathcal U^I_\epsilon$ whose support function has a one-dimensional closed form, (19). The set is representable with exponential cones, and a line search over a single multiplier separates over it (Remarks 6–7).

Setting

Let $d\ge 0$ and $N\ge 1$ (the sample size). For each coordinate $i$ we are given points $\hat u^{(0)}_i<\hat u^{(1)}_i<\cdots<\hat u^{(N)}_i<\hat u^{(N+1)}_i$ . The interval $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ is the known box containing the support, and $\hat u^{(1)}_i,\dots,\hat u^{(N)}_i$ are the order statistics of the $i$ -th coordinates of the data. Let $\Gamma=\Gamma^{KS}\in(0,1)$ be the KS threshold and $0<\epsilon<1$ .

The Value at Risk of $\mathbb P$ in direction $\mathbf v$ is $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^{\mathsf T}\mathbf v\le t)\ge 1-\epsilon\}$ .
The support function of a set is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^{\mathsf T}\mathbf u$ .
The KS region $\mathcal P^{KS}_i$ is the set of Borel probability measures $\mathbb P_i$ on $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ with $\mathbb P_i(\tilde u_i\le\hat u^{(j)}_i)\ge j/N-\Gamma$ and $\mathbb P_i(\tilde u_i<\hat u^{(j)}_i)\le (j-1)/N+\Gamma$ for $j=1,\dots,N$ .
The independent region $\mathcal P^I$ is the set of product measures $\prod_i\mathbb P_i$ with $\mathbb P_i\in\mathcal P^{KS}_i$ .
The vectors $q^L(\Gamma),q^R(\Gamma)\in\Delta_{N+2}$ of (17) are the two boundary distributions of the KS band. With $k=\lfloor N(1-\Gamma)\rfloor$ , $q^L$ puts mass $\Gamma$ at $j=0$ , mass $1/N$ at $j=1,\dots,k$ , and mass $1-\Gamma-k/N$ at $j=k+1$ . Its mirror image is $q^R_j=q^L_{N+1-j}$ .
The relative entropy is $D(\mathbf q,\mathbf p)=\sum_jq_j\log(q_j/p_j)$ .
The uncertainty set (18) is

\mathcal U^I_\epsilon=\Big\{\mathbf u:\exists\,\theta_i\in[0,1],\ \mathbf q^i\in\Delta_{N+2},\ \sum_{j=0}^{N+1}\hat u^{(j)}_iq^i_j=u_i,\ \sum_{i=1}^dD\big(\mathbf q^i,\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R\big)\le\log(1/\epsilon)\Big\}.

Formalization targets

Goal: Theorem 5 (deterministic content)

For every $\mathbf v\in\mathbb R^d$ :

\mathcal U^I_\epsilon\ \text{is nonempty, convex and compact},\qquad \mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)\ \ \forall\,\mathbb P\in\mathcal P^I,

\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)=\inf_{\lambda>0}\Big\{\lambda\log(1/\epsilon)+\lambda\sum_{i=1}^d\log\Big[\max\Big(\sum_{j}q^L_je^{v_i\hat u^{(j)}_i/\lambda},\sum_jq^R_je^{v_i\hat u^{(j)}_i/\lambda}\Big)\Big]\Big\}.\tag{19}

Milestones, in attack order

The Nemirovski–Shapiro bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\lambda\log(1/\epsilon)+\lambda\sum_i\log\mathbb E^{\mathbb P_i}[e^{v_i\tilde u_i/\lambda}]$ for independent, compactly supported marginals.
The boundary laws $q^L$ , $q^R$ belong to $\mathcal P^{KS}_i$ .
Theorem EC.2: for monotone $g$ , $\sup_{\mathcal P^{KS}_i}\mathbb E[g(\tilde u_i)]=\max(\sum_jq^L_jg(\hat u^{(j)}_i),\sum_jq^R_jg(\hat u^{(j)}_i))$ .
(16) combined with EC.2: the Value at Risk over $\mathcal P^I$ is at most the expression in (19), for every $\lambda>0$ .
The Lagrangian dual of $\max\{\mathbf v^{\mathsf T}\mathbf u:\mathbf u\in\mathcal U^I_\epsilon\}$ .
(EC.6): $\max_{\mathbf q\in\Delta}\{\mathbf c^{\mathsf T}\mathbf q-D(\mathbf q,\mathbf p)\}=\log\sum_jp_je^{c_j}$ .
(EC.7): the linear optimization over $\theta_i\in[0,1]$ is solved at an endpoint.

Significance

Theorem 5 gives a data-driven uncertainty set for continuous distributions with independent components. Its guarantee is finite-sample, not asymptotic, and its support function costs one line search over $\lambda$ to evaluate. Theorem 1 of the paper shows that $\mathrm{VaR}\le\delta^*$ for all $\mathbf v$ is equivalent to the probabilistic guarantee for nonempty convex compact sets. So the goal certifies that every robust-feasible solution of a constraint concave in $\mathbf u$ satisfies the chance constraint for every distribution the KS tests cannot reject. Theorem EC.2 is a reusable fact about KS bands: monotone expectations are extremized at the band's two boundary distributions.

The result is proved in the paper, but none of it has been formalized. A formal development would supply:

worst-case expectations over a KS confidence band;
the finite Gibbs variational identity with possibly vanishing reference masses;
a Chernoff-type Value-at-Risk bound for product measures;
a strong-duality statement for an entropy-constrained convex program.

Difficulty

The obvious route to the VaR bound is a union bound over coordinates. It loses a factor of $d$ in $\epsilon$ , which is why the paper uses exponential moments and independence instead. The KS region is infinite dimensional, so the inner supremum of (16) is not a finite linear program. Reducing it to the boundary distributions needs the monotonicity of $u\mapsto e^{v_iu/\lambda}$ , and a measure-level comparison of distribution functions against the band. The support-function identity needs strong duality for a jointly convex divergence constraint. The duality holds because $\theta_i\mapsto\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R$ is affine and $D$ is jointly convex. The reference vector can have zero entries (when $N(1-\Gamma)$ is an integer, or in the middle of the band), so the Gibbs step must handle vanishing masses.

Formalization scope

Data and conventions. Coordinates are Fin d. The points are uhat : Fin d → Fin (N + 2) → ℝ with the page's indices $j=0,\dots,N+1$ , and the KS constraints run over j : Fin N, which is the page's $j-1$ . The order statistics are data. They are ordered, $\hat u^{(0)}_i\le\hat u^{(1)}_i\le\dots\le\hat u^{(N+1)}_i$ (Monotone (uhat i)), as order statistics of a sample in the box are; ties are allowed.
Standing assumptions. $N\ge1$ , $0<\Gamma<1$ and $0<\epsilon<1$ .
Regions. Measures in $\mathcal P^{KS}_i$ are probability measures on $\mathbb R$ carried by the box, and $\mathcal P^I$ consists of the Measure.pi products of such measures, so independence is built in.
Relative entropy. $D$ carries an explicit finiteness predicate ( $q_j>0\Rightarrow p_j>0$ ), so Lean's log 0 = 0 cannot make an infinite divergence finite.
Published definitions. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ , and $\delta^*$ is the published RobustMDP.Shared.supportFunction, a real sSup. The goal proves $\mathcal U^I_\epsilon$ nonempty and compact, so $\delta^*$ is never the junk value $0$ of an empty or unbounded set.
Infima and the multiplier. Infima over $\lambda$ are over $\lambda>0$ and stated with IsGLB. The page's $\lambda\ge0$ gives the same value.
Criterion form of the guarantee. The guarantee is stated as $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)$ for all $\mathbb P\in\mathcal P^I$ . By Theorem 1 (mission I of this series), this criterion is equivalent to the probabilistic guarantee for nonempty convex compact sets.
Coverage of the test. The statement "with probability at least $1-\alpha$ over the sample" is the coverage of $\mathcal P^I$ . It rests on the distribution-free law of the KS statistic (tables) and on combining $d$ tests at level $1-\sqrt[d]{1-\alpha}$ . This part is cited, not formalized.
Ruled out. The VaR inequality is never checked against a $\delta^*$ that sSup collapses to $0$ , and the divergence budget is never relaxed by unguarded logarithms.

Contributions are welcome on any milestone. Milestones 1, 3 and 6 are independent of each other and of the rest; the goal follows from milestones 1–7 together with the convex-analytic facts about $\mathcal U^I_\epsilon$ .

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17(4):969–996, 2006. https://doi.org/10.1137/050622328
M. A. Stephens, EDF statistics for goodness of fit and some comparisons, J. Amer. Statist. Assoc. 69(347):730–737, 1974. https://doi.org/10.1080/01621459.1974.10480196
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

11 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

On the Power and Limitations of Affine Policies in Two-Stage Adaptive Optimization V: The Optimal First Stage over a Dominating Simplex Is a 4√m-ApproximationResearch Paper

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage decision $y(b)$ is chosen afterwards, with the worst case over an uncertainty set $\mathcal U$ to be minimized. Problems of this form arise in capacity planning, network design and inventory control, where the first stage is an investment and the second stage a recourse. Computing the fully adaptable optimum is hard in general, so tractable restrictions are used in practice, most prominently affine policies $y(b)=Pb+q$ (Ben-Tal, Goryashko, Guslitzer, Nemirovski, Math. Program. 2004).

Bertsimas and Goyal (Math. Program. Ser. A, DOI 10.1007/s10107-011-0444-4) characterize how well affine policies perform. Their Section 5 shows a factor $O(\sqrt m)$ when the first-stage matrix satisfies $A\ge 0$ . Section 6, the subject of this mission, drops the sign condition on $A$ : it constructs, from $\mathcal U$ , a polytope $\mathcal U^0$ with at most $m+1$ vertices that dominates $\mathcal U$ , and shows that an optimal first stage for $\mathcal U^0$ is a $4\sqrt m$ -approximate first stage for the original problem.

Timeline. Ben-Tal et al. (2004) introduced affinely adjustable robust counterparts. Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved optimality of affine policies for one-dimensional multistage problems. Bertsimas and Goyal (Math. Oper. Res. 2010) analysed static robust solutions for two-stage problems. The present paper (received 2009, published 2011) gives the $\Theta(m^{1/2})$ picture for affine policies and the general-case first-stage approximation formalized here.

Setting

Fix matrices $A\in\mathbb R^{m\times n_1}$ , $B\in\mathbb R^{m\times n_2}$ and cost vectors $c\in\mathbb R^{n_1}_+$ , $d\in\mathbb R^{n_2}_+$ . The uncertainty set $\mathcal U\subseteq\mathbb R^m_+$ is convex, compact and full-dimensional. A feasible solution of $\Pi_{Adapt}(\mathcal U)$ is a pair $(x,y)$ with $x\ge0$ and, for every $b\in\mathcal U$ , $y(b)\ge0$ and $Ax+By(b)\ge b$ , componentwise. Its worst-case cost is $\sup_{b\in\mathcal U}\, c^Tx+d^Ty(b)$ , and the fully adaptable optimum is

z_{Adapt}(\mathcal U)=\inf_{(x,y)\ \text{feasible}}\ \sup_{b\in\mathcal U}\ c^Tx+d^Ty(b).

An optimal solution attains this value.

For $j=1,\dots,m$ let $\mu_j=\max\{b_j: b\in\mathcal U\}$ and let $\beta^j\in\mathcal U$ be a maximizer, $\beta^j_j=\mu_j$ (display (38)). Algorithm $\mathcal A$ (Fig. 1 of the paper) starts with the index set $J_1=\{1,\dots,m\}$ ; while some $b\in\mathcal U$ has $\sum_{j\in J_1}b_j/\mu_j>\sqrt m$ , it picks a maximizer $u^k$ of that scaled sum over $\mathcal U$ , adds $u^k$ to a running total on the coordinates of $J_1$ , and removes from $J_1$ every coordinate whose total has reached $\mu_j$ . It stops after $K$ iterations and returns $\beta=u^1+\dots+u^K$ . The dominating set is

\mathcal U^0=\operatorname{conv}\{2\sqrt m\cdot\beta^1,\dots,2\sqrt m\cdot\beta^m,\ 2\beta\}.\tag{66}

Formalization targets

Goal: Theorem 6

For every run of Algorithm $\mathcal A$ , every choice of the maximizers $\beta^j$ , and every optimal solution $(\tilde x,\tilde y)$ of $\Pi_{Adapt}(\mathcal U^0)$ ,

\forall b\in\mathcal U\ \ \exists y\ge 0:\quad A\tilde x+By\ge b,\qquad c^T\tilde x+d^Ty\le 4\sqrt m\cdot z_{Adapt}(\mathcal U).

The page states the factor as $O(\sqrt m)$ ; $4\sqrt m$ is the constant its proof establishes.

Milestones

Lemma 12. $\mathcal U^0$ dominates $\mathcal U$ : every $b\in\mathcal U$ has some $b'\in\mathcal U^0$ with $b\le b'$ .
Lemma 13 (inequality). $\Pi_{Adapt}(\mathcal U^0)$ is feasible with finite worst-case cost, and

z_{Adapt}(\mathcal U^0)\le 4\sqrt m\cdot z_{Adapt}(\mathcal U).

The domination claim in the proof of Theorem 6. If $V$ dominates $W$ and $(\tilde x,\tilde y)$ is optimal for $\Pi_{Adapt}(V)$ with finite worst-case cost, then every $b\in W$ can be served from $\tilde x$ at cost at most $z_{Adapt}(V)$ .

Significance

The result gives a first-stage decision with a guarantee of order $\sqrt m$ for two-stage problems with an arbitrary first-stage matrix, a setting where the affine-policy analysis of Section 5 does not apply. The decision is obtained from a problem whose uncertainty set has at most $m+1$ extreme points, so it reduces an adaptive problem over a general convex set to one over a polytope with few vertices. Together with the paper's lower bounds (Theorems 2 and 3, $\Omega(m^{1/2-\delta})$ for affine policies), it places the general-case approximability of the first stage at the same order as the affine-policy gap.

The result is proved in the paper. It has no machine-checked proof that we know of. The formalization produces, beyond the theorem itself, an encoding of model (1) with values that are honest infima, a relational encoding of Algorithm $\mathcal A$ usable for its termination and output properties, and a reusable domination lemma for two-stage problems. Mission IV of this series (the case $A\ge0$ ) formalizes Lemmas 9 and 10 on Algorithm $\mathcal A$ , which the proofs here use.

Difficulty

The obvious argument replaces $\mathcal U$ by a simple set that contains or dominates it, such as the box $\prod_j[0,\mu_j]$ , and solves over that set. This loses a factor $m$ , not $\sqrt m$ : for $\mathcal U=\operatorname{conv}\{0,e_1,\dots,e_m\}$ with $A=0$ , $B=I$ , $c=0$ , $d=e$ , the optimum over $\mathcal U$ is $1$ while the optimum over the box is $m$ . A dominating set with few vertices whose cost is only $O(\sqrt m)$ times the original optimum has to be built from $\mathcal U$ itself, and controlling the cost of its vertex $2\beta$ depends on the number $K$ of iterations of Algorithm $\mathcal A$ , which is bounded only through the potential argument of Lemma 10 in the paper.

A second difficulty is that $z_{Adapt}$ is an infimum, not an attained minimum, over second-stage rules that are arbitrary functions; the cost comparison must work from near-optimal solutions of $\Pi_{Adapt}(\mathcal U)$ .

Formalization scope

Vectors are functions on Fin m, matrices are Matrix (Fin m) (Fin n) ℝ, and inequalities between vectors are componentwise. The paper's coordinate $j$ is Fin index $j-1$ . $z_{Adapt}(\mathcal U)$ is the infimum of the set of bounds $t$ such that some feasible $(x,y)$ satisfies $c^Tx+d^Ty(b)\le t$ for all $b\in\mathcal U$ ; this avoids a real supremum of a possibly unbounded worst case. An optimal solution is a feasible one that achieves every achievable bound. $\mu$ and the maximizers $\beta^j$ enter the theorems as data with their defining properties. Algorithm $\mathcal A$ is a relation on a choice sequence $u^1,u^2,\dots$ : the theorems hold for every run and every choice of maximizers, never for "some simplex dominating $\mathcal U$ ".

Standing assumptions of (1) carried by the goal and Lemma 13: $c\ge0$ , $d\ge0$ , $\mathcal U\subseteq\mathbb R^m_+$ convex, compact and with nonempty interior, and (1) feasible. There is no sign condition on $A$ . Lemma 12 keeps only nonnegativity and full-dimensionality of $\mathcal U$ ; the domination claim is stated for arbitrary scenario sets $V$ and $W$ with $V$ dominating $W$ and assumes that the optimal solution over $V$ has a finite worst-case cost.

The printed Lemma 13 also asserts $z_{Aff}(\mathcal U^0)=z_{Adapt}(\mathcal U^0)$ on the grounds that $\mathcal U^0$ is a simplex. Its $m+1$ generators need not be affinely independent, so this equality is not part of the mission; Theorem 6 does not use it.

A bound on $z_{Adapt}(\mathcal U^0)$ alone is not the goal: the goal requires, for each scenario of the original set $\mathcal U$ , a feasible second stage completing the fixed first stage $\tilde x$ at the stated cost. Lemma 13 also asserts feasibility over $\mathcal U^0$ with a finite bound, so its inequality cannot hold through the value of an infimum over an empty set.

A complete development needs elementary facts about convex hulls of finitely many points (representation by convex weights), the properties of Algorithm $\mathcal A$ (its output bound and termination, Lemmas 9 and 10 of the paper), and $\varepsilon$ -approximation arguments for infima. The encoding of model (1) and of Algorithm $\mathcal A$ is shared with the other missions of this series. Contributions of these supporting lemmas are welcome.

Selected references

D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2011. https://doi.org/10.1007/s10107-011-0444-4
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99, 2004. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35, 2010. https://doi.org/10.1287/moor.1100.0444
D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Math. Oper. Res. 35, 2010. https://doi.org/10.1287/moor.1090.0440

7 thms3 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research·Captain: mikedeng1

Constructing Uncertainty Sets for Robust Linear Optimization 3: The Largest Centrally Symmetric Distortion Inner Approximation of a Polytope Solves a Linear ProgramResearch Paper

Motivation

A robust linear constraint $a'x \ge b$ for all $a \in \mathcal U$ protects a decision $x$ against every realization of the data $a$ in an uncertainty set $\mathcal U$ . Robust optimization took this form in the work of Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Oper. Res. Lett. 1999), where $\mathcal U$ is chosen by the modeller. Bertsimas and Brown (Oper. Res. 2009) tie the choice of $\mathcal U$ to the decision maker's attitude towards risk: on a finite sample $\mathcal A = \{a_1,\dots,a_N\}$ , a coherent risk measure constraint $\mu(\tilde a'x - b) \le 0$ is equivalent to a robust constraint over a convex set built from $\mathcal A$ , and for the distortion risk measures (the law-invariant, comonotone coherent measures, which include CVaR) that set is a polytope of a special kind, a permutohull.

An uncertainty set in practice is often an arbitrary polyhedron, given by the modeller or by previous analysis. Section 4.5 of the paper asks which distortion risk measure best approximates such a polyhedron from inside: the largest permutohull of a given shape contained in it. A positive answer quantifies how conservative a given polyhedral uncertainty set is relative to a distortion risk measure, and gives the risk measure that is closest to it. This mission is the third of a series of three on the paper; the first establishes the permutohull representation of distortion risk constraints, the second the generators of the centrally symmetric distortion measures.

Setting

Fix $N \ge 1$ and data $a_1,\dots,a_N \in \mathbb R^n$ , the columns of a matrix $A$ . Let $e_N \in \mathbb R^N$ have $1/N$ at each entry, so the sample mean is $\hat a = Ae_N$ .

The restricted simplex $\hat\Delta^N$ is the set of probability vectors $q \in \mathbb R^N$ with $q_1 \ge \dots \ge q_N$ . Under the uniform probability on $N$ points, the distortion risk measures are exactly the maps $\mu_q(X) = -\sum_i q_i x_{(i)}$ , $q \in \hat\Delta^N$ , with $x_{(1)} \le \dots \le x_{(N)}$ the ordered values of $X$ (Theorem 4.2 of the paper).
For $q \in \mathbb R^N$ , the $q$ -permutohull is $\Pi_q(\mathcal A) = \operatorname{conv}\{\sum_i q_{\sigma(i)} a_i : \sigma \in S_N\}$ . The robust constraint over $\Pi_q(\mathcal A)$ is the risk constraint for $\mu_q$ .
The symmetric restricted simplex $\hat\Delta^N_{\mathrm{sym}}$ is the set of $q \in \hat\Delta^N$ with $q = 2e_N - q_\sigma$ for some permutation $\sigma$ , where $(q_\sigma)_i = q_{\sigma(i)}$ . For these $q$ the permutohull is centrally symmetric about $\hat a$ .
With $\tilde\pi_q(\mathcal A) = \Pi_q(\mathcal A) - \hat a$ , the Minkowski functional

\|w\|_{q,\mathcal A} = \inf\{\alpha > 0 : w/\alpha \in \tilde\pi_q(\mathcal A)\}

measures $w = a - \hat a$ against the shifted permutohull (12).

The polyhedron is $\mathcal U = \{a \in \mathbb R^n : u_k'a \ge v_k,\ k = 1,\dots,m\}$ (14), with $\hat a \in \mathcal U$ .

The family of candidate inner approximations is obtained by mixing a fixed $\hat q \in \hat\Delta^N_{\mathrm{sym}}$ with the uniform generator: $q = \lambda\hat q + (1-\lambda)e_N$ , $\lambda \in \mathbb R$ .

Formalization targets

Goal: Theorem 4.5

Let $\lambda^*$ be the optimal value of the linear program

\max\ \lambda\quad\text{s.t.}\quad q = \lambda\hat q + (1-\lambda)e/N,\quad e'(s_k + t_k) \ge v_k\ \forall k,\quad s_{k,i} + t_{k,j} \le (u_k'a_j)\,q_i\ \forall i,j,k, \tag{15}

in $s_k, t_k, q \in \mathbb R^N$ and $\lambda \in \mathbb R$ , and $q^* = \lambda^*\hat q + (1-\lambda^*)e_N$ . Then

\Pi_{q^*}(\mathcal A) \subseteq \mathcal U,\qquad \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \mathcal U \implies \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \Pi_{q^*}(\mathcal A),

and, when $\hat q \ne e_N$ , $q^* \in \hat\Delta^N$ if and only if

\lambda^* \le \frac{1}{1 - N\hat q_{\min}}. \tag{16}

Milestones

Proposition 4.2: for $q \in \hat\Delta^N_{\mathrm{sym}}$ with $\Pi_q(\mathcal A)$ of nonempty interior, $\|\cdot\|_{q,\mathcal A}$ is a norm.
Scaling (proof of Lemma 4.2): $\Pi_{\lambda q + (1-\lambda)e_N}(\mathcal A) = \hat a + \lambda\,\tilde\pi_q(\mathcal A)$ for every $q \in \mathbb R^N$ , $\lambda \in \mathbb R$ .
Lemma 4.2: $\|a - \hat a\|_{\lambda q + (1-\lambda)e_N,\mathcal A} = \frac{1}{|\lambda|}\|a - \hat a\|_{q,\mathcal A}$ for $q \in \hat\Delta^N_{\mathrm{sym}}$ , $\lambda \ne 0$ .
Containment as linear constraints (proof of Theorem 4.5): $\Pi_q(\mathcal A) \subseteq \mathcal U$ iff vectors $s_k, t_k$ satisfying the constraints of (15) exist, for every $q \in \mathbb R^N$ .
Nonnegativity (proof of Theorem 4.5): for $\lambda \ge 0$ and $N\hat q_{\min} < 1$ , $\lambda\hat q + (1-\lambda)e_N \in \hat\Delta^N$ iff $\lambda \le 1/(1 - N\hat q_{\min})$ .

Significance

The theorem reduces a geometric question — the largest member of a one-parameter family of centrally symmetric polytopes, each with $N!$ potential vertices, that fits inside an arbitrary polyhedron — to a linear program with $O(mN)$ variables and $O(mN^2)$ constraints. Its solution identifies a distortion risk measure $\mu = \lambda^*\mu_{\hat q} + (1-\lambda^*)\mathbb E[-X]$ , which the paper reads as a mean–deviation measure in the style of a Sharpe ratio, and the bound (16) decides whether the optimal set is itself a distortion set or must be shrunk further.

The results are proved in the paper, with short proofs that pass over several points: the scaling identity is asserted, the duality step leaves the assignment-problem structure implicit, and the norm claim requires a nondegeneracy condition that the page does not state. No machine-checked proof of any of them is known. A formalization fixes the exact hypotheses (nonempty interior for the norm, $\lambda \ne 0$ in (13), $\hat q \ne e_N$ in (16)), and the containment equivalence for arbitrary real weight vectors $q$ is a reusable fact about permutohulls and assignment duality.

Difficulty

The goal combines three ingredients of different nature. The containment equivalence needs that minimizing a linear function over the permutohull is a linear program over the Birkhoff polytope of doubly stochastic matrices, followed by linear programming duality for that program; neither the Birkhoff–von Neumann theorem nor assignment duality is a one-line consequence of what is in Mathlib. The scaling identity is a statement about convex hulls under an affine map and holds for all real $\lambda$ , including the reflected case $\lambda < 0$ ; the maximality claim then needs the central symmetry of $\Pi_{\hat q}(\mathcal A)$ about $\hat a$ , which is a property of $\hat\Delta^N_{\mathrm{sym}}$ (Proposition 4.1 of the paper) and not of a general $q$ . The tempting shortcut — comparing gauges directly — fails at $\lambda = 0$ , where the permutohull is the single point $\hat a$ and the gauge is degenerate.

Formalization scope

Vectors in $\mathbb R^N$ and $\mathbb R^n$ are Fin N → ℝ and Fin n → ℝ, with $0$ -based indices; $a_i$ is a i, $u_k'a$ is a dot product. $\hat\Delta^N$ uses Mathlib's stdSimplex and Antitone. The permutohull is convexHull of the range over Equiv.Perm (Fin N), defined for every real $q$ because (15) evaluates it at mixtures with possibly negative entries. The Minkowski functional is Mathlib's gauge, which takes the value $0$ (not $+\infty$ ) on points no positive multiple of the set reaches; this is why Proposition 4.2 assumes $\Pi_q(\mathcal A)$ has nonempty interior and why the goal states "largest" as set containment. $\hat q_{\min}$ is $\min_i \hat q_i$ . The optimal value $\lambda^*$ is a hypothesis (it is the greatest element of the feasible set of (15)), not a supremum defined by sSup.

Standing assumptions and disclosed additions: $N \ge 1$ ; the polyhedron (14) is not assumed bounded (a generalization); in (13) the right-hand norm is that of $q$ , not $\tilde q$ as printed, and $\lambda \ne 0$ ; in (16), $N\hat q_{\min} < 1$ ; "corresponds to a distortion risk measure" is read, as the proof reads it, as $q^* \in \hat\Delta^N$ . A formalization that assumes $\Pi_{q^*}(\mathcal A) \subseteq \mathcal U$ or the maximality of $\lambda^*$ trivializes the theorem: both are conclusions, and the linear program enters only through its constraints and its optimal value.

A complete development needs: convex hulls under affine maps; the Birkhoff–von Neumann theorem (doubly stochastic matrices are convex combinations of permutation matrices); duality for the assignment linear program; gauge calculus for centrally symmetric convex bodies. The containment equivalence and the scaling identity are reusable beyond this mission. Proofs of any milestone, and of the Birkhoff and assignment-duality infrastructure, are welcome.

Selected references

D. Bertsimas and D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal and A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

7 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons 3: With a Discrete Price Set the Two-Price Stopping-Time Heuristic Is Asymptotically OptimalResearch Paper

Motivation

Airlines, hotels and cruise lines rarely change prices continuously. They sell a fixed product (seats on one flight, rooms on one night) over a finite selling season, and they sell it at a small set of fares, opening and closing fare classes as the season unfolds. Gallego and van Ryzin, in Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), model this as the sale of $n$ items over a horizon of length $t$ , with Poisson demand whose rate depends on the current price. Section 4 of the paper restricts the price to a finite menu and asks how much is lost by using a simple rule that charges only two adjacent prices and switches once. The answer, Theorem 5, gives one explanation of fixed-fare-class yield management: with two fares and one well-timed switch, a seller earns asymptotically the best revenue any policy over the menu can earn. The source of this mission is the published 1994 article.

The paper is the starting point of a long line of work on fluid (deterministic) approximations in revenue management, including Feng and Gallego (1995) on optimal switching times between two prices and later re-solving and bid-price analyses, all of which compare stochastic policies to the value of a deterministic problem in the same way.

Setting

A menu consists of $K\ge2$ prices $p_1<p_2<\dots<p_K$ and Poisson demand rates $\lambda_1>\lambda_2>\dots>\lambda_K>0$ ; the firm may also charge the null price $p_\infty$ , at which demand is $0$ . The revenue rates $r_k=p_k\lambda_k$ satisfy $r_1>r_2>\dots>r_K$ , and the points $(\lambda_k,r_k)$ lie on a concave function on $[0,\infty)$ vanishing at $0$ .

The deterministic problem replaces random demand by its rate. If $t_k\ge0$ is the time spent at price $p_k$ , the problem is the linear program

J^D(n,t)=\sup\Big\{\sum_k r_k t_k:\ \sum_k t_k\le t,\ \sum_k\lambda_k t_k\le n,\ t_k\ge0\Big\}.

Given $n\in\mathbb N$ and $t>0$ , let $k=k^*$ be the index with $\lambda_k t\ge n>\lambda_{k+1}t$ , and put

t_k=\frac{n-\lambda_{k+1}t}{\lambda_k-\lambda_{k+1}},\qquad m=\lceil\lambda_k t_k\rceil,\qquad t_m=\frac{m}{\lambda_k}.

The stopping-time (ST) heuristic starts at price $p_k$ and switches to $p_{k+1}$ at the random time $\tau=\min(T_m,t_m)$ , where $T_m$ is the time of the $m$ -th demand. Sales stop when the $n$ items are gone or at time $t$ . $J^{ST}(n,t)$ is its expected revenue.

Formalization targets

Goal: Theorem 5

For a fixed index $k$ with $1\le k\le K-1$ and any sequences $n_j\in\mathbb N$ , $t_j\to\infty$ with $\lambda_k t_j\ge n_j>\lambda_{k+1}t_j$ ,

\lim_{j\to\infty}\frac{J^{ST}(n_j,t_j)}{J^D(n_j,t_j)}=1.

No rate of convergence is fixed in the goal, and the ratio $n_j/t_j$ may vary along the sequence.

Milestones

Proposition 4. The LP is solved by pricing at $p_{k^*}$ for time $t_{k^*}$ and at $p_{k^*+1}$ for time $t_{k^*+1}=(\lambda_{k^*}t-n)/(\lambda_{k^*}-\lambda_{k^*+1})$ , together with the edge cases $k^*=0$ and $k^*=K$ .
The wasteful heuristic is a lower bound: $J^W(n,t)\le J^{ST}(n,t)$ , where the wasteful heuristic offers $m$ units at $p_k$ during $[0,t_m]$ and $n-m$ units at $p_{k+1}$ afterwards.
Equation (28): the shrunk horizon $t'=t_m+(n-m)/\lambda_{k+1}$ satisfies $t-(\lambda_k-\lambda_{k+1})/(\lambda_k\lambda_{k+1})<t'\le t$ .
The closed form of $J^D$ and $J^D(n,t)<J^D(n,t')+(p_{k+1}-p_k)$ .
Equation (29): $J^{ST}(n,t)/J^D(n,t)\ge J^W(n,t)/J^D(n,t)\ge J^W(n,t')/(J^D(n,t')+(p_{k+1}-p_k))$ .
The wasteful bound: $J^W(n,t')\ge p_k[m-\tfrac12\sqrt m]+p_{k+1}[(n-m)-\tfrac12\sqrt{n-m}]$ and $J^W(n,t')/J^D(n,t')\ge1-\tfrac12(1/\sqrt m+1/\sqrt{n-m})$ .

Significance

Theorem 5 says that a policy with one price change, chosen from the deterministic solution, loses a vanishing fraction of the deterministic revenue. Since $J^D$ bounds the optimal expected revenue over all non-anticipating policies with prices in the menu (§4.0.1 of the paper), the ST heuristic is asymptotically optimal, and the optimal policy, which solves a Hamilton–Jacobi–Bellman system with no closed form, can be replaced by a rule that is computed by hand. The result also shows that a finite menu, together with dynamic allocation of capacity between two neighbouring prices, can realize the effective price of a continuous demand curve.

The theorem is proved in the paper. As far as the platform's index shows, neither this result nor the controlled Poisson sales process it needs has been formalized; Mathlib has the exponential and Poisson distributions but no counting process with a policy-dependent intensity. The mission produces a machine-checked version of the paper's proof chain: the LP solution, the coupling inequality between two heuristics, the deterministic horizon estimate (28), and the Poisson overflow estimate built on Gallego's bound (inequality (18) of the paper, already proved on the platform as PricingRM.DetHeuristic.gallego_bound).

Difficulty

The deterministic parts (Proposition 4, (28), the closed form of $J^D$ ) are finite-dimensional linear algebra. The difficulty sits in the stochastic comparison $J^W\le J^{ST}$ . The ST heuristic's switching time depends on the sales process, and after the switch the remaining stock and the remaining time are both random. The obvious attempt, writing $J^{ST}$ as a sum of two independent Poisson terms, is wrong: the two phases are dependent through $\tau$ . Any comparison has to handle a second phase whose starting stock and starting time are both random, which brings in the behaviour of the sales process after a random time determined by the process itself. The limit step then needs the overflow bound uniformly along sequences whose ratio $n/t$ is not fixed.

Formalization scope

All declarations live in the namespace GVRPricing.StoppingTime. The committed conventions are:

Indices are 0-based (Fin K): Lean index $k$ is the paper's price number $k+1$ , and lamN, pN, rN extend the sequences by $0$ beyond $K$ , matching the paper's $\lambda_{K+1}=r_{K+1}=0$ .
The menu carries the printed conditions plus an added concavity condition: the points $(\lambda_k,r_k)$ lie on a concave function vanishing at $0$ . This is the reading of §4's "corresponding to price $p_k$ , we have a known demand rate $\lambda_k$ " for a regular demand function with concave revenue rate. Without it Proposition 4 and Theorem 5 are false: the menu $\lambda=(3,2,1)$ , $p=(1,1.01,1.5)$ meets every printed condition, but at $t=1$ , $n=1.5$ Proposition 4's allocation earns $1.76$ while a feasible mix of $p_1$ and $p_3$ earns $1.875$ , and the ST ratio tends to about $0.939$ .
$J^D$ is defined directly as the LP value; the reduction from the rate-path problem (11) is the paper's assertion and is not formalized.
The sales process is built from $n$ i.i.d. standard exponential clocks by the time change of the ST policy's cumulative intensity, so at most $n$ items are sold. Time is elapsed time from $0$ . $J^{ST}$ is the expectation of the sum of prices charged at sales in $[0,t]$ , a lower Lebesgue integral of a bounded nonnegative function.
$J^W$ is the paper's two-Poisson formula of p. 1018.
$J^*$ is not defined, so the left ratio of (29) uses $J^D$ in place of $J^*$ (a stronger inequality, since $J^*\le J^D$ ), and the §4.0.1 upper bound $J^*\le J^D$ is not a milestone.
Corrected slips: the page prints $t_{n-m}\doteq n-m/\lambda_{k+1}$ for $(n-m)/\lambda_{k+1}$ ; the wasteful bound is stated at the shrunk horizon $t'$ , where its integrality assumptions hold exactly, instead of along the paper's subsequence; the ratio bound assumes $m<n$ , since $1/\sqrt{n-m}$ is undefined otherwise. Proposition 4 is stated as optimality, without the uniqueness that fails when three menu points are collinear.
Excluded: the edge cases $k^*=0$ and $k^*=K$ of Theorem 5, treated on the page only in an unproved remark.

A trivializing formalization would define $J^{ST}$ through the wasteful formula, or by a closed-form expression, which makes the goal the wasteful bound; here $J^{ST}$ is the expected revenue of the switching rule $\tau=\min(T_m,t_m)$ on the sales process. Likewise the limit is taken along sequences with $t_j\to\infty$ , not at a single $(n,t)$ .

Useful infrastructure, reusable beyond this mission: the exponential-clock construction of a Poisson process with piecewise-constant intensity, the strong Markov property at a stopping time of the clocks, and the expected Poisson overflow $\mathbb E(N_\mu-\mu)^+$ . Contributions to any milestone, and alternative proofs of $J^W\le J^{ST}$ , are welcome.

Selected references

G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 999–1020, 1994. doi:10.1287/mnsc.40.8.999
G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11, 55–60, 1992 (the source of inequality (18)).
Y. Feng, G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995.
P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer-Verlag, New York, 1980 (as cited in the source).

11 thms3 active usersReviewed

Completed

Combinatorics Linear algebra Operations Research·Captain: mikedeng1

On the Abstract Properties of Linear Dependence 4: Orthogonal Subspaces Have Dual MatroidsResearch Paper

Motivation

Hassler Whitney introduced matroids in On the Abstract Properties of Linear Dependence (Amer. J. Math. 57, 1935, doi:10.2307/2371182) to capture what linear dependence among the columns of a matrix and the circuit structure of a graph have in common. One of the central constructions of the paper is duality. For graphs, duality exists only for planar graphs (Whitney, Non-separable and planar graphs, Trans. AMS 34, 1932); for matroids Whitney showed that every matroid has a dual, and that duality has a direct linear-algebra model: the matroid of a subspace of $\mathbb R^n$ and the matroid of its orthogonal complement are duals.

Matroid duality underlies much of combinatorial optimization: the duality between cycles and cuts in graphs, the relation between a linear code and its dual code, the exchange of rank and corank in matroid intersection and partition, and the treatment of network flows as duals of potential problems. Whitney's §§11–13 are where this structure is first defined and where its linear-algebra meaning (Theorem 28) is established.

Setting

A matroid $M$ is a finite set of elements $e_1,\dots,e_n$ with a rank function $r$ on its subsets; equivalently, a family of independent sets, or of bases (maximal independent sets). For a subset $N$ write $\rho(N)$ for its number of elements and

n(N) = \rho(N) - r(N)

for its nullity; $r(M)$ and $n(M)$ are the rank and nullity of the whole set of elements.

Duality (§11). Let $M$ and $M'$ be matroids and $\sigma$ a one-to-one correspondence between their elements. $M'$ is a dual of $M$ (via $\sigma$ ) if, for every subset $N$ of $M$ , with $N'$ the complement in $M'$ of $\sigma(N)$ ,

r(N') = r(M') - n(N). \tag{11.1}

The matroid of a subspace (§12). Let $E_n$ be $n$ -dimensional Euclidean space with coordinates $x_1,\dots,x_n$ , and let $H$ be a hyperplane through the origin, which in Whitney's usage is a linear subspace of any dimension. For a set $S$ of coordinates, project $H$ onto the coordinate subspace $E'_S$ spanned by the axes $x_i$ , $i\in S$ . The matroid associated with $H$ has elements $e_1,\dots,e_n$ , one per coordinate, and gives the set $\{e_i: i\in S\}$ the rank

r_H(S) = \dim \pi_S(H).

If $H$ is the row space of a matrix $\mathbf M$ , then $r_H(S)$ is the rank of the columns of $\mathbf M$ indexed by $S$ , so the associated matroid is the column matroid of $\mathbf M$ .

In the Lean development these objects are WhitneyMatroid.Components.nullity (shared), IsDualVia M M' σ, IsDual M M', subspaceRank H S and IsAssociated M H.

Formalization targets

Goal: Theorem 28

Let $H$ be a subspace of $E_n$ and $H' = H^\perp$ its orthogonal complement. If $M$ and $M'$ are the matroids associated with $H$ and $H'$ , then $M$ and $M'$ are duals under the correspondence of equal coordinates:

\forall N\subseteq\{e_1,\dots,e_n\}:\qquad r_{M'}(\overline N) = r(M') - n_M(N).

Milestones

Theorem 27. For every subspace $H$ there is exactly one matroid associated with $H$ .
Theorem 6 (already proved on the platform). All bases have the same number of elements.
Theorem 7. $B$ is a base iff $r(B)=r(M)$ and $n(B)=0$ .
Theorem 8. If $B$ is a base and $N$ is independent, then $N\cup N'$ is a base for some $N'\subseteq B$ .
Theorem 20. If $M'$ is a dual of $M$ , then $r(M') = n(M)$ and $n(M') = r(M)$ .
Theorem 23. $M'$ is a dual of $M$ via $\sigma$ iff, for every $B$ , $B$ is a base of $M$ exactly when the complement of $\sigma(B)$ is a base of $M'$ .
Theorem 21. Duality is symmetric.
Theorem 22. Every matroid has a dual.

Significance

The result. Theorem 28 identifies abstract duality with orthogonal complementation. With Theorem 23 it says that the column matroid of a real matrix whose rows span $H$ and the column matroid of a matrix whose rows span $H^\perp$ have complementary bases. This is the basis of the standard representation of the dual of a represented matroid ( $[I_r\mid A]$ and $[-A^{\mathsf T}\mid I_{n-r}]$ ), of the cycle/cocycle duality of graphs viewed through incidence matrices, and of the fact that a matroid representable over a field has a dual representable over the same field. Theorems 20–23 are the basic facts every later treatment of matroid duality starts from: duality exchanges rank and nullity, is symmetric, always exists, and is characterized by base complements.

Formalizing it. All of these results are classical and proved in Whitney's paper; what this mission adds is a machine-checked development of Whitney's own definition of duality, the rank identity (11.1), rather than the base-complement definition used in modern libraries. Mathlib defines the dual matroid $M^*$ by base complements and proves that it is a matroid; it does not, at the pinned revision, contain the rank formula (11.1) for $M^*$ , the matroid of a real subspace, or Theorem 28. Theorem 6 is already proved on the platform and enters as a reference. Theorems 7 and 8 are close to Mathlib lemmas and are footholds rather than new content.

Difficulty

The difficulty of the goal is not in the combinatorics but in the passage between the two descriptions of a subspace. The natural first idea is to compare the ranks $r_H(S)$ and $r_{H^\perp}(\overline S)$ directly by counting dimensions of $H$ and $H^\perp$ . This does not close: $r_H(S)$ is the dimension of a projection of $H$ onto coordinates, while $\dim H^\perp = n - \dim H$ only controls $H^\perp$ as a whole, and the rank of a complementary coordinate set in $M'$ is not determined by the dimensions of $H$ and $H^\perp$ alone. Some relation between coordinate projections of $H$ and the structure of $H^\perp$ on the complementary coordinates has to be established. Theorem 27 is itself nontrivial in Lean: the rank function $r_H$ has to be shown to satisfy the matroid axioms, which needs a careful treatment of coordinate projections and of submodularity of dimension. On the abstract side, Theorem 23 needs both directions of the passage between the rank identity and base complements, including the counting step $r(M) + r(M') = \rho(M)$ .

Formalization scope

Matroids are Mathlib Matroid α on a finite type α whose ground set is all of α (Whitney's matroid is its finite set of elements). This finiteness and the ground set convention are part of the definitions; all theorems are stated under them.
Ranks and nullities. Ranks are Mathlib's eRk, finite on a finite type and converted to integers; the nullity $n(N)=\rho(N)-r(N)$ and the identity (11.1) are computed in $\mathbb Z$ . No truncated subtraction appears.
Duality is Whitney's rank identity (11.1) for every subset, for a fixed bijection σ : α ≃ β (IsDualVia) or some bijection (IsDual). It is deliberately not defined as Mathlib's M✶: with that definition Theorem 23 would be nearly definitional and Theorem 28 would lose the rank identity. A formalization that replaces (11.1) by the base-complement condition, or states Theorem 28 only for bases, is not this mission's goal.
Euclidean space is EuclideanSpace ℝ (Fin n) with its standard inner product; the orthogonal hyperplane is Hᗮ. The field is $\mathbb R$ , as in the paper; the analogous statement over other fields with the dot-product annihilator is a generalization and not part of this mission.
The associated matroid is a predicate (IsAssociated M H): ground set Fin n, and the rank of every set $S$ of coordinates equals the finrank of the image of $H$ under the coordinate projection onto $S$ (not of $H\cap E'_S$ , a different set function). Existence and uniqueness is Theorem 27.
Implicit hypotheses made explicit: the ground sets are finite and equal to the whole element type; Whitney's "dimension $r$ " and "dimension $n-r$ " in Theorem 28 are consequences of $H'=H^\perp$ and are not hypotheses. The goal covers $n=0$ , $H=\{0\}$ and $H=E_n$ .
Infrastructure needed and reusable: the matroid of a real subspace (equivalently the column matroid of a real matrix), with its rank function in terms of coordinate projections; the rank formula of the dual matroid; the dimension identity relating projections of $H$ and sections of $H^\perp$ . All are reusable for the other missions of this series (the Fano matroid and binary matroids) and for any later work on represented matroids. Proofs of the milestones, alternative proofs of Theorem 28 through Mathlib's M✶, and supporting lemmas on coordinate projections are welcome.

Selected references

H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
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
J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011, Chapter 2 (duality). https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
Mathlib, Mathlib.Combinatorics.Matroid (Dual, Rank). https://github.com/leanprover-community/mathlib4

12 thms3 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research·Captain: mikedeng1

Robust Solutions of Uncertain Linear Programs II: With Ellipsoidal Uncertainty the Robust Counterpart Is Equivalent to a Conic Quadratic ProgramResearch Paper

Motivation

The data of a linear program are often not known exactly: they are measured or estimated, or they are forecasts. The robust counterpart approach, going back to Soyster (1973), asks for a solution that is feasible for every data matrix in a prescribed uncertainty set and is best among such solutions. Ben-Tal and Nemirovski's 1999 paper [1] showed that the method stays computationally tractable for a broad class of uncertainty sets, the ellipsoidal uncertainties: the robust counterpart of an uncertain LP is then a conic quadratic program (CQP), solvable by interior point methods at roughly the cost of an LP of similar size. This result is the basis of robust linear optimization as it is used today [2], [3]. It is also the reason ellipsoidal sets are the default choice in robust portfolio selection (§4 of the paper) and in many later robust models.

Timeline. Soyster (1973) treated column-wise box uncertainty, for which the counterpart is again an LP [4]. Ben-Tal and Nemirovski (1998) developed the general theory of robust convex optimization [5]. The present paper (1999) proved the ellipsoidal-to-CQP reduction for LPs (Theorem 3.1). Its proof relies on the conic duality theory of Nesterov and Nemirovski (1994) [6].

Setting

An uncertain linear program in the homogeneous form (6) is

\min\{c^Tx \mid Ax \ge 0,\ f^Tx = 1\},

where $c, f \in \mathbb R^n$ are fixed and the matrix $A \in \mathbb R^{m\times n}$ lies in an uncertainty set $\mathcal U$ . A point $x$ is robust feasible if $f^Tx = 1$ and $Ax \ge 0$ for every $A \in \mathcal U$ . The robust counterpart $(P_{\mathcal U})$ minimizes $c^Tx$ over the robust feasible set

G_{\mathcal U} = \{x \mid Ax \ge 0\ \forall A \in \mathcal U,\ f^Tx = 1\}.

An ellipsoid in $\mathbb R^{m\times n}$ (display (14)) is a set

U(\Pi, Q) = \{\Pi(u) \mid \|Qu\| \le 1\},

where $\Pi(u) = P^0 + \sum_{j=1}^L u_jP^j$ is affine in $u \in \mathbb R^L$ , $Q$ is an $M\times L$ matrix, and $\|\cdot\|$ is the Euclidean norm. A singular $Q$ gives an ellipsoidal cylinder, which may be unbounded. An ellipsoidal uncertainty is a set

\mathcal U = \bigcap_{\ell=0}^k U(\Pi_\ell, Q_\ell)

(condition A) that is bounded (condition B) and contains a matrix $A$ with $A = \Pi_\ell(u^\ell)$ and $\|Q_\ell u^\ell\| < 1$ for every $\ell$ (condition C, a Slater condition).

Formalization targets

Goal: Theorem 3.1

For every $x \in \mathbb R^n$ ,

x \in G_{\mathcal U} \iff f^Tx = 1 \ \text{ and }\ \forall i \le m\ \ \exists\, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)} :\ (x, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)}) \text{ satisfies } (\mathcal C_i).

Here $(\mathcal C_i)$ is an explicit system: linear equations and one linear inequality in $(x, \lambda, \mu, \nu)$ , together with the second-order cone constraints $\|\mu^{(i)}_\ell\| \le \nu^{(i)}_\ell$ . Its coefficients are the matrices $P^j_\ell$ and $Q_\ell$ . The robust feasible set is therefore the projection of the feasible set of the conic quadratic program (CQP), which minimizes $c^Tx$ subject to $(\mathcal C_1), \dots, (\mathcal C_m)$ and $f^Tx = 1$ .

Milestones, in the order of the Appendix's proof

$\mathcal U$ equals the image of the feasible set of the problem $(P_i[x])$ under $u \mapsto \Pi_0(u^0)$ (p. 15).
Claim (I): with $f^Tx = 1$ , $x$ is robust feasible iff every $(P_i[x])$ has nonnegative optimal value (p. 15).
Claim (II): conic quadratic duality. A strictly feasible primal that is bounded below has a solvable dual with equal optimal value (p. 15).
Conditions B and C make every $(P_i[x])$ strictly feasible and bounded below (p. 16).

Companion results

The CQP forms (16) and (17) of the simplest cases (a single ellipsoid; constraint-wise ellipsoids), Remark 3.1 (bounded polytopes are ellipsoidal uncertainties), and the robust portfolio counterpart (22).

Significance

The result. Theorem 3.1 turns a semi-infinite constraint system (one constraint for every $A \in \mathcal U$ ) into finitely many conic quadratic constraints whose size is polynomial in the data. Robust LPs with ellipsoidal uncertainty, which by Remark 3.1 include polytopic uncertainty, can therefore be solved by standard conic solvers. Later robust optimization results, such as budgeted uncertainty, affinely adjustable policies and distributionally robust LPs, refine this pattern.

Formalizing it. The theorem is classical and its proof is complete, but no machine-checked proof exists. A formal proof needs a conic quadratic strong duality theorem with dual attainment (claim (II)), which Mathlib does not have in this form. That duality theorem can be reused well beyond this mission. The companion results (16), (17) and (22) are self-contained computations of a minimum of a linear function over a Euclidean ball.

Difficulty

The "if" direction is weak duality: a solution of $(\mathcal C_i)$ certifies that the $i$ -th constraint holds for all of $\mathcal U$ . The content is the "only if" direction. It requires dual attainment, not merely equality of optimal values, because a solution of $(\mathcal C_i)$ must exist. Dual attainment fails without a constraint qualification. Condition C must hold strictly for every ellipsoid, including $\ell = 0$ , and the ellipsoids may be cylinders, so the variables $u^\ell$ can range over unbounded sets even though $\mathcal U$ is bounded. Projecting the problem onto a single parameter space is not available in general, because the maps $\Pi_\ell$ need not be injective.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. The indices $\ell = 0, \dots, k$ are Fin (k + 1), and the $k$ equality multipliers $\lambda_\ell$ , $\ell \ge 1$ , are indexed by Fin k. Every norm is Euclidean, written out as euclidNorm v = √(∑ v_j²), because Mathlib's norm on Fin M → ℝ is the sup norm, under which ellipsoids would become boxes. Condition B is a uniform bound on all matrix entries, and condition C is required for every $\ell = 0, \dots, k$ . The page's words say " $\ell = 1, \dots, k$ ", but its display and the proof use every $\ell$ . Injectivity of $\Pi_\ell$ is not assumed, and neither is §2.1's standing assumption that $\mathcal U$ is convex and closed. An ellipsoidal uncertainty is convex automatically, and closedness is not used, so both omissions generalize the statement. Three printed slips are corrected and disclosed: the sum in the equality constraint of (CQP $_d$ ) runs over $\ell = 0, \dots, k$ ; $(\mathcal C_i)$ has $\varphi^{(i)}[x]$ where the page prints $f^{(i)}[x]$ ; and Remark 3.1 has the factor $2/(r_i - s_i)$ where the page prints $(r_i - s_i)/2$ .

The goal is not the contentless statement "some conic quadratic program has $G_{\mathcal U}$ as a projection", which holds for every closed convex set. It names the system $(\mathcal C_i)$ built from the data $P^j_\ell$ , $Q_\ell$ . The goal also does not mention optimal values, (CQP $_p$ ) or strict feasibility; those are milestones.

Contributions are welcome on the conic duality theorem (II) as a standalone result, on the finite-dimensional facts that minimize a linear function over a Euclidean ball (used in (16), (17) and (22)), and on the goal itself.

Selected references

A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
D. Bertsimas, D. B. Brown, C. Caramanis, Theory and applications of robust optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510
A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
Yu. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

9 thms3 active usersReviewed