All missions

Motivation

A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.

Setting

A network has internal buffers $\mathcal I=\{1,\dots,I\}$, an outside Buffer $0$, activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$.

• $A_{kj}=1$ if activity $j$ needs processor $k$, and $0$ otherwise.
• $B_{ji}=1$ if activity $j$ processes buffer $i\in\mathcal I\cup\{0\}$, and $0$ otherwise. The set $\mathcal B_j=\{i:B_{ji}=1\}$ is the constituency of $j$.
• An input activity has $\mathcal B_j=\{0\}$; a service activity has $0\notin\mathcal B_j$. Every activity is one of the two.
• Each processor serves input activities only (an input processor) or service activities only.
• Activity $j$ has processing rate $\mu_j=1/m_j$ and a nonnegative routing matrix $P^j$.

The input-output matrix is

$$R_{ij}=\mu_j\Big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\Big),\qquad i\in\mathcal I,\ j\in\mathcal J.$$

An allocation $a\in\mathbb R^J_+$ gives the level at which each activity runs. The allocation set $\mathcal A$ consists of the allocations with $\sum_jA_{kj}a_j\le1$ for every processor and $\sum_jA_{kj}a_j=1$ for every input processor. Write $\mathcal E$ for the set of its extreme points, the extreme allocations. For a buffer-level vector $z\in\mathbb R^I_+$ the network pressure is $p(a,z)=z\cdot Ra$. Buffer $i$ is a constituent buffer of $a$ if $\sum_ja_jB_{ji}>0$.

Assumption 1 (EAA). For every $z\in\mathbb R^I_+$ there is $a^*\in\mathcal E$ with $p(a^*,z)=\max_{a\in\mathcal E}p(a,z)$ such that $z_i>0$ for every constituent buffer $i$ of $a^*$.

A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted $i(j)$.

Formalization targets

Goal: Theorem 6 (p. 204)

$$\text{strict Leontief}\ \Longrightarrow\ \forall z\in\mathbb R^I_+\ \exists a^*\in\mathcal E:\ p(a^*,z)=\max_{a\in\mathcal E}p(a,z)\ \text{ and }\ z_i>0\ \text{for every constituent buffer } i \text{ of } a^*.$$

Milestones

1. (§3, p. 201) For every $z\in\mathbb R^I_+$, $\max_{a\in\mathcal A}p(a,z)$ is attained at an extreme allocation.
2. (p. 204) $B_{ji}=0$ and $R_{ij}\le0$ whenever $i\in\mathcal I$, $i\ne i(j)$.
3. (p. 204) Let $\mathcal J_0$ be the set of service activities $j$ with $z_{i(j)}=0$. Setting the coordinates of $\hat a\in\mathcal A$ in $\mathcal J_0$ to zero gives $\tilde a\in\mathcal A$ with $z'R\tilde a\ge z'R\hat a$.
4. (p. 204) It suffices to find $a^*\in\arg\max_{a\in\mathcal E}z'Ra$ with $a^*_j=0$ on $\mathcal J_0$.
5. (p. 204) If $\tilde a\in\mathcal A$ maximizes $z'Ra$ over $\mathcal A$ and vanishes on $\mathcal J_0$, some extreme allocation does both.

Significance

The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with $\rho\le1$. Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.

Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: $R$ from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.

Difficulty

The naive argument stops at "take a maximizing extreme allocation". A maximizer $\hat a$ may run a service activity whose buffer is empty, in which case EAA fails at $\hat a$. Removing such activities gives $\tilde a$, which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of $R$, which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from $\tilde a$ to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope $\mathcal A$. In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.

Formalization scope

• Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer $0$ as 0 and internal buffer $i$ as i.succ. Activities and processors are 0-based.

• Standing assumptions (§2), one predicate Network.Standing.

  • $A$ and $B$ are $0$–$1$ matrices.
  • Every constituency is nonempty, and every activity is an input or a service activity.
  • Every activity needs a processor.
  • Each processor serves input activities only or service activities only.
  • There is an input activity.
  • $P^j\ge0$ and $P^j_{00}=0$.

• Disclosed additions to the page.

  1. Every input processor has an activity. "The input processors are never idle" presupposes it.
  2. $m_j>0$. The page writes "nonnegative" but sets $\mu_j=1/m_j$.
  3. $\mathcal A\neq\emptyset$, an explicit hypothesis of the goal and of milestone 1. The paper presupposes it by listing $\mathcal E=\{a^1,\dots,a^E\}$. It does not follow from the standing assumptions: two input activities needing input processors $\{1,2\}$ and $\{2,3\}$ make (2) infeasible, so $\mathcal E=\emptyset$ and EAA fails in a network that is vacuously strict Leontief. A verification file checks this example in Lean.

• Conventions.

  • $\mathcal E$ is Mathlib's Set.extremePoints ℝ 𝒜.
  • Every "max" and "argmax" is in domination form ($p(a',z)\le p(a^*,z)$ for all $a'$), never sSup. Without attainment the statement would be vacuous.
  • Constituent buffers are internal buffers only. Buffer $0$ has no level.
  • $i(j)$ is written relationally.
  • Row sums of $P^j$ are not imposed.

• Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty $\mathcal E$, and Buffer $0$ must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.

• Infrastructure. Solvers need two results:

  • attainment of a linear maximum on extreme points of a compact convex polyhedron, via IsCompact.extremePoints_nonempty and Krein–Milman;
  • the fact that every extreme point in a convex decomposition of a maximizer with positive weight is a maximizer.

  Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
• J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
• M. Bramson and R. J. Williams, Two workload properties for Brownian networks, Queueing Systems 45(3):191–221, 2003. (no link verified; see the reference list of Dai & Lin 2005)
• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479

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.

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

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

1. 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).
2. 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})$.
3. Inequality (6.8). $1-\frac{2}{\pi}\arcsin(t)\ge 0.878(1-t)$ for all $t\in[-1,1]$.
4. 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

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

1. 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$.
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$.
3. 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$.
4. Lemma 6.9 in the weighted norm (p. 342): $\big(\|\nabla f(x)\|^*_{[1-\gamma]}\big)^2\ge2\alpha(f(x)-f(x^*))$.
5. 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

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