Missions · Prove2Me

Completed

Operations Research Optimization·Captain: mikedeng1

Quantity Flexibility Contracts and Supply Chain Performance 1: Under the Minimum Commitment Policy a Flex Node With At Least Its Customer's Flexibility Keeps Zero InventoryResearch Paper

Motivation

Manufacturers and their suppliers rarely trade on fixed orders. A buyer sends a rolling schedule of intended purchases for the coming periods and revises it every period as its own forecasts change. Left unconstrained, such revisions pass demand volatility up the supply chain and amplify it, the phenomenon studied as the bullwhip effect (Lee, Padmanabhan & Whang 1997). A quantity flexibility (QF) contract limits how far each estimate may move from one period to the next: the buyer commits to a band around its earlier estimate, and the supplier commits to supply anything inside that band. The paper reports QF-type agreements at Sun Microsystems, Solectron, Nippon Otis, Toyota, IBM, Hewlett Packard and Compaq (p. 92).

Tsay & Lovejoy (1999) model a multi-stage chain in which every stage is linked to its neighbours by QF contracts, and ask how the flexibility a node offers its customer, compared with the flexibility it receives from its supplier, determines the inventory the node must carry. This mission formalizes their answer for one node: Proposition 2 (p. 97), which states that a node whose supply side is at least as flexible as its customer side needs no inventory at all.

Setting

Time is discrete, $t = 0, 1, 2, \dots$ . In period $t$ a flex node receives from its customer a release schedule $f(t) = [f_0(t), f_1(t), \dots]$ : $f_0(t)$ is the quantity sold in period $t$ , and $f_j(t)$ is the current estimate of the quantity to be sold in period $t + j$ . The node sends its supplier a replenishment schedule $r(t) = [r_0(t), r_1(t), \dots]$ with the same meaning on the purchase side. Its ending stock evolves as

I(t) = I(t-1) + r_0(t) - f_0(t).

The QF contract on the customer side has output parameters $\alpha^{out}_q \ge 0$ and $0 \le \omega^{out}_q \le 1$ , $q \ge 1$ , and the output IR (Incremental Revision) constraints (6):

(1 - \omega^{out}_j)\, f_j(t) \le f_{j-1}(t+1) \le (1 + \alpha^{out}_j)\, f_j(t), \qquad j \ge 1.

The supplier side has input parameters $(\alpha^{in}_q, \omega^{in}_q)$ and the analogous constraints (7) on $r$ . The cumulative flexibilities (9), (11) are

1 + A_j = \prod_{q=1}^{j}(1 + \alpha_q), \qquad 1 - \Omega_j = \prod_{q=1}^{j}(1 - \omega_q),

on each side, with $A_0 = \Omega_0 = 0$ . The pair of sequences $(A, \Omega)$ is the side's flexibility profile.

The node follows the Minimum Commitment (MC) policy (21)–(23). From $I(t-1)$ , $r(t-1)$ and $f(t)$ it computes, by one recursion on $j \ge 0$ , projected inventories $l_j(t)$ and the new schedule:

l_0(t) = I(t-1),\qquad r_j(t) = \max\Bigl[\frac{(1 + A^{out}_j) f_j(t) - l_j(t)}{1 + A^{in}_j},\ (1 - \omega^{in}_{j+1})\, r_{j+1}(t-1)\Bigr],

l_{j+1}(t) = \bigl[l_j(t) + (1 - \Omega^{in}_j)\, r_j(t) - (1 + A^{out}_j)\, f_j(t)\bigr]^+.

The first term of the maximum is the target $T_j(t)$ of (22): the least supply that covers the largest purchase the customer may still make in period $t + j$ . The second term is the least value the supplier contract allows given last period's schedule.

Formalization targets

Goal: Proposition 2

Under the standing assumptions, if (a) the release schedules are nonnegative and obey (6), (b) the node uses the MC policy, (c) $I(0) = 0$ and the run starts with $r(0) = f(0)$ , and (d) $A^{out}_j \le A^{in}_j$ and $\Omega^{out}_j \le \Omega^{in}_j$ for all $j \ge 1$ , then

I(t) = 0 \quad \text{for all } t.

If moreover $(A^{in}, \Omega^{in}) = (A^{out}, \Omega^{out})$ and $\omega^{in}_q < 1$ for all $q$ , then

r_j(t) = f_j(t) \quad \text{for all } j \ge 0,\ t \ge 1.

Milestones

(8), p. 95: the IR constraints imply the cumulative bounds $(1 - \Omega^{out}_j) f_j(t) \le f_0(t + j) \le (1 + A^{out}_j) f_j(t)$ .
Coverage, p. 108: along the MC run, $r_j(t) \ge T_j(t)$ for every $j$ , hence $I(t) \ge 0$ .
Inventory is non-increasing, p. 108: under (d), $r_0(t) \le f_0(t)$ , hence $I(t) \le I(t-1)$ .
The vanishing step, p. 108: if $l_j(t) = 0$ and $r_j(t) = f_j(t)$ , then $l_{j+1}(t) = 0$ .

Significance

Proposition 2 isolates the source of inventory at an intermediate stage of a QF-linked chain: it is the disparity between the node's input and output flexibility, not the volatility of the forecasts themselves. A node supplied at least as flexibly as it serves can meet every contractual obligation with zero stock, and a node with matched flexibility passes every schedule upstream unchanged, acting as a non-distorting conduit of information and material. The paper uses this to argue that supply flexibility beyond the customer's is wasted at the node unless passed downstream (p. 97). Inventory under a flexibility mismatch, where the node amplifies flexibility, is studied numerically in §5 of the paper.

The result has a short proof in the paper, but that proof routes through formula (33), a closed form of the MC schedule as a maximum over all earlier periods, whose proof is omitted and which needs schedules before any starting period. A machine-checked proof must instead argue directly on a run with a definite start. No part of the paper has been formalized before; this mission also produces a reusable formal model of rolling schedules, QF constraints and the MC policy.

Difficulty

The obvious argument shows $r_0(t) \le f_0(t)$ from the definition of the MC policy at index $0$ alone. That fails: $r_0(t)$ is a maximum that includes the carried-over term $(1 - \omega^{in}_1)\, r_1(t-1)$ , which depends on the whole earlier schedule $r(t-1)$ , and that in turn on $r(t-2)$ , and so on back to the initial schedule. Bounding $r_0(t)$ therefore requires control of every component of every earlier schedule, an invariant over both indices that the paper does not state. The start of the run matters: with an unconstrained initial schedule the claim is false. The equal-flexibility part additionally needs a second induction, on $j$ within each period, interleaved with the recursion that defines $l_j(t)$ and $r_j(t)$ .

Formalization scope

Schedules are functions $\mathbb N \to \mathbb R$ indexed by $j \ge 0$ ; the release schedules are a function $f : \mathbb N \to \mathbb N \to \mathbb R$ with f t j $= f_j(t)$ . The QF parameters are sequences $\mathbb N \to \mathbb R$ whose value at index $0$ is unused. Constraint (6) is stated with the paper's $j$ written $j + 1$ . The MC policy is defined literally by (21)–(23), for every $j \in \mathbb N$ , as one recursion that interleaves $l_j(t)$ and $r_j(t)$ ; the run starts from a given state $(I(0), r(0))$ at period $0$ and applies the policy from period $1$ on. All values are real.

The standing assumptions of p. 95 ( $\alpha \ge 0$ , $0 \le \omega \le 1$ ) are hypotheses. Three hypotheses are added to the page's statement and disclosed in each item:

$f_j(t) \ge 0$ , implicit in the paper ("all quantities are measured in end-item equivalents") and used by its proof;
the start $r(0) = f(0)$ : the paper names no initial schedule, and with a large $r_1(0)$ the conclusion fails at $t = 1$ ;
$\omega^{in}_q < 1$ in the equal-flexibility part only: the paper's proof divides by $1 - \Omega^{in}_j$ , and with $\omega = 1$ allowed the part is false.

A formalization in which the run sets $r(t) := f(t)$ , or in which the MC step drops the carried-over term in (21) or the positive part in (23), would make the goal trivial; the model rules this out by defining the policy exactly as printed. Condition (d) compares the cumulative profiles, not the parameters termwise. Formula (33) and Propositions 1, 3 and 4 are not part of this mission; Proposition 1 (optimality of MC for the open-loop program) is the companion mission.

Contributions welcome: proofs of the milestones, a proof of the goal through an invariant on $(1 - \Omega^{in}_j)\, r_j(t)$ , and lemmas about the MC run reusable for the companion mission.

Selected references

A. A. Tsay and W. S. Lovejoy, Quantity Flexibility Contracts and Supply Chain Performance, Manufacturing & Service Operations Management 1(2):89–111, 1999. https://doi.org/10.1287/msom.1.2.89
A. A. Tsay, The Quantity Flexibility Contract and Supplier–Customer Incentives, Management Science 45(10):1339–1358, 1999. https://doi.org/10.1287/mnsc.45.10.1339
H. L. Lee, V. Padmanabhan and S. Whang, Information Distortion in a Supply Chain: The Bullwhip Effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546

6 thms3 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

The Quantity Flexibility Contract and Supplier-Customer Incentives II: With a Perfect Demand Signal the Transfer Price c̄(ψ) Makes the Quantity Flexibility Contract System-EfficientResearch Paper

Motivation

A manufacturer must commit to production before its retail customer knows what the market will demand, while the customer would rather postpone its purchase until better information arrives. Left uncoordinated, each firm protects itself: the customer inflates forecasts it is not bound by, and the manufacturer, discounting those forecasts, builds less than the supply chain as a whole should. Quantity flexibility (QF) contracts, used in practice in the electronics and computer industries (Sun Microsystems, Solectron, Nippon Otis and others are cited in the paper), address this by tying the customer's forecast to a band: the manufacturer guarantees supply up to a percentage above the forecast, and the customer promises to buy at least a percentage below it.

Tsay (1999) gives a two-stage model of such a contract with a demand signal that arrives between production and purchase, shows that a supply chain without commitment underproduces, and characterizes when a QF contract restores efficiency. This mission formalizes the efficiency result for the case in which the signal predicts demand perfectly (Proposition 6(a)), together with the steps of the equilibrium that it rests on.

Setting

A manufacturer (EM) produces at unit cost $m$ and sells to a retailer at unit transfer price $c$ ; the retailer sells at price $p$ , unsold units are salvaged at $u$ at either site, and each unit of unmet demand costs a goodwill loss $s$ . The standing assumptions are $p > m > 0$ , $u < m$ and $s \ge 0$ .

Before production, the retailer states a forecast $q \ge 0$ . A QF contract $\{c,(\alpha,\omega)\}$ with $\omega\in[0,1]$ and $\alpha\ge-\omega$ obliges the EM to make up to $q(1+\alpha)$ available and the retailer to buy at least $q(1-\omega)$ . The EM then builds $Q$ . A demand signal $\mu$ with distribution function $\Theta$ is observed, the retailer buys $r$ , and market demand is filled from the retailer's stock. In this mission the signal is perfect ( $\sigma_\varepsilon = 0$ ): market demand equals $\mu$ , so its distribution $F$ equals $\Theta$ .

Given $\mu$ , the retailer's profit from buying $r$ is

G(r\mid\mu) = p\min[\mu,r] - c\,r - s[\mu-r]^+ + u[r-\mu]^+,

and it buys $r^*_{QF} = \mu\perp[q(1-\omega),Q]$ , the point of the interval closest to $\mu$ . The EM's expected profit (2) is $\pi_{EM,QF}(Q;q) = (c-u)E_\mu\{r^*_{QF}\} - (m-u)Q$ . The retailer's forecast problem maximizes $\pi_{R,QF}(q) = E_\mu\{G(r^*_{QF}\mid\mu)\}$ with the EM building $q(1+\alpha)$ . A central planner earns $\Pi_{CC}(Q) = E_\mu\{p\min[\mu,Q]-s[\mu-Q]^+ + u[Q-\mu]^+\} - mQ$ , maximized at

Q^*_{CC} = F^{-1}\!\left(\frac{p+s-m}{p+s-u}\right).

The total flexibility of the contract is $\psi = (1+\alpha)/(1-\omega)$ .

Formalization targets

Goal: Proposition 6(a)

With $\sigma_\varepsilon = 0$ , the QF contract with flexibility $\psi$ and transfer price

\bar c(\psi) = u + \frac{m-u}{\dfrac1\psi F\!\left(\dfrac1\psi F^{-1}\!\left(\dfrac{p+s-m}{p+s-u}\right)\right) + \dfrac{m-u}{p+s-u}} \tag{4}

is system-efficient: the retailer's unique optimal forecast is $\hat q = Q^*_{CC}/(1+\alpha)$ , the EM's unique optimal production given $\hat q$ is $\hat q(1+\alpha) = Q^*_{CC}$ , and the resulting expected system profit equals $\max_Q \Pi_{CC}(Q)$ .

Milestones

§4: $Q^*_{CC}$ exists and is the unique maximizer of $\Pi_{CC}$ .
§6.1: given $\mu$ , the retailer's unique optimal purchase in $[a,b]$ is $\mu\perp[a,b]$ .
Proposition 3(a): for $\omega<1$ , the optimal forecast $q^*_{QF}$ is strictly positive, finite, and the unique solution of the first-order condition (3).
§7: for any forecast $q\ge0$ , expected system profit equals $\Pi_{CC}(q(1+\alpha))$ ; hence it is maximal when the production level $q(1+\alpha)$ matches $Q^*_{CC}$ .

Significance

The result shows that one contract form, by choosing the transfer price as a function of the flexibility, yields a whole menu of contracts each of which coordinates the supply chain, so that the two firms can trade price against flexibility without losing system profit. Its corollaries in the paper, that any split of expected profit is achievable by some efficient contract and that more flexibility shifts profit to the manufacturer, rest on (4).

The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development supplies them, makes explicit the regularity the argument needs (finite variance, a continuous and strictly increasing $\Theta$ , a positive efficient quantity), and gives reusable statements about newsvendor objectives with a clipped purchase. To our knowledge none of these results has been formalized before; the platform's quantity-flexibility theorems in other models (no manufacturer production stage, $\alpha = 0$ , retailer side only) do not cover them.

Difficulty

Each firm optimizes its own objective, and the efficient price must work for both at once. Making the retailer's first-order condition hold at $\hat q$ pins down $c$ , so nothing is left to adjust for the EM, whose incentive to build more than the contracted $q(1+\alpha)$ has to be ruled out separately at that same price. The retailer's objective is an expectation of a non-smooth function of a clipped purchase, so its derivative must be computed through the distribution of $\mu$ on two moving thresholds $q(1+\alpha)$ and $q(1-\omega)$ , and strict concavity must come from the strict increase of $\Theta$ rather than from a density.

Formalization scope

All objects live in the namespace TsayQF.EffQF. The law of $\mu$ is a probability measure $\nu$ on $\mathbb R$ with $\mu\in L^2(\nu)$ , whose distribution function cdf ν is differentiable and strictly increasing on $\mathbb R$ (the paper's "differentiable and invertible"). Expectations are Bochner integrals; finite variance makes every integrand integrable. Inverse distribution functions are not used: $Q^*_{CC}$ enters as a real number with the hypothesis $F(Q^*_{CC}) = \kappa_S$ , which determines it uniquely, and (4) is defined in its printed shape. Optimality is IsMaxOn over the decision's natural set: forecasts in $[0,\infty)$ , the EM's production in $[q(1+\alpha),\infty)$ , purchases in $[q(1-\omega),Q]$ , central production in $\mathbb R$ .

Hypotheses made explicit: $Q^*_{CC} > 0$ in the goal and a positive marginal value of the forecast at $q=0$ in Proposition 3(a), both standing for the paper's presumption that demand is almost certainly nonnegative; $\omega<1$ (Proposition 3's case). The transfer price is only required to satisfy $u<c<p+s$ rather than $m<c<p$ , because $\bar c(\psi)$ can exceed $p$ when $s>0$ . The milestones are the $\sigma_\varepsilon = 0$ instances of the paper's general statements.

Two modelling choices are fixed. The retailer's forecast objective takes the EM's production to be $q(1+\alpha)$ , as §6.1 does after Proposition 2; the full game in which the retailer anticipates other EM responses is not modelled, and the goal instead verifies that the EM's unique best response at $\bar c(\psi)$ is exactly $q(1+\alpha)$ . The efficient price is the explicit formula (4), not "a price that makes $Q^*_{CC}$ optimal", which would make the goal a tautology; likewise system efficiency is stated as an inequality against $\Pi_{CC}$ at every production level, not by definition.

Needed infrastructure: derivatives of expectations of piecewise-linear functions of a clipped variable, and the newsvendor fractile characterization. Both are reusable for other contract models. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives, Management Science 45(10):1339–1358, 1999. https://doi.org/10.1287/mnsc.45.10.1339
G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in OR & MS vol. 11, 2003, §6.2.5. https://doi.org/10.1016/S0927-0507(03)11006-7
L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, Wiley, 2nd ed. 2019, Ch. 14. https://doi.org/10.1002/9781119584445

6 thms3 active usersReviewed

Completed

Algebra Group Theory Theoretical Computer Science·Captain: mikedeng1

New Techniques for Noninteractive Zero-Knowledge 4: The Decisional-Linear Commitment Is Perfectly Binding and Extractable, with a Perfectly Sound, Witness-Indistinguishable 0/1 ProofResearch Paper

Motivation

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012) gave NIZK proofs for Circuit SAT of size $O(|C|k)$ for a circuit $C$ and security parameter $k$ , the first perfect NIZK arguments for all of NP, and the first non-interactive zaps based on a standard cryptographic assumption. These constructions use a single algebraic primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys, together with a short proof that a committed value is $0$ or $1$ .

The paper gives two instances of this primitive. One rests on the subgroup decision assumption in composite-order groups. The other, the subject of this mission, rests on the decisional linear assumption of Boneh, Boyen and Shacham (CRYPTO 2004) in prime-order bilinear groups. Prime-order groups are the setting of most later pairing-based proof systems, including the Groth–Sahai proofs (EUROCRYPT 2008), and their decisional-linear instantiation uses commitment keys of the same linear-tuple form as this mission.

Setting

A DLIN bilinear group is a tuple $(p, \mathbb G, \mathbb G_T, e, g)$ : $p$ is a prime, $\mathbb G$ and $\mathbb G_T$ are groups of order $p$ , $e : \mathbb G \times \mathbb G \to \mathbb G_T$ is bilinear ( $e(u^a, v^b) = e(u, v)^{ab}$ for all $u, v \in \mathbb G$ , $a, b \in \mathbb Z$ ), $g$ generates $\mathbb G$ , and $e(g, g)$ generates $\mathbb G_T$ . A triple $(f^r, h^s, g^{r+s})$ is a linear tuple with respect to $(f, h, g)$ .

The scheme (Figure 2 of the paper) works as follows.

Keys. Pick $x, y \in \mathbb Z_p^*$ , $r_u, s_v \in \mathbb Z_p$ , and put $f = g^x$ , $h = g^y$ . A perfectly binding key is $ck = (f, h, u, v, w) = (f, h, f^{r_u}, h^{s_v}, g^{r_u+s_v+z})$ with $z \in \mathbb Z_p^*$ ; its extraction key is $xk = (x, y, z)$ . A perfectly hiding key is $(f, h, f^{r_u}, h^{s_v}, g^{r_u+s_v})$ , a linear tuple; its trapdoor key is $tk = (r_u, s_v)$ .
Commitment. $\mathrm{com}(m; r, s) = (u^m f^r, v^m h^s, w^m g^{r+s}) \in \mathbb G^3$ for $m \in \mathbb Z_p$ , $(r, s) \in \mathbb Z_p^2$ .
Extraction and trapdoor opening. $\mathrm{Ext}_{xk}$ recovers a short $m$ from $c_3 c_1^{-1/x} c_2^{-1/y} = (g^z)^m$ . $\mathrm{Topen}_{tk}(m, (r, s), m') = (r - (m'-m)r_u,\ s - (m'-m)s_v)$ .
0/1 proof. On an opening $(m, r, s)$ with $m \in \{0, 1\}$ and randomness $t \in \mathbb Z_p$ , the prover $P_{01}$ outputs six group elements $\pi_{11}, \dots, \pi_{23}$ . The verifier $V_{01}$ checks six pairing-product equations in $\mathbb G_T$ .

The perfect properties of Section 3 are: homomorphism, perfect binding, perfect extractability, perfect trapdoor opening and its indistinguishability, perfect completeness, perfect soundness, perfect witness indistinguishability (WI), and perfect non-erasure WI. Non-erasure WI asks that a simulator turn the randomness of a proof made with one witness into randomness that explains the same proof under the other witness.

Formalization targets

Goal: Theorem 4, exact part

For every DLIN bilinear group, the scheme of Figure 2 is homomorphic on both kinds of key and perfectly binding and extractable on binding keys. On hiding keys it has perfect trapdoor opening and perfect trapdoor-opening indistinguishability. Its 0/1 proof is perfectly complete on both kinds of key, perfectly sound on binding keys, and perfectly WI and perfectly non-erasure WI on hiding keys. Soundness, for example, reads

V_{01}(ck, c, \pi) \text{ accepts} \implies \exists\, m \in \{0,1\},\ r, s \in \mathbb Z_p:\ c = \mathrm{com}(m; r, s).

Milestones

The milestones follow the paper's proof:

the homomorphism display (p. 11);
the trapdoor-opening identity and the extraction display (Figure 2);
the unique opening $(m, r, s)$ of every $c \in \mathbb G^3$ on a binding key;
completeness;
the six exponent equations obtained from an accepted proof;
the product identity $(r_0+s_0-t_0)(r_1+s_1-t_1) = 0$ ;
"c or $c \cdot \mathrm{com}(-1; 0, 0)$ is a commitment to 0";
the identity $P_{01}(ck, 0, (r_0, s_0); t) = P_{01}(ck, 1, (r_1, s_1); t + r_0 s_1 - s_0 r_1)$ on hiding keys.

Significance

The perfect properties are what the paper's later results consume. Perfect soundness and extractability on binding keys give the perfectly sound NIZK proof of knowledge for Circuit SAT (Theorem 6). Perfect WI, trapdoor opening and non-erasure WI on hiding keys give perfect zero-knowledge (Lemma 8 and Theorem 11) and the adaptive and UC-secure variants of Sections 7 and 8. Theorem 4 transfers all of this to prime-order bilinear groups under the decisional linear assumption.

The theorem is published and its proof is short, but the printed construction contains an error. With the signs of $t$ in $\pi_{12}$ and $\pi_{21}$ as printed in Figure 2, an honest proof fails the fourth and sixth verification equations whenever $2t \ne 0$ . A machine-checked proof fixes the corrected construction, under which the paper's own witness-indistinguishability argument goes through. No formalization of this scheme, or of the decisional linear setting, exists on the platform or in Mathlib.

Difficulty

The algebra is modest. The work lies in carrying exponents in $\mathbb Z_p$ through powers in groups of order $p$ , and in getting the soundness argument right. An accepted proof only constrains discrete logarithms of the proof elements, so the six pairing equations must first be turned into six equations between exponents. That step is valid only because $f$ , $h$ and $e(g, g)$ are nondegenerate. Soundness then needs the observation that the product of two specific linear forms vanishes, and it fails outright on a hiding key ( $z = 0$ ). Witness indistinguishability is an exact identity between proofs, which holds only for the corrected prover.

Formalization scope

Groups. $\mathbb G$ and $\mathbb G_T$ are finite commutative groups of cardinality $p$ , $p$ prime. The pairing is a monoid homomorphism G →* G →* GT, which is equivalent to bilinearity. $g$ generates $\mathbb G$ and $e(g, g)$ generates $\mathbb G_T$ .
Exponents. Exponents are elements of ZMod p, acting through their representative in $\{0, \dots, p-1\}$ .
Keys. The key generators are represented by their supports. A binding key requires $x, y, z \ne 0$ and a hiding key requires $x, y \ne 0$ . Without $z \ne 0$ a "binding" key is hiding and soundness is false. Without $x, y \ne 0$ the verification equations degenerate.
Prover. $P_{01}$ is the corrected prover; the erratum is recorded on every item it affects.
Probabilities. "For all adversaries, probability 1" is stated for every key in the support and every adversarial choice. "Equal probabilities for all adversaries" is stated as equality of probability mass functions over the uniform proof randomness. For perfect properties both readings are equivalent.
Dropped. The computational content is out of scope: the efficiency of the algorithms, key indistinguishability, and the decisional linear assumption itself (Definition 3).
Simulator. The non-erasure simulator is the explicit map $t \mapsto t + r_0 s_1 - s_0 r_1$ that the proof constructs, so the statement cannot be met by an arbitrary unbounded function.
No trivial readings. A trivializing formalization is ruled out. The verifier's equations are not vacuous ( $e(g, g) \ne 1$ , $f, h \ne 1$ ), binding keys have $z \ne 0$ , and the definitions are instantiated on a concrete group of order 5 in a local check: the corrected proof is accepted there and the printed one is rejected.
Contributions. Contributions welcome: proofs of the milestones, and a reusable development of discrete logarithms in groups of prime order.

Selected references

J. Groth, R. Ostrovsky, A. Sahai, New Techniques for Noninteractive Zero-Knowledge, Journal of the ACM 59(3), Article 11, 2012. https://doi.org/10.1145/2220357.2220358
D. Boneh, X. Boyen, H. Shacham, Short Group Signatures, CRYPTO 2004, LNCS 3152. https://doi.org/10.1007/978-3-540-28628-8_3
J. Groth, A. Sahai, Efficient Non-interactive Proof Systems for Bilinear Groups, EUROCRYPT 2008, LNCS 4965. https://doi.org/10.1007/978-3-540-78967-3_24
D. Boneh, E.-J. Goh, K. Nissim, Evaluating 2-DNF Formulas on Ciphertexts, TCC 2005, LNCS 3378. https://doi.org/10.1007/978-3-540-30576-7_18

13 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

A Single-Item Inventory Model for a Nonstationary Demand Process: With Adaptive Base-Stock Control at Two Stages, Upstream Inventory Is N(y₀, σ²∑_{i<K}(1+(L+i)α)²)Research Paper

Motivation

Classical safety-stock formulas assume that demand is stationary: independent and identically distributed around a fixed mean. Many products do not behave that way. Their demand level drifts, and the forecast has to follow it. Graves (A single-item inventory model for a nonstationary demand process, Manuf. Serv. Oper. Manag. 1(1):50–61, 1999) works out what such drift costs in inventory when it is modelled by the simplest nonstationary time series used in forecasting practice. The model is the integrated moving average process of order $(0,1,1)$ , for which the exponentially weighted moving average is the optimal forecast (Muth, 1960; Box, Jenkins and Reinsel, 1994).

The paper answers two questions. For one stage under an adaptive base-stock policy, it gives the exact distribution of the inventory, and hence the safety stock. For two stages in series, it shows that the order stream the downstream stage passes upstream is again of the same type, amplified. This is an explicit instance of the bullwhip effect of Lee, Padmanabhan and Whang (1997). The paper then gives the distribution of the upstream inventory. That last distribution, equation (16), is the goal of this mission.

Setting

Time is indexed by periods $t\in\mathbb Z$ ; operation starts in period $1$ . Fix a mean level $\mu\in\mathbb R$ , a parameter $\alpha$ with $0\le\alpha\le1$ , a downstream lead time $L\in\mathbb N$ and an upstream lead time $K\in\mathbb N$ . The shocks $\varepsilon_1,\varepsilon_2,\dots$ are independent random variables, each normal with mean $0$ and variance $\sigma^2$ .

Downstream stage (§2). The demand $d_t$ is the IMA(0,1,1) process

d_1=\mu+\varepsilon_1,\qquad d_t=d_{t-1}-(1-\alpha)\varepsilon_{t-1}+\varepsilon_t\quad(t\ge2).\tag{1}

The forecast $F_{t+1}$ , made after observing $d_t$ , is the exponentially weighted moving average

F_1=\mu,\qquad F_{t+1}=\alpha d_t+(1-\alpha)F_t\quad(t\ge1).\tag{3}

The order $q_t$ , placed in period $t$ and delivered in period $t+L$ , follows the adaptive base-stock policy

q_t=d_t+L(F_{t+1}-F_t)\quad(t\ge1),\qquad q_t=\mu\quad(t\le0).\tag{7}

The inventory $x_t$ at the end of period $t$ (negative values are backorders) obeys

x_t=x_{t-1}-d_t+q_{t-L}\quad(t\ge1),\tag{6}

where $x_0$ is an initial inventory chosen by the planner. Orders may be negative.

Upstream stage (§3). It sees the orders $q_t$ as its demand. It forecasts them with smoothing constant $\beta=\alpha/(1+L\alpha)$ ,

G_1=\mu,\qquad G_{t+1}=\beta q_t+(1-\beta)G_t\quad(t\ge1),\tag{11}

orders $p_t=q_t+K(G_{t+1}-G_t)$ for $t\ge1$ and $p_t=\mu$ for $t\le0$ (15), and holds inventory

y_t=y_{t-1}-q_t+p_{t-K}\quad(t\ge1),\tag{14}

with initial inventory $y_0$ .

In Lean, IsStage μ α L ε d F q x is the conjunction of (1), (3), (6), (7) and the boundary condition. IsUpstream μ β K q G p y is (11), (14), (15) and its boundary condition. upBeta α L is $\beta$ , and IsTwoStage is the conjunction of the two stages.

Formalization targets

Goal: the upstream inventory distribution (16)

For every period $t\ge K$ (and $t\ge1$ ), the upstream inventory $y_t$ is normally distributed with

\mathbb E[y_t]=y_0,\qquad \operatorname{Std}[y_t]=\sigma\sqrt{\sum_{i=0}^{K-1}\bigl(1+(L+i)\alpha\bigr)^2}.

Milestones, in the paper's order

The closed form of demand (2): $d_t=\varepsilon_t+\alpha\sum_{j<t}\varepsilon_j+\mu$ .
The forecast error (4): $d_t-F_t=\varepsilon_t$ .
The forecast update (5): $F_{t+1}=F_t+\alpha\varepsilon_t=\alpha\sum_{j\le t}\varepsilon_j+\mu$ .
The lead-time form of the inventory (proof of P1): $x_t=x_0-\sum_{j=t+1-L}^{t}d_j+LF_{t+1-L}$ for $t\ge L$ .
Property P1: $x_t=x_0-\sum_{i=0}^{L-1}\varepsilon_{t-i}(1+i\alpha)$ , with $\varepsilon_t=0$ for $t\le0$ .
The downstream inventory distribution (8): $x_t\sim N\bigl(x_0,\ \sigma^2\sum_{i<L}(1+i\alpha)^2\bigr)$ for $t\ge L$ , and $\sum_{i<L}(1+i\alpha)^2=L\bigl(1+\alpha(L-1)+\alpha^2(L-1)(2L-1)/6\bigr)$ .
The orders in closed form (9): $q_t=(1+L\alpha)\varepsilon_t+\alpha\sum_{j<t}\varepsilon_j+\mu$ .
The orders are IMA(0,1,1) (10), with shocks $\zeta_t=(1+L\alpha)\varepsilon_t$ and parameter $\beta$ , and $0\le\beta\le\alpha$ .
The upstream forecast equals the downstream one: $q_t=G_t+\zeta_t$ , $q_t=F_t+(1+L\alpha)\varepsilon_t$ , $G_t=F_t$ .
Property P2: $y_t=y_0-\sum_{i=0}^{K-1}\varepsilon_{t-i}\bigl(1+(L+i)\alpha\bigr)$ , with $\varepsilon_t=0$ for $t\le0$ .

Two further statements of the paper are included as plain theorems: the order amplification $\operatorname{Std}[q_t\mid F_t]=(1+L\alpha)\sigma=(1+L\alpha)\operatorname{Std}[d_t\mid F_t]$ (p. 55), stated as: $q_t-F_t$ and $d_t-F_t$ are independent of $F_t$ with laws $N(0,(1+L\alpha)^2\sigma^2)$ and $N(0,\sigma^2)$ , and the critical-fractile rule (p. 54). Under that rule, setting $x_0=z\,\operatorname{Std}[x_t]$ gives $P(x_t\ge0)=\Phi(z)$ .

Significance

Equation (8) is a closed-form safety-stock formula for nonstationary demand. For $\alpha>0$ the standard deviation of the inventory grows faster than $\sqrt L$ , so the textbook square-root law understates the safety stock. Equation (16) carries the formula one stage up a supply chain. With $\alpha>0$ , the upstream safety stock depends on the downstream lead time $L$ , not only on the upstream lead time $K$ . The paper concludes that shortening the downstream lead time can matter more than shortening the upstream one. P1 and P2 underlie these conclusions: they write each inventory as a fixed linear combination of a bounded window of shocks.

All results here are proved in the paper. None of them, and none of the model's objects, is formalized on Prove2Me or, as far as is known, anywhere else. The mission produces machine-checked versions of the closed forms and distributions. It also produces a reusable statement that a finite linear combination of independent Gaussian shocks is Gaussian, which Mathlib has only for two summands.

Difficulty

The pathwise milestones are inductions on the period, but they are not uniform. The inventory recursion (6) reads orders $L$ periods back, so P1 has two regimes: $t\ge L$ , where every order read is a policy order, and $1\le t<L$ , where some are the boundary orders $q_s=\mu$ . The paper treats the second regime only by "direct substitution", and a single statement has to cover both.

P2 is not a second copy of P1. The upstream stage is defined by its own recursions (11), (14), (15). It becomes an instance of the single-stage model only after (10) and the forecast identity $G_t=F_t$ have been proved, and P1 must then be applied with parameter $\beta$ and shocks $\zeta_t$ . The distributional statements (8) and (16) need the law of a finite weighted sum of independent normal variables. Mathlib provides the two-variable case; the finite-sum version, with a $\mathbb Z$ -indexed window of shocks, has to be built from it.

Formalization scope

All sequences are functions $\mathbb Z\to\mathbb R$ ; lead times are natural numbers, cast to $\mathbb Z$ in indices and to $\mathbb R$ in coefficients, so no truncated subtraction occurs. The model is a predicate on sequences, and the objects $d,F,q,x,G,p,y$ are constrained only by the paper's recursions (1), (3), (6), (7), (11), (14), (15) and the boundary conditions $q_t=p_t=\mu$ for $t\le0$ . None of the closed forms (2), (5), (9), (10), P1 or P2 is built into a definition. In particular the upstream stage is not defined as an instance of the downstream one, which would assume (10). The paper's convention $\varepsilon_t=0$ for $t\le0$ is implemented by a masked sequence masked ε in P1 and P2, not by a hypothesis. The standing assumption $0\le\alpha\le1$ is a hypothesis of every theorem.

In (8) and (16) the shocks live on a probability space $(\Omega,P)$ . They are measurable and mutually independent over periods $t\ge1$ (iIndepFun over $\{s:\mathbb Z\mid 1\le s\}$ ), each with law gaussianReal 0 (σ²). The system equations hold for every outcome, and the initial inventory is a constant. "Normally distributed with mean $m$ and standard deviation $s$ " is the law equality P.map (y t) = gaussianReal m (s²). A statement only about the variance would be weaker than the paper's claim and does not count. The critical-fractile theorem adds $\sigma>0$ and $L\ge1$ ; without them the inventory is constant and the claim fails.

Contributions are welcome on the finite Gaussian-sum lemma, which is independent of this paper, and on any milestone in any order.

Selected references

S. C. Graves, A single-item inventory model for a nonstationary demand process, Manufacturing & Service Operations Management 1(1):50–61, 1999. https://doi.org/10.1287/msom.1.1.50
J. F. Muth, Optimal properties of exponentially weighted forecasts, Journal of the American Statistical Association 55(290):299–306, 1960. https://doi.org/10.1080/01621459.1960.10482056
G. E. P. Box, G. M. Jenkins, G. C. Reinsel, Time Series Analysis: Forecasting and Control, 3rd ed., Prentice Hall, 1994 (book; no DOI for this edition).
H. L. Lee, V. Padmanabhan, S. Whang, Information distortion in a supply chain: the bullwhip effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546

12 thms3 active usersReviewed

Completed

Group Theory Number Theory Theoretical Computer Science·Captain: mikedeng1

New Techniques for Noninteractive Zero-Knowledge 3: The Subgroup-Decision (BGN) Commitment Is Perfectly Binding and Extractable, with a Perfectly Sound, Witness-Indistinguishable 0/1 ProofResearch Paper

Motivation

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. NIZK proofs are a basic building block of public-key cryptography: chosen-ciphertext secure encryption, signature schemes and secure multi-party computation all use them. Groth, Ostrovsky and Sahai, New Techniques for Noninteractive Zero-Knowledge (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006), built the first NIZK proofs for all of NP that are perfectly sound and the first NIZK arguments that are perfectly zero-knowledge, using bilinear groups.

The construction rests on a single primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys (perfectly binding and perfectly hiding) together with a short non-interactive proof that a commitment contains $0$ or $1$ . Section 4 of the paper instantiates this primitive in a bilinear group of composite order $n = pq$ , building on the encryption scheme of Boneh, Goh and Nissim (TCC 2005); Section 5 gives a second instantiation in prime-order groups. Theorem 2 states that the composite-order scheme of Figure 1 has all the required properties. This mission formalizes the part of Theorem 2 that is an exact mathematical statement.

Timeline: Boneh, Goh and Nissim (2005) introduced the subgroup decision assumption and the encryption $g^m h^r$ in groups of order $pq$ . Groth, Ostrovsky and Sahai (Eurocrypt 2006) used it for perfect NIZK; the simple 0/1 proof $\pi = (g^{2m-1}h^r)^r$ used in Figure 1 is due to an observation of Boyen and Waters (Eurocrypt 2006), as the paper's footnote 7 records. The journal version (2012) presents both instantiations through the abstract notion of a homomorphic proof commitment.

Setting

A BGN bilinear group is a tuple $(p, q, \mathbb G, \mathbb G_T, e, g)$ where $p < q$ are primes, $\mathbb G$ and $\mathbb G_T$ are finite commutative groups of order $n = pq$ , $e : \mathbb G \times \mathbb G \to \mathbb G_T$ is bilinear ( $e(u^a, v^b) = e(u, v)^{ab}$ for all $u, v \in \mathbb G$ , $a, b \in \mathbb Z$ ), $g$ generates $\mathbb G$ , and $e(g, g)$ generates $\mathbb G_T$ .

The commitment key is $ck = (n, \mathbb G, \mathbb G_T, e, g, h)$ for an element $h \in \mathbb G$ of one of two kinds:

a perfectly binding key has $h = g^{px}$ with $x$ a unit modulo $q$ , so $h$ has order $q$ ; the extraction key is $q$ ;
a perfectly hiding key has $h = g^x$ with $x$ a unit modulo $n$ , so $h$ generates $\mathbb G$ ; the trapdoor is $x$ .

The commitment to a message $m$ with randomizer $r \in \mathbb Z_n$ is $\mathrm{com}(m; r) = g^m h^r$ . The trapdoor opening is $\mathrm{Topen}_x(m, r, m') = r - (m'-m)/x \bmod n$ . The 0/1 proof for a commitment $c = g^m h^r$ is $\pi = P_{01}(m, r) = (g^{2m-1} h^r)^r$ , and the verifier $V_{01}$ accepts $(c, \pi)$ when $e(c, cg^{-1}) = e(h, \pi)$ . The extractor $\mathrm{Ext}$ computes $c^q$ and searches for $m$ with $c^q = (g^q)^m$ .

Formalization targets

Goal: the exact part of Theorem 2

For every BGN bilinear group, the scheme above satisfies:

\begin{aligned} &\text{(homomorphic, either key)} && \mathrm{com}(m_1+m_2; r_1+r_2) = \mathrm{com}(m_1; r_1)\,\mathrm{com}(m_2; r_2),\\ &\text{(perfect binding)} && \mathrm{com}(m_1; r_1) = \mathrm{com}(m_2; r_2) \Rightarrow m_1 \equiv m_2 \pmod p,\\ &\text{(trapdoor opening)} && \mathrm{com}(m_2; \mathrm{Topen}_x(m_1, r_1, m_2)) = \mathrm{com}(m_1; r_1),\\ &\text{(opening indistinguishability)} && r_1 \text{ uniform} \Rightarrow \mathrm{Topen}_x(m_1, r_1, m_2) \text{ uniform},\\ &\text{(completeness, either key)} && m \in \{0,1\} \Rightarrow V_{01}(\mathrm{com}(m; r), P_{01}(m, r)),\\ &\text{(soundness)} && V_{01}(c, \pi) \Rightarrow \exists\, m \in \{0,1\}, r : c = \mathrm{com}(m; r),\\ &\text{(witness indistinguishability)} && \mathrm{com}(m; r_0) = \mathrm{com}(1-m; r_1) \Rightarrow P_{01}(m, r_0) = P_{01}(1-m, r_1),\\ &\text{(extractability)} && m \in \{0,1\} \Rightarrow \mathrm{Ext}(\mathrm{com}(m; r)) = m, \end{aligned}

with binding, soundness and extractability on binding keys, and trapdoor opening and witness indistinguishability on hiding keys.

Milestones

The milestones follow the proof of Theorem 2 (p. 9) and Figure 1 (p. 10): the homomorphic property; perfect binding; the extraction identity $c^q = (g^q)^m$ ; the trapdoor identity $g^m h^r = g^{m'} h^{r-(m'-m)/x}$ and the uniqueness of openings on a hiding key; the completeness display $e(c, cg^{-1}) = e(g,g)^{m(m-1)} e(h^r, g^{2m-1}h^r) = e(h, \pi)$ ; the decomposition of every element as $g^m h^r$ on a binding key; the step " $e(g,g)^{m(m-1)}$ of order $1$ or $q$ implies $m \equiv 0$ or $1 \pmod p$ "; perfect soundness; and the uniqueness of the proof on a hiding key, which gives witness indistinguishability.

Significance

Theorem 2 is one of the two instantiations on which every exact result of the paper rests. Plugged into the Circuit-SAT construction of Section 6, the binding-key properties give a perfectly sound NIZK proof and a perfect proof of knowledge for every NP relation, and the hiding-key properties give a perfect zero-knowledge NIZK argument. The same composite-order techniques underlie later pairing-based proof systems, notably the Groth–Sahai proofs.

The paper's proof is about one page of group computations and has, as far as the planning of this series found, no machine-checked counterpart. The mission produces a reusable model of composite-order bilinear groups and of the BGN commitment, and checks details the paper leaves implicit: the message space $\mathbb Z_p$ versus exponents taken modulo $n$ , the role of the non-degeneracy of $e$ , and the order arguments behind soundness.

Difficulty

Each property is elementary on its own, but soundness is not a plain computation: the verifier only sees $c$ and $\pi$ , and the conclusion asks for an opening of $c$ with message in $\{0, 1\}$ from a single pairing equation. An argument that only manipulates the equation symbolically cannot reach it; the statement depends on the orders of elements in $\mathbb G_T$ , on $e(g,g)$ generating $\mathbb G_T$ (with a degenerate pairing soundness is false), and on $p$ and $q$ being distinct primes. A second subtlety is that a message is only determined modulo $p$ by a commitment under a binding key, while the conclusion asks for a message that is exactly $0$ or $1$ in $\mathbb Z_n$ .

Formalization scope

$\mathbb G$ , $\mathbb G_T$ are finite commutative groups with Fintype.card = p * q; $e$ is a homomorphism G →* G →* GT, which is exactly bilinearity; $g$ generates $\mathbb G$ and $e(g,g)$ generates $\mathbb G_T$ (both as hypotheses of the structure BGNSetup).
Messages and randomizers are elements of ZMod n; $g^a$ is $g$ to the representative of $a$ in $\{0, \dots, n-1\}$ . The paper's message space is $\mathbb Z_p$ , but $g^m$ is not well defined for $m \in \mathbb Z_p$ in a group of order $pq$ ; binding and extraction therefore compare messages modulo $p$ .
Keys are described by the support of the key generators; each "probability $1$ for every adversary" property is stated for every key in that support and every adversary choice. Trapdoor opening indistinguishability is an equality of probability mass functions. The prover is deterministic, so witness indistinguishability is equality of proofs, and non-erasure witness indistinguishability holds with the empty proof randomness.
Not formalized: the subgroup decision assumption (Definition 1), key indistinguishability, the clause "if the subgroup decision assumption holds", the randomized generator $\mathcal G_{\mathrm{BGN}}$ and its efficiency, and the elliptic-curve example on p. 9.
A trivializing formalization is ruled out: soundness is stated only for binding keys $h = g^{px}$ with $x$ a unit modulo $q$ , with the non-degeneracy of $e$ as a hypothesis, and the extractor is an exhaustive search over $\mathbb Z_p$ , not a test that presupposes $m \in \{0,1\}$ .
The model of composite-order bilinear groups is reusable for other BGN-based results. Proofs of any milestone are welcome; the trapdoor and homomorphism identities are good first targets.

Selected references

J. Groth, R. Ostrovsky, A. Sahai, New Techniques for Noninteractive Zero-Knowledge, Journal of the ACM 59(3), Article 11, 2012. https://doi.org/10.1145/2220357.2220358
D. Boneh, E.-J. Goh, K. Nissim, Evaluating 2-DNF Formulas on Ciphertexts, TCC 2005, LNCS 3378, pp. 325–341. https://doi.org/10.1007/978-3-540-30576-7_18
X. Boyen, B. Waters, Compact Group Signatures Without Random Oracles, Eurocrypt 2006, LNCS 4004, pp. 427–444. https://doi.org/10.1007/11761679_26
T. P. Pedersen, Non-Interactive and Information-Theoretic Secure Verifiable Secret Sharing, Crypto 1991, LNCS 576, pp. 129–140. https://doi.org/10.1007/3-540-46766-1_9
J. Groth, A. Sahai, Efficient Non-interactive Proof Systems for Bilinear Groups, Eurocrypt 2008, LNCS 4965, pp. 415–432. https://doi.org/10.1007/978-3-540-78967-3_24

13 thms3 active usersReviewed

Bandit Algorithms Machine Learning Probability+1·Captain: mikedeng1

Thompson Sampling: An Asymptotically Optimal Finite-Time Analysis: Bernoulli Thompson Sampling Has Regret (1+ε)Σ Δ_a(ln T + ln ln T)/K(μ_a, μ*) + CResearch Paper

Motivation

Thompson Sampling is the oldest bandit algorithm: Thompson proposed it in 1933 for allocating patients between two treatments (Thompson 1933). It keeps a posterior distribution over the unknown mean reward of every action, draws one sample from each posterior, and plays the action whose sample is largest. It is simple, widely used, and in experiments competitive with index policies designed for optimality. For decades it had no matching theoretical guarantee.

The benchmark for a stochastic bandit algorithm is the lower bound of Lai and Robbins (1985): every consistent policy draws a suboptimal arm $a$ at least $(1-o(1))\ln T/K(\mu_a,\mu^*)$ times in $T$ rounds, where $K$ is the Kullback–Leibler divergence. A policy that attains this rate is called asymptotically optimal.

Timeline.

1933: Thompson introduces the algorithm, without analysis.
1985: Lai and Robbins prove the lower bound and construct asymptotically optimal (but complex) policies.
2011–2012: KL-UCB (Garivier and Cappé 2011) and Bayes-UCB (Kaufmann, Cappé and Garivier 2012) attain the bound for Bernoulli rewards with simpler index rules.
2012: Agrawal and Goyal give the first logarithmic regret bound for Thompson Sampling, $O\big((\sum_a 1/\Delta_a^2)^2\ln T\big)$ , which does not have the optimal constant.
2012: Kaufmann, Korda and Munos (arXiv:1205.4217) prove that Thompson Sampling with uniform priors is asymptotically optimal for Bernoulli rewards, with a finite-time bound. This mission formalizes that result.

Setting

There are $K\ge2$ arms. Arm $a$ yields reward $1$ with probability $\mu_a\in(0,1)$ and $0$ otherwise. Arm $1$ is the unique optimal arm: $\mu^*=\mu_1>\mu_a$ for every $a\neq1$ . The gap of arm $a$ is $\Delta_a=\mu^*-\mu_a$ , and $\mu_2$ denotes the largest mean among the suboptimal arms.

Thompson Sampling with uniform priors. Let $N_{a,t}$ be the number of times arm $a$ has been drawn before round $t$ and $S_{a,t}$ the number of rewards equal to $1$ among those draws. With a uniform prior, the posterior of $\mu_a$ is $\mathrm{Beta}(S_{a,t}+1,\,N_{a,t}-S_{a,t}+1)$ . In round $t$ the algorithm draws, independently, a sample $\theta_{a,t}$ from each posterior, plays $A_t=\arg\max_a\theta_{a,t}$ , and observes the reward of $A_t$ .

The regret after $T$ rounds is

\mathcal R(T)=T\mu^*-\mathbb E\Big[\sum_{t=1}^T R_t\Big]=\sum_a\Delta_a\,\mathbb E[N_{a,T}],

where $N_{a,T}$ now counts the draws of $a$ in rounds $1,\dots,T$ . The Bernoulli divergence is $K(p,q)=p\ln\frac pq+(1-p)\ln\frac{1-p}{1-q}$ .

The analysis compares the Thompson samples with two index rules. For an arm with $S$ successes in $N$ draws, at round $t$ of a horizon $T$ , the KL-UCB index is $u=\sup\{x\in[S/N,1):N\,K(S/N,x)\le\ln t+\ln\ln T\}$ , and the Bayes-UCB index $q$ is the quantile of order $1-\frac1{t\ln T}$ of the posterior $\mathrm{Beta}(S+1,N-S+1)$ .

Formalization targets

Goal: Theorem 1 (p. 3)

For every $\epsilon>0$ there is a constant $C$ , depending on $\epsilon$ and the instance, such that for every horizon $T$ ,

\mathcal R(T)\le(1+\epsilon)\sum_{a:\,\mu_a\neq\mu^*}\frac{\Delta_a(\ln T+\ln\ln T)}{K(\mu_a,\mu^*)}+C.

Only the existence of $C$ is asserted; its value is not fixed, so improvements of the lower-order terms do not invalidate the goal.

Milestones

Eq. (1): $\mathcal R(T)=T\mu^*-\mathbb E[\sum_{t=1}^T R_t]=\sum_a\Delta_a\,\mathbb E[N_{a,T}]$ .
Theorem 2 (p. 4): for each suboptimal $a$ and $\epsilon>0$ , $\mathbb E[N_{a,T}]\le(1+\epsilon)\frac{\ln T+\ln\ln T}{K(\mu_a,\mu_1)}+C$ .
Proposition 1 (p. 4): there is $b\in(0,1)$ with $\sum_{t\ge1}\mathbb P(N_{1,t}\le t^b)<\infty$ .
Display (4) (p. 5): $\mathbb E[N_{a,T}]\le A+B+2$ , an under-estimation term $A$ for arm $1$ plus a KL-UCB term $B$ .
Lemma 1 (p. 5): $\sum_t\mathbb P\big(\theta_{1,t}\le\mu_1-\sqrt{6\ln t/N_{1,t}}\big)\le N_0(b)+3+C_b$ .
Lemma 2 (p. 6): $B\le(1+\epsilon)\frac{\ln T+\ln\ln T}{K(\mu_a,\mu_1)}+D$ for large $T$ .
Lemma 3 (p. 9), in its analytic form (§3.4): a bound on the probability that the optimal arm's samples stay below $\mu_2+\delta$ for $f$ rounds.
Lemma 4 (p. 9): saturated suboptimal arms rarely produce samples above $\mu_a+\delta_a$ .
§2 (p. 3): the Beta–Binomial identity (referenced) and the comparison $q<u$ of the two indices.

Significance

The result. Theorem 1 shows that the leading constant of Thompson Sampling's regret equals the Lai–Robbins constant, so no consistent policy does asymptotically better on Bernoulli bandits. It settled a question open since 1933 and is the starting point for later optimality proofs of Thompson Sampling for exponential families and Gaussian rewards. Proposition 1, a summable tail bound on the event that the optimal arm is under-sampled, is the reusable core: it is a deviation inequality for the number of draws of the optimal arm, which a bound on its expectation does not imply.

The formalization. The result is proved on paper; no machine-checked proof of an optimal-constant bound for Bernoulli Thompson Sampling exists. The platform already has the Gaussian frequentist analysis of Lattimore and Szepesvári (Theorem 36.3) and the non-optimal Agrawal–Goyal bound. This mission adds the Bernoulli, Beta-posterior case with the KL constant, the KL-UCB and Bayes-UCB indices with the $\ln t+\ln\ln T$ exploration rate, and the optimal-arm tail bound. Corrected statements are part of the output: the explicit constant $D$ printed at the end of Lemma 2's proof is too small, the constant $C_{\lambda,\mu_1,\mu_2}$ printed for Lemma 3 has the wrong sign, and Lemma 3 as printed quantifies over arbitrary random intervals, which its proof does not support.

Difficulty

The standard proof for an optimistic index policy bounds the draws of a suboptimal arm by an under-estimation term $\sum_t\mathbb P(l_{1,t}<\mu_1)$ and a concentration term. For Thompson Sampling the under-estimation term is not small: once the posterior of arm $1$ is concentrated, $\mathbb P(\theta_{1,t}<\mu_1)$ is close to $1/2$ in every round. Comparing $\theta_{1,t}$ with a lower confidence bound $\mu_1-\sqrt{6\ln t/N_{1,t}}$ instead only helps if $N_{1,t}$ is large with overwhelming probability, and a bound on $\mathbb E[N_{1,t}]$ does not give that.

Proposition 1 supplies it, and it carries most of the difficulty. It must control long stretches of rounds in which arm $1$ is never drawn while several suboptimal arms compete, and it needs the samples of arm $1$ conditioned on its successes at a random time while the arm is not played, an optional-skipping step that the paper leaves implicit and that is the main measure-theoretic obstacle in Lean.

Formalization scope

Representation. The algorithm is the published Thompson Sampling run (AgrawalGoyalTS_TwoArmed_ThompsonSampling) on the published Bernoulli bandit (bernoulliRelativeEntropy). That run is Agrawal–Goyal's Algorithm 2, which passes each reward through a Bernoulli trial of success probability equal to the reward; for $\{0,1\}$ rewards the trial returns the reward almost surely, so the posterior is exactly the paper's. Probabilities are values of tsLaw in $[0,\infty]$ , expectations of counts and the regret are lower integrals in $[0,\infty]$ , and every bound compares with the embedding of a real right-hand side.

Conventions.

Lean arm $0$ is the paper's arm $1$ . Lean round $t$ is the paper's round $t+1$ ; $N_{a,t}$ , $S_{a,t}$ are the counts when $\theta_{a,t}$ is drawn, and the paper's $\ln t$ is $\ln(t+1)$ at Lean round $t$ .
$\sqrt{6\ln t/N_{1,t}}=\infty$ when $N_{1,t}=0$ (p. 4), encoded by cases.
The KL-UCB supremum ranges over $x<1$ , because the real-valued divergence at $q=1$ is a finite junk value; $u=1$ when $N=0$ or $S=N$ , cases the page leaves undefined.
Every constant with a printed dependence list ( $C$ , $D$ , $N$ , $b$ , $C_b$ ) is chosen after the instance (and $\epsilon$ , the arm) and before $T$ .

Added hypotheses and corrections.

$0<\mu_a<1$ for every arm, and $K\ge2$ : not stated in the paper but used by its proof (it divides by $\mu_1(1-\mu_1)$ , and $K(\mu_a,1)=\infty$ ).
Arm $1$ is the unique optimal arm (the paper's standing assumption of §2; its reduction of several optimal arms to one is cited, not proved).
Display (4) and the index comparison are stated for $T\ge3$ (the page's $T\ge e$ ) and rounds $1\le t\le T$ .
Lemma 2 asserts only the existence of $D$ ; Lemma 3 is formalized as the analytic bound of §3.4 with the sign-corrected constant; Lemma 1's $C_b$ is read with the pre-draw count.

Trivializations ruled out. Thompson Sampling is not characterized by a predicate that an arbitrary policy could satisfy: it is the published run, which fixes the posterior draws, the argmax and the updates. The constant is quantified as $\forall\epsilon\,\exists C\,\forall T$ , never $\forall T\,\exists C$ , and no real number is extracted from a possibly infinite expectation.

Infrastructure and contributions. A complete development needs Beta–Binomial duality, Chernoff–Hoeffding bounds for binomial tails, optional skipping for the reward stacks of the played arms, and the KL-UCB counting argument. The Beta–Binomial identity is an open milestone shared with the Agrawal–Goyal mission. Proofs of any milestone, in particular Proposition 1, Lemma 4 and the analytic Lemma 3, are welcome; Lemma 3's bound and the index comparison are pure real analysis and reusable beyond bandits.

Selected references

E. Kaufmann, N. Korda, R. Munos, Thompson Sampling: An Asymptotically Optimal Finite Time Analysis, ALT 2012 (LNCS 7568); arXiv:1205.4217v2. https://arxiv.org/abs/1205.4217
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25, 1933. https://doi.org/10.2307/2332286
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
S. Agrawal, N. Goyal, Analysis of Thompson Sampling for the multi-armed bandit problem, COLT 2012; arXiv:1111.1797. https://arxiv.org/abs/1111.1797
A. Garivier, O. Cappé, The KL-UCB algorithm for bounded stochastic bandits and beyond, COLT 2011; arXiv:1102.2490. https://arxiv.org/abs/1102.2490
E. Kaufmann, O. Cappé, A. Garivier, On Bayesian upper confidence bounds for bandit problems, AISTATS 2012. https://proceedings.mlr.press/v22/kaufmann12.html

17 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

A Note on Probability Distributions with Increasing Generalized Failure Rates II: For IGFR X with Support (α, ∞) and g(ξ) → κ, E[Xⁿ] Is Finite iff κ > nResearch Paper

Motivation

Many models in operations management and economics need the demand or valuation distribution to be regular in some way, so that an optimal price, order quantity or contract is unique. Pricing a service to one customer whose valuation $X$ has survival function $\bar\Phi$ is a typical example. The seller maximizes $p\,\bar\Phi(p)$ . The first-order condition is $\bar\Phi(p)(1-g(p))=0$ , where $g(\xi)=\xi h(\xi)$ is the generalized failure rate and $h$ is the ordinary failure rate. When $g$ is increasing (the IGFR property, introduced by Lariviere and Porteus 2001), the optimal price is unique and solves $g(p^*)=1$ .

The best-known regularity class is the class of IFR laws, those with increasing failure rate. Every IFR law has finite moments of all orders (Barlow and Proschan 1965). IGFR laws are a larger class that includes heavy-tailed laws, and Lariviere (2006) identifies exactly which of their moments are finite. The answer is given by one number, the limit of the generalized failure rate. A consequence used in pricing models is that a valuation law with a finite mean has $g>1$ eventually, so the pricing problem has a finite solution.

Setting

Let $X$ be a nonnegative random variable with distribution function $\Phi(\xi)=\mathbb P(X\le\xi)$ and survival function $\bar\Phi(\xi)=1-\Phi(\xi)$ . Assume $\Phi$ has a density $\phi$ . The failure rate is

h(\xi)=\frac{\phi(\xi)}{\bar\Phi(\xi)},

and the generalized failure rate is $g(\xi)=\xi h(\xi)$ . $X$ is IGFR if $g$ is weakly increasing on $\{\xi:\Phi(\xi)<1\}$ . $X$ has support $(\alpha,\infty)$ , with $\alpha\ge 0$ , if $\Phi(\xi)=0$ exactly for $\xi\le\alpha$ and $\Phi(\xi)<1$ for every $\xi$ . For a real $n>0$ , the $n$ -th moment is $\mathbb E[X^n]=\int x^n\,d\Phi(x)\in[0,\infty]$ .

The comparison law is the Pareto law with scale $S>0$ and parameter $k>0$ , which has density $\phi(\xi)=kS^k\xi^{-k-1}$ for $\xi\ge S$ . Its generalized failure rate is identically $k$ on $[S,\infty)$ , and its $n$ -th moment is finite exactly when $k>n$ . For a level $y$ with $\bar\Phi(y)>0$ , write $X_y$ for $X$ conditional on $X>y$ . A random variable $A$ is stochastically smaller than $B$ if $\mathbb P(A>x)\le\mathbb P(B>x)$ for all real $x$ .

In Lean, $X$ is its law μ : Measure ℝ, $\Phi$ is cdf μ, $\bar\Phi$ is survival μ, $h$ is failureRate μ φ, $g$ is genFailureRate μ φ, and $\mathbb E[X^n]$ is nthMoment μ n.

Formalization targets

Goal: Theorem 2 (p. 603)

Suppose $X$ is IGFR with support $(\alpha,\infty)$ and $\lim_{\xi\to\infty}g(\xi)=\kappa$ , where $\kappa\in[0,\infty]$ may be infinite. Then for every real $n>0$ ,

\mathbb E[X^n]<\infty\iff\kappa>n .

The statement fixes no constants. It covers $\kappa=\infty$ (all moments finite) and the boundary case $n=\kappa$ (infinite moment).

Milestones

The two Pareto facts of the §3 preamble come first:

g_{\mathrm{Pareto}(S,k)}(\xi)=k\ \ (\xi\ge S),\qquad \mathbb E[X_k^n]<\infty\iff k>n .

Six claims from the proof follow:

$\mathbb E[X^n]<\infty$ iff the part of the integral over $\{X>y\}$ is finite.
$h_y=h$ on $(y,\infty)$ .
$\bar\Phi(\xi)=\exp[-\int_0^\xi h]$ .
If $h(\xi)>c/\xi$ beyond $y$ , then $X_y$ is stochastically smaller than $\mathrm{Pareto}(y,c)$ .
The usual stochastic order between nonnegative variables orders their $n$ -th moments.
If $h(\xi)\le c/\xi$ beyond $z$ , then $\mathrm{Pareto}(z,c)$ is stochastically smaller than $X_z$ .

Two consequences stated after the theorem are included as further targets. First, an IGFR law with support $(\alpha,\infty)$ and a finite mean has $g>1$ beyond some finite point. Second, a strictly IGFR law with a finite $(n+1)$ -st moment satisfies the two conditions of Van Mieghem and Dada (1999): $h(\xi)-(n+1)/\xi$ has at most one zero, and $\lim_{\xi\downarrow0}\xi h(\xi)<n+1$ .

Significance

The theorem gives a complete moment criterion for IGFR laws in terms of the single number $\kappa$ . Among IGFR laws, finiteness of the mean, the variance or any higher moment can therefore be read off the tail of $g$ . One consequence is that a finite mean is enough for the IGFR pricing problem to have a finite solution, which replaces the separate condition " $g$ exceeds one at a finite point". The theorem generalizes Lemma 2 of Lariviere and Porteus (2001), and the paper uses it to connect IGFR laws to the Van Mieghem–Dada condition.

The result is proved on paper but has not been formalized. Formalizing it adds three things:

a machine-checked proof of the boundary case $n=\kappa$ , which the printed argument (with $0<\varepsilon<n-\kappa$ ) does not treat;
the Pareto moment and hazard identities, which Mathlib's Pareto.lean lacks;
a reusable link between failure-rate bounds and the usual stochastic order, through the representation $\bar\Phi=\exp(-\int h)$ .

Difficulty

The core of the proof is a comparison: a pointwise bound $h(\xi)\gtrless c/\xi$ beyond a level becomes a stochastic order against a Pareto tail. This needs the representation $\bar\Phi(\xi)=\exp[-\int_0^\xi h]$ , which uses the fundamental theorem of calculus for $\log\bar\Phi$ across the left end of the support, where $\Phi$ may have a kink. It also needs to be stated for the conditional law, whose density is a rescaled restriction.

An obvious first attempt is to bound $\mathbb E[X^n]$ directly by $\int x^n\phi(x)\,dx$ with the given bound on $g$ . That bound controls $\phi/\bar\Phi$ , not $\phi$ , so it says nothing directly. The survival representation is what converts it.

A second obstacle is the boundary case $n=\kappa$ , with $\kappa$ finite. A strict margin $\varepsilon$ is no longer available there. It needs the non-strict bound $g\le\kappa$ , which follows from monotonicity, and a Pareto law with parameter exactly $\kappa$ .

Formalization scope

Laws, not random variables. Every statement is about distributions, so $X$ is represented by a probability measure μ on ℝ with μ (Set.Iio 0) = 0. In the goal, nonnegativity also follows from the support hypothesis, and the separate hypothesis is kept for uniformity with the other items.
The density version is pinned. $h$ and $g$ read $\phi$ pointwise, while "Φ has density φ" determines $\phi$ only up to a null set. The predicate IsRegDensity requires $\phi\ge0$ and $\mu=\phi\cdot\text{Lebesgue}$ . It also requires $\phi(\xi)$ to be the right derivative of $\Phi$ at every point $\xi$ of $\{0<\Phi<1\}$ and $\phi=0$ wherever $\Phi=0$ . The exponential law with $\phi(0)=0$ satisfies all hypotheses of the goal, with $\kappa=\infty$ .
IGFR is weak monotonicity of $g$ on $\{\Phi<1\}$ , as printed. On this set $\bar\Phi>0$ , so Lean's convention $x/0=0$ never enters.
$\kappa$ is an extended nonnegative real. The limit hypothesis is Tendsto (fun ξ => ENNReal.ofReal (g ξ)) atTop (𝓝 κ) with κ : ℝ≥0∞. A real-valued $\kappa$ would silently drop the case $\kappa=\infty$ .
Moments are lower Lebesgue integrals ∫⁻ x, ENNReal.ofReal (x ^ n) ∂μ with a real exponent. The Bochner integral would make "finite" automatic, because it returns $0$ for a non-integrable function, so it is not used.
Conditioning and Pareto. $X_y$ is Mathlib's ProbabilityTheory.cond μ (Set.Ioi y), always with $\bar\Phi(y)>0$ . The Pareto law is Mathlib's paretoMeasure S k. "Stochastically smaller" is the published definition StochasticOrders.Usual.UsualOrder applied with the identity map.
Trivialization is ruled out. The goal is a full equivalence with a possibly infinite $\kappa$ and an infinite-valued moment. It is not the weaker " $\kappa>n$ implies finite", and the hypotheses are jointly satisfiable.
Recorded deviations. The printed bound " $\mathbb E[X^n\mid X\le y]<y^{n+1}$ " is a slip (it fails for $y<1$ ). Only the finiteness it is used for is formalized. The Pareto moment fact is stated as an equivalence, which contains the printed "only if".
Infrastructure. A complete development needs:
- the Pareto moment integral;
- the FTC argument for $\log\bar\Phi$ ;
- the layer-cake formula for moments under the usual order;
- basic facts about cond and cdf.
The survival representation and the failure-rate/Pareto comparisons are reusable for any heavy-tail result stated through hazard rates. Contributions are welcome at every level, including partial results such as the Pareto lemmas alone.

Selected references

M. A. Lariviere, A note on probability distributions with increasing generalized failure rates, Operations Research 54(3):602–604, 2006. https://doi.org/10.1287/opre.1060.0282
M. A. Lariviere and E. L. Porteus, Selling to a newsvendor: an analysis of price-only contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (SIAM Classics reprint 1996). https://doi.org/10.1137/1.9781611971194
J. A. Van Mieghem and M. Dada, Price versus production postponement: capacity and competition, Management Science 45(12):1631–1649, 1999. https://doi.org/10.1287/mnsc.45.12.1631
S. M. Ross, Stochastic Processes, Wiley, 1983.

14 thms3 active usersReviewed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

AdWords and Generalized On-line Matching II: No Randomized Online Algorithm for b-Matching Has Competitive Ratio Better Than 1 − 1/e, for Every Budget bResearch Paper

Motivation

Search engines sell advertising slots query by query. Each advertiser states a bid per keyword and a daily budget; queries arrive one at a time, and the engine must assign each to an advertiser immediately, without knowing which queries will come later. Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007) called this the adwords problem and gave a deterministic online algorithm whose competitive ratio, the worst-case ratio of its revenue to the best offline revenue, tends to $1-1/e$ when bids are small compared to budgets. Section 7 of the same paper shows that this ratio cannot be beaten, even by randomized algorithms and even under the small-bids assumption. That lower bound is the subject of this mission.

Timeline of the special cases:

1990. Karp, Vazirani and Vazirani (STOC 1990) proved that no randomized online algorithm for online bipartite matching (unit bids, unit budgets) has competitive ratio better than $1-1/e$ , and that their algorithm RANKING attains it.
2000. Kalyanasundaram and Pruhs (Theoret. Comput. Sci. 2000) studied online b-matching: budgets of $b$ units and $0/1$ bids. Their deterministic algorithm BALANCE has competitive ratio tending to $1-1/e$ as $b\to\infty$ , and they proved that no deterministic algorithm does better. Whether randomization helps for large $b$ was left open (Kalyanasundaram–Pruhs 1998).
2007. Mehta, Saberi, Vazirani and Vazirani (Theorem 9) closed that question: no randomized online algorithm beats $1-1/e$ for b-matching, for large $b$ .

Setting

An instance of online b-matching has $N$ bidders and a sequence of queries $t = 0,1,\dots,M-1$ . Every bidder has the same integer budget $B\ge1$ . Each query $t$ comes with the set $I(t)$ of bidders that bid $1$ on it; the others bid $0$ .

A deterministic online algorithm $a$ processes the queries in order. When query $t$ arrives it sees the bid sets $I(0),\dots,I(t)$ and nothing later, and it either proposes a bidder or leaves the query unallocated. The proposal succeeds if the bidder bids on the query and has won fewer than $B$ queries so far; the bidder then pays $1$ . The algorithm is not required to be greedy. Its revenue $\mathrm{ALG}_a(I)$ is the number of queries won. A randomized online algorithm $A$ is a probability distribution over deterministic online algorithms, fixed before the instance is chosen; its expected revenue is $\mathbb E_A[\mathrm{ALG}(I)]=\sum_a A(a)\,\mathrm{ALG}_a(I)$ .

An offline allocation $\tau$ assigns each query to a bidder or to nobody, with full knowledge of $I$ . Its revenue is $\mathrm{rev}_B(I,\tau)=\sum_r\min\{B,\ |\{t:\tau(t)=r,\ r\in I(t)\}|\}$ : each bidder pays for the queries it bids on, up to its budget.

The permuted round instances of the proof are as follows. For a permutation $\pi$ of the bidders, the instance $I_\pi$ consists of $N$ rounds $Q_1,\dots,Q_N$ of $B$ queries each, and bidders $\pi(i),\pi(i+1),\dots,\pi(N)$ bid on the queries of round $Q_i$ . The distribution $\mathcal D$ is the uniform distribution over these $N!$ instances, and $\mathbb E_\pi$ denotes the average over it. The paper writes this instance with budget $1$ , bids $\epsilon$ and $1/\epsilon$ queries per round; the Lean development uses the same instance scaled by $B=1/\epsilon$ .

Formalization targets

Goal: Theorem 9

For every $\delta>0$ there is $N_0$ such that for all $N\ge N_0$ , all $B\ge1$ and every randomized online algorithm $A$ for $N$ bidders and $NB$ queries, there are an instance $I$ and an allocation $\tau$ with

\mathrm{rev}_B(I,\tau)=NB\qquad\text{and}\qquad \mathbb E_A[\mathrm{ALG}(I)]\le\Big(1-\frac1e+\delta\Big)NB.

The constant $1-1/e$ is the paper's. The slack $\delta$ is not a weakening of the paper's claim: a competitive ratio better than $1-1/e$ would mean a ratio $1-1/e+\delta'$ for some $\delta'>0$ on every instance. The threshold $N_0$ is independent of the budget, which is how "for large $b$ " is rendered.

Milestones (proof of Theorem 9, p. 15)

Yao step. If every deterministic algorithm $a$ has $\mathbb E_\pi[\mathrm{ALG}_a(I_\pi)]\le V$ , then every randomized $A$ has some $\pi$ with $\mathbb E_A[\mathrm{ALG}(I_\pi)]\le V$ .
The optimum. $\mathrm{rev}_B(I_\pi,\tau_\pi)=NB$ for the allocation $\tau_\pi:Q_i\mapsto\pi(i)$ , and no allocation earns more.
The display. For a deterministic $a$ , with $q_{ij}(\pi)$ the fraction of $Q_i$ won by $\pi(j)$ ,

\mathbb E_\pi[q_{ij}]\le\frac1{N-i+1}\ (j\ge i),\qquad \mathbb E_\pi[q_{ij}]=0\ (j<i).

Per-bidder bound. $\mathbb E_\pi\big[L^a(\pi(j))/B\big]\le\min\{1,\sum_{i=1}^{j}\frac1{N-i+1}\}$ , where $L^a(r)$ is the number of queries bidder $r$ wins.
Summed bound. $\sum_{j=1}^{N}\min\{1,\sum_{i=1}^{j}\frac1{N-i+1}\}\le(1-1/e+\delta)N$ for $N\ge N_0(\delta)$ .
Average revenue. $\mathbb E_\pi[\mathrm{ALG}_a(I_\pi)]\le(1-1/e+\delta)NB$ for $N\ge N_0(\delta)$ , every $B\ge1$ and every deterministic $a$ .

Significance

The result. Theorem 9 shows that the $1-1/e$ ratio attained by BALANCE for large budgets, and by the paper's tradeoff algorithm for adwords with small bids, is optimal among all online algorithms, randomized or not. Since b-matching is a special case of adwords with small bids, the same bound applies to adwords. It also answers the question of Kalyanasundaram and Pruhs on whether randomization helps for b-matching. With $B=1$ it contains the bipartite matching lower bound of Karp, Vazirani and Vazirani.

Formalizing it. The result has been proved since 2007; to our knowledge it has no machine-checked proof. The b = 1 case is posed on the platform as KVVMatching.UpperBound.theorem_2 (Karp–Vazirani–Vazirani), with columns arriving in reverse index order and an analysis of the algorithm RANDOM; this mission poses the budget-uniform statement in its own model. A formalization yields a reusable model of online algorithms with budgets (histories that hide the future, randomized algorithms as mixtures of deterministic rules) and a formal instance of Yao's principle for online problems.

Difficulty

The bound must hold for every deterministic online algorithm, including ones that are not greedy, waste proposals, or base each decision on the entire revealed history. A tempting argument fixes the algorithm's behaviour per round and treats it as oblivious to earlier rounds; that only covers a subclass. The history of the permuted instance reveals, before round $i$ , exactly which bidders dropped out in earlier rounds, so the information available to the algorithm grows round by round, and the bound on $\mathbb E_\pi[q_{ij}]$ has to hold conditionally on everything revealed. Budgets interact across rounds: whether a proposal in round $i$ succeeds depends on wins in earlier rounds. Finally, the printed "at most $N(1-1/e)$ " is false at every finite $N$ : the sum in milestone 5 exceeds $N(1-1/e)$ by a bounded amount (about $0.316$ for large $N$ ), so the analytic step is genuinely asymptotic.

Formalization scope

Representation. Bidders are Fin N and query positions Fin M, both zero-based. An instance is Fin M → Finset (Fin N). A history is Fin M → Option (Finset (Fin N)) with unrevealed entries none. A deterministic algorithm is Fin M → History N M → Option (Fin N), a randomized one is a PMF over deterministic algorithms, and expected revenue is a finite sum.
Conventions. Budgets are a common integer $B$ and bids are $0/1$ ; the paper's budget- $1$ , bid- $\epsilon$ instance is the same instance scaled by $B=1/\epsilon$ . A query in position $t$ belongs to round $\lfloor t/B\rfloor+1$ . Rounds $i$ and positions $j$ in milestones 3–4 are 1-based, as in the paper. "Bidder $j$ " in the proof means the bidder $\pi(j)$ in position $j$ of the permutation. The $j<i$ case of the display is an equality. The comparator in the goal is an explicit allocation of revenue $NB$ , which is the maximum possible.
Ruled out. The algorithm sees only the revealed history, never $I$ or $\pi$ , and the randomized algorithm is chosen before the instance. An algorithm that could see the instance would trivially earn $NB$ , and choosing the instance first would make the goal the averaging statement of milestone 6, not Theorem 9.
Infrastructure. Needed: finite sums over permutations, the exchange of the average over $\pi$ and over the algorithm, invariance of a run under permutations that fix the revealed information, and estimates of harmonic sums $H_N-H_{N-j}$ against $\log$ . The online-algorithm model and the Yao step are reusable for other online lower bounds. Contributions to any milestone are welcome; milestone 5 is pure real analysis and independent of the model.

Selected references

A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized on-line matching, J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
B. Kalyanasundaram, K. R. Pruhs, An optimal deterministic algorithm for online b-matching, Theoret. Comput. Sci. 233, 2000. https://doi.org/10.1016/S0304-3975(99)00140-1
A. C.-C. Yao, Probabilistic computations: toward a unified measure of complexity, FOCS 1977. https://doi.org/10.1109/SFCS.1977.24

8 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Basic Packing of Arborescences: A Digraph with Roots Has an M-Basic Packing of Arborescences iff π Is M-Independent and D Is M-ConnectedResearch Paper

Motivation

Packing arc-disjoint arborescences is one of the basic tractable problems of combinatorial optimization. Edmonds' branching theorem (1973) says that a digraph $D=(V,A)$ contains $k$ arc-disjoint spanning arborescences rooted at a vertex $r$ if and only if every non-empty vertex set $X\subseteq V\setminus r$ is entered by at least $k$ arcs. Its undirected counterpart is the Tutte–Nash-Williams theorem on edge-disjoint spanning trees, and Frank showed how the undirected theorem follows from the directed one through an orientation argument. Both results underlie network-design and connectivity-augmentation algorithms, and the cut condition in Edmonds' theorem is the model for many min–max theorems on packings.

Katoh and Tanigawa (2013), motivated by the rigidity of frameworks with boundaries, introduced matroid-based packings of rooted trees in undirected graphs: the roots of the trees are elements of a matroid, and every vertex must be covered by trees whose roots form a base. Durand de Gevigney, Nguyen and Szigeti (arXiv:1207.1985, 2012) gave the directed counterpart. Their Theorem 1.6 characterizes digraphs with roots that admit a matroid-based packing of arborescences, contains Edmonds' theorem as the special case of the free matroid with all roots at one vertex, and implies Katoh and Tanigawa's undirected theorem through Frank's orientation theorem. Its proof is short and purely combinatorial.

Timeline:

1961: Tutte and Nash-Williams characterize graphs with $k$ edge-disjoint spanning trees.
1973: Edmonds characterizes digraphs with $k$ arc-disjoint spanning arborescences rooted at $r$ .
1980: Frank's orientation theorem for intersecting supermodular demand functions.
2011–2013: Katoh and Tanigawa, rooted-tree decompositions with matroid constraints (undirected).
2012: Durand de Gevigney, Nguyen and Szigeti, the directed theorem (this mission).

Setting

A digraph $D=(V,A)$ has a finite vertex set $V$ and a finite set $A$ of arcs, each with a tail and a head; parallel arcs are allowed. For $X\subseteq V$ , $\varrho_D(X)$ is the set of arcs entering $X$ (tail outside, head inside) and $\rho_D(X)=|\varrho_D(X)|$ . An arborescence rooted at $r$ is a sub-digraph that is a directed tree in which $r$ has in-degree $0$ and every other vertex has in-degree $1$ ; the single vertex $r$ is an arborescence.

Let $S$ be a finite set and $\pi:S\to V$ a placement of its elements at vertices (several elements may sit at one vertex). The triple $(D,S,\pi)$ is a digraph with roots. Write $S_X=\pi^{-1}(X)$ and $S_v=\pi^{-1}(v)$ . Let $M$ be a matroid on $S$ with rank function $r_M$ .

$\pi$ is $M$ -independent if $S_v$ is independent in $M$ for every vertex $v$ .
$(D,S,\pi)$ is $M$ -connected if

\rho_D(X)\ \ge\ r_M(S)-r_M(S_X)\qquad\text{for all non-empty }X\subseteq V.\tag{3}

An $M$ -basic packing of arborescences is a family $(T_s)_{s\in S}$ of pairwise arc-disjoint arborescences of $D$ , $T_s$ rooted at $\pi(s)$ , such that for every vertex $v$ the set $\{s\in S: v\in V(T_s)\}$ is a base of $M$ . The arborescences need not be spanning.

In Lean these are Digraph, Arborescence, MIndependent, MConnected and IsBasicPacking in the namespace BasicPackArb.Main; the proof-side notions (tight sets, domination, good and bad arcs, the parallel extension) are in a second definitions module.

Formalization targets

Goal: Theorem 1.6

\exists\,(T_s)_{s\in S}\ \text{an }M\text{-basic packing of arborescences in }(D,S,\pi)\iff \pi\text{ is }M\text{-independent and }(D,S,\pi)\text{ is }M\text{-connected}.

The statement is universally quantified over the vertex, arc and root types, the digraph, the placement and the matroid. It has no constants.

Milestones

The necessity direction (§2, p. 4).
Claim 2.1: if $r_M(P\cap Q)+r_M(P\cup Q)=r_M(P)+r_M(Q)$ , an element spanned by $P$ and by $Q$ is spanned by $P\cap Q$ .
Claim 2.2 (a), (b), (c): uncrossing of tight sets, the part of a tight set reaching a vertex, and domination along good arcs.
Claim 2.3: with no bad arc, single-vertex arborescences form a basic packing.
The lifting step (p. 5): removing a bad arc $uv$ and adding a root $s'$ parallel to $s$ at $v$ preserves independence, and a packing of the new instance lifts back.
Statement (4) and Claim 2.4: some bad arc can be split off while keeping $M'$ -connectedness.

Significance

The result. Theorem 1.6 is a good characterization: both sides can be certified, and the condition (3) is a cut condition with a submodular right-hand side. It unifies Edmonds' branching theorem (free matroid, all roots at one vertex) with matroid-constrained packings, and through Frank's orientation theorem it yields Katoh and Tanigawa's theorem on rooted-tree decompositions, which is used in combinatorial rigidity. The same paper derives from it a description of the convex hull of basic packings and a polynomial algorithm for the minimum-cost version.

Formalizing it. The result is proved on paper; no machine-checked proof of Theorem 1.6, of Edmonds' branching theorem, or of any of the claims is known on this platform. A formal proof needs a multi-digraph library with arc deletion, arborescences as sub-digraphs, in-degree functions of vertex sets and their submodularity, and matroid rank and span arguments on top of Mathlib's Matroid. The milestones follow the paper's induction on the number of arcs.

Difficulty

The necessity direction is a counting argument. Sufficiency is the substance. The natural first attempt, building the arborescences greedily or splitting $S$ into Edmonds instances, fails because the arborescences are not spanning and the covering condition is a base condition at every vertex, coupled through the matroid. The hard step is Claim 2.4: deleting an arc can destroy condition (3), and it must be shown that some bad arc, together with a suitable new parallel root, can be removed without doing so. Condition (3) has to be controlled for every vertex set at once, with a right-hand side that changes with the matroid. Formally, the lifting step requires gluing two arborescences with an arc and checking that the base condition survives the identification of the parallel pair.

Formalization scope

Vertices: a Fintype V with decidable equality. Arcs: an ambient type with tail, head and a finite arc set arcs, so parallel arcs and loops are allowed and $D-uv$ deletes one arc.
Arborescence: vertex set, arc set inside $A$ with ends in the vertex set, a root of in-degree $0$ , in-degree exactly $1$ at other vertices, every vertex reachable from the root. Under the in-degree conditions this is equivalent to being a directed tree.
The packing is a family indexed by $S$ , not a set of arborescences, so $|S_v|$ equal single-vertex arborescences count separately.
Matroid: Mathlib's Matroid S with ground set all of $S$ (a finite type); rank is Matroid.eRk with values in $\mathbb{N}_\infty$ ; base is IsBase, independence is Indep.
$\mathrm{Span}_M(Q)=\{s: r_M(Q\cup\{s\})=r_M(Q)\}$ , defined literally.
(3) and tightness are written additively, $r_M(S)\le\rho_D(X)+r_M(S_X)$ and $\rho_D(X)+r_M(S_X)=r_M(S)$ , so no truncated subtraction appears. (3) ranges over all non-empty $X$ , including sets that contain roots.
The extension $S'$ is Option S with the new element none; $M'$ is the comap of $M$ along $o\mapsto o.\mathrm{getD}\,s$ , which makes none parallel to $s$ and restricts to $M$ on $S$ .
Claims stated inside the sufficiency proof carry that proof's standing hypotheses explicitly ( $\pi$ $M$ -independent, $M$ -connected, and "no bad arc", "a bad arc exists" or "Claim 2.4 is false" as the page says).

A formalization in which arborescences need not lie in $A$ , or need not be reachable from their root, or in which the packing is a set of arborescences, or the per-vertex condition is "spanning" or "independent" rather than "base", states a different theorem and is ruled out by the definitions above.

Contributions welcome: proofs of the claims in any order, general lemmas on submodularity of $\rho_D$ and on tight-set uncrossing (reusable for other arborescence-packing results), and a proof of Edmonds' branching theorem as a corollary of the goal.

Selected references

O. Durand de Gevigney, V.-H. Nguyen, Z. Szigeti, Basic Packing of Arborescences, arXiv preprint, 2012. https://arxiv.org/abs/1207.1985v1 (published as Matroid-based packing of arborescences, SIAM J. Discrete Math., 2013).
J. Edmonds, Edge-disjoint branchings, in R. Rustin (ed.), Combinatorial Algorithms, Academic Press, 1973, pp. 91–96.
N. Katoh, S. Tanigawa, Rooted-tree decompositions with matroid constraints and the infinitesimal rigidity of frameworks with boundaries, SIAM J. Discrete Math., 2013.
A. Frank, On the orientation of graphs, J. Combin. Theory Ser. B 28 (1980) 251–261.
W. T. Tutte, On the problem of decomposing a graph into n connected factors, J. London Math. Soc. 36 (1961) 221–230; C. St. J. A. Nash-Williams, Edge-disjoint spanning trees of finite graphs, J. London Math. Soc. 36 (1961) 445–450.
A. Frank, Connections in Combinatorial Optimization, Oxford University Press, 2011.

12 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization+1·Captain: mikedeng1

Sample Size Selection in Optimization Methods for Machine Learning 1: With Batch Sizes n_k ≥ a^k, Dynamic Batch Steepest Descent Converges Linearly in Expectation, E[J(w_k) − J(w*)] ≤ Cρ^kResearch Paper

Motivation

Training a model in machine learning means minimizing an expected loss over a data distribution, using a finite sample from it. Two families of methods dominate. Stochastic gradient methods step along the gradient of the loss at one data point: each step is cheap, but the noise forces small steps and many sequential iterations. Batch methods average the gradient over a large set of points: each step is accurate and parallelizes well, but costs a pass over the data. Bottou and Bousquet (The tradeoffs of large scale learning, NIPS 2007) compared the two by the total work needed to reach accuracy $\epsilon$ and concluded that stochastic gradient descent is preferable in large-scale learning.

Byrd, Chin, Nocedal and Wu (Sample size selection in optimization methods for machine learning, Math. Program. 2012) analyse a third option: a dynamic batch method, which takes gradient steps on mini-batches whose size grows over the run. A small batch makes early progress cheap; a large batch later makes the steps accurate. Their Theorem 4.2 shows that when the batch size grows geometrically, steepest descent with a fixed step converges linearly in expectation, and their Corollary 4.3 derives from it a total work bound of the same order as stochastic gradient descent. The analysis underlies a line of work on adaptive sampling and variance-controlled batch methods (for example Friedlander and Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 2012; Bottou, Curtis and Nocedal, Optimization methods for large-scale machine learning, SIAM Review 2018, §5.2).

Setting

Let $(Z,P)$ be a probability space of data points $z$ ; in the paper $z=(x,y)$ is an input–output pair with distribution $P(x,y)$ . The parameter is $w\in\mathbb R^m$ ( $m$ is the number of variables). A per-sample loss $\ell(w;z)$ is given with gradient $\nabla\ell(w;z)$ in $w$ , and the objective is the expected loss (2.1)

J(w)=\int\ell(w;z)\,dP(z).

The gradient of the objective is the expected per-sample gradient, $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$ .

Uniform convexity (4.2): $J$ is twice continuously differentiable and there are constants $0<\lambda<L$ with

\lambda\|d\|_2^2\le d^T\nabla^2J(w)\,d\le L\|d\|_2^2\qquad\text{for all } w,d .

Then $J$ has a unique minimizer $w^*$ .

For a random vector $X\in\mathbb R^m$ , $\|\mathrm{Var}(X)\|_1=\mathbb E\|X-\mathbb EX\|_2^2$ is the sum of its componentwise variances. The variance bound (4.22) asks for a constant $\omega$ with

\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1\le\omega\qquad\text{for all } w .

The algorithm. Fix sample sizes $n_k\ge1$ and a starting point $w_0$ . At iteration $k$ draw a batch $S_k$ of $n_k$ points, independently with law $P$ and independently of earlier batches, form the batch gradient (4.19)

g_k=\frac1{n_k}\sum_{i\in S_k}\nabla\ell(w_k;i),

and take the dynamic batch steepest descent step (4.24)

w_{k+1}=w_k-\frac1L\,g_k .

The iterates $w_k$ are random, and expectations below are over all batches.

Formalization targets

Goal: Theorem 4.2

If $n_k\ge a^k$ for all $k$ , for some $a>1$ , and (4.22) holds, then

\mathbb E[J(w_k)-J(w^*)]\le C\rho^k\quad\text{for all }k,\qquad \rho=\max\{1-\lambda/(4L),\,1/a\}<1,\quad C=\max\{J(w_0)-J(w^*),\,2\omega/\lambda\}.

The constants are the paper's. The goal also asserts that $J(w_k)$ is integrable for every $k$ .

Milestones, in the order the proof uses them

(4.5), p. 8: $\nabla J(w)^T\nabla J(w)\ge\lambda[J(w)-J(w^*)]$ for every $w$ .
Taylor bound, p. 11: $J(w-\frac1Lg)\le J(w)-\frac1L\nabla J(w)^Tg+\frac1{2L}\|g\|^2$ for every $w$ and $g$ .
(4.25), p. 11: at a fixed point $w$ , with $g$ the batch gradient of $n$ i.i.d. draws,

\mathbb E[J(w-\tfrac1Lg)]\le J(w)-\tfrac1L\|\nabla J(w)\|^2+\tfrac1{2L}\mathbb E\|g\|^2,\qquad \mathbb E\|g\|^2=\|\nabla J(w)\|^2+\|\mathrm{Var}(g)\|_1 .

Variance of the batch gradient, p. 12: $\|\mathrm{Var}(g)\|_1\le\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1/n$ .
(4.26), p. 12: $\mathbb E[J(w-\tfrac1Lg)]\le J(w)-\tfrac1{2L}\|\nabla J(w)\|^2+\tfrac1{2Ln}\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1$ .
(4.27), p. 12: $\mathbb E[J(w-\tfrac1Lg)-J(w^*)]\le(1-\tfrac{\lambda}{2L})(J(w)-J(w^*))+\tfrac{\omega}{2Ln}$ .

Milestones 3–6 are the paper's conditional expectations given $w_k$ , stated at a fixed point $w$ with the batch drawn afresh.

Significance

Theorem 4.2 is the convergence guarantee of the dynamic sampling strategy: it says that the noise of a mini-batch gradient does not destroy the linear rate of steepest descent, provided the batch grows geometrically. The rate $\rho$ makes the trade-off explicit: the optimization contracts by $1-\lambda/(4L)$ per step, the noise by $1/a$ , and the slower of the two governs. From it the paper's Corollary 4.3 bounds the total number of sample-gradient evaluations to reach $\mathbb E[J(w_k)-J(w^*)]\le\epsilon$ by $O(L/(\lambda\epsilon))$ , which places dynamic batch methods on the same footing as stochastic gradient descent in the Bottou–Bousquet comparison, while keeping the parallelism of batch methods.

The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization produces a reusable account of the one-iteration analysis of a mini-batch gradient step (descent lemma, variance of an i.i.d. sample mean of random vectors, conditional expectation over a fresh batch), and of the passage from a conditional one-step recursion to an unconditional bound over a run driven by an infinite i.i.d. array. Corollary 4.3 is not part of this mission: it involves $O(\cdot)$ bounds, a cost model for gradient evaluations and an iteration count treated as a real number.

Difficulty

The arithmetic of the induction on p. 12 is short. The difficulty is in making the probability rigorous. The iterate $w_k$ is random, and the paper's one-step bound (4.27) is a conditional expectation given $w_k$ , with $J(w_k)$ on the right-hand side. Turning it into an unconditional recursion requires that the batch of iteration $k$ be independent of $w_k$ , that $w_k$ be a measurable function of the earlier batches, and that $J(w_k)$ and $\|g_k\|^2$ be integrable at every step, none of which is automatic for a run driven by an infinite array of draws. A naive formalization that treats $w_k$ as a fixed point, or $g_k$ as an abstract random vector with a postulated variance bound, skips exactly this content.

The variance identity for a sample mean of random vectors in $\mathbb R^m$ and the bound $\|\nabla J(w)\|\le L\|w-w^*\|$ from (4.2) are standard but not packaged in this form in Mathlib.

Formalization scope

The space is EuclideanSpace ℝ (Fin m). The paper's $\lambda$ is written lam (λ is a Lean keyword). (4.2) is ContDiff ℝ 2 J, 0 < lam < L, and the two-sided bound on fderiv ℝ (fderiv ℝ J) w d d.
$J$ is defined as the Bochner integral $\int\ell(w;z)\,dP(z)$ for a general per-sample loss $\ell$ ; the paper's linear predictor $f(w;x)=w^Tx$ and convex loss $l$ are not used by the theorem and are not assumed. The model assumes: $\ell(w;\cdot)$ integrable; $\nabla\ell(w;z)$ the gradient of $\ell(\cdot;z)$ at $w$ ; $(w,z)\mapsto\nabla\ell(w;z)$ jointly measurable; $\nabla\ell(w;\cdot)$ square-integrable; and $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$ (differentiation under the integral, which the paper uses without proof).
Sampling with replacement. The paper's (3.5) is sampling without replacement from $N$ points; it takes $N\to\infty$ on p. 5, which "also corresponds to the case of sampling with replacement". The formalization draws every point i.i.d. from $P$ : draw $i$ of iteration $k$ is $\xi_{k,i}$ and the law of the whole array is Measure.infinitePi over $\mathbb N\times\mathbb N$ . The finite-population factor $(N-n_k)/(N-1)$ is not modelled.
$w^*$ is a given minimizer of $J$ ; $n_k$ are natural numbers with $a^k\le n_k$ (real powers of a real $a>1$ ); $\omega$ is a real number.
The goal asserts integrability of $J(w_k)$ together with the bound, so the inequality cannot be met by the Bochner integral's value $0$ on a non-integrable function. The batch gradient is the mean over $n_k$ draws at the current iterate, and $w_k$ is the random run: a goal with an abstract random $g_k$ satisfying a postulated variance bound, or with $w_k$ a deterministic sequence, would not be this theorem.
Welcome contributions: the variance of an i.i.d. mean of $\mathbb R^m$ -valued random vectors; the descent lemma and gradient-dominance inequality from Hessian bounds; measurability and independence lemmas for processes driven by Measure.infinitePi. All three are reusable beyond this mission.

Selected references

R. H. Byrd, G. M. Chin, J. Nocedal, Y. Wu, Sample size selection in optimization methods for machine learning, Mathematical Programming 134 (2012) 127–155. https://doi.org/10.1007/s10107-012-0572-5
L. Bottou, O. Bousquet, The tradeoffs of large scale learning, NIPS 2007. https://papers.nips.cc/paper/3323-the-tradeoffs-of-large-scale-learning
M. P. Friedlander, M. Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 34 (2012) A1380–A1405. https://doi.org/10.1137/110830629
L. Bottou, F. E. Curtis, J. Nocedal, Optimization methods for large-scale machine learning, SIAM Review 60 (2018) 223–311. https://doi.org/10.1137/16M1080173

10 thms3 active usersReviewed

Completed

Mathematical Logic Theory of Computation·Captain: mikedeng1

On the (Im)possibility of Obfuscating Programs 1: A Decidable Promise Problem Closed under Functional Equivalence Is Decided by a Simulator Given Only Oracle Access to ⟨M⟩ and the Size 1^|M|Research Paper

Motivation

Program obfuscation asks for a compiler that turns a program into one computing the same function while revealing nothing beyond what black-box access to the function reveals. Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang (J. ACM 59(2), 2012; conference version CRYPTO 2001) showed that this "virtual black box" notion cannot be achieved in general. Part of their motivation is an informal reading of Rice's Theorem: since every non-trivial semantic property of programs is undecidable from the code, "the only useful thing you can do with a machine is run it". Section 5 of the paper asks whether a complexity-theoretic analogue holds, and Appendix A asks what the right computability-theoretic statement is once one passes from languages to promise problems.

Classical Rice's Theorem (Rice, 1953) concerns languages: a decidable set of machines closed under functional equivalence is empty or everything. For promise problems the naive analogue (Conjecture A.1 of the paper) is false: the problem "halts everywhere and outputs 1 on 0" versus "halts everywhere and outputs 0 on 0" is decidable, non-trivial, and closed under functional equivalence. Appendix A replaces "trivial" by "decidable by a simulator that only runs the machine", proves that version (Theorem A.2), and shows that the size bound given to the simulator cannot be dropped (Theorem A.4, a separate mission in this series). This mission formalizes Theorem A.2.

Setting

A machine $M$ is a program for a partial recursive function, identified with its description, a natural number $\ulcorner M\urcorner$ . Its computed function $[M]:\mathbb N\rightharpoonup\mathbb N$ is possibly partial, and $[M]\equiv[M']$ means equality of partial functions. The size $|M|$ is the length of the binary description of $M$ ; there are at most $2^s$ machines of size $s$ .

The bounded run of $M$ is

\langle M\rangle(1^t,x)=\begin{cases} y & \text{if } M(x)\text{ halts with output } y \text{ within budget } t,\\ \bot&\text{otherwise.}\end{cases}

An oracle machine $S$ may query $\langle M\rangle$ at any pair $(t,x)$ of its choice; $S^{\langle M\rangle}(z)$ is its output on input $z$ . Oracle access to $\langle M\rangle$ is what running $M$ provides: one may choose inputs and budgets, but one never sees the code.

A promise problem $\Pi=(\Pi_Y,\Pi_N)$ is a pair of disjoint sets of machines. A machine $T$ decides $\Pi$ if $T(\ulcorner M\urcorner)=1$ for $M\in\Pi_Y$ and $T(\ulcorner M\urcorner)=0$ for $M\in\Pi_N$ ; nothing is asked of $T$ outside $\Pi_Y\cup\Pi_N$ . $\Pi$ is closed under $[\cdot]$ if $[M]\equiv[M']$ implies $M\in\Pi_Y\Leftrightarrow M'\in\Pi_Y$ and $M\in\Pi_N\Leftrightarrow M'\in\Pi_N$ .

A machine $N$ is $n$ -compatible with $M$ if $\langle N\rangle(1^t,x)=\langle M\rangle(1^t,x)$ for all $t\le n$ and all $x$ with $|x|\le n$ , and $S_n$ denotes the set of machines of size $|M|$ that are $n$ -compatible with $M$ .

Formalization targets

Goal: Theorem A.2 (p. A:41)

If $\Pi$ is closed under $[\cdot]$ and decidable, then there is one oracle machine $S$ such that for every machine $M$

M\in\Pi_Y\Rightarrow S^{\langle M\rangle}(1^{|M|})=1,\qquad M\in\Pi_N\Rightarrow S^{\langle M\rangle}(1^{|M|})=0 .

Milestones (proof of Theorem A.2, pp. A:41–A:42)

Fact (1): $n$ -compatibility with $M$ is decidable by one oracle machine with oracle $\langle M\rangle$ , uniformly in $M$ , $N$ , $n$ .
Fact (3): if $[M]\not\equiv[N]$ , there is $n'$ with $N$ not $n$ -compatible with $M$ for every $n>n'$ .
There is $n''$ such that every $N\in S_n$ with $n>n''$ satisfies $[N]\equiv[M]$ .
If some stage $n$ finds $T$ , run for $n$ steps, halting on all of $S_n$ with a common answer $\sigma$ , then $\sigma=T(\ulcorner M\urcorner)$ .
For $M\in\Pi_Y$ (resp. $\Pi_N$ ) such a stage exists, with answer $1$ (resp. $0$ ).

Significance

The result. Theorem A.2 is the precise sense in which a semantic property of programs, decidable from the code on a promise, is decidable without the code: running the program on chosen inputs for chosen budgets, plus a bound on its length, suffices. It is the computability-theoretic counterpart of Conjecture 5.2, the complexity-theoretic statement whose failure (Theorem 5.3, under cryptographic assumptions) is one face of the impossibility of obfuscation. Together with Theorem A.4 it isolates the size bound as the ingredient that makes the generalization true.

Formalizing it. The theorem has a complete proof in the paper, about one page long. No machine-checked version is known: the Prove2Me catalogue has classical Rice's Theorem for index sets of Nat.Partrec.Code (FamousTheorems.rice_theorem, which this proof does not use) but nothing on promise problems, bounded-run oracles, or simulators. A formal proof produces reusable infrastructure: the oracle $\langle M\rangle$ as a total function on query codes, decidability of compatibility relative to it, and a dovetailing simulator assembled as a uniform oracle program.

Difficulty

Each mathematical step is elementary; the work lies in the effective content. The obvious idea, "query $\langle M\rangle$ until $[M]$ is known and then decide", fails: $[M]$ is an infinite object, and no finite set of queries pins it down. The paper's simulator instead uses the size bound to restrict attention to finitely many candidate codes, and needs $T$ to agree on every surviving candidate at a common budget. Turning this into one oracle program requires enumerating all codes of a given size, deciding compatibility from finitely many oracle answers, comparing bounded runs of $T$ , and searching over $n$ , all uniformly in $M$ and with no access to $\ulcorner M\urcorner$ . Termination holds only on promise instances, since $T$ may diverge elsewhere, so the argument cannot assume a total decider.

Formalization scope

Machines are Mathlib's Nat.Partrec.Code; descriptions are Encodable.encode; $[M]$ is Code.eval; $\langle M\rangle(1^t,x)$ is Code.evaln t M x : Option ℕ, with none for $\bot$ . The budget of evaln is fuel rather than a literal Turing-machine step count. It is monotone in $t$ , converges to $[M]$ , and is primitive recursive in $(t,M,x)$ , and these are the only properties of step counts that the proof uses. Inputs are natural numbers, $|x|$ is Nat.size x, and $|M|$ is Nat.size (encode M). Oracle machines are the published uniform oracle programs FriedbergMuchnik.Program with semantics oracleEval (a single syntax tree with an oracle-query instruction, equivalent to relative partial recursiveness). The oracle $\langle M\rangle$ is the total function sending Nat.pair t x to 0 for $\bot$ and to y + 1 for an output $y$ . The simulator's input $1^{|M|}$ is the number $|M|$ , since unary versus binary is immaterial here. " $S^{\langle M\rangle}(1^{|M|})=1$ " means that the run halts with output $1$ . Promise problems carry their disjointness, as in the paper, although no statement uses it. The decider $T$ is a Code applied to descriptions and may diverge off the promise.

The trivializing readings are excluded. $S$ is chosen before $M$ (one program, not one per machine). It receives the size of $M$ , never its description, and many machines share each size. It sees only the finitely many oracle answers a halting run queries. The oracle is the bounded-run function $\langle M\rangle$ , not $[M]$ or the code.

Contributions welcome: proofs of the milestones; a primitive-recursive enumeration of the codes of a given size; a proof that oracle M is uniformly computable from M, which is useful beyond this mission.

Selected references

B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. Vadhan, K. Yang, On the (Im)possibility of Obfuscating Programs, Journal of the ACM 59(2), 2012. https://doi.org/10.1145/2160158.2160159
H. G. Rice, Classes of recursively enumerable sets and their decision problems, Transactions of the AMS 74(2), 1953. https://doi.org/10.1090/S0002-9947-1953-0053041-6
S. Even, A. L. Selman, Y. Yacobi, The complexity of promise problems with applications to public-key cryptography, Information and Control 61(2), 1984. https://doi.org/10.1016/S0019-9958(84)80056-X

8 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Sample Size Selection in Optimization Methods for Machine Learning 2: Steepest Descent with Gradient Error ‖g_k − ∇J(w_k)‖ ≤ θ‖g_k‖ Contracts J by 1 − βλ/L per StepResearch Paper

Motivation

Training a machine-learning model usually means minimizing an expected or empirical loss $J(w)$ over parameters $w \in \mathbb{R}^m$ . Exact gradients of such objectives are expensive, because each one requires a pass over the whole data set; practical methods replace $\nabla J(w_k)$ by a cheaper approximation $g_k$ , for instance a gradient computed on a subsample. This raises a basic question for the analysis of optimization algorithms: how accurate must the approximate gradient be for steepest descent to keep its linear rate of convergence?

Byrd, Chin, Nocedal and Wu (Math. Program. 2012) answer this question with a relative-error condition, and use the answer to motivate a rule that increases the sample size during the run. Their §4.1 treats the deterministic case: the approximations $g_k$ are arbitrary vectors, and only a geometric condition linking $g_k$ to $\nabla J(w_k)$ is assumed. That deterministic result, Theorem 4.1, is the goal of this mission. The stochastic counterpart (Theorem 4.2, dynamic batch sizes) is a separate mission of the same series.

Relative-error conditions of this kind ("the error is a fixed fraction of the step") appear throughout the literature on inexact gradient and inexact Newton methods (e.g. Bertsekas and Tsitsiklis 2000 on gradient methods with errors), and the condition (4.8) below is the deterministic template for the adaptive sampling tests later developed for stochastic optimization.

Setting

Let $J : \mathbb{R}^m \to \mathbb{R}$ be twice continuously differentiable and uniformly convex: there are constants $0 < \lambda < L$ such that

\lambda\|d\|_2^2 \;\le\; d^T \nabla^2 J(w)\, d \;\le\; L\|d\|_2^2 \qquad\text{for all } w, d \in \mathbb{R}^m. \tag{4.2}

Such a $J$ has a unique minimizer $w_*$ ; following the paper, it is normalized so that $J(w_*) = 0$ .

Fix $\theta \in (0,1)$ . Given a sequence of vectors $g_0, g_1, \ldots$ (the approximate gradients), the fixed-steplength steepest descent iteration is

w_{k+1} = w_k - \alpha g_k, \qquad \alpha = \frac{1-\theta}{L}. \tag{4.1, 4.7}

The approximate gradient at iteration $k$ satisfies the relative-error condition if

\|g_k - \nabla J(w_k)\| \;\le\; \theta\, \|g_k\|. \tag{4.8}

Write

\beta = \frac{(1-\theta)^2}{2(1+\theta)^2}. \tag{4.9}

Formalization targets

Goal: Theorem 4.1 (p. 8)

If (4.8) holds at iteration $k$ , then

J(w_{k+1}) \le \Bigl(1 - \frac{\beta\lambda}{L}\Bigr) J(w_k). \tag{4.9}

If (4.8) holds at every iteration, then $w_k \to w_*$ (4.10); every $k > \frac{L}{\beta\lambda}[\log(1/\epsilon) + \log J(w_0)]$ satisfies $J(w_k) < J(w_*) + \epsilon$ (4.11); and

\|g_k\|^2 \le \frac{1}{(1-\theta)^2}\,\frac{2L^2J(w_0)}{\lambda}\Bigl(1-\frac{\beta\lambda}{L}\Bigr)^k. \tag{4.12}

The constants are those of the paper and are kept explicit.

Milestones

In the order the paper's proof uses them:

(4.5) $\nabla J(w)^T\nabla J(w) \ge \lambda[J(w) - J(w_*)]$ and (4.6) $J(w) - J(w_*) \ge \frac{\lambda}{2L^2}\|\nabla J(w)\|_2^2$ , consequences of (4.2) alone (p. 8);
(4.13) $(1-\theta)\|g_k\| \le \|\nabla J(w_k)\| \le (1+\theta)\|g_k\|$ and (4.14) $\nabla J(w_k)^Tg_k \ge (1-\theta)\|g_k\|^2$ under (4.8) (p. 9);
(4.16) the one-step decrease $J(w_{k+1}) \le J(w_k) - \frac{\beta}{L}\|\nabla J(w_k)\|^2$ under (4.8) at $k$ (p. 9);
(4.17) $J(w_k) \le (1 - \beta\lambda/L)^k J(w_0)$ under (4.8) at every earlier iteration (p. 9).

Significance

Theorem 4.1 says that the linear convergence of steepest descent on a uniformly convex function survives arbitrary gradient errors, provided each error is at most a fixed fraction $\theta$ of the approximate gradient's own norm. The price is explicit: the per-step contraction factor is $1 - \beta(\theta)\lambda/L$ instead of a factor of the form $1 - c\lambda/L$ with an absolute constant $c$ , and the iteration bound (4.11) grows like $L/(\beta\lambda)$ times a logarithm. Because (4.8) is relative rather than absolute, no a priori bound on the error is needed, and the error may be large far from the solution. In the paper this is the motivation for requiring the sample variance of a subsampled gradient to be small relative to $\|g_k\|^2$ , which leads to the dynamic sample-size rule analysed in §4.2.

The result is proved in the paper (pp. 9–10). No machine-checked proof of it, or of any relative-error inexact gradient method with explicit constants, has been published. A formal proof provides a checked reference statement for inexact first-order methods with the paper's constants, and the milestones (4.5), (4.6), (4.13), (4.14) are reusable facts about strongly convex smooth functions and about relative-error gradient approximations.

Difficulty

Each step is classical, but the proof combines second-order information with metric estimates. The descent estimate (4.15) needs a second-order Taylor bound from the upper Hessian bound in (4.2), which in Lean means passing from a bound on the second Fréchet derivative to a quadratic upper bound on $J$ along a segment. The inequalities (4.5) and (4.6) relate the gradient norm to the optimality gap through the lower and upper Hessian bounds and the minimizer, and must be derived without an explicit averaged Hessian unless one is built. The convergence $w_k \to w_*$ in (4.10) requires turning convergence of the function values into convergence of the iterates, which again uses uniform convexity. Finally, (4.11) is a logarithmic iteration count whose boundary cases ( $J(w_0) = 0$ , $\epsilon \ge J(w_0)$ ) must be handled. A naive reading of the iteration with exact gradients does not apply: the step is $(1-\theta)/L$ , not $1/L$ , and the direction $-g_k$ is only known to be a descent direction through (4.14).

Formalization scope

The space is EuclideanSpace ℝ (Fin m). Assumption (4.2) is a definition HessianBounds J lam L (with lam for $\lambda$ , a Lean keyword): ContDiff ℝ 2 J, 0 < lam < L, and both bounds on the quadratic form fderiv ℝ (fderiv ℝ J) w d d. The gradient is Mathlib's gradient J. The minimizer is a point wstar with J wstar ≤ J w for all w, and J wstar = 0 is a hypothesis of the goal and of (4.17), exactly as in the paper; (4.5) and (4.6) are stated with $J(w_*)$ and without it. The constant $\beta$ is a definition beta θ; it is never a free variable. The approximate gradients $g_k$ are an arbitrary sequence and nothing is random. The iterates are any sequence with w (k+1) = w k - ((1 - θ) / L) • g k for all k.

The one-step claim (4.9) assumes (4.8) only at the index $k$ ; (4.10)–(4.12) assume it at every index. (4.11) is stated in the form the proof derives in (4.18): every $k$ strictly beyond the bound has $J(w_k) < \epsilon$ . The logarithm is natural; when $J(w_0) = 0$ Lean's convention $\log 0 = 0$ applies, which is harmless because every iterate is then optimal. No positivity hypothesis on $J(w_0)$ is added.

A trivializing formalization is excluded: the step size is fixed by the paper, $\beta$ and the Hessian bounds are pinned, and the hypotheses are satisfiable, e.g. by $J(w) = \tfrac{c}{2}\|w\|^2$ with $\lambda < c < L$ , $w_* = 0$ and $g_k = \nabla J(w_k)$ .

A complete development needs: a second-order Taylor (or mean-value) bound from a Hessian bound, the strong-convexity inequalities (4.5)–(4.6), and elementary real-analysis facts about geometric sequences and logarithms. The milestones (4.5), (4.6), (4.13) and (4.14) are independent of the iteration and reusable. Proofs of any milestone, and alternative proofs with sharper constants stated as separate theorems, are welcome.

Selected references

R. H. Byrd, G. M. Chin, J. Nocedal, Y. Wu, Sample size selection in optimization methods for machine learning, Mathematical Programming 134 (2012), 127–155. https://doi.org/10.1007/s10107-012-0572-5
D. P. Bertsekas, J. N. Tsitsiklis, Gradient convergence in gradient methods with errors, SIAM Journal on Optimization 10 (2000), 627–642. https://doi.org/10.1137/S1052623497331063
L. Bottou, O. Bousquet, The tradeoffs of large scale learning, Advances in Neural Information Processing Systems 20 (2008). https://papers.nips.cc/paper/3323-the-tradeoffs-of-large-scale-learning

8 thms3 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

On the Convergence of the Proximal Algorithm for Nonsmooth Functions Involving Analytic Features: Bounded Proximal Sequences of Łojasiewicz Functions Have Finite Length and a Critical LimitResearch Paper

Motivation

The proximal algorithm is the basic implicit scheme for minimizing a function $f$ : from the current point $x^k$ it moves to a minimizer of $f$ plus a quadratic penalty on the distance travelled. For convex $f$ its convergence theory is classical (Martinet 1970, Rockafellar 1976). For nonconvex, nonsmooth $f$ the situation is different: descent and boundedness give only that limit points are critical, and the whole sequence may fail to converge even for smooth $f$ (Palis–de Melo; Absil, Mahony and Andrews, SIAM J. Optim. 2005).

Attouch and Bolte (Math. Program. 116, 2009, online 2007; author's version hal-00803898) showed that the Łojasiewicz inequality, which holds for real-analytic functions and for continuous subanalytic functions, restores convergence of the whole sequence for the nonsmooth proximal algorithm, together with explicit rates. The argument is Łojasiewicz's original gradient-flow idea transferred to a discrete, nonsmooth setting. It became the template for the later convergence analyses of proximal alternating minimization, forward–backward splitting and PALM under the Kurdyka–Łojasiewicz property, which are used throughout nonconvex optimization, signal processing and machine learning.

Timeline:

1963: Łojasiewicz proves his gradient inequality for real-analytic functions and deduces convergence of bounded gradient trajectories.
2005: Absil, Mahony and Andrews prove convergence of descent methods for analytic cost functions.
2007: Bolte, Daniilidis and Lewis extend the inequality to nonsmooth subanalytic functions with the limiting subdifferential (SIAM J. Optim. 17).
2007/2009: Attouch and Bolte prove the result of this mission for the proximal algorithm.

Setting

Points live in $\mathbb R^n$ with the Euclidean norm $|\cdot|$ . Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ be proper (never $-\infty$ , finite somewhere) and lower semicontinuous, with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$ .

The limiting subdifferential $\partial f(x)$ is the set of limits $x^*$ of Fréchet subgradients $x_j^*\in\hat\partial f(x_j)$ along sequences $x_j\to x$ with $f(x_j)\to f(x)$ . A point with $0\in\partial f(x)$ is critical, and the set of critical points is $\operatorname{crit} f$ .

Fix $0<\lambda_-<\lambda_+<+\infty$ and step sizes $\lambda_k\in(\lambda_-,\lambda_+)$ . From an arbitrary $x^0$ the proximal algorithm produces

x^{k+1}\in\operatorname{argmin}\Big\{f(u)+\frac{1}{2\lambda_k}|u-x^k|^2 : u\in\mathbb R^n\Big\}.\qquad(2)

Any minimizer may be selected. The standing hypotheses are

(H1) $\inf_{\mathbb R^n} f>-\infty$ ;
(H2) the restriction of $f$ to $\operatorname{dom} f$ is continuous;
(H3) the Łojasiewicz property: for every critical point $\hat x$ there are $C,\varepsilon>0$ and $\theta\in[0,1)$ with

|f(x)-f(\hat x)|^\theta\le C|x^*|\qquad\forall x\in B(\hat x,\varepsilon),\ \forall x^*\in\partial f(x),\qquad(5)

with the convention $0^0=0$ (Remark 4). The number $\theta$ in (5) at a point is a Łojasiewicz exponent of that point.

$\omega(x^0)$ denotes the set of limit points of $(x^k)$ .

Formalization targets

Goal: Theorem 4 (convergence)

Under (H1), (H2), (H3), if $(x^k)$ is bounded then

\sum_{k=0}^{\infty}|x^{k+1}-x^k|<+\infty\quad\text{and}\quad x^k\to x^\infty\in\operatorname{crit} f.

It fixes no constants and holds for every admissible step sequence and every selection in (2).

Milestones

(3): $x^{k+1}=x^k-\lambda_k g^{k+1}$ with $g^{k+1}\in\partial f(x^{k+1})$ .
Proposition 2 (i)–(ii): $f(x^k)$ is nonincreasing and $\sum|x^{k+1}-x^k|^2<\infty$ .
Proposition 2 (iii): $\omega(x^0)\subset\operatorname{crit} f$ under (H2).
Proposition 2 (iv): for bounded $(x^k)$ , $\omega(x^0)$ is nonempty, compact and connected, and $d(x^k,\omega(x^0))\to0$ .
Lemma 3 (i): $f$ is constant on a connected set of critical points.
Lemma 3 (ii): (5) holds with common constants on $\{x: d(x,K)\le\varepsilon\}$ for compact connected $K\subset\operatorname{crit} f$ .
(8) and (9), the one-step and summed length estimates of the proof.

Further statements

Theorem 5 (rates): with $\theta$ a Łojasiewicz exponent of $x^\infty$ , $\theta=0$ gives finite termination, $\theta\in(0,\frac12]$ gives $|x^k-x^\infty|\le cQ^k$ with $Q\in[0,1)$ , and $\theta\in(\frac12,1)$ gives $|x^k-x^\infty|\le c\,k^{-(1-\theta)/(2\theta-1)}$ . Also: well-posedness of (2) under (H1), Proposition 2 (v), and Remark 2.

Significance

The theorem turns subsequential convergence into convergence of the whole sequence, with finite length, for a class that includes semi-algebraic, real-analytic and continuous subanalytic functions. Finite length is the property later used to analyse splitting and alternating schemes under the Kurdyka–Łojasiewicz property, and Theorem 5 is the first rate classification by the Łojasiewicz exponent for a nonsmooth algorithm.

The results are proved on paper. No machine-checked proof of Theorem 4 or Theorem 5 is known to exist. A formalization adds a checked convergence theorem for the nonsmooth proximal algorithm with extended-real-valued $f$ , and a reusable set of descent, limit-set and uniformization lemmas that apply to other Łojasiewicz-type analyses.

Difficulty

Descent and $\sum|x^{k+1}-x^k|^2<\infty$ give only $|x^{k+1}-x^k|\to0$ , which does not imply convergence: the iterates can circle a continuum of critical points with square-summable but non-summable steps, as in the counterexamples for smooth functions. The step that must be supplied is summability of $|x^{k+1}-x^k|$ itself. The local inequality (5) holds only near one critical point with its own constants, while the iterates approach a whole compact set $\omega(x^0)$ , so the local constants first have to be made uniform near that set. The nonsmooth setting adds two difficulties: $f$ takes the value $+\infty$ , and subgradients are limits of Fréchet subgradients, so their closure properties have to be established for this subdifferential.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $n=0$ is allowed. $f$ is EReal-valued and proper means never $\bot$ and somewhere not $\top$ . Lower semicontinuity is Mathlib's LowerSemicontinuous. (H2) is ContinuousOn f {x | f x ≠ ⊤}. The limiting subdifferential and $\operatorname{crit} f$ are the published platform definitions NonconvexSplitting.Shared.LimitingSubdiff and NonsmoothLojasiewicz.Continuous.crit. Algorithm (2) is a predicate on a sequence (every step is some minimizer), not a proximal map. Limit points are cluster points of the sequence. The power in (5) is lojPow θ s = if s = 0 then 0 else s ^ θ, which implements $0^0=0$ ; real values of $f$ are used only where $f$ is finite.

Standing assumptions carried by the goal and Theorem 5: $f$ proper and lower semicontinuous, (H1), (H2), (H3), $0<\lambda_-<\lambda_+$ with $\lambda_k\in(\lambda_-,\lambda_+)$ , a sequence complying with (2), and boundedness of its range. Milestones drop the assumptions their claims do not use. The milestones (8) and (9) also assume $x^{k+1}\ne x^k$ for all $k$ and use $\ell=\inf_k f(x^k)$ . Both come from the proof's normalization. This reduction is not a hypothesis of Theorem 4: a goal that assumed it, mentioned the constants $\theta,M,N_0,r$ , or assumed (8) would not be the paper's theorem.

The development needs the closure properties of the limiting subdifferential, the Fermat rule for proximal steps, and compactness and connectedness of limit sets of sequences with vanishing steps. These are reusable for every Łojasiewicz-type convergence proof. Proofs of individual milestones, of the rate lemmas in the proof of Theorem 5, and of the example $f(x)=|x|^2/2$ are welcome.

Selected references

H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116(1–2):5–16, 2009. https://doi.org/10.1007/s10107-007-0133-5 (author's version: https://hal.science/hal-00803898v1)
J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4):1205–1223, 2007. https://doi.org/10.1137/050644641
P.-A. Absil, R. Mahony, B. Andrews, Convergence of the iterates of descent methods for analytic cost functions, SIAM J. Optim. 16(2):531–547, 2005. https://doi.org/10.1137/040605266
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, pp. 87–89.

12 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Theoretical Computer Science·Captain: mikedeng1

Spectral Sparsification of Graphs 2: Every Graph with m Edges Has a (6 log_{4/3} 2m)⁻¹-Conductance Decomposition Cutting at Most Half of Its EdgesResearch Paper

Motivation

A sparse graph that approximates a dense one, in the sense that both have nearly the same Laplacian quadratic form, can stand in for it in every algorithm that only reads cuts or solves Laplacian linear systems. Spielman and Teng introduced such spectral sparsifiers and built them in nearly linear time; the construction is the sparsification step of their nearly-linear-time Laplacian solver (arXiv:0808.4134, SIAM J. Comput. 40(4), 2011).

Sampling edges at random works well only inside a graph of high conductance, where no vertex set is separated from the rest by few edges. A general graph is therefore first cut into pieces of high conductance, with few edges running between the pieces. Section 7 of the paper proves that such a decomposition always exists. A similar result was obtained independently by Trevisan (2005). The decomposition theorem, together with the sampling theorem of §6, already shows that every graph has a spectral sparsifier with $O(n\log^7 n)$ edges; the algorithmic decomposition of §8, which the fast algorithm uses, is an approximate version of it, and its analysis rests on the same certificate lemma.

Setting

Let $G=(V,E)$ be a finite simple undirected graph with $m=|E|$ edges, and write $d_i$ for the degree of vertex $i$ . For disjoint $S,T\subseteq V$ , $E(S,T)$ is the set of edges with one end in $S$ and one in $T$ . The volume of $S\subseteq V$ is $\operatorname{Vol}(S)=\sum_{i\in S}d_i$ ; in particular $\operatorname{Vol}(V)=2m$ .

For a vertex set $B\subseteq V$ and $S\subseteq B$ , the conductance of $S$ inside $B$ is

\Phi^G_B(S)=\frac{|E(S,B-S)|}{\min\big(\operatorname{Vol}(S),\operatorname{Vol}(B-S)\big)},\qquad \Phi^G_B(\emptyset)=1,

and the conductance of $B$ is $\Phi^G_B=\min_{S\subset B}\Phi^G_B(S)$ over proper subsets, with $\Phi^G_B=1$ when $|B|=1$ . Volumes are always measured with the degrees of $G$ , never with the degrees inside the induced subgraph $G(B)$ ; consequently $\Phi^G_B$ is at most the usual conductance of $G(B)$ , and lower bounds on $\Phi^G_B$ transfer to it.

A decomposition of $G$ is a partition $(A_1,\dots,A_k)$ of $V$ . It is a $\varphi$ -decomposition if $\Phi^G_{A_i}\ge\varphi$ for all $i$ , and its boundary is the set of edges between different parts,

\partial(A_1,\dots,A_k)=E\cap\bigcup_{i\neq j}(A_i\times A_j).

In Lean: vol G S, cutEdges G S T $=|E(S,T)|$ , condRel G B S $=\Phi^G_B(S)$ , cond G B $=\Phi^G_B$ , and decompBoundary G P $=\partial(A_1,\dots,A_k)$ for a Finpartition P of the vertex set, all in the namespace SpectralSparsify.Decomp.

Formalization targets

Goal: Theorem 7.1 (p. 17)

Every graph $G$ without isolated vertices has a decomposition $(A_1,\dots,A_k)$ with

\Phi^G_{A_i}\ \ge\ \big(6\log_{4/3}2m\big)^{-1}\quad\text{for all } i,\qquad |\partial(A_1,\dots,A_k)|\ \le\ \frac{|E|}{2}.

The constants are the paper's. Both conditions must hold for one and the same partition.

Milestones

(12), first inequality (p. 18): for $S\subseteq B$ , $R\subseteq B-S$ , $T=R\cup S$ , $|E(T,B-T)|\le|E(S,B-S)|+|E(R,B-S-R)|$ .
The volume bound proving (13) (p. 19): if $\operatorname{Vol}(R)\le\frac12\operatorname{Vol}(B-S)$ and $\operatorname{Vol}(S)=\alpha\operatorname{Vol}(B)$ , then $\operatorname{Vol}(R\cup S)\le\frac{1+\alpha}{2}\operatorname{Vol}(B)$ .
Lemma 7.2, Sparsest Cuts as Certificates (p. 18): let $\varphi\le1$ , and let $S\subset B$ maximize $\operatorname{Vol}(S)$ subject to (C.1) $\operatorname{Vol}(S)\le\operatorname{Vol}(B)/2$ and (C.2) $\Phi^G_B(S)\le\varphi$ . If $\operatorname{Vol}(S)=\alpha\operatorname{Vol}(B)$ with $\alpha\le1/3$ , then

\Phi^G_{B-S}\ \ge\ \varphi\,\frac{1-3\alpha}{1-\alpha}.

The $\varphi/3$ step (proof of Theorem 7.1, p. 19): under the hypotheses of Lemma 7.2 with $\operatorname{Vol}(S)\le\operatorname{Vol}(B)/4$ , $\Phi^G_{B-S}\ge\varphi/3$ .
The per-level cut bound (proof of Theorem 7.1, p. 19): for pairwise disjoint $B_1,\dots,B_r$ and $S_j\subset B_j$ satisfying (C.1) and (C.2) in $B_j$ with $\varphi\ge0$ , $\sum_j|E(S_j,B_j-S_j)|\le\varphi|E|$ .

Significance

The theorem says that every graph is, after removing at most half of its edges, a disjoint union of pieces of conductance $\Omega(1/\log m)$ . By Cheeger's inequality each piece then has normalized spectral gap $\Omega(1/\log^2 m)$ , which is the hypothesis under which the random sampling of §6 produces a spectral approximation; applying the theorem recursively to the removed edges gives the existence of spectral sparsifiers with $O(n\log^7 n)$ edges (§7.2). Decompositions of this kind, now called expander decompositions, have become a standard tool in graph algorithms.

The theorem is proved in the paper; to the knowledge of this mission it has no machine-checked proof. What the mission produces is a formal proof of the existence statement with the paper's explicit constant, a formal Lemma 7.2 (the certificate lemma that also drives the approximate version, Theorem 8.1), and reusable Lean definitions of volume, relative conductance $\Phi^G_B$ and decomposition boundary for finite simple graphs.

Difficulty

The obvious argument, cutting along any sparse set until no sparse set is left, controls the conductance of the final parts but not the number of edges cut: a long sequence of small sparse cuts can remove far more than half of the edges. The difficulty is to show that one well-chosen cut leaves a remainder whose conductance is certified without further search, which is the content of Lemma 7.2. Its hypothesis is a maximality condition over all subsets of $B$ , and its conclusion concerns all subsets of $B-S$ , a different set measured with the same ambient degrees, so the two cannot be compared directly. The existence statement then needs a well-founded description of the recursion, a bound on its depth, and an accounting of the cut edges level by level, all against the explicit constant $(6\log_{4/3}2m)^{-1}$ .

Formalization scope

Graphs are SimpleGraph V on a finite vertex type with decidable adjacency; vertex sets are Finset V; volumes, conductances and the bound on $|\partial|$ are real numbers; decompositions are Finpartition (Finset.univ : Finset V); $\log_{4/3}$ is Real.logb (4/3).

Hypotheses made explicit:

No isolated vertices (∀ v, 0 < G.degree v) in Theorem 7.1, Lemma 7.2 and the milestones that divide by a volume. The paper leaves it implicit: $\Phi^G_B(S)$ is $0/0$ for sets of isolated vertices, and with Lean's $0/0=0$ Lemma 7.2 would be false (one edge plus two isolated vertices is a counterexample). Under the hypothesis $m=0$ forces $V=\emptyset$ , and Theorem 7.1 is then trivially true.
$B$ nonempty in Lemma 7.2 and the $\varphi/3$ step, so that $\alpha=\operatorname{Vol}(S)/\operatorname{Vol}(B)$ is determined.
$\varphi\ge0$ in the per-level bound (the paper's $\varphi$ is positive).

Conventions: $\Phi^G_B$ is the minimum over proper subsets, the empty set contributing $1$ ; $\Phi^G_B=1$ for $|B|\le1$ ; $|E(S,T)|$ counts ordered adjacent pairs in $S\times T$ , which is the edge count for disjoint sets. Neither conclusion of Theorem 7.1 may be dropped: the partition into singletons satisfies the conductance bound and the partition into one part satisfies the boundary bound, so a formalization keeping only one conclusion is trivial.

Not formalized: idealDecomp as an object (step 2 involves a choice, so it is a relation rather than a function; the goal is the existence statement), its termination and depth bound as separate items, the λ-spectral decomposition remark via Cheeger's inequality, the existence sketch for sparsifiers in §7.2, and the algorithmic analogue of §8. Contributions welcome: proofs of the milestones, a formal recursion for idealDecomp, and lemmas on volume and edge-boundary arithmetic that other graph-partitioning missions can reuse.

Selected references

D. A. Spielman, S.-H. Teng, Spectral Sparsification of Graphs, arXiv:0808.4134v3, 2010; SIAM J. Comput. 40(4), 2011. https://arxiv.org/abs/0808.4134
L. Trevisan, Approximation algorithms for unique games, FOCS 2005, pp. 197–205; journal version Theory of Computing 4 (2008) 111–128. https://doi.org/10.4086/toc.2008.v004a005
D. A. Spielman, S.-H. Teng, Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems, STOC 2004, pp. 81–90. https://doi.org/10.1145/1007352.1007372

10 thms3 active usersReviewed

Completed

Graph Theory Linear algebra Probability+2·Captain: mikedeng1

Graph Sparsification by Effective Resistances 1: Sampling O(n log n/ε²) Edges by Effective Resistance Yields a (1±ε) Spectral Sparsifier with Probability 1/2Research Paper

Motivation

Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph $G$ is a graph $H$ on the same vertices with far fewer edges that approximates $G$ for the purpose at hand, so that the algorithm can be run on $H$ instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with $O(n\log n/\varepsilon^2)$ edges preserving the weight of every cut up to a factor $1\pm\varepsilon$ . Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had $O(n\log^c n)$ edges for a large constant $c$ and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.

Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of $O(n\log n/\varepsilon^2)$ edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained $O(n/\varepsilon^2)$ edges deterministically, by a slower method built on the same matrix $\Pi$ .

Setting

Let $G=(V,E,w)$ be a connected weighted undirected graph with $n=|V|$ vertices, $m=|E|$ edges and weights $w_e>0$ . Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).

The incidence matrix $B\in\mathbb R^{m\times n}$ has $B(e,v)=1$ if $v$ is the head of $e$ , $-1$ if $v$ is its tail, and $0$ otherwise; $b_e$ denotes its row for $e$ . $W$ is the diagonal $m\times m$ matrix with $W(e,e)=w_e$ .
The Laplacian is $L=B^{\mathsf T}WB$ , with quadratic form $x^{\mathsf T}Lx=\sum_e w_e\,(x(\mathrm{head}\,e)-x(\mathrm{tail}\,e))^2$ .
$L^{+}$ is the Moore–Penrose pseudoinverse of $L$ : if $L=\sum_{i=1}^{n-1}\lambda_iu_iu_i^{\mathsf T}$ over its nonzero eigenvalues, then $L^{+}=\sum_{i=1}^{n-1}\lambda_i^{-1}u_iu_i^{\mathsf T}$ .
The effective resistance of the edge $e$ is $R_e=b_eL^{+}b_e^{\mathsf T}$ : the potential difference across $e$ when a unit current enters at one end and leaves at the other, the edges being resistors of conductance $w_e$ .
$\Pi=W^{1/2}BL^{+}B^{\mathsf T}W^{1/2}$ is an $m\times m$ matrix with $\Pi(e,e)=w_eR_e$ .
Sparsify $(G,q)$ draws $q$ edges independently with replacement, the edge $e$ with probability $p_e=w_eR_e/\sum_f w_fR_f$ , and gives $e$ the weight $w_e/(qp_e)$ for each time it is drawn. Its output $H$ has Laplacian $\tilde L=B^{\mathsf T}W^{1/2}SW^{1/2}B$ , where $S$ is the random diagonal matrix with $S(e,e)=\#\{\text{draws of }e\}/(qp_e)$ .

Formalization targets

Goal: Theorem 1

There are an absolute constant $C$ and a threshold $N_0$ such that, for every $n\ge N_0$ , every connected weighted graph on $n$ vertices and every $1/\sqrt n<\varepsilon\le1$ , with $q=\lceil 9C^2n\log n/\varepsilon^2\rceil$ , with probability at least $1/2$

\forall x\in\mathbb R^n:\qquad (1-\varepsilon)\,x^{\mathsf T}Lx\;\le\;x^{\mathsf T}\tilde Lx\;\le\;(1+\varepsilon)\,x^{\mathsf T}Lx .

The constant $C$ is left unfixed; the statement asserts the shape $q=O(n\log n/\varepsilon^2)$ with the paper's explicit dependence on $C$ .

Milestones

Lemma 3 (four parts): $\Pi$ is an orthogonal projection; $\operatorname{im}\Pi=\operatorname{im}W^{1/2}B$ ; the eigenvalues of $\Pi$ are $1$ with multiplicity $n-1$ and $0$ with multiplicity $m-n+1$ ; $\Pi(e,e)=\|\Pi(\cdot,e)\|^2$ .
Lemma 4: for a nonnegative diagonal $S$ , $\|\Pi S\Pi-\Pi\Pi\|_2\le\varepsilon$ implies $(1-\varepsilon)x^{\mathsf T}Lx\le x^{\mathsf T}B^{\mathsf T}W^{1/2}SW^{1/2}Bx\le(1+\varepsilon)x^{\mathsf T}Lx$ for all $x$ .
Lemma 5 (Rudelson–Vershynin): for independent samples $y_1,\dots,y_q$ of a random vector with $\|y\|_2\le M$ and $\|\mathbb E\,yy^{\mathsf T}\|_2\le1$ , and $q\ge2$ ,

\mathbb E\Big\|\frac1q\sum_{j=1}^q y_jy_j^{\mathsf T}-\mathbb E\,yy^{\mathsf T}\Big\|_2\le CM\sqrt{\frac{\log q}{q}}\quad\text{whenever the right side is }<1.

Significance

Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with $O(n\log n/\varepsilon^2)$ edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to $1\pm\varepsilon$ , effective resistances, and the condition number of $L$ as a preconditioner, so any algorithm whose output depends on these quantities can run on $H$ . Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where $w_eR_e$ is exactly the statistical leverage of a row.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of $\Pi$ (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.

Difficulty

The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of $H$ equals $L$ , but bounding the deviation uniformly over all $x\in\mathbb R^n$ is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of $n$ in the sample count rather than $\log n$ . Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.

Formalization scope

All declarations sit in the namespace EffResSparsify.Sampling.

Graphs. A structure WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes $V\ne\emptyset$ . In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.
Pseudoinverse. $L^{+}$ is the matrix of the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on Euclidean $\mathbb R^V$ ; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of $Lx=y$ ".
Sampling. $p_e$ is defined as $w_eR_e/\sum_f w_fR_f$ ; the identity $\sum_f w_fR_f=n-1$ is part of the proof. An outcome of Sparsify is a sequence in $E^q$ with probability $\prod_i p_{s_i}$ , and probabilities and expectations are finite sums over $E^q$ , with no measure theory.
Norms and logarithms. $\|\cdot\|_2$ is the $\ell_2$ operator norm on matrices (Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; $\log$ is natural (the base is absorbed into $C$ ).
Constants. In Theorem 1, $\exists C>0,\ \exists N_0,\ \forall n\ge N_0$ precede the graph and $\varepsilon$ ; the sample count is $\lceil 9C^2n\log n/\varepsilon^2\rceil$ , rounded up because the printed value is not an integer. In Lemma 5, $\exists C>0$ precedes the dimension, the distribution, $M$ and $q$ .
Corrected statement. Lemma 5 as printed, with right side $\min(CM\sqrt{\log q/q},1)$ , is false (at $q=1$ the bound is $0$ ). The formal milestone is Rudelson and Vershynin's own Theorem 3.1: $q\ge2$ , and the bound $a=CM\sqrt{\log q/q}$ holds when $a<1$ . It is stated for finitely supported distributions, which is all Theorem 1 uses. Theorem 1 applies it with $a\le\varepsilon/2$ , so the correction does not affect the goal.
Not a trivialization. Theorem 1 does not take Lemma 5, a bound on $\mathbb E\|\Pi S\Pi-\Pi\|_2$ , or a free sample count as a hypothesis; a statement with any of these, or with " $\exists q$ " in place of $\lceil 9C^2n\log n/\varepsilon^2\rceil$ , is a different theorem.

Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.

Selected references

D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
M. Rudelson, R. Vershynin, Sampling from large matrices: an approach through geometric functional analysis, J. ACM 54(4), 2007. https://doi.org/10.1145/1255443.1255449
M. Rudelson, Random vectors in the isotropic position, J. Funct. Anal. 164(1), 1999. https://doi.org/10.1006/jfan.1998.3384
A. A. Benczúr, D. R. Karger, Approximating s-t minimum cuts in Õ(n²) time, STOC 1996. https://doi.org/10.1145/237814.237827
D. A. Spielman, S.-H. Teng, Spectral sparsification of graphs, SIAM J. Comput. 40(4), 2011 (arXiv:0808.4134). https://arxiv.org/abs/0808.4134
J. Batson, D. A. Spielman, N. Srivastava, Twice-Ramanujan sparsifiers, SIAM J. Comput. 41(6), 2012 (arXiv:0808.0163). https://arxiv.org/abs/0808.0163

9 thms3 active usersReviewed

Completed

Linear algebra Markov Chain Quantum Information·Captain: mikedeng1

Search via Quantum Walk 2: Phase Estimation Repeated k Times on the Szegedy Walk W(P) Fixes |π⟩ and Reflects A + B ⊖ |π⟩ up to Error 2^{1−k}Research Paper

Motivation

Many classical search algorithms are random walks: a Markov chain $P$ on a finite state space $X$ is run until it hits a marked state. Szegedy (2004) attached to every such chain a unitary quantum walk $W(P)$ , and Magniez, Nayak, Roland and Santha (SIAM J. Comput. 2011, arXiv:quant-ph/0608026) used it to search quadratically faster than the classical walk for every reversible ergodic chain. The search runs Grover-style rotations, and each rotation needs the reflection $\mathrm{ref}(\pi)$ about the stationary state $|\pi\rangle$ . Preparing $|\pi\rangle$ exactly can cost far more than one step of the walk, so the paper builds an approximate reflection $R(P)$ from the walk alone, by phase estimation. Theorem 6 of the paper is the guarantee for that circuit, and this mission formalizes it.

Timeline:

Jordan, 1875. Two subspaces of a Euclidean space decompose it into one- and two-dimensional invariant pieces ("principal angles").
Cleve, Ekert, Macchiavello and Mosca, 1998 (Proc. R. Soc. A). The phase-estimation circuit $C(U)$ and its output distribution (Theorem 5 of the paper).
Szegedy, 2004. The walk $W(P)$ , and its spectrum in terms of the singular values of the discriminant matrix (Theorem 4 of the paper).
Magniez, Nayak, Roland and Santha, 2007/2011. The circuit $R(P)$ and Theorem 6, the search algorithm (Theorem 7), and the bound $\Delta(P)\ge2\sqrt{\delta(P)}$ relating the phase gap to the eigenvalue gap.

Setting

$X$ is a finite set of size $n$ . A Markov chain is a row-stochastic matrix $P=(p_{xy})_{x,y\in X}$ . It is ergodic if some power of $P$ has all entries positive. A stationary distribution $\pi$ satisfies $\pi_x>0$ , $\sum_x\pi_x=1$ and $\sum_x\pi_xp_{xy}=\pi_y$ . The time-reversed chain $P^*$ is defined by $\pi_xp_{xy}=\pi_yp^*_{yx}$ , and $P$ is reversible if $P^*=P$ .

The space is $\mathcal H=\mathbb C^{X\times X}$ with basis $|x\rangle|y\rangle$ . Put $|p_x\rangle=\sum_y\sqrt{p_{xy}}\,|y\rangle$ and $|p^*_y\rangle=\sum_x\sqrt{p^*_{yx}}\,|x\rangle$ , and

\mathcal A=\mathrm{Span}(|x\rangle|p_x\rangle:x\in X),\qquad \mathcal B=\mathrm{Span}(|p^*_y\rangle|y\rangle:y\in X).

For a subspace $\mathcal K$ , $\mathrm{ref}(\mathcal K)=2\Pi_{\mathcal K}-\mathrm{Id}$ , where $\Pi_{\mathcal K}$ is the orthogonal projector onto $\mathcal K$ . The quantum walk is $W(P)=\mathrm{ref}(\mathcal B)\cdot\mathrm{ref}(\mathcal A)$ , and the stationary state is $|\pi\rangle=\sum_x\sqrt{\pi_x}\,|x\rangle|p_x\rangle$ .

The discriminant matrix is $D(P)=(\sqrt{p_{xy}p^*_{yx}})_{x,y}$ . Its singular values lie in $[0,1]$ . The phase gap $\Delta(P)$ is $2\theta$ , where $\theta$ is the smallest angle in $(0,\pi/2)$ such that $\cos\theta$ is a singular value of $D(P)$ .

The phase-estimation circuit $C(U)$ acts on $\mathbb C^\iota\otimes\mathbb C^{2^s}$ . It is

C(U)=(\mathrm{Id}\otimes F^\dagger)\Big(\sum_{j<2^s}U^j\otimes|j\rangle\langle j|\Big)(\mathrm{Id}\otimes H^{\otimes s}),

where $H^{\otimes s}$ is the Walsh–Hadamard matrix and $F$ is the $2^s$ -point Fourier transform.

The circuit $R(P)$ uses $s=\lceil\log_2(2\pi/\Delta(P))\rceil$ and acts on $\mathcal H\otimes(\mathbb C^{2^s})^{\otimes k}$ . It is built in three steps:

$V$ applies $C(W(P))$ $k$ times, each time to the system register and a fresh ancilla register.
$F_{\neq0}$ multiplies by $-1$ every basis state with a non-zero estimate in some register.
Then $R(P)=V^\dagger F_{\neq0}V$ .

Formalization targets

Goal: Theorem 6, properties 2 and 3

For $P$ ergodic and reversible on $n\ge2$ states, and every integer $k\ge0$ :

R(P)\,|\pi\rangle|0^{ks}\rangle=|\pi\rangle|0^{ks}\rangle,\qquad \big\|(R(P)+\mathrm{Id})\,|\psi\rangle|0^{ks}\rangle\big\|\le2^{1-k}\|\psi\|\quad(\psi\in\mathcal A+\mathcal B,\ \psi\perp|\pi\rangle).

Milestones

The milestones follow the order in which the paper's proof uses them:

Theorem 4 (Szegedy). The spectrum of $W(P)$ on $\mathcal A+\mathcal B$ . On that space $W(P)$ has the eigenvalues $1$ (on $\mathcal A\cap\mathcal B$ ), $-1$ , and $e^{\pm2i\theta}$ for $\cos\theta$ a singular value of $D(P)$ in $(0,1)$ , with matching multiplicities. The mission has two items for it: the full statement, and the direction the proof uses.
§3.2. For ergodic reversible $P$ , $|\pi\rangle$ is the only $1$ -eigenvector of $W(P)$ in $\mathcal A+\mathcal B$ , up to scalars, and every other eigenvalue $\mu$ there satisfies $|1-\mu|\ge|1-e^{i\Delta(P)}|$ .
Theorem 5, properties 2 and 3. $C(U)$ fixes $|\psi\rangle|0^s\rangle$ when $U\psi=\psi$ . If $U\psi=e^{2i\theta}\psi$ with $\theta\in(0,\pi)$ , it outputs $|\psi\rangle|\omega\rangle$ with $|\langle0^s|\omega\rangle|=|\sin(2^s\theta)|/(2^s\sin\theta)$ .
Single-copy bound. For $\Delta/2\le\theta\le\pi-\Delta/2$ and the $s$ above, $|\sin(2^s\theta)|/(2^s\sin\theta)\le1/2$ .
$k$ -copy bound. For $\psi\in\mathcal A+\mathcal B$ with $\psi\perp|\pi\rangle$ , the all-zero-estimate component $\psi_0$ of $V|\psi\rangle|0^{ks}\rangle$ has $\|\psi_0\|\le2^{-k}\|\psi\|$ . For every $\psi$ , $\|(R(P)+\mathrm{Id})|\psi\rangle|0^{ks}\rangle\|=2\|\psi_0\|$ .

Significance

Theorem 6 replaces the reflection about $|\pi\rangle$ with a circuit that only calls the walk. Its cost scales as $1/\Delta(P)$ rather than as the cost of preparing $|\pi\rangle$ . Combined with $\Delta(P)\ge2\sqrt{\delta(P)}$ , where $\delta(P)$ is the eigenvalue gap, this gives the search cost $S+\frac1{\sqrt\varepsilon}\big(\frac1{\sqrt\delta}U+C\big)$ of Theorem 7, up to logarithmic factors. The same approximate-reflection device recurs in later quantum-walk and amplitude-amplification algorithms.

The results are proved in the paper, which takes Theorem 4 from Szegedy and Theorem 5 from Cleve et al. As far as the platform index shows, none of Theorems 4, 5 or 6 has a machine-checked proof. The mission produces three reusable components: a Lean definition of the Szegedy walk and of the phase-estimation circuit, a formal Jordan-type spectral theorem for products of two reflections, and the analysis of phase estimation on an eigenvector.

Difficulty

Most of the work is linear algebra. The proof of Theorem 6 has a short outline: expand $\psi$ in eigenvectors of $W(P)$ , apply Theorem 5 to each, and bound each amplitude by $1/2$ . Three steps carry the weight:

Theorem 4. The eigen-decomposition of $W(P)$ on $\mathcal A+\mathcal B$ is Jordan's two-subspace decomposition, with the multiplicities read off the singular value decomposition of $D(P)$ . The decomposition has to be built, and the cases at singular values $0$ and $1$ have to be handled separately.
Uniqueness of $|\pi\rangle$ . This step needs ergodicity, through Perron–Frobenius, and reversibility, because $D(P)$ is then symmetric and its singular values are the moduli of the eigenvalues of $P$ . Without reversibility $D(P)$ can have the singular value $1$ twice, and property 3 then fails.
Repetition. The $k$ phase estimations share one system register. Their product acts on an eigenvector as a tensor power on the ancillas. This needs the eigenvectors of the unitary $W(P)$ restricted to the invariant subspace $\mathcal A+\mathcal B$ to be orthogonal.

Formalization scope

$\mathcal H$ is EuclideanSpace ℂ (X × X), with the first coordinate the first register.
The ancilla register is indexed by Fin (2^s), and $k$ registers by Fin k → Fin (2^s); the all-zeros state is the zero index.
$\mathrm{ref}(\mathcal K)$ is Mathlib's Submodule.reflection.
The stationary distribution $\pi$ is passed as data with its defining hypotheses. "Ergodic" is Matrix.IsPrimitive.
Singular values of the real matrix $D(P)$ are LinearMap.singularValues.
When $D(P)$ has no singular value in $(0,1)$ , the paper leaves $\Delta(P)$ undefined, and the formalization sets $\Delta(P)=\pi$ .
$\log_2$ is Real.logb 2 and the ceiling is Nat.ceil.

Deviations from the page.

Reversibility, the standing assumption of §3.2, is a hypothesis of the goal.
Property 3 is stated for vectors and is homogeneous in $\|\psi\|$ .
Theorem 5 is stated for any finite-dimensional unitary, not only $2^m\times2^m$ , and with $|\sin(2^s\theta)|$ , because the printed right-hand side can be negative.
The single-copy bound also covers the eigenvalue $-1$ .

Only exact statements are formalized. The cost halves (gate counts, calls to $c$ - $W(P)$ , " $s\in\log_2(1/\Delta)+O(1)$ ", the qubit count, uniformity) are out of scope.

The circuit $R(P)$ is the explicit composition above, built from $C(W(P))$ . It is neither "some circuit with properties 2–3" nor anything defined through the projector onto $|\pi\rangle$ , either of which would make the goal a tautology.

Contributions welcome: proofs of the milestones, Jordan's lemma for two subspaces as a standalone result, and the bound $\Delta(P)\ge2\sqrt{\delta(P)}$ of §3.3.

Selected references

F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1), 2011. https://arxiv.org/abs/quant-ph/0608026 (v4), https://doi.org/10.1137/090745854
M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004. https://doi.org/10.1109/FOCS.2004.53
R. Cleve, A. Ekert, C. Macchiavello, M. Mosca, Quantum algorithms revisited, Proc. R. Soc. Lond. A 454, 1998. https://doi.org/10.1098/rspa.1998.0164
C. Jordan, Essai sur la géométrie à n dimensions, Bull. Soc. Math. France 3, 1875. https://doi.org/10.24033/bsmf.90

11 thms3 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

Efficient Algorithms for Online Decision Problems 3: Follow the Lazy Leader (FLL, FLL) Matches FPL, FPL in Expectation Each Period and Updates with Probability at Most εAResearch Paper

Motivation

In an online linear decision problem a decision maker chooses, on each period $t = 1, 2, \dots$ , a decision $d_t$ from a set $\mathcal D \subset \mathbb R^n$ , and only then learns a state vector $s_t \in \mathcal S \subset \mathbb R^n$ and pays the cost $d_t \cdot s_t$ . The online shortest path problem, the experts problem, online binary search trees and list update are all of this form. Kalai and Vempala showed that a single offline optimisation oracle $M(s) = \operatorname{arg\,min}_{d \in \mathcal D} d \cdot s$ is enough to compete with the best fixed decision in hindsight: Follow the Perturbed Leader plays the leader of a randomly perturbed history (Kalai & Vempala 2005; the idea goes back to Hannan 1957).

Each period of FPL calls the oracle once and may change the decision. When an oracle call is expensive, or when switching decisions carries a cost (rotating a search tree, re-routing traffic), this is wasteful. The same paper introduces Follow the Lazy Leader: versions FLL and FLL* of FPL and FPL* that correlate the perturbations across periods so that the decision rarely changes, while each single period is distributed exactly as before. Lemma 1.2 of the paper is the statement that this works, and it is the result of this mission.

Setting

Vectors are elements of $\mathbb R^n$ ; $|x|_1 = \sum_i |x_i|$ , and $s_{1:t} = s_1 + \dots + s_t$ with $s_{1:0} = 0$ .

An argmin oracle for $\mathcal D$ is a map $M$ with $M(x) \in \mathcal D$ and $M(x) \cdot x \le d \cdot x$ for all $d \in \mathcal D$ . The decisions are assumed to have $L^1$ diameter at most $D$ , and the states satisfy $|s|_1 \le A$ for $s \in \mathcal S$ .
The states $s_1, s_2, \dots \in \mathcal S$ form a fixed sequence (an oblivious adversary).
For $\varepsilon > 0$ , $U$ is the uniform law on the cube $[0, 1/\varepsilon]^n$ and $\mu$ is the Laplace law with density $d\mu(x) = (\varepsilon/2)^n e^{-\varepsilon |x|_1}$ .

The four algorithms, period $t$ :

FPL( $\varepsilon$ ) plays $M(s_{1:t-1} + p)$ with $p \sim U$ ; FPL*( $\varepsilon$ ) does the same with $p \sim \mu$ .
FLL( $\varepsilon$ ) draws one offset $p \sim U$ at the start, which fixes the grid $G = \{p + \tfrac1\varepsilon z : z \in \mathbb Z^n\}$ , and plays $M(g_{t-1})$ , where the grid point $g_{t-1} = g(s_{1:t-1}, p)$ is the unique point of $G$ in $s_{1:t-1} + [0, 1/\varepsilon)^n$ .
FLL*( $\varepsilon$ ) draws $p_1 \sim \mu$ , plays $M(s_{1:t-1} + p_t)$ , and then sets $p_{t+1} = p_t - s_t$ with probability $\min\{1, d\mu(p_t - s_t)/d\mu(p_t)\}$ and $p_{t+1} = -p_t$ otherwise. Accepting keeps the evaluation point fixed: $s_{1:t} + p_{t+1} = s_{1:t-1} + p_t$ . The law of $p_t$ is written $\nu_t$ .

Formalization targets

Goal: Lemma 1.2 (p. 295)

For every period $t \ge 1$ :

\mathbb E_{p\sim U}\big[s_t \cdot M(g(s_{1:t-1}, p))\big] = \mathbb E_{p\sim U}\big[s_t \cdot M(s_{1:t-1} + p)\big], \qquad \Pr_{p\sim U}[g_{t-1} \ne g_t] \le \varepsilon A,

\mathbb E_{p_t\sim \nu_t}\big[s_t \cdot M(s_{1:t-1} + p_t)\big] = \mathbb E_{p\sim \mu}\big[s_t \cdot M(s_{1:t-1} + p)\big], \qquad \Pr\big[s_{1:t} + p_{t+1} \ne s_{1:t-1} + p_t\big] \le \varepsilon A .

The first line is the FLL half, the second the FLL* half. The constant $\varepsilon A$ is the paper's.

Milestones

Lemma 3.2 (p. 300): $U(\{x : x - v \in [0,1/\varepsilon]^n\}) \ge 1 - \varepsilon |v|_1$ .
The grid point is uniform (pp. 302–303): $g(x, p)$ with $p \sim U$ has the law of $x + p$ .
FLL update bound (p. 303): $\Pr_{p\sim U}[g(x,p) \ne g(x+v,p)] \le \varepsilon |v|_1$ .
Display (8) (p. 304): one FLL* update maps $\mu$ to $\mu$ .
Induction (p. 304): $\nu_t = \mu$ for every $t \ge 1$ .
Switching bound (p. 304): for any law of $p_t$ , $\Pr[p_{t+1} \ne p_t - v] \le \varepsilon |v|_1$ .

Significance

Lemma 1.2 transfers every guarantee proved for FPL and FPL* to FLL and FLL*: Theorem 1.1 of the paper bounds expected costs period by period, so equal per-period expectations give the same additive bound $\text{min-cost}_T + \varepsilon RAT + D/\varepsilon$ and the same multiplicative bound for the lazy algorithms. In addition, the expected number of oracle calls and decision changes over $T$ periods is at most $\varepsilon A T$ , which is $O(\sqrt T)$ at the usual tuning $\varepsilon \sim 1/\sqrt T$ . The paper uses this for online binary search trees with few rotations.

The result is proved in the paper. As far as is known there is no machine-checked proof of it. This mission produces a Lean statement of all four claims and of the six steps of the proof, against explicit Lean definitions of the grid point, the FLL* step and the law sequence $\nu_t$ . The uniformity of a random-grid point and the invariance of a Laplace law under a Metropolis-type step are reusable facts beyond online learning.

Difficulty

The FLL half asks for the exact law of the grid point $g(x, p)$ , a piecewise translation of $p$ whose pieces depend on $x$ . The page settles it in one line ("by symmetry"); in Lean it is an equality of push-forward measures, and the obvious attempt, a single change of variables $p \mapsto p + c$ , fails because the shift $c$ is different on different pieces of the cube.

The FLL* half is a statement about measures on $\mathbb R^n \times \mathbb R^n$ given as a mixture of point masses. The page argues with densities, pointwise in $x$ ; the formal statement is an equality of measures, with the update written as a Measure.bind against a kernel whose two branches move mass in different directions. The density computation of display (8) does not by itself give this equality.

Formalization scope

Vectors are Fin n → ℝ, $d \cdot s$ is dotProduct, $|x|_1$ is written out as ∑ i, |x i|. States are indexed from 1; s 0 is unused.
$s_{1:t}$ is prefixSum and $U$ is perturbLaw n ε from the published definition OracleRO.ApproxFPL.FPL. The oracle is the predicate IsArgminOracle Dset M, and every statement holds for every such $M$ .
The Laplace law laplaceLaw n ε carries its normalising constant $(\varepsilon/2)^n$ , so it is a probability measure for $\varepsilon > 0$ .
The grid point fllGridPoint ε x p is the explicit formula $p_i + \lceil \varepsilon(x_i - p_i) \rceil / \varepsilon$ . It is the unique grid point in the half-open cube for $\varepsilon > 0$ , and it is measurable. The half-open and closed cubes differ by a null set, and the closed-cube law is used throughout.
The FLL* update is the joint law fllStarJoint ε v ν of $(p_t, p_{t+1})$ , built with Measure.bind and Measure.dirac. The acceptance probability is $\min\{1, e^{-\varepsilon(|p-v|_1 - |p|_1)}\}$ . The law fllStarLaw ε s t is the recursion started at $\mu$ , not $\mu$ itself.
"Performing an update" on period $t$ means $g_{t-1} \ne g_t$ for FLL and $s_{1:t} + p_{t+1} \ne s_{1:t-1} + p_t$ for FLL*.
Hypotheses not on the page: measurability of $M$ and $\varepsilon > 0$ .

The formalization rules out the following trivializations:

the grid point is not a Classical.choose;
the integrands are bounded and measurable, because $M$ maps into a set of finite diameter, so the expectations are not the junk value $0$ of a non-integrable function;
$\nu_t$ is defined by the chain and not as $\mu$ , so claim 3 does not compare a law with itself;
FLL's grid point is compared with FPL's point $s_{1:t-1} + p$ , not with itself.

Welcome contributions:

the uniformity of $x + ((p - x) \bmod L)$ under the uniform law on a box;
Measure.bind lemmas for finite mixtures of Dirac kernels;
the change of variables for the Laplace density under reflection and shift.

Selected references

A. Kalai, S. Vempala, Efficient algorithms for online decision problems, Journal of Computer and System Sciences 71(3):291–307, 2005. https://doi.org/10.1016/j.jcss.2004.10.016
J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III, Annals of Mathematics Studies 39, 97–139, 1957. https://doi.org/10.1515/9781400882151-005
A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-based robust optimization via online learning, Operations Research 63(3):628–638, 2015. https://doi.org/10.1287/opre.2015.1374

11 thms3 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

Search via Quantum Walk 1: Recursive Amplitude Amplification with Approximate Reflections R(βᵢ), βᵢ = 18γ/(4π³i²), Finds a Marked Element with Probability at Least 1/12 − 3γResearch Paper

Motivation

Grover's algorithm finds a marked element among $N$ with $O(\sqrt N)$ queries by alternating two reflections: one about the initial state and one that flips the sign of marked states. In quantum-walk search, the initial state $|\pi\rangle$ encodes the stationary distribution of a Markov chain, and the reflection about $|\pi\rangle$ is too expensive to implement exactly. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026, SIAM J. Comput. 2011) obtain the reflection approximately, by phase estimation on the quantum walk, and need a search procedure that tolerates the approximation error without paying extra cost to reduce it. Their Section 4 supplies one: a variant of the recursive amplitude amplification (RAA) of Høyer, Mosca and de Wolf (ICALP 2003) in which the reflection about $|\pi\rangle$ is replaced, at recursion level $i$ , by an approximate circuit of precision $\beta_i=\frac{18}{4\pi^3}\gamma/i^2$ . The two lemmas of that section, stated "in full generality for potential further applications" (p. 11), are the exact engine of the paper's headline Theorem 3 (search with cost $S+\frac1{\sqrt\varepsilon}(\frac1{\sqrt\delta}U+C)$ ).

Timeline: Grover (1996) gives quadratic speedup for unstructured search; Brassard, Høyer, Mosca and Tapp (2002) generalize it to amplitude amplification; Høyer, Mosca and de Wolf (2003) introduce RAA to tolerate a bounded-error marking reflection; Szegedy (2004) defines quantum walks for arbitrary reversible chains with detection guarantees; Magniez, Nayak, Roland and Santha (STOC 2007, SIAM 2011) adapt RAA to an approximate initial-state reflection and obtain search, not only detection, for every reversible ergodic chain.

Setting

Let $X$ be a finite set and $M\subseteq X$ a set of marked elements. The state space is $\mathcal H=\mathbb C^{X\times X}$ . The initial state $|\pi\rangle\in\mathcal H$ is any unit vector (Lemmas 1 and 2 never use its quantum-walk form), and the marked weight is $p_M=\|\Pi_M|\pi\rangle\|^2$ , where $\Pi_M$ projects onto the basis states $|x\rangle|y\rangle$ with $x\in M$ .

For each level $i\ge1$ an extra register $K_i$ (a finite-dimensional space with a basis state $|0\rangle$ ) is given together with a unitary $R_i$ on $\mathcal H\otimes K_i$ , playing the role of $R(\beta_i)$ :

R_i|\pi\rangle|0\rangle=|\pi\rangle|0\rangle,\qquad \|(R_i+\mathrm{Id})|\psi\rangle|0\rangle\|\le\beta_i\|\psi\|\ \text{ whenever }\langle\pi|\psi\rangle=0 .

On $\mathcal H\otimes K_1\otimes\cdots\otimes K_T$ the marked subspace $\tilde{\mathcal M}$ consists of states whose first register is marked, and $\mathrm{ref}(\tilde{\mathcal M}^\perp)=\mathrm{Id}-2\Pi_{\tilde M}$ .

Approximate RAA $(i,\gamma)$ is the unitary $A_i$ with $A_0=\mathrm{Id}$ and

A_i=A_{i-1}\cdot O_i\cdot A_{i-1}^\dagger\cdot\mathrm{ref}(\tilde{\mathcal M}^\perp)\cdot A_{i-1},

where $O_i$ multiplies by $-1$ every basis state in which some register $K_j$ , $j<i$ , is not $|0\rangle$ , and otherwise applies $R_i$ to $\mathcal H\otimes K_i$ . Write $|\varphi_i\rangle=A_i|\pi\rangle|0^S\rangle$ and $\sin\phi_i=\|\Pi_{\tilde M}|\varphi_i\rangle\|$ .

Tolerant RAA $(t_{\max},\gamma)$ first samples $x$ (succeeding with probability $p_M$ ); otherwise, for $i=1,\dots,t_{\max}$ , it applies $A_i$ to the state left over from the previous failed measurement, $|\psi_i\rangle=A_i|\nu^\perp_{i-1}\rangle$ with $|\nu^\perp_0\rangle=|\pi\rangle|0^S\rangle$ , and measures $\{\Pi_{\tilde M},\mathrm{Id}-\Pi_{\tilde M}\}$ ; a failure collapses the state to $|\nu_i^\perp\rangle=\Pi_{\tilde M^\perp}|\psi_i\rangle/\|\Pi_{\tilde M^\perp}|\psi_i\rangle\|$ .

Formalization targets

Goal: Lemma 2 (p. 15)

Let $0<\gamma\le1/40$ , let $\varepsilon>0$ satisfy $p_M\ge\varepsilon$ whenever $p_M>0$ , and let $t_{\max}$ be the smallest non-negative integer with $3^{t_{\max}}\sin^{-1}\sqrt\varepsilon\in[\pi/4,3\pi/4]$ . The probability $P_{\rm succ}$ that Tolerant RAA $(t_{\max},\gamma)$ ends with a marked element satisfies

M=\emptyset\Rightarrow P_{\rm succ}=0,\qquad p_M>0\Rightarrow P_{\rm succ}\ge\frac1{12}-3\gamma .

Lemma 1 (p. 12)

With $t$ the smallest non-negative integer such that $3^t\sin^{-1}\sqrt{p_M}\in[\pi/4,3\pi/4]$ , for every $\gamma>0$ ,

\|\Pi_{\tilde M}A_t|\pi\rangle|0^S\rangle\|\ge\frac1{\sqrt2}-\gamma .

Milestones

In the order of the proofs: Fact 1 (the error operator $E_i=A_{i-1}O_iA_{i-1}^\dagger-\mathrm{ref}(\varphi_{i-1})$ kills $|\varphi_{i-1}\rangle$ and has norm $\le\beta_i$ on states with clean registers $K_{\ge i}$ ); the one-level bound $|\sin\phi_{i+1}-\sin3\phi_i|\le\beta_{i+1}|\sin2\phi_i|$ ; the two trigonometric inequalities on $[0,\pi/4]$ ; the surrogate bound $\tilde e_i\le\gamma\bar\phi_i/\pi\le\gamma$ ; Lemma 1; the three terms of the drift recursion (5); and the accumulated drift $\delta_t=\||\psi_t\rangle-|\varphi_t\rangle\|\le\pi/8+9\gamma/8$ .

Significance

Lemma 2 turns any family of approximate reflections whose error decays like $1/i^2$ into a search procedure that succeeds with constant probability, needs only a lower bound $\varepsilon$ on $p_M$ , and costs $O(3^{t_{\max}})=O(1/\sqrt\varepsilon)$ calls. Combined with the phase-estimation reflection of the paper's Theorem 6 it yields Theorem 3, the general quantum-walk search theorem that has become the standard tool for walk-based algorithms (element distinctness, triangle finding, group commutativity). Nothing in the lemma refers to Markov chains, so it applies to any setting with an approximate reflection about the initial state.

The results are proved in the paper. None of them is machine-checked: the platform holds a formal Grover search with one marked basis state and exact reflections, but no amplitude amplification with approximate or recursive reflections. A formal proof would also settle the steps the paper passes over quickly, notably that the trigonometric inequalities, claimed for angles in $[0,\pi/4]$ , are applied to the actual angles $\phi_i$ , which may exceed $\pi/4$ by $O(\gamma)$ at the last level.

Difficulty

The ideal analysis (every reflection exact, angle tripled at each level) is a two-dimensional rotation argument. With approximate reflections the state leaves the plane spanned by $|\mu_0\rangle$ and $|\mu_0^\perp\rangle$ , and each level both triples the error already present and injects a new one; the errors stay bounded only because $\sum_i\beta_i$ converges and the injection at level $i$ is weighted by $\sin2\phi_i$ . Fact 1 is not a restatement of the hypothesis on $R(\beta)$ : it holds only because step 4 flips the phase of states whose earlier registers are dirty, and because $A_{i-1}$ never touches $K_{\ge i}$ . In Lemma 2 the attempts reuse the leftover state, not a fresh $|\pi\rangle|0^S\rangle$ , so the state at the decisive attempt $t$ has drifted; bounding the drift needs the normalised unmarked parts $|\mu_k^\perp\rangle$ to move little from level to level, which again depends on the error bounds of Lemma 1.

Formalization scope

$\mathcal H\otimes K_1\otimes\cdots\otimes K_T$ is EuclideanSpace ℂ (X × X × ((j : Fin T) → κ (j+1))); operators are complex matrices. Registers are 0-based in Lean (index $j$ is $K_{j+1}$ ).
$R_i$ is required only at the precisions $\beta_i$ actually used, which is weaker than the paper's "for any $\beta>0$ ". Property 3 is stated in the homogeneous form $\le\beta_i\|\psi\|$ .
"Undo" is the conjugate transpose. $t$ and $t_{\max}$ are explicit naturals with "satisfies the condition and no smaller one does". $\sin^{-1}$ is Real.arcsin; the interval is closed.
The success probability of Tolerant RAA is defined from the measurement rule, $p_M+(1-p_M)\big(1-\prod_{i=1}^{t_{\max}}(1-\|\Pi_{\tilde M}|\psi_i\rangle\|^2)\big)$ , with post-measurement states computed from the actual $|\psi_i\rangle$ ; registers are not reset. The classical sample succeeds with probability $\|\Pi_M|\pi\rangle\|^2$ , which is $\sum_{x\in M}\pi_x$ in the paper's walk setting.
" $M$ non-empty" in Lemma 2 is read as $p_M>0$ , as in the paper's proof. Edge-case hypotheses: $\|\pi\|=1$ ; $\phi_i\le\pi/3$ in the one-level bound (so $\sin3\phi_i\ge0$ ); $p_M<1$ in the last drift term; $1\le i<t$ and $T\ge t$ in the drift bounds.
Cost is not formalized: property 1 of $R(\beta)$ , the cost $c_2$ of $-\mathrm{ref}(M)$ and every "incurs a cost of order" clause are out of scope. The data-structure subscript $d$ is omitted, as in the paper's own error analysis.
A formalization in which step 4 applies an exact reflection about $|\pi\rangle$ or $|\varphi_{i-1}\rangle$ , or in which the success probability is computed from ideal angles instead of the actual states, would make the lemmas statements about exact RAA; the definitions apply the given $R_i$ and measure the actual states.

Contributions welcome: proofs of the trigonometric milestones and of $\tilde e_i\le\gamma\bar\phi_i/\pi$ (pure real analysis), Fact 1 (finite-dimensional linear algebra with a block structure on registers), and the vector inequality $\|u/\|u\|-v/\|v\|\|\le2\|u-v\|/\|v\|$ that the drift bounds share. The register and controlled-unitary infrastructure is reusable for other recursive quantum algorithms.

Selected references

F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1), 2011; arXiv:quant-ph/0608026v4. https://arxiv.org/abs/quant-ph/0608026
P. Høyer, M. Mosca, R. de Wolf, Quantum search on bounded-error inputs, ICALP 2003. https://arxiv.org/abs/quant-ph/0304052
G. Brassard, P. Høyer, M. Mosca, A. Tapp, Quantum amplitude amplification and estimation, Contemp. Math. 305, 2002. https://arxiv.org/abs/quant-ph/0005055
L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. https://arxiv.org/abs/quant-ph/9605043
M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004. https://doi.org/10.1109/FOCS.2004.53

14 thms3 active usersReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Stochastic Machine Scheduling with Precedence Constraints 2: LP-Based Graham List Scheduling Is a (2 − 1/m + max{1, (m − 1)Δ/m})-Approximation for P|in-forest|E[Σ w_j C_j]Research Paper

Motivation

Scheduling jobs whose durations are uncertain is the normal situation in project management, manufacturing and computing: a job's processing time becomes known only when the job finishes, but a distribution for it is available in advance. Stochastic machine scheduling models this by random, independent processing times $P_j$ and asks for a scheduling policy, a rule that decides online which jobs to start, using only the information observed so far, that minimizes the expected total weighted completion time $\mathrm E[\sum_j w_jC_j]$ . Optimal policies are known only in a few special cases, and they can depend on the full conditional distributions of the remaining processing times, so the research focus has been on simple policies with provable performance guarantees.

Skutella and Uetz (SIAM J. Comput. 34(4), 2005) gave the first constant-factor guarantees for stochastic parallel-machine scheduling with precedence constraints. Their policies are list scheduling policies whose priority list comes from an optimal solution of a linear program built on the load inequalities of Möhring, Schulz and Uetz (J. ACM 46(6), 1999). This mission formalizes their second main result: for in-forest precedence constraints and no release dates, plain Graham list scheduling in LP order is a $(2-\tfrac1m+\max\{1,\tfrac{m-1}{m}\Delta\})$ -approximation.

Timeline.

1966/1969: Graham shows list scheduling is a $(2-1/m)$ -approximation for the makespan with precedence constraints, for any list.
1999: Möhring, Schulz and Uetz prove the load inequalities for nonanticipatory policies and obtain constant guarantees for $P\,|\,r_j\,|\,\mathrm E[\sum w_jC_j]$ without precedence constraints.
2001: Chekuri, Motwani, Natarajan and Stein give, among other results, a 2-approximation for deterministic in-tree scheduling by list scheduling (their Lemma 4.16 contains the deterministic counterpart of Lemma 4.3 below).
2005: Skutella and Uetz extend these ideas to stochastic processing times with precedence constraints (Theorem 4.1, general precedence; Theorem 4.5, in-forests).

Setting

There are a finite set $V$ of jobs, $m\ge1$ identical parallel machines, and nonnegative weights $w_j$ . Jobs are processed nonpreemptively; each machine handles one job at a time. Precedence constraints form an acyclic digraph $(V,A)$ : an arc $(i,j)$ means $j$ starts only after $i$ completes. The constraints form an in-forest if each job has at most one successor. There are no release dates.

The processing times $P_j\ge0$ are independent random variables. A realization is a vector $p$ ; a schedule assigns start times $S_j$ , with completion times $C_j=S_j+p_j$ ; it is feasible if it respects precedence and at most $m$ jobs are in process at any time. A policy $\Pi$ maps each realization to a feasible schedule, and it is nonanticipatory if what it has started by time $t$ depends only on what has been observed by $t$ (the processing times of completed jobs and which jobs are still running).

With $\mu_j=\mathrm E[P_j]$ and $\Delta\ge0$ a common bound with $\operatorname{Var}[P_j]\le\Delta\mu_j^2$ (i.e. $\mathrm{CV}[P_j]\le\sqrt\Delta$ ), define

f(W)=\frac1{2m}\Big(\Big(\sum_{j\in W}\mu_j\Big)^2+\sum_{j\in W}\mu_j^2\Big)-\frac{(m-1)(\Delta-1)}{2m}\sum_{j\in W}\mu_j^2 .

The LP-relaxation minimizes $\sum_jw_jC^{\mathrm{LP}}_j$ subject to $\sum_{j\in W}\mu_jC^{\mathrm{LP}}_j\ge f(W)$ for all $W\subseteq V$ , $C^{\mathrm{LP}}_j\ge C^{\mathrm{LP}}_i+\mu_j$ for arcs $(i,j)$ , and $C^{\mathrm{LP}}_j\ge\mu_j$ . A priority list $L$ sorts the jobs by nondecreasing $C^{\mathrm{LP}}_j$ ; $B_j$ is the set of jobs up to and including $j$ in $L$ , and $A_j$ the jobs after $j$ .

Graham's list scheduling starts, at every decision time, as many available jobs as possible in the order of $L$ . For a schedule, a critical predecessor of $j$ is a predecessor that completes last among $j$ 's predecessors, at a positive time; following critical predecessors backwards gives the critical chain of $j$ , whose total processing time is $\ell_j(p)$ .

Formalization targets

Goal: Theorem 4.5

For every feasible nonanticipatory policy $\Pi$ ,

\mathrm E\Big[\sum_jw_jC^{\mathrm{Graham}}_j(P)\Big]\ \le\ \Big(2-\frac1m+\max\Big\{1,\frac{m-1}m\Delta\Big\}\Big)\,\mathrm E\Big[\sum_jw_jC^\Pi_j(P)\Big].

Milestones

Lemma 4.3: in Graham's schedule for an in-forest, no job of $A_j$ is processed during $[r_j(p),S_j(p)[$ .
Lemma 4.4: $\mathrm E[C_j(P)]\le\frac{m-1}m\mathrm E[\ell_j(P)]+\frac1m\sum_{i\in B_j}\mathrm E[P_i]$ , together with its per-realization form.
Theorem 3.1: the load inequalities $\sum_{j\in W}\mathrm E[P_j]\mathrm E[C^\Pi_j(P)]\ge f(W)$ for every nonanticipatory $\Pi$ .
§3 LP-relaxation: the expected completion times of any policy are LP-feasible.
Lemma 3.3: $\frac1m\sum_{k\in B_j}\mu_k\le(1+\max\{1,\frac{m-1}m\Delta\})C^{\mathrm{LP}}_j$ .
Critical-chain lower bound (§4, p. 798): $\ell_j(p)\le C_j(p)$ in every feasible schedule.

Significance

The theorem gives a constant performance guarantee for stochastic in-forest scheduling, uniform in the distributions once their coefficients of variation are bounded. For NBUE distributions (exponential, uniform, Erlang, …), where $\Delta=1$ , the guarantee is $3-1/m$ , compared with $3+2\sqrt2$ for general precedence constraints and release dates with Algorithm CMNS (Table 1, p. 792). The analysis shows that for in-forests, deliberate idle time is unnecessary: Lemma 4.3 replaces it.

The result is proved in the paper, partly by reference: Theorem 3.1 and Lemma 3.3 are cited from Möhring, Schulz and Uetz. To our knowledge none of these results has a machine-checked proof. A complete formalization requires the load inequalities of stochastic scheduling, which are of independent use for every LP-based stochastic scheduling result, and a reusable treatment of list schedules, critical chains and nonanticipatory policies.

Difficulty

Two parts carry the weight. The first is the load inequalities (Theorem 3.1): they hold for nonanticipatory policies only, because a policy's start time of job $j$ must be independent of $P_j$ ; turning the informal "dynamic view" of policies into a statement that yields this independence, and then the variance bookkeeping, is the probabilistic core. The second is Lemma 4.3: the naive argument "a waiting job of high priority blocks lower-priority jobs" fails for general precedence constraints, where Graham's algorithm can be arbitrarily bad; the in-forest structure is used through a counting argument at time $r_j(p)$ , in which the critical predecessors of the jobs started at that time must be distinct.

Formalization scope

Lean represents jobs by a Fintype V, precedence by a relation A : V → V → Prop with acyclic transitive closure, and in-forests by "at most one outgoing arc". Schedules are start-time vectors in ℝ, with machine capacity by counting jobs in process on half-open intervals. Policies are maps from realizations to start times with an explicit nonanticipation condition. Graham's list scheduling is characterized by rules (feasibility, greedy, list order, decision times); critical chains are taken for every admissible tie-breaking selector. The CV bound includes $\mathrm E[P_j^2]<\infty$ and $\mathrm E[P_j]>0$ . Zero processing times are allowed.

Standing assumptions and disclosed additions: processing times are independent and nonnegative; the comparator policies have integrable completion times; the completion times and critical-chain lengths of Graham's schedule are assumed almost-everywhere measurable (the paper asserts measurability in §5 without proof); " $\alpha$ -approximation" is stated against every comparator policy rather than an optimal one.

A trivializing formalization is ruled out: the comparator ranges over every feasible nonanticipatory policy with integrable completion times, $C^{\mathrm{LP}}$ is optimal over all load inequalities $W\subseteq V$ , and the Graham family must satisfy the rules for every nonnegative realization.

Welcome contributions: the load inequalities, existence and measurability of Graham schedules, and general lemmas on list schedules.

Selected references

M. Skutella and M. Uetz, Stochastic machine scheduling with precedence constraints, SIAM J. Comput. 34(4) (2005) 788–802. https://doi.org/10.1137/S0097539702415007
R. H. Möhring, A. S. Schulz and M. Uetz, Approximation in stochastic scheduling: the power of LP-based priority policies, J. ACM 46(6) (1999) 924–942. https://doi.org/10.1145/331524.331530
C. Chekuri, R. Motwani, B. Natarajan and C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1) (2001) 146–166. https://doi.org/10.1137/S0097539797327180
R. L. Graham, Bounds on multiprocessing timing anomalies, SIAM J. Appl. Math. 17(2) (1969) 416–429. https://doi.org/10.1137/0117039
R. H. Möhring, F. J. Radermacher and G. Weiss, Stochastic scheduling problems I: General strategies, Z. Oper. Res. 28 (1984) 193–260. https://doi.org/10.1007/BF01919323

11 thms3 active usersReviewed

Convex Optimization Linear algebra Machine Learning+1·Captain: mikedeng1

Nuclear-Norm Penalization and Optimal Rates for Noisy Low-Rank Matrix Completion 2: If λ ≥ 3‖M‖∞ on a Linear Subspace, a Sharp Oracle Inequality with the Restricted Constant μ₅(A)Research Paper

Motivation

Estimating a large matrix that is approximately low rank from a few noisy linear measurements is a basic problem of high-dimensional statistics. It covers matrix completion (recovering a ratings table from a small sample of entries), multi-task regression and quantum state tomography. The standard estimator penalizes the nuclear norm, the sum of the singular values, which is the convex surrogate of the rank. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a variant of this estimator that uses the known distribution of the design. Their Theorem 1 proves sharp oracle inequalities, with leading constant 1, under a global isometry condition on the design (Assumption 1).

Global isometry is a strong requirement. For sparse vectors, the analogous requirement was relaxed to the restricted eigenvalue condition of Bickel, Ritov and Tsybakov (Ann. Statist. 37, 2009), which only asks for curvature on a cone of approximately sparse directions. The random-design version is due to Koltchinskii (Bernoulli 15, 2009), and a matrix version of the cone appears in Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731). Theorem 2 of the paper is the matrix counterpart of the restricted eigenvalue analysis for this estimator. It keeps the leading constant 1, and the price is a stronger tuning condition, λ ≥ 3‖M‖∞ instead of 2‖M‖∞. Section 5.4 of the same paper derives from it a sharp sparsity oracle inequality for the ordinary vector Lasso.

Setting

Observe n pairs (Xᵢ, Yᵢ), i = 1, …, n, where Xᵢ is a random m₁ × m₂ real matrix and Yᵢ a real random variable, satisfying the trace regression model

\mathbb E(Y_i \mid X_i) = \operatorname{tr}(X_i^\top A_0),

for an unknown matrix A₀. Write ⟨A, B⟩ = tr(AᵀB), and let ‖A‖₁, ‖A‖₂ and ‖A‖∞ be the nuclear, Frobenius and operator norms, the last being the largest singular value. The design enters through the bilinear form

\langle A, B\rangle_{L_2(\Pi)} = \frac1n\sum_{i=1}^n \mathbb E\big(\langle A, X_i\rangle\langle B, X_i\rangle\big),

with semi-norm ‖A‖_{L₂(Π)}. Two random objects are built from the sample: the noise matrix M = (1/n) Σᵢ (YᵢXᵢ − 𝔼(YᵢXᵢ)), and, for λ > 0 and a set 𝔸 of matrices, the estimator Â^λ, any minimizer over 𝔸 of

L_n(A) = \|A\|_{L_2(\Pi)}^2 - \Big\langle \frac2n\sum_{i=1}^n Y_iX_i, A\Big\rangle + \lambda\|A\|_1 .

Let A = Σ_{j≤r} σⱼ uⱼvⱼᵀ be a singular value decomposition, with support (S₁, S₂), the spans of the uⱼ and of the vⱼ. Write 𝒫_A⊥(B) = P_{S₁⊥} B P_{S₂⊥} for the part of B orthogonal to both singular spaces, and 𝒫_A(B) = B − 𝒫_A⊥(B). When 𝔸 is a linear subspace and c₀ ≥ 0, the cone ℂ_{A,c₀} consists of the B ∈ 𝔸 with ‖𝒫_A⊥(B)‖₁ ≤ c₀‖𝒫_A(B)‖₁. The restricted constant μ_{c₀}(A) is the infimum of the μ′ > 0 such that ‖𝒫_A(B)‖₂ ≤ μ′‖B‖{L₂(Π)} for every B ∈ ℂ{A,c₀}. The paper uses μ(A) := μ₅(A).

Formalization targets

Goal: Theorem 2, (2.19)

Let 𝔸 be a linear subspace. If λ ≥ 3‖M‖∞, then

\|\hat A^\lambda - A_0\|_{L_2(\Pi)}^2 \le \inf_{A \in \mathbb A}\Big[\|A - A_0\|_{L_2(\Pi)}^2 + \lambda^2\mu^2(A)\operatorname{rank}(A)\Big].

The bound is deterministic: it holds for every realization of the sample on which λ ≥ 3‖M‖∞. A₀ need not lie in 𝔸, and nothing is assumed about the design beyond what makes the objects finite.

Milestones

The milestones are the displays of the proof, in the order the proof uses them:

(2.8), the inequality obtained from the first-order optimality condition of the estimator, which the proof of Theorem 1 already uses;
(2.20), in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0;
(2.21), the splitting of ⟨M, Â^λ − A⟩ along 𝒫_A and 𝒫_A⊥;
(2.22), the inequality (λ − 2Δ)‖𝒫_A⊥(Â^λ − A)‖₁ ≤ (λ + 2Δ)‖𝒫_A(Â^λ − A)‖₁ with Δ = ‖M‖∞;
the membership Â^λ − A ∈ ℂ_{A,5} and the resulting bound by μ(A);
the final two-step display with the constant 1 + 2√2/3.

Significance

Theorem 2 gives a sharp oracle inequality whose only design-dependent quantity is a restricted constant. That constant is finite in situations where the global isometry of Theorem 1 fails. The result covers every linear subspace 𝔸, for example all matrices, the diagonal matrices or matrices with a prescribed sparsity pattern. In the diagonal case it becomes a sharp sparsity oracle inequality for the vector Lasso under a restricted eigenvalue condition (the paper's Theorem 14). The oracle inequalities of Bickel, Ritov and Tsybakov under the same condition have a leading constant larger than 1.

The result is proved in the paper, in about half a page that leans on the proof of Theorem 1. No machine-checked version exists. A formalization pins down two things the printed proof leaves to the reader: the convex-analytic optimality condition behind (2.8), and the "obvious modification of (2.10)" and "some algebra" behind (2.20) and the final display. It also reuses and extends the platform's matrix vocabulary: nuclear and operator norms, SVD data, and the tangent and normal projections of the matrix completion missions.

Difficulty

The estimator is defined implicitly as a minimizer, so the analysis has to go through first-order conditions. Those require the subdifferential of the nuclear norm and a choice of subgradient that matches the support of the comparison matrix A. Mathlib has neither a characterization of this subdifferential nor the monotonicity argument in matrix form. The obvious route, copying Theorem 1, fails at the step that uses Assumption 1 to pass from Frobenius to L₂(Π) norms: without a global isometry, that comparison is available only on the cone ℂ_{A,5}, and the error is known to lie there only in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0 and only for λ ≥ 3‖M‖∞. The constant 5 = (λ + 2Δ)/(λ − 2Δ) at λ = 3Δ is not slack. A linear subspace, not just a convex set, is needed so that Â^λ − A lies in 𝔸, where the cone lives.

Formalization scope

Matrices are RealMatrix m₁ m₂ from the published MatrixCompletion definitions. These supply ⟨·,·⟩ (matrixInner), the nuclear, Frobenius and operator norms, SVD data SVD A r, the sign matrix Σuⱼvⱼᵀ, and 𝒫_A, 𝒫_A⊥ (tangentProjection, normalProjection). This mission adds two definition files.

Model. ⟨·,·⟩{L₂(Π)}, M, L_n and the estimator, all at a fixed outcome ω. The structure TraceRegression holds the standing assumptions: measurable Xᵢ and Yᵢ, square-integrable entries of Xᵢ, integrable Yᵢ and YᵢXᵢ, and 𝔼(Yᵢ | σ(Xᵢ)) = tr(XᵢᵀA₀) almost surely. The page leaves the integrability implicit. Without it a Bochner integral would silently be 0 and ‖·‖{L₂(Π)} would be meaningless. Expectations of matrices are entrywise. Independence of the pairs (p. 1) is not assumed: Theorem 2 does not use it. The estimator is any minimizer of L_n over 𝔸.
Cone and restricted constant. ℂ_{A,c₀} ⊆ 𝔸 and the predicate "μ′ is a cone constant". μ(A) can be +∞ (no constant exists), and a real infimum of an empty set is 0. So every statement is made for every cone constant μ′ for (A, 5). This is equivalent to the infimum form and makes the bound vacuous exactly when the paper's is. A formalization with a real sInf would make (2.19) false and is ruled out.

The other conventions are these. "inf over A ∈ 𝔸" is a bound for every A ∈ 𝔸. rank(A) is Matrix.rank. n ≥ 1 and λ > 0 are assumed, as on the page. (2.8) is stated for a convex 𝔸, as in the proof of Theorem 1 where it is derived. (2.21) is stated for an arbitrary matrix in place of Â^λ − A. No printed statement needed correction.

A complete development needs the subdifferential of the nuclear norm ((2.1) of the paper), the first-order condition for constrained convex minimization, the identity (2.9) and the facts (2.10), and trace duality, which is on the platform as matrix_trace_duality_inequality. The subdifferential of the nuclear norm and the projection estimates are reusable well beyond this mission. Contributions of those general lemmas are welcome.

Selected references

V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4, 2016 (Ann. Statist. 39(5), 2302–2329, 2011). https://arxiv.org/abs/1011.6256
P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. https://doi.org/10.1214/08-AOS620
V. Koltchinskii, The Dantzig selector and sparsity oracle inequalities, Bernoulli 15(3), 799–828, 2009. https://doi.org/10.3150/09-BEJ187
S. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers, arXiv:1010.2731, 2010 (Statist. Sci. 27(4), 2012). https://arxiv.org/abs/1010.2731
G. A. Watson, Characterization of the subdifferential of some matrix norms, Linear Algebra Appl. 170, 33–45, 1992. https://doi.org/10.1016/0024-3795(92)90407-2

14 thms3 active usersReviewed

Linear algebra Markov Chain·Captain: mikedeng1

Search via Quantum Walk 3: For an Irreducible Chain with Positive Self-Loops the Discriminant diag(π)^{1/2}·P·diag(π)^{−1/2} Has Exactly One Singular Value Equal to 1Research Paper

Motivation

Quantum walks give quadratic speed-ups for a class of search problems that classical algorithms solve by running a Markov chain until it hits a marked state. Ambainis's element-distinctness algorithm (Ambainis 2007) and Szegedy's quantization of reversible Markov chains (Szegedy 2004) are the two starting points. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026v4, SIAM J. Comput. 2011) combined them into one search algorithm whose cost is governed by the eigenvalue gap of a reversible chain $P$ .

For a non-reversible chain the relevant spectral quantity is not the eigenvalue gap of $P$ . It is the singular value gap of a related matrix, the discriminant $D(P)$ . In §5 the paper observes that its search algorithm and the proof of its main theorem carry over to non-reversible chains once the eigenvalue gap of $P$ is replaced by the singular value gap of $D(P)$ . Positivity of that gap therefore decides whether the algorithm can be used at all. The paper also notes that irreducibility, and even ergodicity, does not guarantee a positive gap. Its Proposition 3 (p. 17, proved in the appendix on pp. 20–21) gives a simple sufficient condition: every state has a positive probability of staying where it is. This mission formalizes that proposition.

Setting

Let $X$ be a finite set of states. A Markov chain on $X$ is a real matrix $P=(p_{xy})_{x,y\in X}$ with nonnegative entries whose rows sum to one; $p_{xy}$ is the probability of moving from $x$ to $y$ . The graph underlying $P$ has an edge $x\to y$ whenever $p_{xy}>0$ . The chain is irreducible if this graph is strongly connected, so that every state can be reached from every other state.

A stationary distribution of $P$ is a vector $\pi=(\pi_x)_{x\in X}$ with

\pi_x>0,\qquad \sum_x \pi_x=1,\qquad \sum_x \pi_x p_{xy}=\pi_y\quad(y\in X).

Every irreducible chain has exactly one.

The discriminant of $P$ is the matrix

D(P)=\operatorname{diag}(\pi)^{1/2}\cdot P\cdot \operatorname{diag}(\pi)^{-1/2},\qquad D(P)_{xy}=\frac{\sqrt{\pi_x}\,p_{xy}}{\sqrt{\pi_y}},

viewed as an operator on $\mathbb C^X$ with the inner product $\langle u,w\rangle=\sum_x\overline{u_x}w_x$ . Its singular values $\sigma_0\ge\sigma_1\ge\dots\ge\sigma_{|X|-1}\ge 0$ are the square roots of the eigenvalues of $D(P)^\dagger D(P)$ , repeated according to multiplicity. The vector $v=(\sqrt{\pi_x})_{x\in X}$ satisfies $D(P)v=v$ and $v^{\mathsf T}D(P)=v^{\mathsf T}$ , so $1$ is always a singular value of $D(P)$ . When $P$ is reversible, $D(P)$ is symmetric and its singular values are the absolute values of the eigenvalues of $P$ . In general the two can differ.

Formalization targets

Goal: Proposition 3

If $P$ is an irreducible Markov chain on a finite state space $X$ with $p_{xx}>0$ for every $x$ , then $D(P)$ has exactly one singular value equal to $1$ :

\#\{\,i<|X|:\ \sigma_i(D(P))=1\,\}=1 .

Together with the bound below, this says that $1=\sigma_0>\sigma_1$ , i.e. the singular value gap $1-\sigma_1$ is positive. The goal asserts no explicit lower bound on the gap, so it does not depend on any quantitative estimate.

Milestones, in the order the proof uses them

Eq. (9). For unit vectors $u,v\in\mathbb C^X$ ,

|u^\dagger D(P)v|\le\Bigl(\sum_{x,y}|u_x|^2p_{xy}\Bigr)^{1/2}\Bigl(\sum_{x,y}|v_y|^2\tfrac{\pi_x}{\pi_y}p_{xy}\Bigr)^{1/2}\le 1 .

Lemma 3. Every singular value of $D(P)$ lies in $[0,1]$ .
§5, p. 17. $v=(\sqrt{\pi_x})$ is a left and right eigenvector of $D(P)$ with eigenvalue $1$ .
Equality case. If $u,w$ are unit vectors with $u^\dagger D(P)w=1$ , then $u_x=w_y\sqrt{\pi_x/\pi_y}$ whenever $p_{xy}>0$ .
Path chaining. If $u_y=u_x\sqrt{\pi_y/\pi_x}$ along every edge $x\to y$ and $P$ is irreducible, then $u_y=u_{x_1}\sqrt{\pi_y/\pi_{x_1}}$ for all $x_1,y$ .

Significance

The result. Proposition 3 is what makes the search algorithm of the paper usable with non-reversible chains. Theorem 8 of the paper bounds the cost of finding a marked element in terms of the singular value gap of $D(P)$ , and it needs that gap to be positive. The hypothesis $p_{xx}>0$ costs little: replacing $P$ by $\alpha I+(1-\alpha)P$ for any $\alpha\in(0,1)$ makes every self-loop positive and keeps the stationary distribution. The proposition also connects to the classical study of non-reversible chains: the squared singular values of $D(P)$ are the eigenvalues of the multiplicative reversiblization $PP^*$ , which Fill (1991) used to bound convergence to stationarity.

Formalizing it. The proposition and its proof are in the paper and are not in dispute. To our knowledge neither is machine-checked anywhere. The work is a formal proof of the known argument. It exercises Mathlib's recently added singular values of linear maps between finite-dimensional inner product spaces and its theory of irreducible nonnegative matrices, in a setting where the matrix is neither symmetric nor normal.

Difficulty

The obvious route goes through eigenvalues. Irreducibility plus self-loops make $P$ aperiodic, so by Perron–Frobenius the eigenvalue $1$ of $P$ is simple and every other eigenvalue has modulus less than $1$ . This does not settle the question. The singular values of a non-normal matrix are not the moduli of its eigenvalues, and the paper points out ergodic chains whose discriminant has zero singular value gap even though their eigenvalue gap is positive. Simplicity of the eigenvalue $1$ of $P$ therefore says nothing about the multiplicity of the singular value $1$ of $D(P)$ .

The real content is the equality case of a Cauchy–Schwarz inequality in $\mathbb C^{X\times X}$ . It has to be translated into an edge-by-edge relation between the coordinates of the left and right singular vectors, then propagated along directed paths of the chain's graph. The self-loops are what identify the left and right singular vectors with each other. Bookkeeping that is routine on paper costs effort here: passing between the eigenvalue sequence of $D(P)^\dagger D(P)$ and the dimension of its $1$ -eigenspace, and between paths in Mathlib's quiver of positive entries and chains of equalities.

Formalization scope

States and chain. The state space is a Fintype with decidable equality. $P$ is a real matrix in Matrix.rowStochastic ℝ X, and irreducibility is Mathlib's Matrix.IsIrreducible (nonnegative entries and a strongly connected quiver with an edge $x\to y$ iff $p_{xy}>0$ ). For a row-stochastic matrix this agrees with "every state is reachable from every other state".
Stationary distribution. It enters as data $\pi$ with the three properties above. Positivity is explicit because $\operatorname{diag}(\pi)^{-1/2}$ needs it. Existence and uniqueness (Perron–Frobenius) are neither needed nor stated.
Discriminant. $D(P)$ is the complex matrix with entries $\sqrt{\pi_x}p_{xy}/\sqrt{\pi_y}$ , acting on EuclideanSpace ℂ X. Its singular values are Mathlib's LinearMap.singularValues, a sequence indexed by $\mathbb N$ that is $0$ beyond $|X|$ . The goal counts the indices $i<|X|$ with $\sigma_i=1$ . The inner product $u^\dagger D(P)w$ is Mathlib's inner ℂ u (D(P) w). Since the equality-case milestone assumes this equals $1$ exactly, no phase ambiguity remains.
What is not assumed. Reversibility of $P$ is not assumed. Neither is aperiodicity, primitivity, or a "lazy" bound $p_{xx}\ge 1/2$ : the hypothesis is exactly $p_{xx}>0$ for every $x$ .
Ruled-out trivializations. " $1$ is a singular value of $D(P)$ " holds for every chain and is not the goal. The goal is that this singular value has multiplicity one. A conclusion such as "some singular value is $<1$ " would also be too weak.
Cost. The paper's search algorithm and its cost bounds (Theorem 8) are out of scope. This mission is purely linear-algebraic.
Welcome contributions. Proofs of the milestones. The path-chaining milestone is a reusable fact about functions that are multiplicative along the edges of a strongly connected quiver. A general lemma relating the multiplicity of a singular value to the dimension of an eigenspace of $T^\dagger T$ would be useful well beyond this mission.

Selected references

F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1):142–164, 2011; arXiv:quant-ph/0608026v4. https://arxiv.org/abs/quant-ph/0608026 (DOI 10.1137/090745854)
M. Szegedy, Quantum speed-up of Markov chain based algorithms, Proc. 45th IEEE FOCS, 32–41, 2004. https://doi.org/10.1109/FOCS.2004.53
A. Ambainis, Quantum walk algorithm for element distinctness, SIAM J. Comput. 37(1):210–239, 2007; arXiv:quant-ph/0311001. https://arxiv.org/abs/quant-ph/0311001
J. A. Fill, Eigenvalue bounds on convergence to stationarity for nonreversible Markov chains, with an application to the exclusion process, Ann. Appl. Probab. 1(1):62–87, 1991. https://doi.org/10.1214/aoap/1177005981

7 thms3 active usersReviewed

Completed

Machine Learning Optimization·Captain: mikedeng1

Efficient Algorithms for Online Decision Problems 2: For Nonnegative Decisions and States, FPL*(ε/2A) Has Expected Cost at Most (1 + ε)·min-cost_T + 4AD(1 + ln n)/εResearch Paper

Motivation

Many sequential decision problems have a combinatorial decision set and a linear cost: choosing a path in a graph whose edge delays change every day, choosing a binary search tree for a stream of requests, or choosing one of $n$ experts whose losses are revealed after each round. Classical weighted-majority algorithms keep one weight per decision, which is exponential in the size of a path or tree. Kalai and Vempala (J. Comput. System Sci. 71 (2005)) showed that one call per round to an offline optimiser, applied to the cumulative costs plus a random perturbation, already gives online guarantees comparable to those of the exponential-weights algorithms. The idea goes back to Hannan's perturbed algorithm (1957); the paper's contribution is a short, general analysis in the linear setting.

The paper proves two guarantees for Follow the Perturbed Leader. The additive one (Theorem 1.1(a), a sister mission) bounds the regret by a term growing like $\sqrt T$ . This mission formalizes the multiplicative one, Theorem 1.1(b): for nonnegative costs, a variant with exponentially distributed perturbations pays at most a factor $1+\varepsilon$ more than the best fixed decision in hindsight, plus a term independent of the horizon. Such "small-loss" bounds matter when the best decision has small total cost, since the regret then scales with that cost rather than with $T$ .

Setting

Fix a dimension $n$ . A decision set $\mathcal D \subset \mathbb R^n$ and a state set $\mathcal S \subset \mathbb R^n$ are given; choosing $d\in\mathcal D$ in state $s\in\mathcal S$ costs $d\cdot s$ . In this mission both sets are nonnegative: $\mathcal D, \mathcal S \subset \mathbb R^n_+$ .

The decision set is accessed only through an argmin oracle $M:\mathbb R^n\to\mathcal D$ with

M(x)\cdot x \le d\cdot x \quad\text{for all } d\in\mathcal D,

i.e. $M(x)=\arg\min_{d\in\mathcal D} d\cdot x$ with arbitrary tie-breaking. For a state sequence $s_1,\dots,s_T\in\mathcal S$ write $s_{1:t}=s_1+\dots+s_t$ ; the benchmark is

\text{min-cost}_T=\min_{d\in\mathcal D}\sum_{t=1}^T d\cdot s_t = M(s_{1:T})\cdot s_{1:T}.

Two parameters measure the instance: the $\ell_1$ -diameter $D\ge |d-d'|_1$ for $d,d'\in\mathcal D$ , and the state size $A\ge |s|_1$ for $s\in\mathcal S$ , where $|x|_1=\sum_i|x_i|$ .

The algorithm FPL*( $\varepsilon$ ) acts as follows on each period $t$ : draw $p_t$ from the probability law $\mu_\varepsilon$ with density

\frac{d\mu_\varepsilon}{dx}(x)=\Big(\frac{\varepsilon}{2}\Big)^n e^{-\varepsilon|x|_1},

so each coordinate is $\pm r/\varepsilon$ with $r$ standard exponential, and play $M(s_{1:t-1}+p_t)$ . Its expected cost against a fixed state sequence is

\mathbb E[\text{cost of FPL}^*(\varepsilon)]=\sum_{t=1}^T\int s_t\cdot M(s_{1:t-1}+p)\,d\mu_\varepsilon(p).

In Lean these are IsArgminOracle Dset M, laplaceLaw n ε and fplStarExpectedCost M s ε T; $s_{1:t}$ is the published OracleRO.ApproxFPL.prefixSum s t.

Formalization targets

Goal: Theorem 1.1(b)

For nonnegative $\mathcal D,\mathcal S$ , $A>0$ and $0<\varepsilon\le 1$ ,

\mathbb E[\text{cost of FPL}^*(\varepsilon/2A)]\le(1+\varepsilon)\,\text{min-cost}_T+\frac{4AD(1+\ln n)}{\varepsilon}.

Intermediate statements (milestones, in attack order)

For any fixed $p_1$ : $\sum_{t=1}^T M(s_{1:t}+p_1)\cdot s_t\le M(s_{1:T})\cdot s_{1:T}+D|p_1|_\infty$ (p. 303, by Lemma 3.1).
The expected maximum of $n$ independent standard exponentials is at most $\ln n+1$ (end of §2, p. 299).
$\mathbb E_{p\sim\mu_\varepsilon}|p|_\infty\le(1+\ln n)/\varepsilon$ (pp. 299, 303).
Equation (7): $\mathbb E[M(s_{1:t-1}+p)\cdot s_t]=\int (M(s_{1:t}+y)\cdot s_t)\,e^{-\varepsilon(|y+s_t|_1-|y|_1)}\,d\mu_\varepsilon(y)$ .
Equation (6): $\mathbb E[M(s_{1:t-1}+p)\cdot s_t]\le e^{\varepsilon A}\,\mathbb E[M(s_{1:t}+p)\cdot s_t]$ .
For $0<\varepsilon\le 1/A$ : $e^{\varepsilon A}\le 1+2\varepsilon A$ .
For $0<\varepsilon\le 1/A$ : $\mathbb E[\text{cost of FPL}^*(\varepsilon)]\le(1+2\varepsilon A)\big(\text{min-cost}_T+D(1+\ln n)/\varepsilon\big)$ .

Statement 7 is the bound for an arbitrary parameter; the goal is its evaluation at $\varepsilon/2A$ .

Significance

The result is the first multiplicative guarantee for a perturbation algorithm that needs only an offline linear optimiser. With $\varepsilon$ tuned to $\text{min-cost}_T$ it gives $\mathbb E[\text{cost}]\le\text{min-cost}_T+4\sqrt{\text{min-cost}_T\,AD(1+\ln n)}+4AD(1+\ln n)$ (p. 294). The paper applies it to online shortest paths, to the tree-update problem (giving the first efficient $(1+\varepsilon)$ -competitive algorithm there), and to adaptive Huffman coding. The lazy variant FLL* of the same paper, whose per-period behaviour coincides with FPL*, inherits the bound; that is the third mission of this series.

The theorem is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces a formal proof of Theorem 1.1(b) as printed, together with the reusable ingredients: the multivariate Laplace law with its normalisation, its translation identity (7), and the expected maximum of i.i.d. exponentials. The paper's argument has small gaps that a formalization must close, notably the condition $\varepsilon\le 1$ , which (b) omits but its proof uses.

Difficulty

The deterministic part is the be-the-leader argument with a shared perturbation; it is a finite-sum induction. The probabilistic part is where the work is. The obvious approach, bounding the difference between following and being the perturbed leader by the measure of a symmetric difference of translated sets as in the additive case, gives an additive term proportional to $T$ and cannot give a multiplicative factor. Instead (6) needs the density ratio of $\mu_\varepsilon$ under translation by $s_t$ , which requires a change of variables against a density on $\mathbb R^n$ , together with the nonnegativity of the integrand; without nonnegativity the inequality fails. The bound on $\mathbb E|p|_\infty$ requires the expected maximum of $n$ exponentials, which is not in Mathlib, and the identification of the coordinates of $\mu_\varepsilon$ as independent scaled Laplace variables, which requires factoring a product density.

Formalization scope

Vectors are Fin n → ℝ; $d\cdot s$ is ⬝ᵥ; $|x|_1$ is written $\sum_i|x_i|$ ; $|x|_\infty$ is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The decision set is Dset, the diameter Ddiam. States are indexed from $1$ ; s 0 is unused. The oracle is a hypothesis IsArgminOracle Dset M on an arbitrary function, so the theorems hold for every tie-breaking rule. The paper's parameters are hypotheses ∀ d d' ∈ Dset, ∑ i, |d i - d' i| ≤ Ddiam and ∀ x ∈ S, ∑ i, |x i| ≤ A. The bound $R\ge|d\cdot s|$ of the paper is not used by part (b) and is omitted.

Hypotheses added to the page, each necessary: measurability of $M$ (the expectations presuppose it); $\varepsilon>0$ ; $A>0$ (the parameter $\varepsilon/2A$ presupposes it); $\varepsilon\le1$ in the goal (used by the proof, p. 303); and $n\ge1$ only in the statement about a maximum over $n$ variables. Two printed slips are corrected, not copied: "exponential distributions with mean $\varepsilon$ " (rate $\varepsilon$ is meant) and " $|p_1|_\infty\le(1+\ln n)/\varepsilon$ " (an expectation is meant).

Trivializing formalizations are ruled out as follows. The law $\mu_\varepsilon$ carries its normalising constant $(\varepsilon/2)^n$ and is shown to be a probability measure in a sorry-free sanity file; it is not the uniform law of FPL. The cost uses $M(s_{1:t-1}+p)$ , not the be-the-leader $M(s_{1:t}+p)$ . The oracle is not built with Classical.epsilon. All integrands are measurable and bounded (because $\mathcal D$ has finite diameter), so no integral vanishes for lack of integrability; the sanity file checks this on a two-expert instance that satisfies every hypothesis.

A complete development needs Lebesgue change of variables under translation for densities on Fin n → ℝ, Fubini for product densities, the tail-integral formula for expectations, and a union bound. The Laplace law, its translation identity, and the expected maximum of exponentials are reusable beyond this mission; contributions of those as standalone lemmas are welcome.

Selected references

A. Kalai and S. Vempala, Efficient algorithms for online decision problems, J. Comput. System Sci. 71(3):291–307, 2005. https://doi.org/10.1016/j.jcss.2004.10.016
J. Hannan, Approximation to Bayes risk in repeated plays, in Contributions to the Theory of Games III, Ann. of Math. Studies 39, Princeton University Press, 1957, pp. 97–139 (reference [14] of Kalai and Vempala).

11 thms3 active usersReviewed

Completed

Machine Learning Optimization·Captain: mikedeng1

Efficient Algorithms for Online Decision Problems 1: Follow the Perturbed Leader FPL(ε) Has Expected Cost at Most min-cost_T + εRAT + D/εResearch Paper

Motivation

In an online decision problem a decision maker chooses actions one period at a time, and only after each choice learns what that choice cost. The classical instance is prediction with expert advice: each day one of $n$ experts is followed, and afterwards every expert's loss is revealed. The goal is a strategy whose total cost is close to that of the best single fixed action in hindsight, whatever the sequence of costs.

Many structured problems have exponentially many actions, such as paths in a graph whose edge delays change daily. Weighted-majority methods keep one weight per action and are then inefficient. A. Kalai and S. Vempala (J. Comput. System Sci. 71 (2005) 291–307) showed that it suffices to be able to solve the offline problem: given total costs, find the best single action. Their algorithm, Follow the Perturbed Leader (FPL), adds a random perturbation to the accumulated costs and calls the offline solver once per period. The idea goes back to J. Hannan (1957); the paper's analysis made it short and broadly applicable, and FPL has since become a standard tool in online learning and online combinatorial optimization.

Timeline.

1957: Hannan introduces perturbed play, with perturbations growing like $\sqrt t$ , and obtains additive bounds for finitely many actions.
2005: Kalai and Vempala analyse FPL for linear costs over an arbitrary decision set with an offline oracle: an additive bound (Theorem 1.1(a), the goal here), a multiplicative bound (Theorem 1.1(b)), and lazy variants.

Setting

Decisions and states are vectors in $\mathbb R^n$ . The decision set is a possibly infinite set $\mathcal D \subset \mathbb R^n$ and the state set is $\mathcal S \subset \mathbb R^n$ . In period $t = 1, 2, \dots$ the decision maker picks $d_t \in \mathcal D$ , then the state $s_t \in \mathcal S$ is revealed, and the cost is the dot product $d_t \cdot s_t$ . The state sequence is fixed in advance (an oblivious adversary).

Write $s_{1:t} = s_1 + \dots + s_t$ , with $s_{1:0} = 0$ . The offline oracle is a map $M : \mathbb R^n \to \mathcal D$ with

M(s) \in \operatorname*{arg\,min}_{d \in \mathcal D} d \cdot s .

Because costs are linear, the best fixed decision after $T$ periods has cost

\text{min-cost}_T = \min_{d \in \mathcal D} \sum_{t=1}^T d \cdot s_t = M(s_{1:T}) \cdot s_{1:T}.

Three parameters measure an instance, with $|x|_1 = \sum_i |x_i|$ :

the diameter $D \ge |d - d'|_1$ for all $d, d' \in \mathcal D$ ;
the cost bound $R \ge |d \cdot s|$ for all $d \in \mathcal D$ , $s \in \mathcal S$ ;
the state size $A \ge |s|_1$ for all $s \in \mathcal S$ .

FPL( $\varepsilon$ ), for a parameter $\varepsilon > 0$ : in each period $t$ , draw $p_t$ uniformly at random from the cube $[0, 1/\varepsilon]^n$ and play $M(s_{1:t-1} + p_t)$ . Its expected cost is $\mathbb E[\text{cost of FPL}(\varepsilon)] = \sum_{t=1}^T \mathbb E\,[M(s_{1:t-1} + p_t) \cdot s_t]$ .

Hannan( $\delta$ ): the same rule with $p_t$ uniform on $[0, \sqrt t/\delta]^n$ .

Formalization targets

Goal: Theorem 1.1(a)

For every state sequence $s_1, \dots, s_T \in \mathcal S$ and every $0 < \varepsilon \le 1$ ,

\mathbb E[\text{cost of FPL}(\varepsilon)] \le \text{min-cost}_T + \varepsilon R A T + \frac{D}{\varepsilon}.

The constants are the paper's. With $\varepsilon = \sqrt{D/(RAT)}$ the expected regret is at most $2\sqrt{DRAT}$ .

Milestones (the paper's proof path)

Display (4), "be the leader": $\sum_{t=1}^T M(s_{1:t}) \cdot s_t \le M(s_{1:T}) \cdot s_{1:T}$ .
Lemma 3.1: for any $T > 0$ and vectors $p_0 = 0, p_1, \dots, p_T$ ,

\sum_{t=1}^T M(s_{1:t} + p_t) \cdot s_t \le M(s_{1:T}) \cdot s_{1:T} + D \sum_{t=1}^T |p_t - p_{t-1}|_\infty .

Display (5): for $p_1 \in [0, 1/\varepsilon]^n$ , $\sum_t M(s_{1:t} + p_1) \cdot s_t \le M(s_{1:T}) \cdot s_{1:T} + D|p_1|_\infty \le M(s_{1:T}) \cdot s_{1:T} + D/\varepsilon$ .
Lemma 3.2: the cubes $[0, 1/\varepsilon]^n$ and $v + [0, 1/\varepsilon]^n$ overlap in at least a $(1 - \varepsilon |v|_1)$ fraction.

Companion: Theorem 3.3

For any state sequence in $\mathcal S$ , any $\delta > 0$ and any $T > 0$ ,

\mathbb E[\text{cost of Hannan}(\delta)] \le M(s_{1:T}) \cdot s_{1:T} + 2\delta R A \sqrt T + \frac{D\sqrt T}{\delta}.

This bound needs no knowledge of $T$ . It is included as a separate theorem, not a milestone of the goal.

Significance

The result. Theorem 1.1(a) reduces online linear optimization over any decision set to its offline counterpart, at the price of one oracle call per period and regret $O(\sqrt{DRAT})$ . Applied to online shortest paths, spanning trees and other combinatorial problems it gives efficient algorithms where weighted majority would maintain exponentially many weights. Later uses of FPL (approximate oracles, robust optimization via online learning) start from this bound.

Formalizing it. The theorem has been proved in print for twenty years; it has no machine-checked proof that we know of. The platform already holds a formalization of Ben-Tal, Hazan, Koren and Mannor's approximate-oracle variant (OracleRO.ApproxFPL), which takes a maximising oracle and an oscillation bound $R$ and therefore yields a weaker constant ( $2\varepsilon RAT$ ) in this setting. This mission states the exact-oracle bound with the paper's constant $\varepsilon RAT$ , where $R$ bounds $|d \cdot s|$ itself. A correct proof must handle that constant carefully; see the next section.

Difficulty

Display (4), Lemma 3.1 and display (5) are finite-sum arguments from the defining property of $M$ . Lemma 3.2 is a statement about Lebesgue measure of a cube and its translate.

The central difficulty is the stability step: bounding, period by period, how much worse it is to play $M(s_{1:t-1} + p_t)$ than $M(s_{1:t} + p_t)$ . The obvious argument says that the two perturbed points have laws that agree on a $(1 - \varepsilon|s_t|_1)$ fraction, and on the rest "one can only be $R$ larger". Under the printed definition of $R$ the difference of two costs $d \cdot s_t - d' \cdot s_t$ can be as large as $2R$ , so this per-period bound fails for costs of mixed sign: with $n = 1$ , $\mathcal D = \{-1, 1\}$ and suitable $s_{1:t-1}$ , the per-period difference is $2\varepsilon s_t^2$ , while $\varepsilon R A = \varepsilon s_t^2$ . The theorem itself, with $\varepsilon RAT$ , remains true, but a proof cannot proceed by the per-period comparison as written. Proving the goal with the stated constant, rather than $2\varepsilon RAT$ , is the substantive part of the mission.

Formalization scope

Vectors are Fin n → ℝ; $d \cdot s$ is dotProduct (⬝ᵥ); $|x|_1$ is written out as $\sum_i |x_i|$ ; $|x|_\infty$ is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The sets are Dset and S; the diameter is Ddiam.
States are a sequence s : ℕ → Fin n → ℝ indexed from $1$ (s 0 is unused); the hypothesis $s_t \in \mathcal S$ is imposed for $1 \le t \le T$ .
The oracle is the predicate IsArgminOracle Dset M: $M(x) \in \mathcal D$ and $M(x) \cdot x \le d \cdot x$ for all $d \in \mathcal D$ . Every theorem quantifies over all such $M$ ; the oracle is never a chosen Classical.epsilon minimiser.
Parameters $D$ , $R$ , $A$ are hypotheses over the sets exactly as printed on p. 294 (not the weaker "reasonable decisions" variant of the paper's footnote 4). Each statement takes only the parameters it uses.
Shared definitions come from the published OracleRO.ApproxFPL.FPL: prefixSum s t $= s_{1:t}$ ; perturbLaw n ε, the uniform law on $[0, 1/\varepsilon]^n$ ; and fplExpectedReward M s ε T $= \sum_{t=1}^T \int s_t \cdot M(s_{1:t-1} + p)\, dU(p)$ , which with an argmin oracle is the expected cost of FPL( $\varepsilon$ ) (its name reflects a maximisation source). Using one integral per period is the paper's own observation that fresh and shared perturbations give the same expectation.
Added hypotheses, each disclosed in the item: $\varepsilon > 0$ and $\delta > 0$ (the page divides by them); measurability of $M$ (the expectations require it). With $R$ bounding $|d \cdot s|$ and $M(x) \in \mathcal D$ , every integrand is bounded and measurable, so every expectation is a genuine integral and no bound holds vacuously. The page's $\varepsilon \le 1$ is kept in the goal although the bound does not use it. $T$ is unrestricted where the page allows it.
Not a trivialization. The expected cost uses $M(s_{1:t-1} + p)$ , the decision available before $s_t$ is seen; replacing it by the "be the leader" decision $M(s_{1:t} + p)$ would make the goal follow from display (5) alone. The uniform law is normalised (a probability measure for $\varepsilon > 0$ ).
Corrected reading. Display (5) on the page prints $M(s_t + p_1)$ ; the statement uses $M(s_{1:t} + p_1)$ , which is what Lemma 3.1 gives and what the text says it applies.
Not included. The per-period stability inequality of the printed proof, which is false for costs of mixed sign.

Contributions welcome: proofs of the milestones, the goal and Theorem 3.3, and reusable lemmas on uniform laws over translated cubes.

Selected references

A. Kalai, S. Vempala, Efficient algorithms for online decision problems, J. Comput. System Sci. 71(3) (2005) 291–307. https://doi.org/10.1016/j.jcss.2004.10.016
J. Hannan, Approximation to Bayes risk in repeated plays, in: Contributions to the Theory of Games, vol. 3, Princeton University Press, 1957, pp. 97–139 (reference [14] of Kalai–Vempala, https://doi.org/10.1016/j.jcss.2004.10.016).
A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-based robust optimization via online learning, Oper. Res. 63(3) (2015) 628–638. https://doi.org/10.1287/opre.2015.1374

7 thms3 active usersReviewed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

What Can We Learn Privately? III: An ε-Local Algorithm Simulates Any t-Query Statistical Query Algorithm from O(t log(t/β) b²/(ε²τ²)) SamplesResearch Paper

Motivation

In the local model of differential privacy, no trusted curator ever sees the raw data: each individual randomizes their own record before handing it to the analyst. This is how private telemetry is collected in practice (randomized response and its descendants), and it raises a basic question: which learning tasks remain possible when the learner only sees locally randomized records?

Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith answered it in What Can We Learn Privately? (arXiv:0803.0924v3, the accepted version of SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are the arXiv v3's). They showed that local private learning is equivalent, up to polynomial factors, to learning in Kearns' statistical query (SQ) model (Kearns 1998), where an algorithm sees a distribution only through approximate expectations. This mission formalizes one direction of that equivalence: every SQ algorithm can be run by a local algorithm (§5.1.1, Theorem 5.7). The other direction (Lemma 5.8) is a separate mission of this series.

Timeline. Blum, Dwork, McSherry and Nissim (PODS 2005) observed that SQ algorithms can be simulated by a trusted curator adding noise to sums. Dwork, McSherry, Nissim and Smith (TCC 2006) introduced the Laplace mechanism. Kasiviswanathan et al. (FOCS 2008; journal version 2011) showed the simulation works even in the local model, with each record entering a single randomizer.

Setting

A database is a vector $z=(z_1,\dots,z_n)\in D^n$ ; two databases are neighbors if they differ in exactly one entry. A randomized algorithm $A$ is $\varepsilon$ -differentially private if $\Pr[A(z)\in S]\le e^{\varepsilon}\Pr[A(z')\in S]$ for all neighbors $z,z'$ and all measurable sets $S$ of outputs. An $\varepsilon$ -local randomizer is an $\varepsilon$ -differentially private map applied to a single record: $\Pr[R(u)\in S]\le e^{\varepsilon}\Pr[R(u')\in S]$ for all $u,u'$ .

The Laplace distribution $\mathrm{Lap}(s)$ has density $\frac1{2s}e^{-|x|/s}$ .

An SQ oracle $SQ_P$ for a distribution $P$ on $D$ receives a query $g:D\to[-b,b]$ and a tolerance $\tau$ , and may return any $v$ with $|v-\mathbb E_{u\sim P}[g(u)]|\le\tau$ . An SQ algorithm with $t$ queries asks $(g_0,\tau_0),\dots,(g_{t-1},\tau_{t-1})$ , where $(g_k,\tau_k)$ may depend on the earlier answers $a_0,\dots,a_{k-1}$ (adaptive), and outputs a function of all answers. A vector $a$ is a valid transcript against $SQ_P$ if every $a_k$ is within $\tau_k$ of the true mean of the query $g_k$ asked at that point.

For one query $g$ , the randomizer $R_g(u)=g(u)+\eta$ with $\eta\sim\mathrm{Lap}(2b/\varepsilon)$ is applied to each record, and the local algorithm $\mathcal A_g$ outputs the average $\frac1n\sum_i(g(z_i)+\eta_i)$ . The simulation of an SQ algorithm answers its $k$ -th query $g_k$ by running $\mathcal A_{g_k}$ on the $k$ -th block of $m$ fresh entries $z_{km},\dots,z_{km+m-1}$ and finally outputs what the SQ algorithm outputs on these answers.

Formalization targets

Goal: Theorem 5.7 (local simulation of SQ)

There is an absolute constant $c>0$ such that, for every SQ algorithm with $t$ queries into $[-b,b]$ , and every $\varepsilon>0$ ; the accuracy claim further takes every tolerance at least $\tau$ , $\varepsilon\le1$ , $\varepsilon\tau\le4b$ and $0<\beta<1$ :

\text{the simulation is }\varepsilon\text{-differentially private for every block size }m\text{ and every }n\ge tm,

m\ \ge\ c\,\frac{\ln(t/\beta)\,b^2}{\varepsilon^2\tau^2},\ z\sim P^n\ \Longrightarrow\ \Pr\bigl[\text{the simulated answers are a valid transcript against }SQ_P\bigr]\ \ge\ 1-\beta .

On that event the simulation outputs exactly what the SQ algorithm outputs against a valid oracle. The constant is left unspecified, as in the paper.

Milestones

$R_g$ is an $\varepsilon$ -local randomizer; $\mathcal A_g$ is $\varepsilon$ -differentially private (p. 20).
Hoeffding's bound for the empirical mean of $g$ : $\Pr[|\frac1n\sum g(u_i)-v|\ge\tau/2]\le2e^{-\tau^2n/(8b^2)}$ .
The average of $n$ i.i.d. $\mathrm{Lap}(2b/\varepsilon)$ variables lies in $[-\tau/2,\tau/2]$ with probability at least $1-\beta/2$ once $n\ge c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$ .
Lemma 5.6: $\mathcal A_g$ approximates $\mathbb E_P[g]$ within $\pm\tau$ with probability $1-\beta$ from $n\ge c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$ samples.

Significance

Theorem 5.7 is the inclusion "SQ ⊆ local" in the paper's characterization of local private learning: every concept class learnable with statistical queries is learnable by an $\varepsilon$ -local algorithm, with sample size growing like $t\log(t/\beta)b^2/(\varepsilon^2\tau^2)$ . Combined with the converse simulation (Lemma 5.8), it identifies local private learnability with SQ learnability (Theorem 5.14). It thereby transfers the known SQ lower bounds, such as the one for parity, to the local model. It also shows that nonadaptive SQ algorithms become noninteractive local protocols.

The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization fixes what "the simulation gives the same output" means against an adversarial oracle and an adaptive algorithm. It also supplies reusable Lean objects for local differential privacy, Laplace noise and SQ algorithms.

Difficulty

The privacy half is the easy-looking part, but it is adaptive: the query asked in block $k$ depends on the noisy answers from blocks $0,\dots,k-1$ . A database change in block $k$ therefore changes the law of all later answers, not only $a_k$ . The argument must use that every entry enters exactly one randomizer and compose along the adaptive transcript.

The accuracy half has the same adaptivity issue: the union bound over queries needs, for each $k$ , the failure probability of block $k$ conditioned on everything before it. That is where the fresh blocks and measurability are used. The concentration step for Laplace averages is sub-exponential, not sub-Gaussian. The naive use of the paper's appendix lemma (A.3) fails: it is stated as an equality for every deviation $\delta>0$ , but its proof only covers deviations of order the Laplace scale.

Formalization scope

Databases are Fin n → D (0-based). Randomized algorithms are identified with the laws of their outputs (Measure); differential privacy is required on all measurable sets. An SQ algorithm is a deterministic adaptive strategy (SQAlg): a randomized one is a mixture over its coins, to which the result transfers. "At most $t$ queries" is "exactly $t$ " after padding with dummy queries. Queries are real valued with $|g|\le b$ , as the paper allows after Definition 5.4. Block $k$ consists of the database indices $km,\dots,km+m-1$ , so the blocks are disjoint by construction, and the simulated answers are a deterministic function of the database and the $t\times m$ noise array. The natural logarithm replaces the paper's base 2, which only changes $c$ . Constants are existential and quantified before everything else.

Explicit choices, each recorded in the item that makes it:

$\varepsilon\tau\le4b$ in Lemma 5.6, the Laplace step and Theorem 5.7. Without it the printed statements are false: for $\varepsilon\tau/b$ large a single sample is allowed, and its Laplace noise exceeds $\tau$ too often.
$\varepsilon\le1$ in Lemma 5.6 and in the accuracy half of Theorem 5.7 (the privacy half holds for every $\varepsilon>0$ ). Without it the threshold $c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$ can be smaller than the sample size needed to estimate $\mathbb E[g]$ at all. The paper's own remark about an $O(\varepsilon^{-2})$ factor presumes $\varepsilon=O(1)$ .
$\beta\le1/2$ in the Laplace step, which is false for $\beta$ near $1$ .
Each query is jointly measurable in (earlier answers, record), and the output map is measurable for the privacy claim.
"Gives the same output as $\mathcal A_{SQ}$ " is "the simulated answers are a valid transcript against $SQ_P$ ". Accuracy bounds the measure of the failure event by $\beta$ .
"Noninteractive if nonadaptive" and "efficient" are not formalized.

A trivializing formalization is ruled out: the oracle is not replaced by the exact expectation, accuracy is required for every query actually asked (not only the first), privacy holds for every database (not only i.i.d. samples), and the constant $c$ cannot depend on $t$ , $\beta$ , $\varepsilon$ , $\tau$ , $b$ or the algorithm.

Needed infrastructure: the Laplace distribution as a probability measure and its moment generating function, a Hoeffding bound for bounded i.i.d. variables, the Laplace mechanism, and adaptive composition along a transcript. All of these are reusable beyond this mission. Proofs of the milestones, of standalone Laplace and composition lemmas, and of the goal are welcome.

Selected references

S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, https://arxiv.org/abs/0803.0924 ; DOI https://doi.org/10.1137/090756090
M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. https://doi.org/10.1145/293347.293351
C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating noise to sensitivity in private data analysis, TCC 2006, LNCS 3876, 265–284. https://doi.org/10.1007/11681878_14
A. Blum, C. Dwork, F. McSherry, K. Nissim, Practical privacy: the SuLQ framework, PODS 2005, 128–138. https://doi.org/10.1145/1065167.1065184
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

9 thms3 active usersReviewed

Completed

Analysis Optimal Transport·Captain: marwahaha

A counterexample to the Monge ansatz for the three-marginal Coulomb costOpen Problem

Motivation

An optimal coupling can exist even when no deterministic transport maps attain its cost. The target separates attainment from equality of infima for a three-marginal repulsive cost. The pinned manuscript supplies the research context.

Setting

All three marginals are the same smooth compactly supported probability density in real three-space, with smooth compactly supported square root. Coincident points have infinite Coulomb cost.

Formalization target

The selected goal is OAI.Problem356.coulomb_counterexample_and_equal_infima. Its central assertion is

\inf_{T_2,T_3}\int c(x,T_2x,T_3x)\,d\mu=\min_{\pi\in\Pi(\mu,\mu,\mu)}\int c\,d\pi.

The theorem states, without a proof being verified here, that there exists a function ρ on three-dimensional Euclidean space ℝ³ satisfying a full Coulomb conclusion. This means ρ is a nonnegative C^∞ function with compact support, whose square root is also C^∞ with compact support, and with integral 1 over ℝ³; its density measure μ (Lebesgue measure weighted by ρ) is a probability measure. Consider three-marginal couplings of μ, namely probability measures on triples (x,y,z) of points of ℝ³ all of whose three coordinate marginals equal μ, with cost 1/|x−y| + 1/|x−z| + 1/|y−z| valued in [0,∞] (the inverse of distance zero is ∞). The Kantorovich value of μ is the infimum of the expected cost over all such couplings, and the theorem asserts it is finite and attained by some coupling. Further, no pair of measurable maps T₂,T₃ each preserving μ (pushing μ forward to itself) is a Monge optimizer: for every such pair, the expected cost of the triple (x,T₂x,T₃x) under μ is strictly larger than the Kantorovich value. Nevertheless, the Monge value, the infimum of this graph cost over all such pairs of μ-preserving maps, equals the Kantorovich value, and for every ε>0 there are μ-preserving maps T₂,T₃ with finite graph cost at most the Kantorovich value plus ε.

Significance and status

The goal includes a finite attained Kantorovich value, no Monge minimizer, equal infima and arbitrarily accurate finite-cost maps. Other dimensions and Riesz exponents are not part of this selected target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Every measure-preserving pair of maps must be strictly suboptimal, while a sequence of such pairs still approaches the coupling minimum.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

OpenAI, A counterexample to the Monge ansatz for the three-marginal Coulomb cost, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

36 thms3 active usersReviewed

All missions

Quantity Flexibility Contracts and Supply Chain Performance 1: Under the Minimum Commitment Policy a Flex Node With At Least Its Customer's Flexibility Keeps Zero InventoryResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Quantity Flexibility Contract and Supplier-Customer Incentives II: With a Perfect Demand Signal the Transfer Price c̄(ψ) Makes the Quantity Flexibility Contract System-EfficientResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 6(a)

Milestones

Significance

Difficulty

Formalization scope

Selected references

New Techniques for Noninteractive Zero-Knowledge 4: The Decisional-Linear Commitment Is Perfectly Binding and Extractable, with a Perfectly Sound, Witness-Indistinguishable 0/1 ProofResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4, exact part

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Single-Item Inventory Model for a Nonstationary Demand Process: With Adaptive Base-Stock Control at Two Stages, Upstream Inventory Is N(y₀, σ²∑_{i<K}(1+(L+i)α)²)Research Paper

Motivation

Setting

Formalization targets

Goal: the upstream inventory distribution (16)

Milestones, in the paper's order

Significance

Difficulty

Formalization scope

Selected references

New Techniques for Noninteractive Zero-Knowledge 3: The Subgroup-Decision (BGN) Commitment Is Perfectly Binding and Extractable, with a Perfectly Sound, Witness-Indistinguishable 0/1 ProofResearch Paper

Motivation

Setting

Formalization targets

Goal: the exact part of Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Thompson Sampling: An Asymptotically Optimal Finite-Time Analysis: Bernoulli Thompson Sampling Has Regret (1+ε)Σ Δ_a(ln T + ln ln T)/K(μ_a, μ*) + CResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 3)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Note on Probability Distributions with Increasing Generalized Failure Rates II: For IGFR X with Support (α, ∞) and g(ξ) → κ, E[Xⁿ] Is Finite iff κ > nResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 603)

Milestones

Significance

Difficulty

Formalization scope

Selected references

AdWords and Generalized On-line Matching II: No Randomized Online Algorithm for b-Matching Has Competitive Ratio Better Than 1 − 1/e, for Every Budget bResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 9

Milestones (proof of Theorem 9, p. 15)

Significance

Difficulty

Formalization scope