Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A self-similar measure on the line is the natural probability measure on the attractor of finitely many contracting similarities , chosen with probabilities . Self-similar measures are the basic test case for fractal dimension theory; Bernoulli convolutions, the laws of , are the classical example. When the pieces are well separated, the dimension is given by the entropy-to-Lyapunov formula . When they overlap, dimension can drop, and the question is exactly how much. If two compositions of the same length coincide as maps (an exact overlap), information is genuinely lost; the entropy-rate dimension conjecture, formulated in Varjú's survey, predicts that this is the only mechanism: the dimension equals , where is the entropy rate of the random walk on composed maps.
This mission asks for a formal proof of that formula, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a finite nonempty alphabet and with , ; different symbols may give the same map, and ratios may be negative and unequal. Let be a probability vector with all . The self-similar measure is the Borel probability measure with
For a word let , and let be the random affine map when the letters are independent with law . With logarithms in base ,
where is Shannon entropy of the distribution of the map (coinciding words are merged). The lower Hausdorff dimension of is . The system has no exact overlaps if distinct words of the same length give distinct maps.
If there are no exact overlaps, the attractor is compact and nonempty, the equation has a unique solution , and .
If for all and there are no exact overlaps, then .
For every such family and every strictly positive probability vector ,
No separation assumption is made; exact overlaps and repeated generators are allowed.
The result itself. It removes every arithmetic and separation hypothesis from the dimension theory of self-similar measures on the line: the only way dimension can drop below is through exact overlaps, and then the drop is exactly measured by the map entropy. Without exact overlaps it gives the classical formula (Corollary 6.2, p. 19), and hence the dimension of every self-similar set without exact overlaps (Corollary 6.3), which is the exact-overlaps conjecture for sets. It asserts nothing about absolute continuity.
Formalizing it. Hausdorff dimension and self-similar measures exist only partially in Mathlib, and the proof needs a quantitative entropy calculus for finite laws at multiple scales. A formal proof would certify the general theorem together with the consequences that previously required separate arithmetic hypotheses. The only external input is the Feng–Hu exact-dimensionality theorem.
Hochman's method yields the formula under exponential separation of cylinders, but Baker and Bárány–Käenmäki showed that without exact overlaps cylinders can still come superexponentially close, so no lower bound on the separation is available, and exact overlaps add further collisions. The proof must therefore detect entropy hidden at arbitrarily fine scales with no control on the smallest positive distance. The preprint does this with a finite-law pair estimate independent of minimal separation (Lemma 3.2, p. 9), conditioning on block types to recover the map-entropy rate when addresses collide (Lemma 4.1, p. 13), and disjoint windows of entropy gain whose depths are chosen adaptively (Section 5).
System ι over a nonempty Fintype ι carries ratio, offset, weight with , , . SelfSimilar S μ is the equation for a probability measure on .wordAffine composes maps as and records (slope, translation); mapMass merges words with equal complete maps; walkEntropy n is base-2 Shannon entropy of ; entropyRate is the sInf over of ; lyapunov is base-2.lowerHausdorffDimension μ is an iInf in ℝ≥0∞ of dimH E over measurable with ; the goal compares it to ENNReal.ofReal (min 1 (h/χ)).NoExactOverlaps is injectivity of wordAffine on all words; words of different lengths always differ in slope modulus, so this matches the same-length condition of the source. The homogeneous milestone allows a single map, a degenerate case where both sides are .codingPoint and word functions, equivalent to the definitions above.A linear projection can concentrate a measure even when the measure has no atoms; how much depends on how much mass sits near the affine subspaces that the projection collapses. Quantitative versions of this principle go back to the potential-theoretic projection method of Kaufman and Mattila, which relates ball-growth bounds to the behaviour of projections. This preprint proves explicit, dimension-dependent versions for random exact projections and applies them to a learning question: how many noiseless Gaussian measurements does a learner with bits of memory need to recover a unit vector to angular accuracy ?
The answer proved here is that bits force measurements, matching the real-valued randomized Kaczmarz scale, and more generally for every .
Let be uniform probability on . A finite measure on satisfies an all-ball mass bound with constants if for every ball. For an orthonormal -frame , is the image measure on and its density. The Riesz functional of is .
In the finite-state regression experiment, the signal ; at each step a row arrives with its exact label . A learner keeps one of states, may use arbitrary measurable randomized transitions of the current state and pair, stops by a deterministic horizon , and outputs a unit vector from its terminal state, stopping index and fresh randomness. Success means .
In Lean (OAI.ProjectionMoments, OAI.NoiselessRegression), learners are FiniteKernelLearner d M T (Markov-kernel transitions on completed observations, states Fin (2^M)), mixed over a seed space Ξ with probability ρ; seededSuccess is uniform-prior success; AllBallMass ν K β, coordinateDensity, frameLaw, capMeasure, rieszPotential encode the geometric objects.
OAI.ProjectionMoments.mainA conjunction of the paper's results, including:
also under an every-signal guarantee.
The result. The projection moment estimates are general statements about finite measures with ball-growth control and apply beyond learning. In the learning application they give three proofs, with different stopping and accuracy costs, that bits cannot beat the sample scale for exact Gaussian measurements, plus an explicit trade-off for all .
Formalizing it. The results are in an unrefereed preprint; there is no machine-checked proof. The conjunct FixedQuadraticMemory coincides with part of the goal of the companion mission on Memory and precision in noiseless Gaussian regression, so progress here is shared.
Integrated density norms do not determine density values on a matrix-dependent graph, so pointwise statements need an explicitly chosen density version. The high moments of projected densities require controlling collisions of independent points under projection, which leads to inverse affine heights whose integrability must be extracted from the ball-growth hypothesis at all scales. In the learning application, conditioning on an exact label produces a singular posterior, so arguments that track a posterior density fail.
EuclideanSpace ℝ (Fin d); frames are orthonormal families Fin k → E drawn by frameLaw; densities are ℝ≥0∞-valued with explicit measurable versions.d/4, d/8, d/16); block counts appear as (T+k-1)/k.FiniteKernelLearner with CompletedRules almost surely in the seed; success probabilities are ℝ≥0∞.The goal has no trivial reading: each conjunct quantifies over all measures or learners satisfying the stated hypotheses, and the hypotheses are satisfiable.
Needed infrastructure: Stiefel and Haar measures, Gaussian polar decomposition of matrices, Gram–Schmidt Jacobians, spherical caps, Riesz potentials. Contributions proving individual conjuncts (for example Theorem 3.3) are welcome.
Draw independent fair bits , compute a one-bit summary , and send the bits through independent binary symmetric channels with crossover probability , producing . Which summary tells the receiver the most about ? Kumar and Courtade conjectured that a single coordinate, , is optimal: bits for every Boolean , in every dimension and at every noise level (ISIT 2013; IEEE Trans. Inf. Theory 2014). The Courtade–Kumar (most informative Boolean function) conjecture is a basic question about how noise destroys information on the discrete cube, connecting information theory with Boolean Fourier analysis and hypercontractivity.
This mission asks for a formal proof of a sharp contraction theorem for arbitrary randomized binary summaries, whose Boolean case is the Courtade–Kumar conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let with uniform measure; information is in nats unless stated. For put
with ; is the increasing branch . A soft channel is , the conditional mean of an auxiliary sign given ; its information is . For let with independent signs , and let , so . For an interior field with , the production is with ; the rate is defined by ; (zero for ); .
For , and every Boolean on ,
with equality for every coordinate and its complement.
The goal OAI.SoftChannel204.fullMain is the conjunction of:
with equality for every soft coordinate , ; and for the joint law of . 2. Corollary 1.2. For Boolean with and : , strictly below when and ; coordinates and their negations attain ; and the bits conversion . 3. Theorem 1.3. For every interior : .
The result itself. It settles the Courtade–Kumar conjecture and strengthens it in two directions: to randomized summaries at fixed initial information, and to a bias-dependent bound that is strictly better for nonconstant biased outputs. Theorem 1.3 is a mean-dependent entropy-production inequality, stronger than the scalar rate needed for Theorem 1.1. Several independent proofs of the Boolean conjecture were announced in the same period; the preprint compares its production profile with that of Chen et al. in Section 8.
Formalizing it. All objects are finite sums over , so the statements are elementary to state in Lean. The proof requires an explicit three-point optimizer for a joining problem, convexity facts about and (Lemmas 2.2–2.4, pp. 5–6), dimension induction and integration along the noise semigroup. A formal proof would give a checked solution of a conjecture with several competing announced proofs, some computer-assisted.
The local-to-global method of Chen, Gohari and Nair needs a local inequality to pass from the two halves of the cube to the whole. The natural information-only profile fails the corresponding local comparison for some coupled pair laws, so the induction must carry the mean as well. The preprint uses the maximum of two profiles, and ; it must solve the minimization of the joining cost exactly (Section 3), pay the interior pair with a variance-refined one-bit inequality (Lemma 4.1, p. 12), and control the common-output corners by a thinning argument (Theorem 6.1, p. 17). The linear bound from the log-Sobolev inequality does not suffice; the nonlinear surplus above is where the difficulty lies.
Cube n = Fin n → Bool, averages are finite sums divided by , logs are natural; sign maps Bool to .psiInv is Function.invFunOn psi (Icc 0 1); since is strictly increasing on and , this is the paper's branch.noise ρ u y = ∑ x, kernel ρ y x * u x with kernel the product of , which is . Mutual information is the finite sum over the joint table, with terms omitted where the joint probability is .F is stated as psiInv s * artanh (psiInv s) and is only used on ; for interior , and , so reserve and hybrid are evaluated in their source domain.i : Fin n. The milestone (separate definition file) uses the crossover form with bits.Given vectors in the Euclidean unit ball of that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on ? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is , the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs , chosen once and for all, such that every signed prefix is , independently of . Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.
Work in Euclidean space with norm , and let satisfy ; repetitions and zero vectors are allowed. A prefix sum is for (the empty sum is ). For a zero-sum family, the Steinitz quantity
is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant is its supremum over all such families.
There is an absolute constant such that for all and all with :
The constant is not fixed. The simplex example in the source shows , so the order is optimal. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: . Theorem 1.1 settles the prefix-discrepancy question of Bansal et al., removing the term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.
Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.
Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a factor, because the probability that a random walk stays in a ball of radius for steps decays with . The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.
EuclideanSpace ℝ (Fin d), indexed by Fin N, with and .SignedPrefixBound C asks for signs (as reals) with every signed prefix at most . OrderingPrefixBound C asks, for zero-sum families, for a permutation with every reordered prefix at most . The goal is ; the same constant serves both, as stated in the source.The triangular Hilbert transform is a bilinear singular integral on the plane that couples translations in two different coordinate directions:
Paired with a third function, it becomes a trilinear form whose three inputs depend on the three pairs of variables of . This "triangular" or entangled structure defeats the time–frequency methods that handle the one-dimensional bilinear Hilbert transform. Boundedness of this operator is a model problem for multilinear singular integrals with simplex structure, and is closely tied to norm convergence and variation of ergodic averages for two commuting transformations. Thiele listed the symmetric case () as Problem 13 in the 2017 collection Some problems in harmonic analysis.
For complex functions on and , the hard truncation is
and the maximal truncation is
For the finite truncations converge absolutely outside a common null set, and is measurable (Lemma 7.1 of the source).
There is an absolute constant such that, for all complex ,
The Lean goal also includes the measure-theoretic preliminaries of Lemma 7.1: almost every point is a point where all finite truncations converge absolutely, and is almost-everywhere measurable. The goal statement is published on the platform with status Open.
The result itself. A uniform bound for the maximal operator controls a truncation chosen independently at each point, which is stronger than a uniform bound on each . It yields existence of the joint principal value almost everywhere and in (Theorem 7.2). By duality and a determinant-one change of variables, it gives endpoint-uniform bounds for the symmetric trilinear triangular form , which resolves Thiele's Problem 13 positively. Earlier bounds all grew with the number of scales.
Formalizing it. The estimate is a clean statement in Mathlib's and lower-integral language. Its proof combines matrix trace inequalities, Gaussian heat-flow energies and discretization limits, all of which would have to be built. The finite-dimensional matrix inequalities (Sections 2–3 of the source) are self-contained and reusable for other entangled multilinear forms.
Time–frequency analysis, which handles the one-dimensional bilinear Hilbert transform, does not adapt to the triangular form because its three inputs are entangled: each depends on a different pair of variables, so no single frequency-localization serves all three. Energy and telescoping methods (Kovač; Durcik) work for bipartite forms, but the triangular cycle is the documented obstruction. Previous cancellation estimates lose a factor depending on the number of scales . The maximal version adds a further difficulty: the truncation endpoints vary from point to point, so the energy argument must tolerate entries that switch on and off at independently chosen scales, without losses depending on the number of scales or on matrix dimensions.
ℝ × ℝ → ℂ with Lebesgue measure; hypotheses are MemLp F 3 and MemLp G 3 (which include a.e. strong measurability).truncation F G E z is the Bochner integral of over , with endpoints packaged as Endpoints ().GoodPoint requires integrability on the annuli for all , hence on every finite annulus. maximal is the ℝ≥0∞-valued supremum over all endpoint pairs at good points, and elsewhere. The goal asserts that almost every point is good, so this junk value cannot help.ℝ≥0∞, compared with eLpNorm F 3 * eLpNorm G 3. The constant is an existential ℝ≥0, so it is finite and independent of .Finite games in strategic form are the basic model of strategic interaction in economics, engineering and computer science. Potential games (Monderer and Shapley, 1996, DOI 10.1006/game.1996.0044) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics converge to one.
Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) decompose every finite game canonically into a potential, a harmonic and a nonstrategic component, by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games are the complement of potential games, and their equilibria behave in the opposite way: they generically have no pure Nash equilibrium. This mission formalizes the paper's positive result on the harmonic side. In every harmonic game, whatever the number of players and strategies, the profile in which every player randomizes uniformly over its strategies is a mixed Nash equilibrium. Rock–paper–scissors and matching pennies are the familiar two-player instances.
A finite game has a finite set of players and, for each player , a nonempty finite strategy set with elements. A strategy profile is . We write for the strategies of the players other than , , and for with player 's strategy replaced by . A game is identified with its utilities , , which form an element of , where carries .
Two profiles are -comparable if they are distinct and differ only in player 's strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function on ordered pairs of profiles with on edges and off edges. The space of edge flows carries . The combinatorial gradient is , with the edge indicator, and is its adjoint. Restricting to -comparable pairs gives , and is the flow of payoff differences of . With (Moore–Penrose pseudoinverse) and , Definition 4.2 of the paper sets
A game is a harmonic game if , and a normalized harmonic game if .
A mixed strategy of player is a probability vector , and a mixed strategy profile is . The mixed extension is (34). The payoff of the pure strategy against is (35). A mixed Nash equilibrium (Definition 5.1.1) is a mixed profile with for every and . A probability distribution on profiles is a correlated equilibrium (Definition 5.1.2) if for all and . The uniformly mixed strategy profile (Definition 5.2) has for every and .
For every harmonic game , the uniformly mixed strategy profile is a mixed Nash equilibrium:
Theorem 5.4 is the counterpart, for harmonic games, of the existence of pure equilibria in potential games. It exhibits an explicit equilibrium that does not depend on the payoffs at all, only on the strategy counts . Corollary 5.2, a milestone here, adds that at any mixed equilibrium of a harmonic game every player is indifferent among all its pure strategies, including those outside the support. That is much stronger than the usual support condition. Proposition 5.2 shows that the correlated equilibria of a normalized harmonic game are the points of the probability simplex in a linear subspace determined by the utilities. The paper uses that description in its later analysis of two-player harmonic games.
The results are proved in the paper; none of them is machine-checked. The formalization connects the paper's operator layer (flows on the game graph, the gradient and its adjoint with the -weighted inner product, pseudoinverses) with standard equilibrium notions on finite games. It reuses published definitions of lotteries, the mixed extension and correlated equilibria.
The equilibrium statement follows quickly once Lemma 5.2 is available. The difficulty lies in translating the harmonic condition, a statement about the adjoint of an operator on edge flows, into an identity about payoffs. That needs the explicit form of , which depends on the in the inner product of . It also needs the fact that kills the nonstrategic component, and a computation of the flow of across the boundary of the set of profiles in which player plays . Corollary 5.2 needs the passage from mixed profiles to product distributions on profiles and a careful accounting of sums over against sums over full profiles.
The first idea, to use the normalization , is not available. The goal concerns all harmonic games, not only normalized ones, and normalization alone does not give indifference against uniform opponents: the harmonic condition is essential.
Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper (). The hypothesis [∀ m, Nonempty (E m)] is stated explicitly on the game theorems, because the uniform profile is a probability vector only if . A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted sum inner product of p. 14. is the subspace of edge flows with the inner product of (7). is Mathlib's adjoint, and the pseudoinverse is defined directly. and are defined by (28), and harmonic games are the submodule H ⊔ N. Lotteries, mixed profiles and the mixed extension (34) come from the published agt_games definitions; correlated equilibrium is the published HartSchmeidler.Finite.IsCorrelatedEq. The pure-deviation payoff (35), mixed Nash equilibrium with pure deviations (Definition 5.1.1, as printed), and the uniform profile are defined in the mission. Sums over are written as sums over the profiles with player 's strategy fixed, so each is counted once.
The goal concerns mixed Nash equilibria. Stating it for the uniform product distribution as a correlated equilibrium, or for normalized games only, would be a weaker statement and is not the target. No hypothesis is added beyond the nonemptiness of the strategy sets.
Contributions welcome: proofs of the milestones, and general lemmas on adjoints of graph gradients and on product distributions that are reusable beyond this mission.
Many data matrices are, to a good approximation, the sum of a sparse matrix (few nonzero entries) and a low-rank matrix. In system identification the low-rank part models a system of small order and the sparse part a system with sparse impulse response; in statistics the same structure appears in latent-variable graphical models, where a sparse inverse covariance is corrupted by a low-rank effect of hidden variables; in signal and image processing it separates a slowly varying background from sparse outliers. Recovering the two components from their sum is NP-hard in general, so a convex relaxation is the natural tractable approach.
Chandrasekaran, Sanghavi, Parrilo and Willsky (arXiv:0906.2220, SIAM J. Optim. 21(2), 2011, doi:10.1137/090761793) introduced the convex program that minimizes a weighted sum of the entrywise norm and the nuclear norm, and gave a deterministic condition under which it recovers both components exactly. The condition is an uncertainty principle between the support of the sparse matrix and the row and column spaces of the low-rank matrix. Their analysis was followed by probabilistic guarantees for the same program under random sparsity patterns (Candès, Li, Ma, Wright, Robust Principal Component Analysis?, J. ACM 2011, arXiv:0912.3599).
All matrices are real and square, . For a matrix :
The two rank-sparsity incoherence quantities are
Small says that the elements of are not concentrated on few entries; small says that the elements of have diffuse spectra.
Given and a trade-off parameter , the decomposition program is
If
then for every
the pair is the unique optimum of (1.3); moreover always lies in this interval (for ).
Theorem 2 is a deterministic exact-recovery guarantee: it involves no randomness, only the support of and the row and column spaces of , and so it applies to any fixed instance for which and can be bounded. Combined with the paper's bounds of by the maximum number of nonzeros per row or column and of by the coherence of the singular vectors, it yields explicit sparsity-versus-incoherence trade-offs under which (1.3) succeeds. It is the starting point of the analysis of sparse-plus-low-rank decompositions in robust PCA, latent-variable graphical model selection and system identification.
The theorem is proved in the paper. No machine-checked proof of it, of Propositions 1–2, or of the subdifferential characterizations (4.4)–(4.5) is known to exist. A formalization adds: a checked account of the edge cases the paper leaves implicit (a zero sparse or low-rank component, the open endpoints of the -interval), a reusable library of the two tangent spaces and their projections for the Prove2Me matrix-completion definitions, and the nuclear-norm subdifferential (Watson's theorem), which is used throughout low-rank recovery.
The obvious argument writes down a dual certificate and checks four conditions; the work is in showing that one exists. The natural candidate is defined implicitly, as the unique element of with prescribed projections onto and , and its existence is a linear-algebra fact about two transverse subspaces, not a formula. Bounding its components outside and requires coupled estimates in two different norms, the spectral norm and the entrywise maximum, related only through and . On the convex-analysis side, the "only if" direction of the nuclear-norm subdifferential characterization (4.5) is a genuine theorem about singular values, not a computation.
Statements follow the arXiv v1 preprint (arXiv:0906.2220v1), with its numbering and page numbers. Matrices are Matrix (Fin n) (Fin n) ℝ; the rectangular remark of §3 is not formalized. The nuclear norm, spectral norm, , trace inner product, , , the SVD datum and are the published Prove2Me definitions matrix_completion_basic, matrix_completion_svd and matrix_completion_tangent. The SVD of is an explicit argument: , and are taken with respect to it, and every statement holds for every compact SVD. and are real suprema of bounded sets containing , hence maxima. Subgradients use the inequality ; means for a subgradient .
"Unique optimum" is strict: every other feasible pair has strictly larger objective, so a statement only asserting that minimizes the objective, or a definition of or that collapses to , does not count. The upper end of the -interval is stated as , which is the paper's condition when and means "no upper bound" when ; the "specifically" clause assumes and because it divides by and needs .
A complete development needs: the subdifferentials of the and nuclear norms, the fixed-point and norm properties of (in particular ), and the direct-sum argument for . The nuclear-norm subdifferential and the bounds are reusable across all of low-rank matrix recovery. Proofs of any milestone, and lemmas that shorten the Appendix B estimates, are welcome.
In a flexible commitments contract a retailer announces, before a selling horizon starts, a vector of planned orders (commitments) to its supplier, who uses them to plan capacity. During the horizon the retailer may deviate from the commitments, but pays penalties for each deviation and for changes between successive commitments. Such contracts were studied with stochastic demand by Bassok and Anupindi, Tsay and Lovejoy, and others, typically by dynamic programming over a discretized state space.
Ben-Tal, Golany, Nemirovski and Vial (2005) treat the retailer's problem as a robust multiperiod linear program: demand is only known to lie in an uncertainty set, decisions may adapt to observed demand, and the retailer minimizes its worst-case total cost. Most of the paper approximates this problem by affinely adjustable decision rules. For one important case, however, the paper shows that the problem can be solved exactly: when the uncertainty set is a box, nature may be restricted to the finitely many corner trajectories of the box. That reduction, Proposition 1 of the Appendix, is the subject of this mission, together with the general principle behind it (Lemma 2), which applies to any multistage worst-case problem with polyhedral dynamics and convex polyhedral costs.
Data. There are periods. Period carries an ordering cost , a holding cost , a shortage cost , penalties for ordering above or below the commitment, and penalties for raising or lowering the commitment relative to the previous one. A salvage value applies to the final inventory; put for and . The initial inventory and a nominal previous commitment are given, as are order bounds and cumulative bounds , possibly infinite.
Decisions. Before any demand is observed the retailer fixes commitments and amounts . Demand lies in a product set . The order and the cost bounds of period are decision rules, functions of the past demands ; the inventory is a function of . This nonanticipativity is required on trajectories of .
The min-max RSFC problem (5)–(6). A policy is feasible if for every and every : ; the order and cumulative-order bounds hold; and ; and ; and , . The optimal value is
Box uncertainty (9)–(10). with ; its extreme points are .
Convex polyhedral functions. A function is a c.p.f. if its domain is the solution set of finitely many linear inequalities and is convex and lower semicontinuous on it. Lemma 2 concerns the generic problem : minimize, over decision rules , the worst case over of , subject to , and .
The data are arbitrary reals (bounds in ) and the values are compared in the extended reals, so the statement covers infeasible and unbounded instances.
Proposition 1 turns a semi-infinite multistage problem into a finite one: with box uncertainty, the min-max RSFC problem is equivalent to a linear program over the scenario tree of the corner trajectories, problem of §2.3. The paper uses this exact value as a benchmark for its affinely adjustable approximation in the simulation study. Lemma 2 is the transferable statement: in any multistage worst-case problem whose stage costs are convex polyhedral and whose dynamics are linear with a uniform box on the decisions, the adversary may be restricted to the vertices of each period's uncertainty polytope.
The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a reusable notion of convex polyhedral function in the extended reals, closure properties of that class (partial minimization over a polyhedral box, affine substitution, finite maxima, sums), and a formal worst-case Bellman equation for nonanticipative policies. The corrected form of the -box step also records precisely when the paper's informal "for large enough" argument is valid.
The natural argument, "a convex function attains its maximum over a polytope at a vertex", applies to one stage only. In a multistage problem the cost of the last stage depends on the earlier decisions, which depend on earlier demands, so the worst case is not a convex function of the whole trajectory. The proof must therefore pass through a dynamic programming recursion, and the class of stage costs must be closed under the recursion: the optimal last-stage value as a function of the previous decision must again be convex polyhedral. That closure (the value of a parametric problem with a convex polyhedral objective and a box constraint) is where the work is: the domain is a projection of a polyhedron, and attainment and lower semicontinuity have to be shown with infinite values allowed.
A second difficulty is bookkeeping. The RSFC problem must be rewritten as an instance of Lemma 2 with the right stage vectors so that nonanticipativity of in is preserved, and the bounded problem must be related back to the unbounded one, which can have value .
Periods of the RSFC model are Fin T, 0-based. Policies are functions of the whole demand trajectory with nonanticipativity imposed on trajectories of the uncertainty set; a policy that sees future demand is not admissible, which rules out the clairvoyant reading under which the statement changes. Optimal values are EReal infima of suprema: for infeasible problems and possibly , never a real sInf that would turn both into . The c.p.f. definition requires the domain to be exactly a finite system of linear inequalities, so it cannot be satisfied vacuously.
The standing assumptions of §2.2, and (1) , are not imposed, and no sign is assumed on any cost or penalty: Proposition 1 holds without them, so the formal statement is a generalization. The norm is Mathlib's default norm on Fin m → ℝ. Lemma 2's families are indexed by with the paper's indices; B t, C t stand for , . Two printed slips are corrected in the statements: (38) keeps the that the page drops, and the -box step is stated in the corrected sandwich form because the literal claim fails when the value is .
Useful infrastructure: convex polyhedral functions in EReal, Fourier–Motzkin projection of polyhedra, maximum principle for convex functions on polytopes, extreme points of convex hulls of finite sets. Contributions to any milestone, and to general lemmas on these topics, are welcome.
Airlines, hotels and car-rental firms sell reservations ahead of service, and a fraction of those reservations cancel or do not show up. Overbooking — accepting more reservations than there is capacity — recovers revenue that cancellations would otherwise destroy, at the risk of denying service to some customers. In practice inventory is often substitutable: a passenger booked in economy can be upgraded to business, a guest booked in a standard room can be given a suite. With substitution, the right overbooking level for one reservation class depends on the levels of all the others.
Karaesmen and van Ryzin (Operations Research 52(1):83–104, 2004) model this as a two-period problem: overbooking decisions in a reservation period, followed by an optimal assignment of the customers who actually show up to inventory classes in a service period. Their structural result, Theorem 2, establishes the shape of the expected net revenue as a function of the overbooking levels. That shape is what justifies critical-level booking policies and the stochastic-gradient method of their §4, and it is the textbook account of joint overbooking with substitution (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 4.4).
There are reservation classes and inventory classes . Class is virtual: assigning a customer to it means the customer is denied service.
Reservation period. The firm holds reservations of class and chooses overbooking levels . Accepting a class- reservation earns ; a cancellation of class is refunded , with . The number of class- customers who survive to the service period is a random variable with values in . The family has the semigroup property: if and are independent with the laws of and , then has the law of . The binomial model ( for integer ) and the Poisson model () both have it. The survivals of different classes are independent.
Service period. Given the survivals , net benefits (of either sign) and capacities , the firm solves the transportation problem
Expected net revenue. The objective of the reservation period is
to be maximized over .
A function on is submodular on if for , with the componentwise maximum and minimum.
For every with levels in the parameter set , every class and all ,
and is submodular on :
The first statement is the paper's componentwise concavity (6); the second is its submodularity, proved in the paper through the pairwise inequality (7) and Theorem 1.
Componentwise concavity of implies that for each reservation class there is a critical booking level beyond which expected revenue does not increase, other levels held fixed. Submodularity implies that these critical levels are nonincreasing in the bookings accepted for any other class: heavier overbooking in one class leaves less spare substitute capacity for the others. These two properties underpin the heuristics and the stochastic-gradient optimization of §4–§5 of the paper.
The result is proved in the paper (for , with the general case described as straightforward). A machine-checked version would cover the general semigroup case, which includes the binomial model the paper calls realistic, real-valued levels and arbitrary step sizes. The platform already holds a proved special case, RevenueManagement.joint_overbooking_concave_submodular (Talluri–van Ryzin, Proposition 4.4): Poisson survivals, integer levels and unit steps only. This mission generalizes it in all three respects and also formalizes the transportation-problem facts (LP duality, submodularity and concavity of ) as reusable statements.
The obvious route — differentiate and use concavity of — fails twice. First, is piecewise linear and the survivals are discrete, so there is nothing to differentiate; under the binomial model is only defined at integer levels. Second, concavity of alone does not survive the expectation: is a mixture over laws that change with , and a concave function of a random vector whose law moves with the parameter need not be concave in the parameter. The semigroup property is what replaces a change of law by the addition of an independent block of survivors, and that coupling must be built for every coordinate and every pair of coordinates at once. On the LP side, submodularity of a transportation-problem value in its demands is a lattice-programming fact (Topkis, Theorem 3.4.1; Shapley 1962), not a consequence of concavity.
All declarations are in the namespace SubstOverbooking.Structure. Reservation classes are Fin n (0-based), inventory classes Fin (m + 1) with 0 the virtual denied-service class. Conventions committed to:
SupermodularOn applied to .A formalization that fixes Poisson laws, integer levels or unit steps, or that defines or through the inequalities to be proved, is the already-proved special case or an empty statement, and is not the goal.
A complete development needs finite LP duality for the transportation problem, the lattice-programming argument for Lemma 1, product measures and image measures on , and the coupling of the semigroup property. The LP and lattice parts are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1 (for instance via monotonicity of optimal duals, after Erlenkotter 1970).
Conic quadratic (second-order cone) programs are solved in practice by primal-dual interior-point methods. Each iteration solves a Newton system for the central-path equations, and for non-polyhedral cones that system is only guaranteed to be well posed after the problem is scaled: the primal point and the dual slack are transformed by a matrix chosen from the current iterate. Among the scalings analysed by Monteiro and Tsuchiya (2000), the best complexity bounds are obtained with the Nesterov–Todd (NT) scaling of Nesterov and Todd (1997), which maps and to the same point.
Andersen, Roos and Terlaky (2003) describe the conic quadratic interior-point solver of MOSEK. Their Lemma 4.2 gives the NT scaling in closed form for each of the three cone types they use. It is what makes the NT direction cheap: each cone block of is determined by one vector , and , and their inverses can be applied in time linear in the dimension. For the quadratic cone the formula goes back to Tsuchiya (1999); the paper re-derives it and extends it to the rotated quadratic cone.
Fix one cone block of dimension . Coordinates are , denotes the subvector of coordinates , and is the Euclidean norm. The block is one of
A scaling matrix (Definition 3.3) is a symmetric positive definite with . For the scaled points are and . The pair is an NT scaling of when , equation (28); equivalently , equation (29).
For in the interior of the cone:
the following matrices make an NT scaling: for ;
for ; and
for . In the last two cases , equations (33) and (35).
Lemma 3.3 i)–iii) (scaling preserves and rescales , by ); (30) on its own; the normalization and the square (62) of the arrow form (31); positivity of the radicand of (32); the identity and the formula (32); for the rotated cone, the transport (63) by , the identities and , and . Two companions: Lemma 4.3, , and Lemma 3.3 iv), that a scaling maps the cone and its interior onto themselves.
The result. Lemma 4.2 turns the NT scaling, defined implicitly by (28), into explicit data: one scalar and one vector per cone. Combined with Lemma 4.3 it shows that every product with , or their inverses in the scaled Newton system (27) is a rank-one correction of a signature matrix, which is what the paper's implementation relies on. The rotated-cone formula (34) is the paper's own addition and is what lets rotated cones be handled natively instead of through a change of variables.
Formalizing it. The result is proved on paper; no machine-checked version is known to exist, and the platform has no formalization of second-order-cone scalings. The work is the matrix algebra of the Lorentz group — the signature matrix , the matrices with , and their action on and — which is reusable for every second-order-cone algorithm.
Most of the items are finite-dimensional identities, but they are identities between block matrices of arbitrary size with entries that are nested square roots, and they hold only on the interior of the cone, where the radicands are positive. The derivation in the paper runs backwards: it assumes has the shape (31) and solves for , taking a square root without fixing its sign. The goal asks for the forward direction — that the displayed , , do satisfy (28) and — which needs the normalization , positive definiteness of , and, for the rotated cone, the reduction to the quadratic cone through with and .
kind : ConeKind, and vectors are Fin d → ℝ.0. is written as a sum of squares (tailSq x 1); Mathlib's norm on Fin d → ℝ, which is the sup norm, is never used.A complete development needs:
Matrix.PosDef and Matrix.inv;Lemmas about (closure under products and inverses, invariance of ) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for positive definiteness of (31).
In a road or communication network, each user picks a route to minimize its own delay, without regard to the delay it imposes on others. The outcome is an equilibrium that is in general not socially optimal: Braess's paradox shows that adding a road can make every user worse off, and Pigou's two-link example shows that selfish users can incur a third more total delay than a central planner would. Transportation science has studied such equilibria since Wardrop (1952) and Beckmann, McGuire and Winsten (1956). The computer-science question of how much is lost, uniformly over all networks, was answered for linear delays by Roughgarden and Tardos in How Bad is Selfish Routing? (FOCS 2000; J. ACM 2002, doi:10.1145/506147.506153). Their bound became the first instance of the price of anarchy for nonatomic routing and the template for a large literature on the inefficiency of equilibria.
Timeline. Wardrop (1952) states the equilibrium principle. Beckmann et al. (1956) and Dafermos–Sparrow (1969) characterize equilibria and optima by convex programs. Koutsoupias and Papadimitriou (1999) introduce the worst-case ratio of equilibrium to optimum. Roughgarden and Tardos (2000/2002) prove the bound for linear latencies, tight by Pigou's example. Roughgarden (2003) and Correa, Schulz and Stier-Moses (2004) extend the analysis to general latency classes.
A network has finitely many edges and finitely many routes ; a route is the set of edges it uses, recorded by a incidence. There are commodities; each route serves one commodity , and is the set of routes serving . Commodity has a positive rate . A flow assigns a nonnegative amount to each route; it is feasible for if for every . The edge flow is .
Each edge has a linear latency with . The latency of a route is , and the cost of a flow is
A feasible flow is at Nash equilibrium if no small amount of flow on a route can reduce its latency by moving to another route of the same commodity (Definition 2.1); equivalently (Lemma 2.2), every used route of commodity has minimum latency among the routes in . A flow is optimal if it is feasible and has minimum cost among feasible flows. The marginal cost of edge is , and .
The Lean development uses the names pathLatency, cost, IsNashFlow, IsOptimalFlow, linLatency, marginalLatency and minMarginalPathCost for these objects.
For every instance with linear latencies , every Nash flow and every feasible flow ,
This is the paper's , stated without the ratio.
The bound says that, with linear delays, selfish routing never costs more than times the optimum, independently of the network's size and topology and of the number of commodities. It explains why Braess-type phenomena are bounded in magnitude, and it yields consequences for mechanical networks of strings and springs (Corollary 4.6 of the paper). The inequality for every feasible is the basic input to later work on bicriteria bounds, Stackelberg routing, tolls and the general price-of-anarchy framework.
The result is proved in the paper and in textbooks (Nisan et al., Algorithmic Game Theory, ch. 18). No machine-checked proof is known to exist on Prove2Me or in Mathlib. A formalization produces a checked model of nonatomic routing (route flows, Nash and optimal flows) together with the first-order characterization of optimal flows for convex quadratic costs, both of which are reusable for the other results of the paper and for later routing papers.
The equilibrium bound is not a pointwise inequality between the two flows: the Nash flow and an arbitrary feasible flow can use entirely different routes. The step that requires real work is the comparison between an optimal flow for the rates and an arbitrary flow for the rates (Lemma 4.4), which rests on the characterization of optimal flows of a convex program (Lemma 4.1(b)). That characterization is a Karush–Kuhn–Tucker statement over a polytope of route flows; the paper cites it rather than proving it, and Mathlib has no ready-made version. The naive approach, bounding each edge's cost separately, fails because the two flows load different edges.
Fin J, Fin R, Fin Sd. A route is a column A j r of the incidence; the commodity of route r is s r. The paper's simple paths in a directed graph are one instance, so all statements are a disclosed generalization; copies of one path serving two commodities are two routes.KellyStochasticNetworks.linkFlow and KellyStochasticNetworks.wardropFeasible; the Wardrop condition is KellyStochasticNetworks.IsWardropEquilibrium.0 < rate i), as on p. 6. Linear latencies have , and only their values at nonnegative arguments matter.Needed infrastructure: the edge/route exchange of summation, the first-order optimality conditions for a convex differentiable function on a product of simplices, and the convexity inequality . Contributions of a general KKT lemma for separable convex costs on flow polytopes are reusable beyond this mission.
Many problems in system identification, collaborative filtering, low-dimensional embedding and model reduction ask for the simplest matrix consistent with a set of linear observations, where "simplest" means "of least rank". Given a linear map and a vector , the affine rank minimization problem is
This problem is NP-hard in general: it contains the problem of finding the sparsest solution of a linear system as the special case of diagonal matrices. A standard heuristic, popularized in control by Fazel, Hindi and Boyd, replaces the rank by the nuclear norm , the sum of the singular values, which is the convex envelope of the rank on the unit ball of the operator norm. The resulting problem is a semidefinite program and can be solved efficiently.
Recht, Fazel and Parrilo (arXiv:0706.4138, SIAM Review 2010) gave the first general conditions under which this heuristic provably returns the minimum-rank solution. Their argument transfers the compressed sensing theory of Candès and Tao (Decoding by linear programming, 2005) and Candès, Romberg and Tao from sparse vectors and the norm to low-rank matrices and the nuclear norm. This mission formalizes the paper's deterministic recovery theorem (Section 3).
Matrices are real matrices. For matrices of the same size, is the trace inner product. With the singular values of , the three norms used are the operator norm , the Frobenius norm , and the nuclear norm .
A linear map is given by measurement matrices through ; is the Euclidean norm of the vector .
For an integer , the -restricted isometry constant (Definition 3.1) is the smallest with
Fix a matrix of rank at most , put , and consider the nuclear norm minimization problem
If and , then ; precisely,
The statement holds for every linear map, every and every of rank at most . The constant is the paper's; the paper notes (p. 14) that its derivation is chosen for simplicity and is not optimal.
Theorem 3.3 is a deterministic certificate: it separates the question "does nuclear norm minimization recover low-rank matrices?" into a property of the measurement map alone, with an absolute constant independent of , , and . Section 4 of the same paper then shows that random maps with i.i.d. Gaussian or Bernoulli entries satisfy with high probability once is of order , so a matrix with entries is determined by far fewer measurements than entries and is found by a semidefinite program.
The theorem is proved in the paper, and the sparse-vector analogue has been formalized on this platform (HighDimProb.SparseRecovery.rip_implies_exact_recovery, from Vershynin's textbook; CandesTao.Decoding.decoding_by_lp). The matrix version is not formalized. A machine-checked proof needs the basic theory of singular values for rectangular real matrices (the norm comparisons (2.1), additivity of the nuclear norm, the triangle inequality for the nuclear norm, and block decompositions via the singular value decomposition), most of which Mathlib lacks in this form. That infrastructure is reusable for every nuclear-norm result on the platform.
For sparse vectors the analogous proof splits the error vector by its support, and every step is coordinatewise. For matrices there is no common basis: the error and the target have different singular vectors, and the restricted isometry inequality controls only matrices of low rank. The first obstacle is therefore to split into a piece of rank at most and a piece whose row and column spaces are orthogonal to those of , so that the nuclear norm is additive. The second is that the triangle inequality, additivity and the norm chain (2.1) for the nuclear norm are themselves nontrivial statements about singular values. Applying the restricted isometry inequality directly to fails, because need not have low rank.
Matrix (Fin m) (Fin n) ℝ; rank is Matrix.rank; transpose is Xᵀ. The norms and the inner product are opNorm, frobeniusNorm, nuclearNorm and traceInner of the published module HighDimStat_MatrixRank_Core, which defines the nuclear norm as the sum of the square roots of the eigenvalues of .Xs : Fin p → Matrix (Fin m) (Fin n) ℝ and evaluated by observationOp; measNorm Xs X is .ripConst Xs r is the infimum of the admissible ; the set is nonempty and closed, so the infimum is attained. It is defined for every , not only , since the goal uses . The paper's normalization is not assumed.Welcome contributions: a rectangular SVD with ordered singular values, the triangle inequality and duality for nuclearNorm, and the attainment and monotonicity lemmas for ripConst.
The support vector machine (SVM) is a linear classifier trained by minimising a regularised hinge loss. For training sets with millions of examples, solving the SVM problem to high accuracy by interior-point or dual decomposition methods is too slow, and what is needed is an algorithm whose cost per iteration does not grow with the number of examples. Pegasos (Primal Estimated sub-GrAdient SOlver for SVM), introduced by Shalev-Shwartz, Singer and Srebro in 2007 and analysed in its final form by Shalev-Shwartz, Singer, Srebro and Cotter in Mathematical Programming (2011, doi:10.1007/s10107-010-0420-4), is a stochastic sub-gradient method on the primal SVM objective with step size . Its analysis showed that the number of iterations needed for accuracy is , independent of the training-set size, and the method became a standard baseline for large-scale linear SVM training.
The analysis rests on a logarithmic-regret bound for online gradient descent on strongly convex functions, due to Hazan, Agarwal and Kale (Machine Learning 69, 2007), which the paper re-proves for non-smooth functions as its Lemma 1 and then applies to the Pegasos iterates in its Theorem 1.
A training set consists of examples , , with and labels . The hinge loss of a weight vector on is . For a regularisation parameter , the SVM objective (Eq. (1)) is
and denotes a minimiser of (Eq. (9)). For a mini-batch of example indices, the instantaneous objective (Eq. (7)) is
Mini-batch Pegasos (Fig. 2 of the paper) starts at . At each round it receives a mini-batch , forms the sub-gradient
of at , and sets with . Optionally it then applies the projection step (6), , which maps to the closest point of the Euclidean ball of radius . A function is -strongly convex if is convex, and is a sub-gradient of a convex at if for every .
In the Lean development these objects are svmObj, instObj, subgrad, projBall and run in the namespace Pegasos.Analysis; the hinge loss is UnderstandingML.hingeLoss, sub-gradients are UnderstandingML.IsSubgradient, and " is the projection of onto " is LogRegretOCO.OGD.IsProj B v z.
Assume for every , and set when the projection step is performed and when it is not. Then for every sequence of mini-batches and every ,
The constants are the paper's and are stated exactly; a version with a single constant for both variants, or with an unspecified constant, is a weaker theorem.
Theorem 1 is the deterministic core of every guarantee in the paper. Taking expectations over uniformly random mini-batches turns its left side into the expected objective of the iterates and its right side into plus the rate, which yields the iteration bound and, via Markov-type arguments, the high-probability bounds of the later sections. Because the bound holds for every sequence of mini-batches, it is also an online-learning regret bound for the sequence of instantaneous objectives.
The result is proved in the paper and is classical. To our knowledge it has no machine-checked proof. Formalizing it produces a verified logarithmic-regret lemma for non-smooth strongly convex sub-gradient descent with an arbitrary closed convex feasible set (the platform currently has the twice-differentiable version with a bounded feasible set), a verified sub-gradient calculus for the regularised hinge loss, and an exact treatment of the Pegasos iteration including both the projected and unprojected variants.
The obvious argument applies Lemma 1 with the ball of radius in both variants and the sup of over that ball. This fails twice. Without the projection step the iterates are not confined to that ball, so a separate argument (the closed form (13)) is needed to bound them, and it gives the different constant . With projection, Lemma 1 requires the comparator to lie in the ball, and is not implied by the elementary comparison , which only gives ; the paper obtains the sharp radius through duality. In Lemma 1 itself, the telescoping only closes because the step size is matched exactly to the strong-convexity modulus; any off-by-one in the step indexing breaks the cancellation.
Vectors are EuclideanSpace ℝ (Fin n), examples are indexed by Fin m, labels are real numbers with the hypothesis , and , are hypotheses. A mini-batch is a -tuple Fin k → Fin m: an injective tuple is a subset of size as in Fig. 2, a non-injective one is the multi-set with repetitions the paper also allows. The theorem is stated for every sequence of mini-batches A : ℕ → Fin k → Fin m; no probability space appears, because the proof never uses that the batches are random. Iterations are 1-based: run … 1 = 0, the step producing uses and the batch only, and index 0 is unused. The variant is selected by a Boolean flag, and depends on it. is any with for all , minimising the full objective (1), not the instantaneous ones. Strong convexity is the paper's own definition, convexity of . At the projection formula is evaluated with Lean's , which gives the intended value . The paper's display (12) has two printed slips (the sign of the term and for ); the Lean states the correct update, and Eq. (13) is correct as printed.
A trivializing formalization is ruled out: the goal is stated for the concrete iteration run, not for an abstract sequence assumed to be sub-gradient steps or projections, and those facts are separate milestones.
A complete development needs the sub-differential sum rule for a convex function plus a quadratic, convexity of the hinge loss, the variational characterisation of the projection onto a ball, the harmonic-sum bound , and a proof of (through duality or a direct optimality argument). Lemma 1 and the sub-gradient lemmas are reusable for any strongly convex stochastic sub-gradient method. Proofs of any milestone, and alternative proofs of the bound on that avoid the dual problem, are welcome.
Scheduling jobs on identical parallel machines to minimize the total weighted completion time , the problem , is one of the basic NP-hard problems of machine scheduling. On a single machine it is solved by Smith's ratio rule (Smith 1956); with several machines the only hard decision is which jobs share a machine. Section 6 of M. Skutella's paper Convex quadratic and semidefinite programming relaxations in scheduling (J. ACM 48 (2001)) observes that this decision is a graph partitioning problem: the cost of a schedule is, up to a constant, the weight of the edges that a partition of a weighted complete graph does not cut. Minimizing on machines is therefore equivalent to Max--Cut on that graph, and the paper shows that the equivalence preserves approximation in a quantified way.
The reduction explains, from the graph side, why semidefinite rounding works for two machines: with the 0.878-approximation for MaxCut of Goemans and Williamson (1995) it gives a 1.122-approximation for (Corollary 6.2 of the paper). For general , the uniform random partition is both a -approximation for Max--Cut and randomized rounding of the optimum of the convex quadratic relaxation (CQP).
There are jobs and identical machines. Job has a processing time and a weight . Smith's order puts when , ties broken by index. An assignment is a partition of the jobs; each machine processes its jobs in the order without idle time, so the completion time of is
The value of is , and is the minimum value over all assignments.
The graph is the complete graph on in which the edge with has weight ; is its total weight. A partition induces the -cut , the edges whose endpoints lie in different parts, of weight ; is the maximum weight of an -cut.
The convex quadratic relaxation (CQP) of §2.2, specialised to identical machines, has variables with and objective where
Its optimum value is .
For , any assignment whose -cut weighs at least satisfies
That is, a -approximation algorithm for Max--Cut translates into a -approximation algorithm for . The constant is a parameter, so the goal does not depend on the best known cut algorithm.
The result. Theorem 6.1 makes Max--Cut algorithms usable for scheduling with an explicit loss: a cut algorithm with ratio close to yields a schedule within of optimal. For and the Goemans–Williamson ratio the guarantee is , better than the of Theorem 2.6 b) and the of the paper's semidefinite rounding in §5. In the other direction, (38) bounds the maximum cut of by the scheduling lower bound , which is how a relaxation for scheduling becomes a bound for a cut problem. The problem itself is better understood today: has a polynomial-time approximation scheme (Skutella and Woeginger 2000), and a fully polynomial one for fixed (Sahni 1976). The reduction remains of interest as a structural identity between the two problems and as the source of the closed-form relaxation bound (37).
Formalizing it. All statements are proved in the paper; none is known to have a machine-checked proof. The mission produces a formal model of identical-machine scheduling under Smith's rule, of the weighted graph and its -cuts, and of (CQP) for identical machines, together with the closed-form optimum of (CQP) (Lemma 2.5), which is the basis of the guarantee of Theorem 2.6 b).
The bookkeeping identity (36) and the final chain of inequalities are finite-sum manipulations. The substance is Lemma 2.5: that the uniform vector minimizes the quadratic objective (11) over the product of simplices. The objective is not separable, since the term couples jobs through Smith's order, and its convexity on the feasible region (the positive semidefiniteness established in Lemma 2.4 of the paper) is the fact on which optimality and, with distinct positive ratios, uniqueness rest. The relaxation half of (37), that is at most the value of every schedule, needs the observation that evaluated at the 0/1 vector of an assignment equals the value of that assignment.
Jobs are Fin n and machines Fin m, 0-based; Smith's order is cross-multiplied (, or equality and ), equal to the ratio definition because . Assignments are functions Fin n → Fin m, and every machine is sequenced by ; by Smith's rule (p. 7 of the paper, a classical result it cites) this loses no optimality, so is the minimum over assignments and is never a primitive: "within factor of " is stated against the value of every assignment. Likewise "weight at least " is stated as for every assignment , so no supremum of an empty or unbounded set can enter. The edge weight is attached to the ordered pair with and is zero on the other orientation, so each edge of is counted once. Standing hypotheses on every theorem: , (p. 2 of the paper) and (needed for ). Theorem 6.1 keeps the page's .
Not formalized: polynomial running time, the phrase "approximation algorithm" beyond the value bound it asserts, and the semidefinite results of §5 and Corollary 6.2. A trivializing reading, such as stating the cut condition against a junk-valued supremum or replacing by a free variable, is excluded by the encodings above.
The development needs only finite sums over Fin types and real arithmetic; the model of identical-machine scheduling under Smith's rule and the closed form of (CQP) are reusable for other results on . Proofs of the milestones, alternative proofs of Lemma 2.5 (the KKT argument the paper mentions, or Goemans' symmetrization argument it gives), and a proof of Theorem 2.6 b) are all welcome.
Retailers in many categories accept returns of products that are not defective: a consumer buys, learns whether the product suits them, and may send it back for a refund. Returns of this kind are a large cost item in retailing, and the refund a retailer offers is an operational decision on a par with its price and its stocking quantity. Xuanming Su, Consumer Returns Policies and Supply Chain Performance (SSRN 1020451, version of August 2008; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240), studies this decision first for a single seller and then in a supply chain.
This mission formalizes the supply chain part, Section 5 of the paper. A classical result of supply chain contracting is that a manufacturer can align a retailer's ordering decision with the interest of the whole chain by a buy-back contract, which pays the retailer a credit for unsold units (Cachon, Supply Chain Coordination with Contracts, 2003). Su shows that once the retailer also sets a consumer returns policy, the standard buy-back no longer coordinates, and identifies three contracts that do. The companion mission (mission 1 of this series) formalizes the single-seller results of Sections 3–4, in particular Proposition 2, which gives the supply chain optimum used here.
A consumer who buys at price learns a valuation , drawn independently from a law with finite mean , and then either keeps the product or returns it for the refund . Keeping is optimal when . Write
for the probabilities of keeping and returning. A consumer's expected utility from buying is , which is therefore the reservation price: all consumers buy if and none buys otherwise (the demand rule (6)). Market demand has distribution function and ; a stock sells in expectation when consumers buy, and nothing when they do not. Write for these expected sales. The production cost is , leftover and returned units are salvaged at , and .
The total supply chain profit is
A manufacturer sells to a retailer, who sets , and (except in Proposition 4) . The contracts are:
The supply chain optimum, from Proposition 2 of the paper, is
For and , the differentiated buy-back
makes the supply chain optimum a retailer optimum and gives the retailer the share :
and the contract is implementable: , , .
The results separate what a contract must observe in order to coordinate a chain with consumer returns: either the manufacturer distinguishes returned from unsold units (Propositions 3 and 4), or it observes sales (Proposition 5). The negative results (milestones 1 and 8) show why the standard buy-back and a kept-only rebate fail: each distorts the retailer's refund away from the salvage value. These statements are proved in the paper by short arguments; none of them has, to the knowledge of this mission, a machine-checked proof. Formalizing them yields a reusable model of a newsvendor with an endogenous price and refund under valuation uncertainty, and a checked account of the coordination conditions, including the boundary cases (, atoms in the valuation law) that the paper does not discuss.
Each result combines two optimizations, and neither is routine at the generality of the formal statements. The first is over price and refund jointly: the demand rule makes every profit discontinuous in and , and the refund problem must be solved for an arbitrary valuation law, where atoms make the tie rule at matter. The second is a newsvendor problem in for an arbitrary demand law: the paper writes the optimal stock as of a fractile, which presumes a continuous, strictly increasing , whereas here may jump or be flat and the optimal stock is any solution of the fractile equation. The obvious reduction, "the retailer's profit is , so its maximizer is the chain's", is not available: that identity holds only at the chain's price and refund, and away from them the retailer's profit is not proportional to . In Proposition 4 the manufacturer's deviation to a refund below acts on the consumers' purchase decision, and the paper's remark that no one then buys is false when almost surely, so that case needs its own argument.
Prices, refunds, costs, quantities and profits are real numbers. The valuation law is a probability measure on with integrable identity (a strict generalization of the paper's density ); and , matching the rule "keep iff ". The demand law is a probability measure on with , and is SupplyChainTheory.expSales from the published module SupplyChainTheory_contracts. Every profit includes the demand rule (6): without it, (15) and (31) are unbounded in . Optimization is over all real and and all , nonnegative stocks and demand being the paper's setting; with negative stocks the profits are unbounded. Optimality of the paper's closed-form triple is claimed, never uniqueness, and "induces the retailer to maximize supply chain profit" is stated as "the chain-optimal triple is a retailer optimum"; that the triple maximizes is Proposition 2, formalized in mission 1, and not restated. The optimal stock is any solution of the fractile equation, and no continuity of is assumed. The Nash equilibrium of Proposition 4 is written as the two best-response inequalities. Proposition 5 adds the hypothesis , implied by the paper's range (p. 19) and necessary: for the retailer's profit is unbounded. The kept-only rebate of Sec. 5.4 has no printed formula; its profit is (24) with the rebate removed from the returned-units term. Printed page numbers equal PDF page numbers throughout the source. A formalization in which the retailer's profit is defined as , or in which the optimization is restricted to , would make the goal trivial and is excluded: (31) is stated with free , , , and the contract enters only through hypotheses.
The model module (SuReturns.Coordination.Model) restates the single-seller objects of mission 1 in this sub-namespace. Contributions welcome: proofs of the two optimization steps as reusable lemmas (the refund step for a general valuation law and the newsvendor step for an arbitrary demand law), which serve every milestone here.
Financial institutions, insurers and engineers who manage the risk of a decision describe it by a statistic of the loss distribution that the decision induces. The value-at-risk (VaR) at confidence level , the -quantile of the loss, became an industry and regulatory standard in the 1990s, but it is not subadditive and behaves erratically as a function of the decision when the loss distribution has atoms, as it always does in scenario-based models. The conditional value-at-risk (CVaR), roughly the average of the losses beyond VaR, was proposed as a replacement that is coherent in the sense of Artzner, Delbaen, Eber and Heath and that can be optimized.
In an earlier paper (Rockafellar and Uryasev, 2000) the same authors showed, for loss distributions with continuous distribution functions, that CVaR is the minimum value of an explicit convex function of one real variable, and that VaR is a minimizer. That formula turned CVaR minimization over a portfolio into a linear program and is the reason CVaR is used in practice. The paper formalized here (Rockafellar and Uryasev, Research Report #2001-5, 2001, published in J. Banking & Finance 2002) defines CVaR for general loss distributions, discrete ones included, and proves that the minimization formula survives.
Timeline.
A decision lies in a set ; an uncertain outcome has a Borel probability law that does not depend on . The loss is , where is continuous in on , measurable in , and for each . A confidence level is fixed.
When jumps across at , the tail distribution keeps only the part of that atom needed to give the tail total mass one: the atom is split.
For each : is finite and convex (hence continuous), and
the minimum being attained and the argmin a nonempty closed bounded interval; in particular .
A companion item states Corollary 7: , strictly when .
Theorem 10 is what makes CVaR computable and optimizable. Since , minimizing CVaR over is the joint minimization of over ; with a finite scenario set and a loss linear in , that is a linear program, and VaR comes out as a by-product. The convexity and sublinearity of CVaR in (Corollary 11), its coherence (Corollary 12) and the equivalence of CVaR-constrained and CVaR-penalized problems (Theorem 14) are all derived from it. The formula is the basis of CVaR portfolio optimization software and of a large literature on risk-averse stochastic programming.
The result has been proved since 2001 and is not open. To our knowledge it has no machine-checked proof with CVaR defined independently: the CVaR items already on Prove2Me take as the definition of CVaR, which makes (28) true by definition. This mission produces a formal proof that the tail-mean definition, with its atom splitting, agrees with the minimization formula for every integrable loss, together with reusable facts about one-sided derivatives of and the argmin of the Rockafellar–Uryasev function.
The minimization side is elementary convex analysis in one variable once the one-sided derivatives are known; computing them requires passing a limit under the expectation, with the jumps of handled separately for right and left limits. The step that does not follow from that analysis is the identification of the minimum value with . When the loss has an atom at that straddles level , neither nor equals the minimum value; only the mean of the distribution with the split atom does. The obvious approach, proving the formula for continuous laws and passing to a limit, does not deliver the identity at the level of the defined objects; the identity has to be proved directly from the definition of the tail distribution, through Proposition 6.
Fin m → ℝ) with its Borel σ-algebra and a probability measure P. The paper's support set is not modelled: a law on is a law on concentrated on , and no statement uses .P.real). is , as the paper defines it in (2).MultistageStochastic.valueAtRisk P (f x) β (a real infimum, referenced, not redefined); is a real infimum. Both are meaningful because is a probability measure and , and those hypotheses are carried wherever they appear.Defining CVaR as , or as the quantile average, or by formula (21), would make the goal or a milestone true by definition; CVaR is defined here as the mean of the -tail distribution, and any such redefinition is ruled out.
A complete development needs: right-continuity and limits of distribution functions, dominated convergence for the difference quotients of , the uniqueness of a probability measure on with given distribution function, and one-variable convex analysis linking one-sided derivatives to minimizers. The derivative and argmin lemmas are reusable for any Rockafellar–Uryasev-type objective. Proofs of any milestone, and Lean lemmas that bridge valueAtRisk (stated with ENNReal) and P.real, are welcome.
A correlated equilibrium (Aumann, 1974) is a probability distribution over the strategy profiles of a game such that no player gains by deviating from the strategy it recommends. It is the natural solution concept for repeated play by adaptive agents, because the set of correlated equilibria is a polytope described by linear inequalities and, as Hart and Mas-Colell showed, it can be reached by simple learning rules that use only a player's own past payoffs and regrets.
Hart and Mas-Colell's paper (Econometrica 68 (2000) 1127–1150) has two procedures. Its Main Theorem concerns regret matching (2.2), in which a player switches away from its last strategy with probabilities proportional to its regrets; it is the subject of a companion mission. Section 3 studies a variant in which, at every period, the player plays an invariant vector of the regret matrix, and proves with Blackwell's approachability theorem (Blackwell, 1956) that the player's regrets vanish almost surely, whatever the other players do. This result, Theorem A, is the target of this mission. It is the conditional ("internal") counterpart of Hannan's no-regret property (Hannan, 1957) and the template for later internal-regret algorithms in online learning (Cesa-Bianchi and Lugosi, 2006).
Timeline. Hannan (1957) gave a procedure with vanishing unconditional regret; Blackwell (1956) proved the approachability theorem and derived a universally consistent procedure from it; Foster and Vohra (1997) obtained convergence to correlated equilibria through calibrated forecasts; Fudenberg and Levine (1995, 1999) introduced universal consistency and calibrated smooth fictitious play; Hart and Mas-Colell (2000) gave Theorem A and regret matching.
A finite game has a finite set of players, a finite nonempty strategy set for each player, and payoffs on . For and , is 's payoff when 's coordinate of is replaced by .
The game is played at . After the history each player chooses a mixed action, and given the players randomize independently. For in the regret of player for not having played whenever it played is
With , a probability vector satisfies (3.1) if
i.e. is an invariant distribution of the transition matrix of regret matching. The empirical distribution of play is .
If at every period player plays a probability vector satisfying (3.1), then, whatever the other players do,
The Corollary (p. 1134): if every player follows (3.1), converges almost surely to the set of correlated equilibria. The equivalence of (3.1) with invariance for the (2.2) matrix (p. 1133). Theorem B (p. 1139): the procedure proportional to unconditional regrets satisfies Hannan's universal consistency (4.1).
Theorem A shows that conditional regrets can be driven to zero by a stationary rule of fixed size , with no assumption on the other players beyond conditional independence. Combined with the Proposition of §3 it gives the Corollary: if all players follow such a rule, play converges to the set of correlated equilibria. The same argument with a different vector payoff yields Theorem B, a short proof of Hannan consistency. The approachability reduction used here is the standard route from vector-valued games to no-regret learning.
Theorem A and Blackwell's theorem are proved results. What this mission adds is a machine-checked development: a formal statement of Theorem A for arbitrary opponents, a formal statement of Blackwell's procedure in Hart and Mas-Colell's form (condition (3.2) via the support function, opponents that see the whole history), and the algebra connecting the two. Prove2Me already has Blackwell's original THEOREM 1 (strategies depending only on past payoff vectors, geometric separation condition); it is a different statement, and deriving this one from it, or proving it directly, is part of the work.
The algebra (milestones 1–5) is finite-dimensional and elementary, apart from the existence of an invariant vector, which needs a fixed-point or Perron–Frobenius type argument for a matrix that is not stochastic. The probabilistic core is milestone 6. The geometric picture of the paper (Figure 1) shows that the expected next average payoff moves closer to , but that controls only , not the realized averages (footnote 15 of the paper); the opponent adapts to the whole history, so the increments are neither independent nor identically distributed, and the almost-sure statement has to be obtained on a measure known only through its conditional laws given each history.
stdSimplex. is EuclideanSpace ℝ L with its inner product and Euclidean distance.play τ is ); every regret quantity is a function of a finite history Fin t → S, and every statement uses histories of length .IsLUB/¬ BddAbove.Useful infrastructure, reusable beyond this mission: the existence of invariant vectors of nonnegative matrices, projections onto orthants, and a general Blackwell approachability theorem for history-dependent opponents. Proofs of any milestone, of the companions, and alternative proofs of Theorem A are welcome.
Block coordinate descent (BCD), also called the nonlinear Gauss–Seidel method or alternating minimization, minimizes a function of several blocks of variables by exactly minimizing over one block at a time while the others are held fixed. It is used wherever the subproblem in a single block is cheap even though the joint problem is not: alternating least squares, EM-type updates, matrix and tensor factorization, Lasso-type regression with separable penalties, and decomposition methods for large structured programs.
Classical convergence theory for BCD asks for differentiability and strict convexity or uniqueness of block minimizers (Bertsekas and Tsitsiklis, 1989; Grippo and Sciandrone, 2000). Many applications have a nondifferentiable, extended-valued objective: a smooth or merely continuous coupling term plus separate penalties or constraint indicators on each block. Tseng (2001) gave convergence results for this setting. Its §5, formalized here, shows that the separable structure lets one drop continuity of on a level set and replace strict convexity by quasiconvexity and hemivariance in each block.
Timeline. Auslender (1976) proved convergence of cyclic BCD for strongly convex continuous on a product of closed convex sets with convex . Bertsekas and Tsitsiklis (1989, Prop. 3.9 in §3.3.5) treated continuously differentiable convex with block-wise unique minimizers. Grippo and Sciandrone (2000, Prop. 5.1) extended this to continuously differentiable, blockwise strictly pseudoconvex with each the indicator of a closed convex set. Tseng (2001, Prop. 5.1 and Thm. 5.1) covers lower semicontinuous, extended-valued under Assumptions B1–B3 and C1 or C2 below.
Fix and block dimensions . A point is with . The objective has form (1):
with and each taking values in . The effective domain of is .
A function is quasiconvex if for all and , and hemivariate if it is not constant on any nondegenerate line segment contained in .
The BCD method starts at . At iteration it chooses a block and sets and for . Under the essentially cyclic rule there is a constant such that every block is chosen at least once in any consecutive iterations.
A point is a coordinatewise minimum point of if for every block and every .
The assumptions of §5 are:
Under B1–B3, C1 or C2, and boundedness of for some ,
Without the level-set bound, for every essentially cyclic BCD sequence that is defined,
The milestone list follows the paper's proof: attainment of the block minimization on a bounded level set (p. 478); monotonicity of and membership of cluster points in (p. 485); claim (11), that consecutive iterates share limits along subsequences; its iterate (20) over a window of steps; inequality (21) at cluster points; Proposition 5.1 itself; and the remark (p. 483) that a quasiconvex hemivariate function has at most one minimum point.
The result. Theorem 5.1 guarantees that exact block minimization, applied in any order that visits every block within a bounded window, cannot accumulate at points where a single-block move still decreases . It applies to objectives that are neither differentiable nor continuous on their domain and that need not be convex, which covers problems with constraint indicators on each block and couplings with finite values on the boundary of their domain (Assumption C2). Convexity in each block alone is not enough for results of this kind: the paper notes (pp. 483–484) that Theorem 4.1(b) becomes false under that weaker hypothesis, because Powell's three-variable example is convex in each variable.
The formalization. The result is proved in the paper; no machine-checked proof of it, or of a BCD convergence theorem of this kind, has been published. A formal proof would supply a reusable account of extended-valued lower semicontinuous functions on product spaces, of subsequence arguments for descent methods, and of quasiconvexity and hemivariance, none of which is packaged for this purpose in Mathlib.
The obvious argument fixes a cluster point and a block and passes to the limit in the block-optimality of the iterates. That needs the iterates in which block was last updated to converge to the same , and nothing forces consecutive iterates to be close: BCD can oscillate between distinct limit points of different subsequences. Claim (11) supplies this, and it is where quasiconvexity and hemivariance are spent. The second obstacle is passing to the limit in , which is only continuous on its domain and only lower semicontinuous globally; Assumption C1 or C2 is what keeps the comparison points inside .
(k : Fin N) → EuclideanSpace ℝ (Fin (n k))), with 0-based blocks: paper block is Lean index . The product carries the sup norm of the blocks; boundedness, convergence, cluster points and semicontinuity are the same as for the Euclidean norm.EReal). Standing hypotheses: and every never take the value , so is never and is exactly when one summand is. The objective is always the sum , defined once, never a free function with an equation hypothesis.A statement that assumes claim (11), (20) or (21), or that the values converge, would trivialize the goal; the goal and Proposition 5.1 assume none of these.
A complete development needs: compactness of closed bounded sets in the product space and minimization of lower semicontinuous EReal functions on compact sets; subsequence extraction for cluster points; and the segment argument behind (11). Contributions of general lemmas on quasiconvex and hemivariate functions, and on lower semicontinuity of finite sums of EReal functions that avoid , are reusable beyond this mission and welcome.
AdaBoost (Freund and Schapire, 1996) combines many weak classifiers, such as small decision trees, into a single strong classifier by repeatedly reweighting the training data. In the late 1990s it was among the most accurate off-the-shelf classifiers, but why it worked was unclear. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) gave a statistical explanation: AdaBoost fits an additive model by stagewise minimization of the exponential criterion , and the population minimizer of that criterion is half the log-odds of the class probability. Boosting is therefore a form of additive logistic regression. This reading underlies gradient boosting, LogitBoost, and the later theory of classification-calibrated surrogate losses.
The exponential criterion was introduced by Schapire and Singer (1998) as an upper bound on misclassification error, and Breiman (1997) used it in his analysis of AdaBoost. Lemma 1 of the 2000 paper is the statement that identifies its population minimizer.
A feature ranges over a measurable space and a label takes the values and . The pair has a joint law , a probability measure on , with marginal on . Disintegrating gives the conditional class probabilities and .
For a function the exponential criterion (11) is the joint expectation
a number in . Its conditional version at is . Given a current estimate , the weighted conditional expectation with weight is
and . The half log-odds is
Assume for -almost every . Then is measurable, and for every measurable ,
and, for -almost every , (13) and (14) hold:
Lemma 1 is what makes the rest of the paper a statement about logistic regression. Because the minimizer of is the half log-odds, an additive model built by minimizing estimates , and the transform (13) converts it into a class probability. Result 2 shows that one population step of Real AdaBoost from any starting point already reaches , so the many iterations used in practice come from the crude approximation of conditional expectations by trees, not from the criterion. Corollary 3 gives the first-order condition used to interpret the AdaBoost weights. The other missions of this series (Discrete AdaBoost, LogitBoost, Gentle AdaBoost, multiclass LogitBoost) all rest on these population facts.
All of these results are proved in the paper; none is open. What this mission adds is a machine-checked version in the population setting, with conditional probabilities obtained from an honest disintegration of the joint law instead of being postulated. No formalization of the exponential criterion's population minimizer is known to exist on the platform or in Mathlib. The pointwise calculus is elementary; the work is in the measure-theoretic layer.
The paper's proof minimizes the conditional criterion pointwise and sets the derivative to zero. Turning this into a statement about requires three things the one-line proof does not mention. First, the joint expectation must be rewritten as an iterated integral, which needs the disintegration of and measurability of everything integrated. Second, the pointwise minimizer must itself be a measurable function of , which the calculus says nothing about. Third, the comparison is against every measurable competitor, including those with , so integrability cannot be assumed. Corollary 3 has a further difficulty: it assumes nothing about the class probabilities, so a proof must show that optimality of forces them strictly between and almost everywhere, a fact the paper's one-line proof does not address.
Labels live on Bool, with sgn true = 1 and sgn false = -1. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν] on an arbitrary measurable space X. is (ν.condKernel x {b}).toReal, read off Mathlib's conditional kernel. It is determined only -almost everywhere, so (13), (14), Corollary 3 and the identity of Result 2 are almost-everywhere statements; the conditional formula and its derivative hold at every . is a lower Lebesgue integral in . Competitors range over all measurable functions . Derivatives are stated with HasDerivAt.
The hypothesis almost everywhere is added to Lemma 1 and Result 2. Without it the ratio in (12) is or undefined, Real.log 0 = 0 would give a junk value, and no minimizer of exists. Corollary 1 assumes both labels occur in the region, which is the sample counterpart.
Several formalizations would make the targets trivial, and none is used here. Defining through its conditional formula would make milestone 1 a definition and the goal pointwise, so is the joint expectation under . A Bochner integral would return for a non-integrable and make every such a minimizer, so takes values in . A bare deriv is at points of non-differentiability. Writing the logistic transform as in place of would lose the factor that (15) records.
A complete development needs the disintegration of a measure on , iterated lower integrals, measurability of the conditional kernel, and elementary calculus of . Lemmas about conditional expectations against condKernel on a finite label set, and the measurability of , are reusable in the other missions of this series. Contributions of either kind are welcome.
Boosting combines many weak classifiers into a strong one. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) explained the two-class AdaBoost algorithms statistically: in the population, boosting fits an additive logistic regression model by stagewise optimization of a criterion on the log-odds scale. Section 5 of that paper carries the explanation to classes. It answers two questions a practitioner faces when boosting a multiclass problem:
The paper's answer to the second question is LogitBoost for classes (Algorithm 6). Result 6 asserts that it takes quasi-Newton steps on the multinomial log-likelihood. Algorithm 6 underlies later multiclass gradient boosting, where the per-class Newton step with a diagonal Hessian and the factor reappears (Friedman, Ann. Statist. 29 (2001)).
Fix classes, labelled , and a measurable space of features. A probability measure on is the joint law of the feature and the class . The classes are mutually exclusive.
Definition 1 (p. 354) introduces the symmetric multiple logistic transformation
and states that it is equivalent to
For this is the two-class .
AdaBoost.MH (Algorithm 5) treats each class against the rest. Its population criterion is .
LogitBoost ( classes) (Algorithm 6, population version) keeps a fit and the probabilities given by (40). For each class it forms the working response and weight
It takes the weighted conditional mean , and updates
The multilogit parametrization with base class writes , so that . The multinomial log-likelihood of one observation is
Result 6 states that the LogitBoost algorithm ( classes, population version) uses quasi-Newton steps for fitting an additive symmetric logistic model by maximum likelihood. The goal states, for every and every current fit , the three facts the Derivation makes precise:
each minimizing the class--against-the-rest exponential criterion.
The result places J-class LogitBoost inside likelihood theory. Its population step is a Newton-type step for multinomial maximum likelihood. Two approximations separate it from the full Newton step: the Hessian is replaced by its diagonal, and the base class is averaged out. Result 5 shows that AdaBoost.MH, in contrast, solves decoupled one-against-the-rest problems whose implied probabilities need not sum to one. That contrast is the paper's argument for the coupled procedure.
All statements here are proved in the paper by direct calculation. They have not been formalized before. The mission produces machine-checked versions of the population claims and of the algebra behind them. That algebra comprises the softmax/centred-logit equivalence, the multinomial score and Hessian in base-class coordinates, and the base-class averaging identity. These pieces are reusable for any multinomial logistic or softmax model.
There is no deep step. The work lies in keeping two parametrizations apart: the base-class multilogit coordinates , with free entries, and the symmetric centred coordinates , with entries summing to zero. The derivatives are taken in . The algorithm and (40) live in . The step is converted back by symmetrization. Mixing the two makes the averaging identity false or vacuous.
A second point is that the update is not the Newton step . The page states this explicitly: for full Newton stepping the symmetrization would be redundant. The tempting shortcut of proving that Algorithm 6 equals the full Newton step therefore does not prove Result 6.
Fin J, with where needed.Fin J.ν.condKernel x.Trivializing encodings are ruled out:
HasDerivAt along coordinate lines, and the Hessian is the derivative of an explicitly given partial derivative, never a deriv equation that would be a junk at non-differentiable points.All objects are defined in one definitions file in the namespace AddLogReg.Multiclass. Proofs of any of the milestones are welcome. Lemmas on the softmax map, such as positivity, the derivative of log-sum-exp in base coordinates and shift invariance, are reusable beyond this mission.
Block coordinate descent (BCD), also called the nonlinear Gauss–Seidel method or alternating minimization, minimizes a function of several blocks of variables by minimizing over one block at a time with the others held fixed. It is used wherever the full problem is hard but each block subproblem is easy: proximal point methods, the Arimoto–Blahut algorithm for channel capacity, alternating projections, matrix factorization, and sparse regression with separable penalties. The basic question is what the limit points of the method are. Without assumptions they need not even be stationary: Powell (1973) gave a smooth three-variable function on which cyclic coordinate descent cycles among nonstationary points.
P. Tseng's 2001 paper (JOTA 109, 475–494) gave conditions under which the cluster points are stationary for nondifferentiable objectives of the form , with smooth on its domain and each an arbitrary extended-real function of one block. The paper is a standard reference for BCD on composite problems.
Timeline. Auslender (1976) treated the convex nondifferentiable case; Grippo and Sciandrone (Oper. Res. Lett. 26, 2000) the continuously differentiable case with closed convex block constraints, under pseudoconvexity assumptions; Zadeh (1970) the unconstrained differentiable case; Powell (1973) the counterexamples. Tseng (2001) unifies these in Theorem 4.1, which this mission targets, and adds a quasiconvex–hemivariate result (§5, the sibling mission).
Let and . A point is with coordinate blocks , and is the vector whose th block is and whose other blocks are zero. The objective has effective domain and, at , lower directional derivative
The BCD method starts at ; iteration chooses a block and sets
Under the essentially cyclic rule there is such that every block is chosen at least once in any consecutive iterations; the cyclic rule chooses block at iterations . The level set is .
A point is stationary if for all , and a coordinatewise minimum point if for all and all . The function is regular at if for every with for all . It is pseudoconvex in if whenever , is supported on blocks and , and ; it has at most one minimum in if every block- section has at most one minimum point.
Assume is compact and is continuous on . Then the BCD iterates are defined, and essentially cyclic runs are bounded. Moreover:
In (c), a cluster point at which is regular is moreover stationary.
The proof's steps, in attack order: the descent and attainment step; the limit relations (6)–(8) for the window limits of a convergent subsequence; claim (9) for (a), (b); the window collapse for (c); the §3 remark that a regular coordinatewise minimum is stationary; and parts (a), (b), (c) separately. Lemma 3.1 (regularity of under the smoothness assumptions A1 or A2 on ) is a companion target.
Theorem 4.1 is the convergence result that the paper's applications rest on: the proximal minimization algorithm, the Arimoto–Blahut algorithm and an algorithm of Han are all instances of BCD on functions of the form , and Lemma 3.1 supplies the regularity that turns coordinatewise minima into stationary points. Part (b) is sharp: Powell's example shows it fails if pseudoconvexity is weakened to convexity in each block.
None of these results has a machine-checked proof on the platform. A formalization would provide a reusable framework for block methods on extended-real objectives: one-sided directional derivatives in , block pseudoconvexity, and the subsequence-of-windows argument that recurs in the analysis of Gauss–Seidel and alternating methods.
The obvious argument says that a cluster point is the limit of iterates that each minimize in one block, so it minimizes in every block. This fails: the iterate that minimizes in block is not the iterate converging to but one of neighbours in a window, and these neighbours may converge to different points . Each is minimal only in its own block . Combining these windowed facts into a statement about one point is the content of the theorem. Under (a), (b) this uses regularity and pseudoconvexity in pairs, propagated along the window by induction (claim (9)). Under (c) it uses uniqueness of block minima to show that the window collapses. Powell's example shows that some such hypothesis is necessary. A second difficulty is extended-real bookkeeping: takes the value , directional derivatives may be , and limits must be taken in .
The Lean development lives in namespace TsengBCD.Stationary. The conventions are:
EReal. The standing hypothesis is that never takes the value , together with .dirDeriv is the EReal liminf over .Fin N indices and each block is EuclideanSpace ℝ (Fin (n k)). The product carries the sup norm, which does not affect any statement.s r is the block of iteration . The cyclic rule is s r = r mod N, and is .Continuity on . The hypothesis " is continuous on " is formalized as continuity of , as a map into , at every point of . The weaker reading, continuity of the restriction , makes the printed theorem false. Take , , and
with . Then is a compact ellipse together with the isolated point , and the restriction of to is continuous. The cyclic iterates have both coordinates positive and never meet the lines or . They converge to , yet . Part (c), which for has no uniqueness hypothesis, would assert that is a coordinatewise minimum. The limit step (7) of the proof needs continuity at points approached from outside . This repair excludes the paper's later application to the Arimoto–Blahut algorithm (Example 6.2), which is not part of this mission.
Trivializations ruled out. The goal does not assume the window limits, the relations (6)–(9) or the block pattern ; these appear only in milestones. The existence of runs is part of the goal, so the cluster-point claims are not vacuous.
Infrastructure needed. A complete development needs:
EReal liminf calculus (liminf of sums; nonnegativity of difference quotients);The EReal directional-derivative lemmas and the window extraction are reusable for the sibling mission (Theorem 5.1) and for other block methods. Proofs of any milestone are welcome, as are counterexamples showing that a hypothesis cannot be dropped.
Interior-point methods for linear programming are usually analysed under two assumptions: a strictly feasible starting point is known, and the problem has an optimal solution. In practice neither is known in advance. The homogeneous self-dual embedding of Ye, Todd and Mizuno (Math. Oper. Res. 19(1), 1994) removes both assumptions. It embeds a standard-form linear program and its dual into one artificial program that always has an obvious interior starting point. A solution of the artificial program either yields optimal solutions of the original pair or certifies that one of them is infeasible. The embedding underlies the infeasibility detection of several interior-point LP and conic solvers.
The paper's main result is an iteration bound. Section 4, "Analysis of the output", asks a different, practical question: what can be read off the iterates if the algorithm is stopped early, at an approximate solution? Theorem 8 answers it. This mission formalizes Theorem 8 and the results its proof uses.
Let , , . The primal and dual programs are
with dual slack . An optimal solution pair is an optimal of (LP) together with an optimal of (LD).
Write for the all-ones vector and set , , . The homogeneous self-dual program (HLP), in the paper's normalization , , has variables with , , :
is its feasible set and the subset with . A self-complementary solution is an optimal solution of (HLP). A strictly self-complementary one also has and . For a point of (HLP) put , and for let
The predictor–corrector algorithm with starts at . At even (predictor step) it solves the Newton system (11)–(12) with target and moves along the direction by the largest step that stays in (13). At odd (corrector step) it solves the system with target and takes a full step.
For every predictor–corrector sequence :
for all .
In the order the proof uses them:
Theorem 8 is a stopping criterion. Either stays bounded away from zero, which happens exactly when (LP) has an optimal solution, or and go to zero at the same rate while stays bounded away from zero. An implementation can therefore watch and and decide the status of (LP) from an approximate iterate, without the exact rounding procedure needed for the bound. The bounds hold for real data, with no integrality and no bit length.
Theorem 8 has a published proof on one page, building on the self-duality facts of §2 and the Mizuno–Todd–Ye step analysis. None of it is machine-checked. A complete development would give a verified account of the homogeneous self-dual embedding, including:
These are the ingredients of every analysis of the embedding. Homogeneous self-dual programs appear on Prove2Me in other conventions (Vanderbei's (22.4) and (22.21), Matoušek's (SD)), but their statements concern different programs: no artificial variable , no normalizing row. They do not formalize any statement here.
The two branches of Theorem 8 rest on facts of different depth.
The obvious first idea is to treat Theorem 8 as a consequence of Theorem 6. It fails: Theorem 8 is about every iterate of an infinite run and uses no iteration count. The constant depends on the instance and is not explicit.
A : Matrix (Fin m) (Fin n) ℝ, b : Fin m → ℝ, c : Fin n → ℝ, with no rank assumption and no integrality. (LP)/(LD) feasibility and optimality are built on the published general-form LP definition LinearOptimization_DualLP. "(LP) has a solution (feasible and bounded)" in Theorem 3 is read as "(LP) has an optimal solution".y x τ θ s κ. The slacks are pinned to the constraint expressions. (HLP) is defined for general ; the instance (7) is obtained by substitution. Optimality means minimizing the objective over , not "", so Theorem 2 (iv) is not built into the definition.IsPCSequence: , and each step is for some solution of (11)–(12). The relation is needed because is not unique when is rank-deficient.Needed infrastructure: LP duality and Goldman–Tucker strict complementarity for real standard-form programs, and the skew-symmetric orthogonality lemma. These are reusable well beyond this mission. Proofs of any milestone, and alternative arguments (e.g. via the central-path limit) for the existence of , are welcome.
Many linear programs that arise in combinatorial optimization have a few "complicating" constraints on top of a set over which linear optimization is easy: multicommodity flow, where is a product of single-commodity flow polytopes; scheduling and the Held–Karp bound, where is a polytope of assignments or trees. Plotkin, Shmoys and Tardos showed that for such problems an approximate solution can be found with a number of calls to the linear optimizer over that depends on the required accuracy and on a structural quantity, the width, but only logarithmically on the number of constraints. Their packing and covering algorithms (§§2–3 of the paper) assume nonnegative data. Section 4 removes that assumption and treats an arbitrary system of linear inequalities over a convex set. This framework, later known as the multiplicative-weights method for linear programs, is among the standard tools of approximation algorithms (Arora, Hazan and Kale's 2012 survey gives the modern account).
Timeline. Shahrokhi and Matula (1990) gave an exponential-potential algorithm for the maximum concurrent flow problem. Plotkin, Shmoys and Tardos (FOCS 1991; Cornell ORIE Technical Report 999, 1992; Mathematics of Operations Research 1995) generalized it to fractional packing, covering and the general problem of this mission. Grigoriadis and Khachiyan (1994–1996) obtained related bounds for block-angular and convex resource-sharing problems. Garg and Könemann (1998) and Arora, Hazan and Kale (2012) gave width-free or simplified variants.
An instance of the GENERAL problem consists of an arbitrary real matrix with rows , an arbitrary vector , a convex set , and a positive vector that sets the scale of the allowed error. The question is whether some satisfies . Such a point is an exact solution; a point with is an -approximate solution.
For write
the least with ; it may be negative. The width is . Access to is through subroutine (10): given in , return minimizing over . For a dual vector let . The relaxed optimality conditions for a point with and a dual vector are
The dual solution corresponding to with parameter is , and its potential is . Procedure IMPROVE-GENERAL (Figure 4) starts from with , fixes and a step size , and, while and fails, replaces by , where is the oracle's answer for the current dual solution. The driver calls IMPROVE-GENERAL repeatedly, stopping with an -approximate solution or with a report that none exists.
For every , every start and every exact minimizing oracle, the driver stops; an output point is an -approximate solution; an infeasibility report is correct ( with ); and the number of oracle calls is at most
The result gives an -relaxed decision procedure for any system of linear inequalities over a convex set with a linear-optimization oracle, with no sign conditions on the data. Its oracle-call count is independent of and logarithmic in , which is what makes it useful when is large and has a fast combinatorial optimizer. The simultaneous packing-and-covering problem is the special case where every row is either nonnegative or nonpositive; the paper's width-reduction techniques (§5) and applications (§6) build on this procedure and on its packing and covering counterparts.
The paper's statements use and ; this mission states the explicit constants that the paper's own proofs give. The result is proved in the literature; no machine-checked proof of it is known on Prove2Me or in Mathlib. It also records a gap in Figure 4 (below) and states the theorem for the smallest correction that makes the paper's proof go through. Formalizing the analysis yields reusable potential-function arguments (second-order bounds on , geometric decrease of a potential between two levels) of the kind used throughout multiplicative-weights analyses.
The correctness half is short; the complexity half carries the weight. Lemma 4.3 needs a second-order bound on the exponential that is valid only when the step changes each exponent by at most , so the step size must be tied to and . Theorem 4.4 then has to control the potential between a ceiling and a floor while moves, and Theorem 4.5 has to sum the per-call bounds over a sequence of calls whose halves each time, so that the last call dominates.
The first reading of Figure 4 fails here: Figure 4 fixes and from , but the loop runs for every . For the hypothesis of Lemma 4.3 fails, and the decrease bound from its proof becomes negative for . At , the hypothesis of Lemma 4.2 requires , which the printed does not meet, so and the infeasibility certificate are not guaranteed. With the printed parameters, the iteration bound is not established by the paper's argument.
Fin m with ([NeZero m]), coordinates by Fin n; is a real matrix and , real vectors with ; is a convex set. No sign hypothesis is put on , or .Fin m, second-order bounds on Real.exp and monotonicity of Real.log, convex combinations, induction over fuelled recursions. The potential-decrease lemmas are reusable for the packing and covering missions of the same paper. Proofs of any milestone are welcome independently.A retailer deciding how many variants of a product to carry (colours, sizes, flavours) faces a trade-off. A broader assortment captures customers whose favourite variant would otherwise be missing, but it splits demand into more, smaller streams, each of which needs its own safety stock. van Ryzin and Mahajan (Management Science 45(11), 1999) combine a multinomial logit model of customer choice with a newsvendor model of inventory and show that the optimal assortment always consists of the most popular variants for some (their Theorem 1). That reduces "how much variety" to a single index, and the paper's Theorem 2 then answers which economic parameters push that index up or down: the selling price, the strength of the customers' outside option, and the store's traffic volume. These comparative statics are the paper's main managerial predictions (high-margin categories and high-traffic "super stores" carry more variety; categories with a weak outside option carry less), and they are what later work on assortment planning cites the model for.
There are variants . Variant has a preference and the option of buying nothing has preference . The variants are numbered so that , and denotes the set of the most popular variants (, ).
When the store offers an assortment , each customer buys variant with the multinomial logit share
Each variant sells at price and costs per unit, with . Let be the standard normal distribution function and define the critical fractile ; it moves with .
Two models of aggregate demand are compared. In the independent population model, customers arrive on average, demand for variant is normal with mean and standard deviation , where and , and each variant is stocked at its newsvendor optimum. The resulting optimal expected profit is
In the trend-following population model all customers make the same choice, so variant sells units with probability and nothing otherwise, and the optimal expected profit is
Inside the proofs, and denote the shares on and on .
For all :
The goal is a single Lean theorem whose conjuncts are (a), (b) and (c), each for every admissible value of the parameters held fixed. In the trend-following half of (b) it carries the extra hypothesis ; see Formalization scope.
together with the strict version. 3. Equation (14): if and only if , with the strict version. 4. and the left side of (13) are increasing in on . 5. As , , so . 6. As , the numerator of the right side of (13) converges to a positive constant. 7. The left side of (13) is increasing (and unbounded) in .
The result. Theorem 2 gives three qualitative predictions with opposite signs, all from one model: higher margins favour broader assortments, a vanishing outside option favours narrower ones (customers then buy something regardless, so extra variants mainly cannibalise each other and add safety stock), and in the independent model higher volume favours broader assortments through risk pooling, a scale economy that the trend-following model does not have because its profit is proportional to . Combined with Theorem 1 these statements locate the optimal number of variants, not only its direction of change.
Formalizing it. The theorem is proved in the paper, but the published argument is a sketch: the positivity of the limiting numerator in (b) is asserted ("one can easily show"), and the trend-following half of (b) is dispatched in one sentence that does not cover every case (see below). A machine-checked development fixes exactly which hypotheses each part needs. No part of this paper has been formalized before, and Mathlib has no normal quantile function; the development of and of the monotonicity of in is reusable for any newsvendor analysis.
The comparisons are between finite sums of real powers of shares whose denominators all move with the parameter. Three steps are not routine. For (a), the left side of (13) is a product of and , and is not monotone in (it decreases while , i.e. while ); so monotonicity of the product depends on the shape of the normal distribution, and part (a) also needs this left side to grow without bound, which the paper does not state. For (b), the positivity of the limiting numerator is where the ordering and enter; it fails for unordered preferences. For the trend-following half of (b), the positive parts make the comparison piecewise, and the strict inequality can fail outright.
All objects live in RetailVariety.Statics. Variants are Fin n, 0-based (the paper's variant is ⟨j-1, _⟩), and is A n i, the indices with value below , so . The preferences are v : Fin n → ℝ with 0 < v j and Antitone v; is a separate real v0, not a variant. The shares are share v v0 S j. is ProbabilityTheory.cdf (gaussianReal 0 1), and is criticalFractile p c, the infimum of ; it is a function of , never a free parameter. Powers are real powers (Real.rpow); shares of offered variants are positive, so the convention does not enter. is max x 0. Price, cost, volume, , and are explicit arguments of profitI and profitT.
"Sufficiently high/low" is encoded as an eventual statement: ∀ᶠ p in atTop, ∀ᶠ v0 in 𝓝[>] 0 (a right limit, since ), ∀ᶠ lam in atTop. Fixed parameters stay in the paper's ranges: , , throughout, and in (a), in (b) and (c).
One deviation from the printed statement. In the trend-following model, part (b) as printed is false: with , , and , every share is below , so for every . The goal therefore assumes for that conjunct only (the most popular variant earns a positive margin on when ); the condition is also necessary for the strict inequality.
Formalizations that would trivialize the mission are ruled out: an existential ("for some ") in place of the eventual quantifiers; non-strict inequalities in the goal; a critical fractile independent of ; dropping the trend-following half of (a); and equal preferences or a fixed number of variants.
Needed infrastructure: the normal quantile and its basic properties, monotonicity facts about the normal distribution function and density, limits of the shares as , and elementary inequalities for with . Proofs of any milestone, and of the quantile facts as standalone lemmas, are welcome.
Prediction with expert advice asks a learner to predict a binary label on each of a sequence of trials, after seeing the predictions of a pool of candidate functions, and to make few more mistakes than the best member of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) gave the deterministic algorithm WM and its randomized variant WMR, and proved worst-case bounds that hold for every sequence of trials, with no probabilistic assumption on the data. Their §8 asks how good such bounds can possibly be when the data contain anomalies: disagreements with a candidate function, counted relative to the best-fitting member of the pool. Such disagreements can arise from noise in the instances or labels, or from instances that do not determine the label.
For the randomized algorithm WMR the expected number of mistakes grows, by Corollary 6.1 of the paper, at rate per anomaly, which tends to as . Theorem 8.2 shows that no randomized learner, however it is built, can do better than rate : an adversary who fixes the sequence in advance can force half the noise-free optimum plus one expected mistake per anomaly. Together with the deterministic counterpart, Theorem 8.1 (rate ), it locates the cost of label noise in online learning exactly. Mistake-bound lower bounds of this kind are a standard reference point for the analysis of online classification and of the expert-advice algorithms descended from WM (Cesa-Bianchi and Lugosi, Prediction, Learning, and Games, 2006).
Timeline: Littlestone (1988) characterized the optimal noise-free mistake bound by complete mistake trees (the Littlestone dimension); Littlestone and Warmuth (FOCS 1989; journal version 1994) introduced WM and WMR and proved Theorems 8.1 and 8.2.
Let be an arbitrary domain and a pool of functions , finite or infinite. A trial is a pair with and ; a sequence of trials is a finite list , in which an instance may repeat with different labels. The number of anomalies of with respect to is , and is the collection of sequences for which some has at most anomalies.
A deterministic algorithm maps the past trials and the current instance to a predicted label; counts its wrong predictions, and
A randomized algorithm uses random choices independent of the sequence. On a fixed sequence its behaviour at trial is summarized by , the probability that it predicts given the preceding instances and labels and the current instance; its expected number of mistakes is , and
the infimum ranging over all maps from (past trials, current instance) to .
For every pool with and every integer ,
Both sides live in ; when the statement says .
"For any pool of functions there exists a complete -mistake tree" ([Lit88]). On the platform this is the proved Lemma 21.7 of Shalev-Shwartz and Ben-David, , together with Lemma 21.6, for every ; a tree shattered by is a complete mistake tree.
The theorem shows that the expected-mistake bound of WMR is optimal in its dependence on the number of anomalies: its coefficient of approaches , and no randomized learner achieves a smaller one on every pool with two or more functions. It also quantifies the advantage of randomization: the deterministic rate is (Theorem 8.1), the randomized rate is , and the noise-free term halves. The lower bound is obliviously adversarial, since the sequence is chosen before any coin is tossed, so it applies equally to the stronger model in which the adversary adapts to the learner's predictions.
The result has been proved since 1994. To our knowledge it has no machine-checked proof; the platform holds the Littlestone-dimension characterization of the noise-free optimum (Shalev-Shwartz and Ben-David, Chapter 21) but no statement about anomalies or randomized lower bounds. This mission formalizes the definitions of anomalies, and , and the theorem.
An adversary against a randomized learner cannot react to its predictions: the whole sequence, instances and labels, must be fixed in advance, so the adaptive adversary that proves the deterministic bound is not directly available. The lower bound must instead come from the learner's prediction probabilities, which depend only on the sequence prefix; the content of the theorem is that this information is enough to construct, for every learner, one fixed sequence that stays inside while forcing the stated expected count. Taking the infimum over learners inside an extended-real supremum over sequences of every length adds bookkeeping when is infinite.
Sequences are Fin T → X × Bool for every T : ℕ. Deterministic algorithms, the mistake count, shattered trees and the Littlestone dimension are reused from the published definition UnderstandingML_Online (OnlineAlg, mistakes, ShattersTree, ldim, soa); randomized algorithms are its OnlineAlgR X := List (X × Bool) → X → ℝ restricted by IsRandAlg to values in , and the expected mistake count is its cumLoss. is a natural number. takes values in ℕ∞ and in ℝ≥0∞; the paper's "minimum" is read as an infimum. is F.Nontrivial, which admits infinite pools.
The reduction of randomized algorithms to probability maps is the main modelling choice: on a fixed sequence the expected number of mistakes of any algorithm whose randomization is independent of the sequence equals , and every map with values in is realized by such an algorithm, so the two infima coincide. Dropping the constraint , or quantifying only over deterministic algorithms, gives a different quantity and is ruled out.
Needed: the definitions above, and the existence of a complete -mistake tree, available through the proved platform theorems on ldim and soa. Lemmas relating mistakes along a path of a shattered tree to ldim, and a reusable statement that an oblivious adversary can force expected loss per trial, would serve other lower bounds in the Littlestone–Warmuth series and in online learning generally. Contributions of such lemmas are welcome.