All missions

Motivation

Unit commitment (UC) is the day-ahead decision of an electricity system operator: which generators to switch on in each hour of the next day, and how much each of them should produce. System operators solve UC problems every day, and their cost and reliability are first-order concerns of power-system operations. With a large share of wind and solar generation, the net load (demand minus renewable output) at each node is uncertain at commitment time, and robust optimization is one of the standard ways to commit units that remain operable for every load trajectory in an uncertainty set.

The robust UC literature first adopted the two-stage model (Jiang et al. 2012; Zhao and Zeng 2012; Bertsimas et al. 2013): commitments are chosen first, then the dispatch is chosen after the whole day's net loads are revealed. In reality the operator learns the loads hour by hour, so the dispatch at hour $t$ may only use what has been observed up to $t$. Lorca, Sun, Litvinov and Zheng (2016) introduced the multistage robust UC model that imposes this non-anticipativity, and asked when the extra realism matters. Their answer is this mission's goal: it matters only through the ramping constraints.

Setting

There are generators $i\in\mathcal N_g$, net-load nodes $j\in\mathcal N_d$, lines $l\in\mathcal N_l$ and hours $t\in\mathcal T=\{1,\dots,T\}$.

• A commitment $(x,u,v)$ consists of on/off, start-up and shut-down indicators $x_i^t,u_i^t,v_i^t\in\{0,1\}$. The set $X$ of admissible commitments is cut out by the logical constraints (1b)–(1g): the start-up/shut-down identity $x_i^t-x_i^{t-1}=u_i^t-v_i^t$ and minimum up and down times $UT_i,DT_i$.
• For a commitment $x$ and the hour-$t$ net loads $d^t\in\mathbb R^{N_d}$, the dispatch set without ramping $\Omega_t^{NR}(x,d^t)$ is the set of $p^t\in\mathbb R^{N_g}$ with generation limits $p_i^{\min}x_i^t\le p_i^t\le p_i^{\max}x_i^t$, line limits $|\alpha_l^\top(B^pp^t-B^dd^t)|\le f_l^{\max}$ and energy balance $\sum_ip_i^t=\sum_jd_j^t$.
• The ramping constraints (1i) couple consecutive hours: $-RD_i^tx_i^t-SD_i^tv_i^t\le p_i^t-p_i^{t-1}\le RU_i^tx_i^{t-1}+SU_i^tu_i^t$.
• The budget uncertainty set is $\mathcal D=\prod_t\mathcal D^t$ with

• The commitment cost is $F(x)=\sum_t\sum_i(G_ix_i^t+S_iu_i^t)$ and the dispatch cost is $\sum_t\sum_iC_ip_i^t$.

The two-stage robust UC (2) minimizes over $X$

where the dispatch $p$ is chosen knowing the whole trajectory $d$. The multistage robust UC (5) minimizes over $X$

over policies $p^t(d^{[t]})$ that depend only on $d^{[t]}=(d^1,\dots,d^t)$ and satisfy the dispatch constraints for every $d\in\mathcal D$.

Formalization targets

Goal: Theorem 1 (p. 11)

With the ramping constraints deleted from both models,

and consequently the two problems have the same optimal value over $X$.

Milestones (the steps of the paper's proof)

Both sides are compared with problem (1P), whose objective is

1. Part (i): the dispatch set without ramping is separable over time; the uncertainty set (3) is separable over time; hence the two-stage objective equals the (1P) objective.
2. Part (ii): the multistage objective equals the nested max-min value of $(\widetilde M^{NR})$; one stage of the nested problem splits off the later value; backward induction gives the sum of per-period worst cases; hence the multistage objective equals the (1P) objective.

Companion results (Example 1, Propositions 1–2, pp. 7–9)

On a two-bus, two-hour system with line limit and ramp rates equal to $1$, the two-stage model is feasible (Proposition 1), yet under its commitment no causal dispatch policy is feasible (Proposition 2). These show that the hypothesis "without ramping constraints" cannot be dropped.

Significance

The theorem locates exactly where multistage robust UC differs from the two-stage model: in the inter-temporal coupling created by ramping. Without ramping, the hourly dispatch problems decouple and so does the uncertainty set, so seeing the future gives the dispatch no advantage. With ramping, Example 1 shows the two-stage model can certify a commitment that fails in real-time operation. The practical message drawn in the paper is that the multistage model is useful precisely when ramping capability is a scarce resource, which is the situation of systems with high renewable penetration.

The result is proved in the paper. As far as is known it has not been machine-checked. This mission produces a formal model of robust UC (commitment logic, network-constrained dispatch, budget uncertainty, non-anticipative policies) together with a checked proof of the equivalence and of the counterexample. The model is a reusable base for later formal work on robust and multistage power-system models, such as the affine-policy results of the same paper.

Difficulty

The two separability steps are short on paper but must be carried out in the extended reals, where infeasible dispatch problems have value $+\infty$ and sums of extended reals are not well behaved in general; the argument has to show that no $-\infty$ arises. The main gap is the multistage side. The paper passes from the policy formulation (5) to the nested max-min formulation (6) by a remark, without proof. Formally, the value of an optimization over non-anticipative policies, which are functions on the whole uncertainty set, has to be identified with a backward max-min recursion over the per-hour sets, in both directions and without any attainment of the minima. A tempting shortcut, defining the multistage model as the nested formula, would prove nothing about policies and is excluded.

Formalization scope

• Hours are Fin T, 0-based: Lean period $t$ is the paper's $t+1$. Generators, nodes, buses and lines are Fin Ng, Fin Nd, Fin Nb, Fin Nl.
• The initial status $x^0$ and dispatch $p^0$, which (1c) and (1i) use at the first hour, are data fields; the paper leaves them implicit.
• Commitment variables are real-valued with the constraint $\{0,1\}$ inside $X$. The index ranges of (1d)–(1g) avoid natural-number subtraction.
• All optimal values are in EReal; an infimum over an empty set is $+\infty$, the paper's convention for infeasibility.
• Standing assumptions of the budget set (3), carried as hypotheses: $\Gamma\ge0$ and $\hat d_j^t>0$. They make $\bar d\in\mathcal D$, so every $\mathcal D^t$ is nonempty.
• Policies are functions of the hour and the whole trajectory; non-anticipativity is the requirement that the dispatch at hour $t$ depends only on the net loads up to hour $t$. Without this requirement the multistage model would coincide with the two-stage model by definition and the theorem would be empty.
• "Equivalent" is formalized as equality of the two objectives at every commitment in $X$, plus equality of the optimal values.
• Example 1 is formalized on its own: two buses, the commitment $((1,1),(1,1))$, energy balance, ramp bounds $\pm1$ and the line limit $1$ on the net injection at bus $A$. It is not an instance of the budget set (3).

Contributions welcome: proofs of the milestones and the goal, and lemmas on infima and suprema of sums over product sets in EReal, which are reusable beyond this mission.

Selected references

• Á. Lorca, X. A. Sun, E. Litvinov, T. Zheng, Multistage adaptive robust optimization for the unit commitment problem, Operations Research 64(1), 2016. https://doi.org/10.1287/opre.2015.1456
• D. Bertsimas, E. Litvinov, X. A. Sun, J. Zhao, T. Zheng, Adaptive robust optimization for the security constrained unit commitment problem, IEEE Transactions on Power Systems 28(1), 2013. https://doi.org/10.1109/TPWRS.2012.2205021
• R. Jiang, J. Wang, Y. Guan, Robust unit commitment with wind power and pumped storage hydro, IEEE Transactions on Power Systems 27(2) 800–810, 2012.
• L. Zhao, B. Zeng, Robust unit commitment problem with demand response and wind energy, IEEE Power and Energy Society General Meeting, 2012, 1–8.
• J. Ostrowski, M. F. Anjos, A. Vannelli, Tight mixed integer linear programming formulations for the unit commitment problem, IEEE Transactions on Power Systems 27(1), 2012 (cited for the form of (1d)–(1g)).

Motivation

First-order methods such as the gradient method, Nesterov's accelerated method and the Heavy-ball method are usually analysed one at a time, each with its own hand-built potential function. Lessard, Recht and Packard (SIAM J. Optim. 26(1), 2016; read here in arXiv:1408.3595v7) observed that such a method is a linear dynamical system in feedback with the gradient map, and that tools from robust control, the integral quadratic constraints (IQCs) of Megretski and Rantzer (IEEE TAC 42(6), 1997), turn the question "does this method converge linearly, and at what rate?" into the feasibility of a small semidefinite program. The size of that program depends on the algorithm, not on the dimension of the optimization problem.

The paper's main result, Theorem 4, is the certificate behind this approach. It has been the starting point of a line of work on automated and computer-aided analysis of optimization algorithms, including the design of new methods with provably optimal rates.

Setting

An iterative algorithm is a linear system $G$ with state $\xi_k \in \mathbb R^{n_\xi}$, driven by an input $u_k \in \mathbb R^d$ and producing an output $y_k \in \mathbb R^d$:

The loop is closed by a map $\varphi$ from sequences to sequences, $u = \varphi(y)$. For the gradient method, $A = I$, $B = -\alpha I$, $C = I$ and $u_k = \nabla f(y_k)$.

Instead of $\varphi$ itself, one uses a constraint that $\varphi$ is known to satisfy. A filter $\Psi$ is a second linear system with state $\zeta_k \in \mathbb R^{n_\zeta}$, inputs $(y_k, u_k)$ and output $z_k \in \mathbb R^{n_z}$:

Given a reference point $(y_\star, u_\star)$, the pair $(\zeta_\star, z_\star)$ is the fixed point of the filter: $\zeta_\star = A_\Psi\zeta_\star + B^y_\Psi y_\star + B^u_\Psi u_\star$ and $z_\star = C_\Psi\zeta_\star + D^y_\Psi y_\star + D^u_\Psi u_\star$. Assume $\rho(A_\Psi) < 1$ (all eigenvalues of $A_\Psi$ have modulus less than one) and let $M$ be a symmetric matrix. The map $\varphi$ satisfies the $\rho$-hard IQC defined by $(\Psi, M, \rho, y_\star, u_\star)$ if, for every input sequence $y$, with $u = \varphi(y)$ and $z = \Psi(y,u)$,

It satisfies the pointwise IQC if each term $(z_k - z_\star)^\top M (z_k - z_\star)$ is nonnegative.

Eliminating $y$, the systems $G$ and $\Psi$ combine into one linear system with state $x_k = (\xi_k, \zeta_k)$:

The condition number of a symmetric positive definite $P$ is $\operatorname{cond}(P) = \lambda_{\max}(P)/\lambda_{\min}(P)$, and $\|\cdot\|$ is the Euclidean norm.

Formalization targets

Goal: Theorem 4

Let $(\xi_\star, \zeta_\star, y_\star, u_\star, z_\star)$ be a fixed point of $G$ and $\Psi$ ($\xi_\star = A\xi_\star + Bu_\star$, $y_\star = C\xi_\star$, and the filter equations above), let $0 < \rho \le 1$, and suppose $\varphi$ satisfies the $\rho$-hard IQC defined by $(\Psi, M, \rho, y_\star, u_\star)$. If there are $P \succ 0$ and $\lambda \ge 0$ with

then every trajectory of the interconnection, $\xi_{k+1} = A\xi_k + B\,\varphi(C\xi)_k$, satisfies

Milestones

The milestones follow the paper's proof: the elimination (3.6) of $y$; the one-step inequality (3.10) obtained from the LMI at a fixed point of (3.7); its weighted telescoped sum; the decay $(x_k - x_\star)^\top P (x_k - x_\star) \le \rho^{2k}(x_0 - x_\star)^\top P (x_0 - x_\star)$ in the $P$-weighted norm; and the passage to the Euclidean norm with the factor $\sqrt{\operatorname{cond}(P)}$. Two companion statements are included: a pointwise IQC implies the $\rho$-hard IQC for every $\rho > 0$ (the remark after Theorem 4), and Proposition 2 (for $\rho \ge 0$), the Lyapunov characterisation $\rho(T) < \rho \iff \exists P \succ 0,\ T^\top P T - \rho^2 P \prec 0$.

Significance

Theorem 4 reduces a statement about all functions in a class, for instance all strongly convex functions with Lipschitz gradients in every dimension, to a semidefinite feasibility problem with a handful of variables. The paper uses it to recover the known rates of the gradient method and to compute numerically certified rates for Nesterov's method, and the same template underlies later rate certificates for proximal, operator-splitting and distributed methods. The pointwise remark is what lets the sector IQC of gradients be plugged in directly.

The theorem is proved in the paper; nothing about it is open. To our knowledge neither the IQC framework nor Theorem 4 has a machine-checked proof. A formal development gives the first verified version of the certificate, and with it a route by which a numerically found LMI solution, once checked exactly, yields a verified convergence rate for a concrete algorithm.

Difficulty

The argument is short; the difficulty is in the bookkeeping. The IQC is a statement about every input sequence, while the conclusion concerns one trajectory of the closed loop, so the proof has to instantiate the IQC at the trajectory's own output $y = C\xi$ and match the filter state it produces with the $\zeta$-component of the combined state. The weights $\rho^{-2t}$ must line up with the telescoping of the one-step inequality, and the final step needs the eigenvalue bounds $\lambda_{\min}(P)\|v\|^2 \le v^\top P v \le \lambda_{\max}(P)\|v\|^2$ together with the fact that $\zeta_0 = \zeta_\star$ removes the filter state from the initial error. Block matrices indexed by sums of index types make each of these steps heavier in Lean than on paper.

Formalization scope

Vectors are Fin n → ℝ, matrices are Matrix (Fin a) (Fin b) ℝ, and sequences are ℕ → Fin n → ℝ indexed from $0$. The norm is written out as $\sqrt{v^\top v}$, because Mathlib's norm on Fin n → ℝ is the sup norm, under which the constant $\sqrt{\operatorname{cond}(P)}$ would be wrong. The combined state lives on Fin nξ ⊕ Fin nζ and the LMI on (Fin nξ ⊕ Fin nζ) ⊕ Fin d, assembled with Matrix.fromBlocks, fromRows and fromCols; "$\preceq 0$" is positive semidefiniteness of the negated matrix. $\operatorname{cond}(P)$ is the largest over the smallest eigenvalue of the Hermitian matrix $P$, and $\rho(A_\Psi) < 1$ is stated over the complex spectrum.

The page allows $0 \le \rho$; since the weights $\rho^{-2t}$ are undefined at $\rho = 0$, every statement that uses them assumes $\rho > 0$. Proposition 2 is printed without a sign condition and is false for $\rho < 0$; it is stated for $\rho \ge 0$. The IQC hypothesis quantifies over every input sequence and every $k$, with the filter started at $\zeta_\star$; replacing it by the IQC along the single closed-loop trajectory, starting the filter at $0$, or reading $\|\cdot\|$ as the sup norm would each change the theorem, and none is the formalization. The trajectory in the goal is universally quantified ("for any $\xi_0$"); its existence is not assumed. The hypotheses $\rho(A_\Psi) < 1$ and $M = M^\top$ are kept as on the page although the proof does not use them. A sanity instance outside the proposal (the scalar gradient method with the sector IQC, $\rho = 1/2$, $P = 1$, $\lambda = 1/4$) checks in Lean that all hypotheses of the goal can hold at once.

The development needs only Mathlib's linear algebra: block matrices, PosDef/PosSemidef, the spectral theorem for Hermitian matrices, and finite sums. The Euclidean-norm lemma (decay in a $P$-norm implies decay in the Euclidean norm with factor $\sqrt{\operatorname{cond}(P)}$) and Proposition 2 are reusable beyond this mission. Proofs of any milestone, and of Proposition 2 in either direction, are welcome.

Selected references

• L. Lessard, B. Recht, A. Packard, Analysis and Design of Optimization Algorithms via Integral Quadratic Constraints, SIAM J. Optim. 26(1):57–95, 2016. https://doi.org/10.1137/15M1009597 (arXiv version used: https://arxiv.org/abs/1408.3595v7)
• A. Megretski, A. Rantzer, System Analysis via Integral Quadratic Constraints, IEEE Trans. Automat. Control 42(6):819–830, 1997. https://doi.org/10.1109/9.587335
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

For a finite graph, the Cheeger constant measures how hard it is to cut the vertex set into two pieces, and the spectral gap of the graph Laplacian measures how fast random walks mix. The two Cheeger inequalities (Dodziuk 1984; Alon and Milman 1985; Alon 1986) bound each quantity by a function of the other, and they underlie the theory of expander graphs, with uses in derandomization, error-correcting codes and the analysis of Markov chains.

High-dimensional expanders extend this theory from graphs to simplicial complexes. Linial and Meshulam (2006) and Gromov (2010) introduced combinatorial and topological notions of expansion for complexes; the spectral side is Eckmann's discrete Hodge theory (1944), in which each dimension carries its own Laplacian. Parzanchevski, Rosenthal and Tessler (arXiv:1207.0638, Combinatorica 2015) defined a $d$-dimensional Cheeger constant $h(X)$ through partitions of the vertices into $d+1$ blocks and proved the analogue of the upper Cheeger inequality, $\lambda(X)\le h(X)$, for complexes with a complete skeleton. This mission formalizes that theorem.

Setting

Let $V=\{0,1,\dots,n-1\}$ and $d\ge1$. A finite $d$-complex with a complete skeleton $X$ on $V$ consists of all subsets of $V$ with at most $d$ elements together with a set $X^d$ of $(d+1)$-element subsets, the $d$-cells. A set of $j+1$ vertices is a $j$-cell; $X^{d-1}$ is therefore the set of all $d$-element subsets.

Each cell is oriented by the increasing order of its vertices, $\sigma=[\sigma_0,\dots,\sigma_j]$ with $\sigma_0<\dots<\sigma_j$. The space $\Omega^{j}$ of $j$-forms consists of the real functions on $j$-cells, with inner product

The co-boundary $\partial_d^*:\Omega^{d-1}\to\Omega^d$ and the boundaries $\partial_d:\Omega^d\to\Omega^{d-1}$, $\partial_{d-1}:\Omega^{d-1}\to\Omega^{d-2}$ are

where $v\sim\sigma$ means that $v\notin\sigma$ and $\{v\}\cup\sigma$ is a cell, and $[v,\sigma_0,\dots]$ equals $(-1)^k$ times the increasingly oriented cell when $v$ has $k$ smaller vertices in $\sigma$. The upper Laplacian is $\Delta^+=\partial_d\partial_d^*$ on $\Omega^{d-1}$, and $Z_{d-1}=\ker\partial_{d-1}$ is the space of $(d-1)$-cycles.

The spectral gap is the least eigenvalue of $\Delta^+$ on the cycles (Definition 2.1):

For sets $A_0,\dots,A_d\subseteq V$, let $F(A_0,\dots,A_d)$ be the set of $d$-cells with exactly one vertex in each $A_i$. The Cheeger constant is (Definition 1.1)

the minimum over partitions of $V$ into nonempty sets $A_0,\dots,A_d$. For $d=1$, $Z_0$ is the space of functions summing to zero, $\Delta^+$ is the graph Laplacian, and $h$ is the usual Cheeger constant $\min_{A}\,n|E(A,\bar A)|/(|A||\bar A|)$.

Formalization targets

Goal: Theorem 1.2 (Cheeger Inequality)

for every finite $d$-complex $X$ with a complete skeleton on $n\ge d+1$ vertices.

Milestones

1. The chain-complex identity $\partial_{d-1}\partial_d=0$ (p. 6).
2. The form $f$ of (4.1), built from a partition, is a $(d-1)$-cycle (p. 12).
3. $\partial_d^*$ is the adjoint of $\partial_d$: $\langle\partial_dg,f\rangle=\langle g,\partial_d^*f\rangle$ (p. 6).
4. Rayleigh's principle (4.2): $\lambda(X)\langle f,f\rangle\le\langle\Delta^+f,f\rangle=\langle\partial_d^*f,\partial_d^*f\rangle$ for $f\in Z_{d-1}$ (p. 12).
5. $\langle f,f\rangle=n\prod_{i=0}^d|A_i|$ for the form (4.1) (p. 13).
6. (4.3): $|(\partial_d^*f)(\sigma)|$ equals $n$ for $\sigma\in F(A_0,\dots,A_d)$ and $0$ for the other $d$-cells (p. 13).
7. $\langle\partial_d^*f,\partial_d^*f\rangle=n^2|F(A_0,\dots,A_d)|$ (p. 14).

Milestones 2 and 5–7 hold for every partition, not only a minimizing one.

Significance

The result. Theorem 1.2 shows that a large spectral gap forces every partition of the vertices into $d+1$ blocks to be crossed by many $d$-cells, so spectral information certifies combinatorial expansion of a complex. The paper uses it with the spectral analysis of Gundert and Wagner to show that Linial–Meshulam random complexes $X(d,n,C\log n/n)$ have Cheeger constant of order $\log n$ for large $C$ (Corollary 1.3). The paper also shows that the converse direction fails: a triangulation of the Möbius strip has $h(X)=1\tfrac14$ but $\lambda(X)=0$, so no lower bound of the form $C\cdot h(X)^m\le\lambda(X)$ holds.

Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof requires a signed simplicial chain complex with explicit orientations, the adjoint relation between boundary and co-boundary, and a Rayleigh-quotient bound for a symmetric operator on an invariant subspace. These are the basic tools for any further formal work on spectral high-dimensional expansion, including the Mixing Lemma of the same paper (the companion mission of this series).

Difficulty

The graph proof plugs a two-valued test function into the Rayleigh quotient. In dimension $d$ the test vector must be a $(d-1)$-cycle, and an indicator of a block is not one. The paper's form (4.1) assigns to a $(d-1)$-cell whose vertices meet $d$ distinct blocks the size of the missing block, with the sign of a permutation of the blocks. Showing that this form is a cycle and that its co-boundary has absolute value exactly $n$ on $F(A_0,\dots,A_d)$ and $0$ elsewhere is a case analysis over how the vertices of a cell fall into blocks, and every case depends on the orientation signs. A convention error in any of the operators or in the form makes one of these identities fail. A second, smaller difficulty is that $\lambda(X)$ is a minimum over the spectrum on a subspace, so the Rayleigh bound must be proved for $\Delta^+$ restricted to $Z_{d-1}$, which it preserves.

Formalization scope

• Vertices are Fin n; a complex is a structure holding its $d$-cells as Finset (Finset (Fin n)), each of size $d+1$; the complete skeleton is built into the type. Complexes without $d$-cells are allowed.
• Forms are EuclideanSpace ℝ over the subtype of $k$-element vertex sets, so no form is supported on sets of the wrong size. $\Omega^d$ is modelled on all $(d+1)$-element sets; $\partial_d^*$ vanishes off $X^d$ and $\partial_d$ ignores values there.
• Orientation is by the order of Fin n; the sign of vertex $v$ in cell $\tau$ is $(-1)^{\#\{w\in\tau:w<v\}}$. Boundary and co-boundary are both defined by their formulas; their adjointness is milestone 3.
• The spectral gap is not defined by sInf. The goal states that some eigenvalue $\mu$ of $\Delta^+$ on $Z_{d-1}$ (a nonzero cycle $f$ with $\Delta^+f=\mu f$) is at most the Cheeger ratio of every partition, which is equivalent to $\lambda(X)\le h(X)$. A partition is a family A : Fin (d+1) → Finset (Fin n) of nonempty, pairwise disjoint sets covering the vertices.
• Added hypotheses: $d\ge1$ (the Laplacians act on $\Omega^{d-1}$) and $n\ge d+1$ (presupposed by the paper, since $h$ minimizes over partitions into $d+1$ nonempty sets; for $n\le d$ the cycle space is $0$).
• Ruled out: forms supported off the $d$-element sets (they would be spurious cycles with eigenvalue $0$), an eigenvalue set read through sInf (empty sets give $0$), unsigned boundaries (for which $\partial\partial\ne0$), cocycles $\ker\partial_d^*$ in place of cycles $\ker\partial_{d-1}$ (on which $\Delta^+$ is zero), and arbitrary disjoint families in place of partitions (empty blocks give ratio $0$).
• Needed infrastructure: sign bookkeeping for faces of sorted finsets, the spectral theorem for symmetric operators on a finite-dimensional inner product space restricted to an invariant subspace (Mathlib's LinearMap.IsSymmetric), and counting cells by blocks of a partition. The chain-complex and adjointness lemmas are reusable in any formal development of simplicial Hodge theory; contributions there are welcome.

Selected references

• O. Parzanchevski, R. Rosenthal, R. J. Tessler, Isoperimetric inequalities in simplicial complexes, Combinatorica 35 (2015). arXiv:1207.0638v3, doi:10.1007/s00493-014-3002-x
• B. Eckmann, Harmonische Funktionen und Randwertaufgaben in einem Komplex, Comment. Math. Helv. 17 (1944), no. 1, 240–255.
• N. Alon, V. D. Milman, λ₁, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985), 73–88. doi:10.1016/0095-8956(85)90092-9
• N. Linial, R. Meshulam, Homological connectivity of random 2-complexes, Combinatorica 26 (2006), 475–487. doi:10.1007/s00493-006-0027-9
• A. Gundert, U. Wagner, On Laplacians of random complexes, Proceedings of the 2012 Symposium on Computational Geometry, ACM, 2012, 151–160.
• M. Gromov, Singularities, expanders and topology of maps. Part 2: From combinatorics to topology via algebraic isoperimetry, Geom. Funct. Anal. 20 (2010), no. 2, 416–526.

Decisions with covariate information

In many operational problems the decision $z$ is taken after observing covariates $x$ (weather, calendar, prices) that carry information about an uncertain quantity $Y$ (demand, yield, return). The target is the conditional stochastic program: minimize $\mathbb E[c(z,Y)\mid X=x]$ over a feasible set $\mathcal Z$. Kannan, Bayraksan and Luedtke (Math. Program. 2023) approach it in two steps: fit a regression model of $Y$ on $X$, then use the regression residuals as scenarios of the uncertainty at the new covariate $x$. Their earlier work (Kannan, Bayraksan, Luedtke, arXiv:2207.13554) analysed the sample average approximation built in this way (ER-SAA). The 2023 paper wraps the same scenarios in a distributionally robust problem, to protect against the small-sample error of the regression and of the residuals.

This mission formalizes the paper's rate of convergence for a family of ambiguity sets that contains sample robust optimization and reweighting (φ-divergence, CVaR) sets as special cases.

Setting

Responses $Y\in\mathbb R^{d_y}$ follow $Y=f^*(X)+\varepsilon$, with regression function $f^*$ and error $\varepsilon$ of law $P_\varepsilon$. A known nonempty closed convex set $\mathcal Y$ contains the range of $Y$, with orthogonal projection $\mathrm{proj}_{\mathcal Y}$. From data $\mathcal D_n=\{(y^i,x^i)\}_{i=1}^n$, with $\varepsilon^i=y^i-f^*(x^i)$, one computes a regression estimate $\hat f_n$ and residuals $\hat\varepsilon^i_n=y^i-\hat f_n(x^i)$. At a covariate realization $x$ the scenarios are $\mathrm{proj}_{\mathcal Y}(\hat f_n(x)+\hat\varepsilon^i_n)$.

The true problem (3) is $v^*(x)=\min_{z\in\mathcal Z}g(z;x)$ with $g(z;x)=\mathbb E[c(z,f^*(x)+\varepsilon)]$, and the full-information SAA objective (4) is $g^*_n(z;x)=\frac1n\sum_i c(z,f^*(x)+\varepsilon^i)$.

The unified ambiguity family of §5 has two radii. $\mu_n(x)\ge0$ is the radius of balls $\hat{\mathcal Y}^i_n=\{y\in\mathcal Y:\|y-\mathrm{proj}_{\mathcal Y}(\hat f_n(x)+\hat\varepsilon^i_n)\|\le\mu_n(x)\}$ around each scenario. $\mathfrak P_n=\mathfrak P_n(x;\zeta_n(x))$ is a set of probability vectors that shrinks to the uniform weights. The worst-case expected cost over the distributions $\sum_ip_i\delta_{\bar y^i}$ with $p\in\mathfrak P_n$ and $\bar y^i\in\hat{\mathcal Y}^i_n$ is the ER-DRO objective

and the ER-DRO problem (8) is $\hat v^{DRO}_n(x)=\min_{z\in\mathcal Z}\hat g^{ER}_{s,n}(z;x)$, with optimal solution $\hat z^{DRO}_n(x)$. Taking $\zeta_n\equiv0$ gives sample robust optimization; taking $\mu_n\equiv0$ gives ambiguity sets with the same support as the empirical residual distribution. The intermediate objective $g^*_{s,n}(z;x)=\sup_{p\in\mathfrak P_n}\sum_ip_i\,c(z,f^*(x)+\varepsilon^i)$ reweights the true scenarios.

Formalization targets

Goal: Theorem 17 (p. 24)

Assume the following:

• Assumption 9: $c(z,\cdot)$ is Lipschitz on $\mathcal Y$, with constants $L(z)$ bounded on $\mathcal Z$.
• Assumption 12: $\sup_{p\in\mathfrak P_n}\sum_i(p_i-\frac1n)^2=C_\zeta n^{-(1+r)}$.
• Assumption 13: a uniform weak LLN for $c^2$.
• Assumption 14: a functional CLT for $\sqrt n(g^*_n-g)$ in $C(\mathcal Z)$.
• Assumption 15: the regression rate $\|f^*(x)-\hat f_n(x)\|^2=O_p(n^{-r})$ and $\frac1n\sum_i\|f^*(x^i)-\hat f_n(x^i)\|^2=O_p(n^{-r})$ with $0<r\le1$.
• The radius is $\mu_n=C_\mu n^{-r/2}$.