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?
Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.
Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.
Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.
All matrices are with complex entries, . A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. , is its largest eigenvalue and its spectral norm. Functions of s.a. matrices are defined spectrally: if then , and is defined the same way on positive-definite matrices. is the semidefinite order: is positive semidefinite.
Let be a probability space with a filtration , and write . The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence of random matrices is adapted when each is -measurable. A matrix martingale is an adapted sequence of s.a. matrices with and ; its difference sequence satisfies .
The hypotheses of the main theorem are: is an adapted sequence of random s.a. matrices, and is a fixed (non-random) sequence of s.a. matrices, with
The variance parameter is .
For all ,
In the order they are used:
Corollary 7.2 is the martingale form, . Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, for a matrix-valued function of independent variables whose changes in one coordinate have squares bounded by .
The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor , and a variance parameter equal to the norm of the sum rather than the sum of the norms . In the commuting case the two coincide; in general the first can be smaller by a factor of up to . The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).
Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.
The scalar proof of Azuma's inequality multiplies conditional moment generating functions, , and bounds each factor. For matrices this fails: unless and commute, and is false, so the Golden–Thompson inequality cannot be iterated over terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis bounds squares, not the matrices themselves; it does not give , so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.
Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. is the supremum of the real spectrum, which is why is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by , so is never truncated. The bound is required almost surely. The bounds are deterministic matrices. The infimum over in Proposition 3.1 is posed as the bound for each at which the expectation is finite.
The hypotheses must not be made vacuous. Integrability of each is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is and the centring hypothesis would say nothing. The are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.
Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given is replaced by the expectation over at each fixed value with ; by independence these agree. Corollary 7.2 adds the hypothesis that is almost surely constant, without which .
A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.
A retailer who orders a seasonal product before demand is known faces the newsvendor trade-off. Ordering too much leaves unsold stock, and ordering too little forgoes sales. A risk-neutral newsvendor orders a critical fractile of demand. A risk-averse one orders less, since inventory is a risky investment, and this reduction has been shown under constant and decreasing absolute risk aversion (Eeckhoudt, Gollier and Schlesinger, Management Science 41(5), 1995, doi:10.1287/mnsc.41.5.786). Agrawal and Seshadri (2000) and Chen and Federgruen (2000) reached related conclusions.
Demand for many products moves with traded financial quantities: a stock index, a commodity price, an exchange rate. V. Gaur and S. Seshadri (Manufacturing & Service Operations Management 7(2), 2005, pp. 103–120, doi:10.1287/msom.1040.0061) ask what happens when the newsvendor can trade a financial instrument correlated with demand. Their Proposition 7 answers one half of the question: hedging moves the risk-averse newsvendor's order up, towards the risk-neutral quantity. This mission formalizes Proposition 7 and the steps of its appendix proof. The source is the published article, a library scan.
Let be the price at time of a traded asset, with law on . Demand is with . Here is the scaled forecast error, independent of , with law , and . The unit selling price, cost and salvage value are . In the paper's scaled units ((11), p. 110) these collapse into one cost parameter with and , and an initial-wealth term .
A hedge is a portfolio with time- payoff for a nondecreasing function , and time-0 price . It is a fair gamble, (display (12)). A firm that stocks units and shorts units of the hedge ends with the scaled wealth (14)
A decision maker with utility ranks by , and maximizes it over .
The absolute risk aversion is and the absolute prudence is . The utility displays DARA or CARA when is decreasing or constant, and DAP when prudence is decreasing or constant.
The hedge ratio is bounded by , chosen so that is nondecreasing in for . Beyond the firm over-hedges: its expected profit falls as the asset price rises.
For an increasing, concave, differentiable utility with constant or decreasing absolute risk aversion and constant or decreasing absolute prudence,
stated as: is nondecreasing on .
Proposition 7 reverses the conclusion of Eeckhoudt et al. Those authors find that an additional uncorrelated background risk lowers the risk-averse newsvendor's order. Here a correlated financial position that offsets the inventory risk raises it. Hedging therefore increases expected profit as well as reducing variance, and brings a risk-averse firm's operational decision closer to the risk-neutral one. The result is one of the basic statements linking operational and financial risk management in supply-chain finance.
The formalization adds three things.
The obvious argument signs the cross-partial derivative directly: , with of mean zero. That needs the sign of a covariance between and , a weight that depends on both and and is not monotone in either.
The paper first conditions on and splits the weight into two terms. The first is a conditional mean of . The second is concentrated on the sell-out event. Each term then needs its own monotonicity in .
Neither ingredient can be dropped. Without the conditional mean payoff decreases in and the first term changes sign.
Two further obstacles are technical:
Representation.
MDPFinance.FinancialMarkets.arrowPrattCoefficient, referenced rather than redefined.Conventions.
Integrability. The goal and the increasing-differences milestone assume integrability of , , and of their products with on the whole region, which is the regularity the proof uses. Without it a Bochner integral would silently be : the objective would be constant in and every a maximizer. A hypothesis set that forces would also trivialize the goal. A sorry-free check file exhibits the utility class, the standing assumptions and the -condition with for , with equal probability and .
Infrastructure and contributions. A one-variable Chebyshev association inequality for monotone functions is needed. So are differentiation under the integral, or an integrated mean-value argument, for piecewise-linear payoffs, and the step from increasing differences plus a unique maximizer to a monotone argmax. All three are reusable. Proofs of the milestones in any order are welcome, as are alternative arguments that avoid the cross-partial derivative altogether.
Interior-point methods solve linear, second-order cone and semidefinite programs in polynomial time, and they are the engine of most conic optimization software. The general theory of Nesterov and Nemirovskii (1994) covers any convex cone with a self-concordant barrier, but its methods are essentially primal and short-step: their analysis controls the barrier only inside a unit Dikin ellipsoid around the current point. Practical codes for linear programming, in contrast, use symmetric primal-dual methods that take long steps, a large fraction of the way to the boundary.
Nesterov and Todd (1997) isolated the class of cones and barriers for which the primal-dual long-step theory of linear programming carries over: self-scaled cones with self-scaled barriers. The class contains the nonnegative orthant, the second-order cone and the cone of positive semidefinite matrices, and their products. This mission formalizes the paper's §8 result: a primal-dual potential-reduction method with joint scaling decreases a symmetric potential function by an absolute constant at every iteration, which yields an iteration bound.
Timeline. Todd and Ye (1990) introduced the symmetric primal-dual potential function for linear programming with a short-step method. Kojima, Mizuno and Yoshise (1991) gave a symmetric long-step primal-dual potential-reduction method for linear complementarity problems; their Lemma 2.5 is the linear-programming case of the key inequality posed here. Nesterov and Nemirovskii (1994, §4.5) extended Ye's non-symmetric method to general cones. Nesterov and Todd (1997) extended the method of Kojima et al. to self-scaled cones; the companion paper (1998) treats short-step and functional-proximity variants.
Let be a finite-dimensional real vector space with dual and pairing . Let be a proper cone: closed, convex, with nonempty interior, and pointed (it contains no line). Its dual cone is .
A -self-concordant logarithmically homogeneous barrier for is a convex function on that tends to at the boundary, satisfies the self-concordance inequality , the bound , and for . Its conjugate barrier is
is -self-scaled (Definition 2.1) if for all , and . For , the scaling point is the with .
The distance to the boundary is measured by
so for ; local norms are .
The problem is the primal-dual pair , with surjective. For the primal-dual potential is
One iteration from a strictly feasible : take the scaling point and ; solve
put , , and accept any with .
with and , and the same bound for every accepted step , whose iterate is again strictly feasible. The constant is the paper's.
In attack order: the structure of Hessians (Theorem 3.1), existence and uniqueness of scaling points (Theorem 3.2), convexity of (Lemma 3.1) and the third-derivative bounds (Corollary 3.2 (i)–(ii)); the long-step Hessian comparison (Theorem 4.1), its corollaries (Corollary 4.1 (i)–(ii)), the barrier estimate (4.8) (Theorem 4.2) and the scalar monotonicity facts (Proposition 4.1); separability along orthogonal boundary directions (Lemma 5.1, Theorem 5.1) and the key inequality
and unique solvability of the projection system (Proposition 6.1).
A constant decrease of per iteration gives, through the bound of Nesterov–Nemirovskii (Theorem 8.1 of the paper), primal and dual solutions within of optimal in iterations when , with step sizes that are long (a fixed fraction of the distance to the boundary) rather than confined to a Dikin ellipsoid. Theorems 4.1–4.2 and 5.2 are reused by the potential-reduction and path-following analyses of the same paper and by later work on symmetric cones.
The results are proved in the paper. They are not formalized anywhere known to us: Mathlib has no self-concordant barriers, and the platform has the definitions of self-scaled barriers (from the companion 1998 paper) but none of these theorems. The mission produces machine-checked versions of the paper's structure theory of self-scaled barriers (§§3–5) and of the per-iteration decrease of its primal-dual method.
The obvious attempt bounds the change of and along the step by self-concordance alone. Self-concordance controls only for , so it cannot certify a step of length , which may be far outside the Dikin ellipsoid. The long-step analysis needs Theorem 4.1, which compares Hessians all the way to the boundary and holds for self-scaled barriers but fails for general self-concordant ones. The constant decrease then needs a lower bound on , where is the scaled norm of the right-hand side of (8.1); that bound is Theorem 5.2, whose proof rests on the separability of along orthogonal boundary directions (Theorem 5.1), a structural property with no analogue for general barriers.
EuclideanSpace), identified through the inner product; is ContinuousLinearMap.adjoint A. is hess F (derivative of gradient F), is fderiv ℝ (hess F) x u, is ContinuousLinearMap.inverse.IsProperCone, IsSelfScaledBarrier, conj, IsScalingPoint, IsPrimalStrict, IsDualStrict, sigma, lnorm (SelfScaledIPM.ShortStep), and ConvexOptimization.dualCone. The barrier definition includes nondegeneracy of on , which follows from the other axioms for a pointed cone. conj K F is a supremum over and is only evaluated at points of . is an infimum, equal to the page's minimum at interior centres.IsProperCone K, IsSelfScaledBarrier K F ν and ; the paper derives from pointedness.SelfScaledLongStep.PrimalDual.Defs): the projection system (6.4), the potential , the system (8.1), and . The projection system is shared, under the same name, with the other missions of this series.Thompson Sampling is the oldest bandit algorithm: Thompson proposed it in 1933 for allocating patients between two treatments (Thompson 1933). It keeps a posterior distribution over the unknown mean reward of every action, draws one sample from each posterior, and plays the action whose sample is largest. It is simple, widely used, and in experiments competitive with index policies designed for optimality. For decades it had no matching theoretical guarantee.
The benchmark for a stochastic bandit algorithm is the lower bound of Lai and Robbins (1985): every consistent policy draws a suboptimal arm at least times in rounds, where is the Kullback–Leibler divergence. A policy that attains this rate is called asymptotically optimal.
Timeline.
There are arms. Arm yields reward with probability and otherwise. Arm is the unique optimal arm: for every . The gap of arm is , and denotes the largest mean among the suboptimal arms.
Thompson Sampling with uniform priors. Let be the number of times arm has been drawn before round and the number of rewards equal to among those draws. With a uniform prior, the posterior of is . In round the algorithm draws, independently, a sample from each posterior, plays , and observes the reward of .
The regret after rounds is
where now counts the draws of in rounds . The Bernoulli divergence is .
The analysis compares the Thompson samples with two index rules. For an arm with successes in draws, at round of a horizon , the KL-UCB index is , and the Bayes-UCB index is the quantile of order of the posterior .
For every there is a constant , depending on and the instance, such that for every horizon ,
Only the existence of is asserted; its value is not fixed, so improvements of the lower-order terms do not invalidate the goal.
The result. Theorem 1 shows that the leading constant of Thompson Sampling's regret equals the Lai–Robbins constant, so no consistent policy does asymptotically better on Bernoulli bandits. It settled a question open since 1933 and is the starting point for later optimality proofs of Thompson Sampling for exponential families and Gaussian rewards. Proposition 1, a summable tail bound on the event that the optimal arm is under-sampled, is the reusable core: it is a deviation inequality for the number of draws of the optimal arm, which a bound on its expectation does not imply.
The formalization. The result is proved on paper; no machine-checked proof of an optimal-constant bound for Bernoulli Thompson Sampling exists. The platform already has the Gaussian frequentist analysis of Lattimore and Szepesvári (Theorem 36.3) and the non-optimal Agrawal–Goyal bound. This mission adds the Bernoulli, Beta-posterior case with the KL constant, the KL-UCB and Bayes-UCB indices with the exploration rate, and the optimal-arm tail bound. Corrected statements are part of the output: the explicit constant printed at the end of Lemma 2's proof is too small, the constant printed for Lemma 3 has the wrong sign, and Lemma 3 as printed quantifies over arbitrary random intervals, which its proof does not support.
The standard proof for an optimistic index policy bounds the draws of a suboptimal arm by an under-estimation term and a concentration term. For Thompson Sampling the under-estimation term is not small: once the posterior of arm is concentrated, is close to in every round. Comparing with a lower confidence bound instead only helps if is large with overwhelming probability, and a bound on does not give that.
Proposition 1 supplies it, and it carries most of the difficulty. It must control long stretches of rounds in which arm is never drawn while several suboptimal arms compete, and it needs the samples of arm conditioned on its successes at a random time while the arm is not played, an optional-skipping step that the paper leaves implicit and that is the main measure-theoretic obstacle in Lean.
Representation. The algorithm is the published Thompson Sampling run (AgrawalGoyalTS_TwoArmed_ThompsonSampling) on the published Bernoulli bandit (bernoulliRelativeEntropy). That run is Agrawal–Goyal's Algorithm 2, which passes each reward through a Bernoulli trial of success probability equal to the reward; for rewards the trial returns the reward almost surely, so the posterior is exactly the paper's. Probabilities are values of tsLaw in , expectations of counts and the regret are lower integrals in , and every bound compares with the embedding of a real right-hand side.
Conventions.
Added hypotheses and corrections.
Trivializations ruled out. Thompson Sampling is not characterized by a predicate that an arbitrary policy could satisfy: it is the published run, which fixes the posterior draws, the argmax and the updates. The constant is quantified as , never , and no real number is extracted from a possibly infinite expectation.
Infrastructure and contributions. A complete development needs Beta–Binomial duality, Chernoff–Hoeffding bounds for binomial tails, optional skipping for the reward stacks of the played arms, and the KL-UCB counting argument. The Beta–Binomial identity is an open milestone shared with the Agrawal–Goyal mission. Proofs of any milestone, in particular Proposition 1, Lemma 4 and the analytic Lemma 3, are welcome; Lemma 3's bound and the index comparison are pure real analysis and reusable beyond bandits.
Estimating a large matrix that is approximately low rank from a few noisy linear measurements is a basic problem of high-dimensional statistics. It covers matrix completion (recovering a ratings table from a small sample of entries), multi-task regression and quantum state tomography. The standard estimator penalizes the nuclear norm, the sum of the singular values, which is the convex surrogate of the rank. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a variant of this estimator that uses the known distribution of the design. Their Theorem 1 proves sharp oracle inequalities, with leading constant 1, under a global isometry condition on the design (Assumption 1).
Global isometry is a strong requirement. For sparse vectors, the analogous requirement was relaxed to the restricted eigenvalue condition of Bickel, Ritov and Tsybakov (Ann. Statist. 37, 2009), which only asks for curvature on a cone of approximately sparse directions. The random-design version is due to Koltchinskii (Bernoulli 15, 2009), and a matrix version of the cone appears in Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731). Theorem 2 of the paper is the matrix counterpart of the restricted eigenvalue analysis for this estimator. It keeps the leading constant 1, and the price is a stronger tuning condition, λ ≥ 3‖M‖∞ instead of 2‖M‖∞. Section 5.4 of the same paper derives from it a sharp sparsity oracle inequality for the ordinary vector Lasso.
Observe n pairs (Xᵢ, Yᵢ), i = 1, …, n, where Xᵢ is a random m₁ × m₂ real matrix and Yᵢ a real random variable, satisfying the trace regression model
for an unknown matrix A₀. Write ⟨A, B⟩ = tr(AᵀB), and let ‖A‖₁, ‖A‖₂ and ‖A‖∞ be the nuclear, Frobenius and operator norms, the last being the largest singular value. The design enters through the bilinear form
with semi-norm ‖A‖_{L₂(Π)}. Two random objects are built from the sample: the noise matrix M = (1/n) Σᵢ (YᵢXᵢ − 𝔼(YᵢXᵢ)), and, for λ > 0 and a set 𝔸 of matrices, the estimator Â^λ, any minimizer over 𝔸 of
Let A = Σ_{j≤r} σⱼ uⱼvⱼᵀ be a singular value decomposition, with support (S₁, S₂), the spans of the uⱼ and of the vⱼ. Write 𝒫_A⊥(B) = P_{S₁⊥} B P_{S₂⊥} for the part of B orthogonal to both singular spaces, and 𝒫_A(B) = B − 𝒫_A⊥(B). When 𝔸 is a linear subspace and c₀ ≥ 0, the cone ℂ_{A,c₀} consists of the B ∈ 𝔸 with ‖𝒫_A⊥(B)‖₁ ≤ c₀‖𝒫_A(B)‖₁. The restricted constant μ_{c₀}(A) is the infimum of the μ′ > 0 such that ‖𝒫_A(B)‖₂ ≤ μ′‖B‖{L₂(Π)} for every B ∈ ℂ{A,c₀}. The paper uses μ(A) := μ₅(A).
Let 𝔸 be a linear subspace. If λ ≥ 3‖M‖∞, then
The bound is deterministic: it holds for every realization of the sample on which λ ≥ 3‖M‖∞. A₀ need not lie in 𝔸, and nothing is assumed about the design beyond what makes the objects finite.
The milestones are the displays of the proof, in the order the proof uses them:
Theorem 2 gives a sharp oracle inequality whose only design-dependent quantity is a restricted constant. That constant is finite in situations where the global isometry of Theorem 1 fails. The result covers every linear subspace 𝔸, for example all matrices, the diagonal matrices or matrices with a prescribed sparsity pattern. In the diagonal case it becomes a sharp sparsity oracle inequality for the vector Lasso under a restricted eigenvalue condition (the paper's Theorem 14). The oracle inequalities of Bickel, Ritov and Tsybakov under the same condition have a leading constant larger than 1.
The result is proved in the paper, in about half a page that leans on the proof of Theorem 1. No machine-checked version exists. A formalization pins down two things the printed proof leaves to the reader: the convex-analytic optimality condition behind (2.8), and the "obvious modification of (2.10)" and "some algebra" behind (2.20) and the final display. It also reuses and extends the platform's matrix vocabulary: nuclear and operator norms, SVD data, and the tangent and normal projections of the matrix completion missions.
The estimator is defined implicitly as a minimizer, so the analysis has to go through first-order conditions. Those require the subdifferential of the nuclear norm and a choice of subgradient that matches the support of the comparison matrix A. Mathlib has neither a characterization of this subdifferential nor the monotonicity argument in matrix form. The obvious route, copying Theorem 1, fails at the step that uses Assumption 1 to pass from Frobenius to L₂(Π) norms: without a global isometry, that comparison is available only on the cone ℂ_{A,5}, and the error is known to lie there only in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0 and only for λ ≥ 3‖M‖∞. The constant 5 = (λ + 2Δ)/(λ − 2Δ) at λ = 3Δ is not slack. A linear subspace, not just a convex set, is needed so that Â^λ − A lies in 𝔸, where the cone lives.
Matrices are RealMatrix m₁ m₂ from the published MatrixCompletion definitions. These supply ⟨·,·⟩ (matrixInner), the nuclear, Frobenius and operator norms, SVD data SVD A r, the sign matrix Σuⱼvⱼᵀ, and 𝒫_A, 𝒫_A⊥ (tangentProjection, normalProjection). This mission adds two definition files.
TraceRegression holds the standing assumptions: measurable Xᵢ and Yᵢ, square-integrable entries of Xᵢ, integrable Yᵢ and YᵢXᵢ, and 𝔼(Yᵢ | σ(Xᵢ)) = tr(XᵢᵀA₀) almost surely. The page leaves the integrability implicit. Without it a Bochner integral would silently be 0 and ‖·‖{L₂(Π)} would be meaningless. Expectations of matrices are entrywise. Independence of the pairs (p. 1) is not assumed: Theorem 2 does not use it. The estimator is any minimizer of L_n over 𝔸.sInf would make (2.19) false and is ruled out.The other conventions are these. "inf over A ∈ 𝔸" is a bound for every A ∈ 𝔸. rank(A) is Matrix.rank. n ≥ 1 and λ > 0 are assumed, as on the page. (2.8) is stated for a convex 𝔸, as in the proof of Theorem 1 where it is derived. (2.21) is stated for an arbitrary matrix in place of Â^λ − A. No printed statement needed correction.
A complete development needs the subdifferential of the nuclear norm ((2.1) of the paper), the first-order condition for constrained convex minimization, the identity (2.9) and the facts (2.10), and trace duality, which is on the platform as matrix_trace_duality_inequality. The subdifferential of the nuclear norm and the projection estimates are reusable well beyond this mission. Contributions of those general lemmas are welcome.
Many estimation problems in statistics and machine learning ask for an unknown matrix observed only through noisy linear measurements: matrix completion (recover a large matrix from a few noisy entries, as in collaborative filtering), multi-task regression, and quantum state tomography. A common structural prior is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of the singular values. Penalizing a least-squares criterion by the nuclear norm gives an estimator that can be computed by convex optimization.
Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a nuclear-norm penalized estimator in the general trace regression model and prove that it satisfies sharp oracle inequalities: the excess prediction error is bounded by the best approximation error over a class of matrices with leading constant exactly , plus a remainder governed by either the nuclear norm ("slow rate") or the rank ("fast rate") of the approximating matrix. A distinctive feature of their estimator is that it uses the known design distribution , which the empirical-risk estimators of the earlier literature (Candès and Plan 2010; Rohde and Tsybakov 2011; Negahban and Wainwright 2011) do not exploit; for noisy matrix completion the previously available bounds were suboptimal. Their Theorem 1 is the deterministic core from which the paper's matrix completion rates (Theorem 4) follow by bounding one random matrix in operator norm.
Let , , be random pairs, a real matrix and a real number, satisfying the trace regression model
for an unknown matrix . Let be the law of and . The inner product and semi-norm are
For a matrix with singular values , is the nuclear norm, the Frobenius norm, and the operator norm. If is a singular value decomposition, the pair is the support of , and is the orthogonal projector onto .
Given a set of matrices and , the estimator is
The random matrix
carries all the noise. Assumption 1 asks for a constant with for all .
If , then for any set
and if moreover is convex and Assumption 1 holds,
and, for every with support ,
The theorem is deterministic: it holds at every realization of the sample at which .
The milestones follow the paper's proof: the subdifferential of the nuclear norm (2.1); the basic inequality of p. 7 and the slow-rate bound (2.3); the first-order condition (2.6); the identity (2.9) and the facts (2.10); the inequality (2.11); the decomposition bound (2.12)–(2.14); the bound on via (2.15); and the combined inequality (2.17). The rank bound (2.16) is included as a supporting statement (not a milestone).
Theorem 1 separates the statistical problem into a deterministic oracle inequality and a single probabilistic estimate, . Any concentration bound for (matrix Bernstein for uniform sampling, Gaussian bounds for fixed designs) then gives a rate. The paper uses it to obtain matrix completion rates which its minimax lower bounds show to be optimal up to logarithmic factors on the class of matrices of rank at most with entries bounded by . The leading constant means the bounds remain informative when is not low rank but only well approximated by low-rank matrices.
The result has been proved on paper since 2011; to our knowledge no machine-checked proof exists. A formal proof requires the subdifferential of the nuclear norm and its interplay with the singular-subspace projections, which are reusable for every nuclear-norm method (singular value thresholding, robust PCA, multi-task learning).
The slow-rate bound (2.3) is a short computation from the definition of a minimizer and trace duality. The fast-rate bounds (2.4)–(2.5) are not: a minimizer comparison alone gives only as remainder, which does not scale with . One needs the variational inequality (2.6) over the convex set , the exact description (2.1) of the nuclear-norm subdifferential at an arbitrary comparison matrix , and a decomposition of along the support of in which the component orthogonal to the support is controlled in operator norm and the rest in Frobenius norm. Formally, (2.1) itself requires identifying the abstract singular values with a given decomposition and characterizing the operator-norm ball as the dual of the nuclear norm.
Matrices are RealMatrix m₁ m₂ = Matrix (Fin m₁) (Fin m₂) ℝ, with the published MatrixCompletion definitions supplying the Frobenius inner product matrixInner, nuclearNorm (sum of Mathlib's singular values), spectralNorm (operator norm), frobeniusNorm, SVD data SVD A r and the projections twoSidedSingularProjection (), tangentProjection () and normalProjection (). The sample lives on a probability space (Ω, P) with 0 < n; expectations of matrices are entrywise. Conventions committed to:
sInf is used).A.rank.Ruling out trivializations: the goal states (2.3)–(2.5) with the paper's constants and remainder terms, not the intermediate bound (2.17), and is pinned down as a minimizer over , not an arbitrary matrix.
Welcome contributions: proofs of the nuclear-norm subdifferential (2.1) and of the projection facts, which are reusable well beyond this mission, and the measure-theoretic identity from the model.
Obstacle problems, contact problems and control-constrained optimal control problems lead, after discretization, to complementarity systems of the form "find and with and ". The primal-dual active set strategy solves such systems by guessing which constraints are active, solving one linear system, and updating the guess. Each iteration costs a single linear solve, and in practice the method stops after few iterations.
Hintermüller, Ito and Kunisch (SIAM J. Optim. 13(3), 2002; authors' version hal-01660511v1) showed that the strategy is a semismooth Newton method for a reformulation of the complementarity system through a max-function, which gives local superlinear convergence. For convergence from arbitrary initial data the paper gives three sufficient conditions on the matrix. The first is that is an M-matrix (Theorem 3.2), a class that many discretized second-order elliptic operators belong to. The M-matrix property is not stable under small perturbations: off-diagonal entries may become positive (p. 10). Theorem 3.4, the subject of this mission, shows that global convergence nevertheless survives small perturbations of an M-matrix. The paper notes that this also makes it relevant for numerical implementations.
Fix , vectors and a parameter . Vectors are ordered componentwise. For a matrix the problem is
with the maximum taken componentwise. The paper writes for the matrix and calligraphic , for the active and inactive index sets.
The primal-dual active set algorithm starts from an arbitrary pair . Given it sets
and determines from
For an index set with complement , is the principal submatrix of on and the block with rows in and columns in . The step above is uniquely solvable exactly when is invertible.
A square matrix is an M-matrix if it is nonsingular, for , and entrywise. For a rectangular matrix , is the matrix norm subordinate to the one-norms on both spaces, i.e. the maximal absolute column sum .
Let be an M-matrix. There is such that for every with , every and every , with :
The threshold is left unspecified; the theorem asserts only its existence.
A companion statement records the paper's remark after the theorem: for small, is a P-matrix.
The result. Theorem 3.2 makes global convergence depend on a sign pattern, which a perturbation of any size can destroy. Theorem 3.4 replaces the sign pattern by a neighbourhood: every matrix close enough to an M-matrix in inherits unique solvability of (3.1), well-posedness of every iteration, and convergence from every starting point. As the paper observes, solvability of (3.1) for every is equivalent to being a P-matrix (Berman–Plemmons, Thm. 10.2.15), so the theorem also yields a sufficient condition for the P-matrix property.
Formalizing it. The paper's argument is a short sketch that refers back to the proof of Theorem 3.3 and asserts that " can be chosen sufficiently small". A formalization makes the uniformity of that choice explicit (it depends only on ), checks the strict decrease of the merit function including its equality case, and fixes the role of the first iterate, from which the sign facts used in (3.8) hold. To our knowledge none of the three global convergence theorems of the paper has a machine-checked proof.
The obvious argument is to transfer Theorem 3.2 by continuity. It fails because the M-matrix proof is monotonicity-based: it shows , and that ordering uses and , sign conditions that a perturbation breaks immediately. What survives is weaker: a scalar merit function whose decrease must be quantified. The perturbation has to be controlled uniformly over all index sets, both in the multiplier term (where the decrease must remain strict whenever ) and in the coupling term , whose positive part must be absorbed by . Finally, strict decrease of a merit function does not by itself give convergence; the finiteness of the possible active sets must be combined with it.
Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ; index sets are Finset (Fin n) and blocks are submatrices along subtype inclusions. Conventions committed to:
IsUnit of the determinant), because Lean's inverse of a singular matrix is ; it is stated for any finite index type so that it applies to principal blocks;The goal does not assume that is a P-matrix, that its principal blocks are invertible, that , or that the merit function decreases: all of these are consequences. A version with chosen after , , or the run, or with any of these as hypotheses, would be trivial or different and is ruled out. Well-definedness is a conclusion, so runs from every initial pair exist and the convergence conclusion is not vacuous.
In the g-estimate, the page's final is a misprint for ; the statement uses .
A complete development needs: principal submatrices of M-matrices, Neumann series for matrices with the column-sum norm, the block form of one step and the identity (3.8), the sign facts on and on for , and continuity of principal minors for the P-matrix statement. The M-matrix and Neumann-series lemmas are reusable beyond this mission. Proofs of any milestone, of the companion, or of the goal through another argument are welcome.
The sample average approximation (SAA) method replaces an expectation in a stochastic program by the average over a random sample and solves the resulting deterministic problem. It is the standard way to solve two-stage stochastic linear programs with large or continuous scenario sets, and it underlies the stochastic counterpart and sample-path optimization methods of the 1990s. A basic question is how large the sample has to be.
For smooth problems the SAA optimal solution converges to the true one at the rate of the central limit theorem. A. Shapiro and T. Homem-de-Mello (SIAM J. Optim. 11(1), 2000) observed that for problems whose optimum is a sharp minimum, as is typical of two-stage linear programs with finitely many scenarios, the picture is different. In §2 of the paper they prove that the SAA problem then returns the exact true solution with probability one for all sufficiently large . In §3, formalized here, they show that the probability of the complementary event, the SAA solution not being exactly , decays exponentially in . One consequence they draw is that a modest sample can find the optimum of a problem with an astronomically large number of scenarios. This mission is the second of three on the paper; the first formalizes the almost sure statement (Theorem 2.1), the third the polyhedral case with multiple optima (Theorem 3.2).
Let be a probability measure on a sample space , , and . The true problem (1.1) is
Given an i.i.d. sample with law , the SAA problem (1.2) is
and denote the sets of optimal solutions of (1.1) and (1.2). For a function , is its directional derivative, and is that of . is the tangent cone of at , and .
The standing hypotheses are those of Theorem 2.1 of the paper: (i) is convex for every ; (ii) is finite valued; (iii) is closed and convex; (iv) Assumption (A): and is a sharp minimum, i.e. there is with
Section 3 adds Assumption (B): with (3.1), there is such that for -almost every . It holds whenever is finite.
The event of interest is
that the SAA problem has the unique optimal solution .
For a direction , and (3.5) is the one-dimensional rate function of . On the Banach space , (3.4) is the rate function of the random element .
Under (i)–(iv) and Assumption (B) there is a constant with
The goal asserts the existence of an exponential rate and does not fix its value.
With from (2.2) and from (B),
which is (3.8) combined with (3.15).
In the order of the proof:
Theorem 3.1 says that at a sharp minimum the SAA method is exact except on an event of probability . The sample size needed for a given confidence therefore grows only logarithmically in the confidence level, and it does not depend on the number of scenarios. This is the basis of the paper's numerical observation that problems with very many scenarios are solved exactly from samples of a few hundred. The explicit constant relates the rate to two interpretable quantities: the sharpness of the optimum and the bound on the subgradients of at .
The result is proved in the paper. As far as is known it has no machine-checked proof. A complete formalization produces three things. First, a Lean proof that the SAA problem recovers a sharp optimum exactly with exponentially small failure probability. Second, the elementary facts about cumulant generating functions of bounded variables, (3.11)–(3.13), which are reusable in any Chernoff-type argument. Third, the link between the rate function of a -valued random element and its one-dimensional projections, (3.6).
The event is controlled by the positivity of a whole function, , on the infinite set . A Chernoff bound for each fixed direction is easy, but there are uncountably many directions, so a union bound over is not available. The paper handles this with Cramér's theorem in the separable Banach space , and that infinite-dimensional large deviations upper bound is not in Mathlib. A proof must either develop that bound or find a finite-dimensional substitute that keeps an exponential rate.
A second difficulty is conversion. Cramér's theorem gives a rate in terms of , and that infimum must be shown positive. Positivity comes from the sharpness constant through the strong convexity of the one-dimensional rate functions, which needs the bounds (3.11)–(3.13) on the cumulant generating function.
EuclideanSpace ℝ (Fin m). The scenario space carries the law of one scenario. The sample is one i.i.d. sequence of -valued maps on a separate probability space , and uses its first terms. Optimal sets are written without infima: encodes "nonempty and equal to ".limUnder of the difference quotient as . Every statement assumes (i), under which the limit exists. The tangent cone is Mathlib's tangentConeAt, which for convex is the closure of the cone of feasible directions.logMGF and legendre, under which for is a genuine value, not a default.ProbabilityTheory.cgf and its analyticity); and an exponential upper bound for empirical means in or a substitute. The cumulant generating function lemmas and any Banach-space Cramér bound are reusable beyond this mission. Contributions are welcome for any milestone, and for alternative proofs of the goal that avoid Cramér's theorem in function space.Learning with errors (LWE) asks to recover a secret vector from noisy inner products , where the are uniform and the errors are drawn from a narrow distribution on . Regev introduced the problem and showed that solving it is at least as hard as solving worst-case lattice problems by a quantum algorithm (Regev 2009). The same paper uses LWE to build a public-key cryptosystem, the ancestor of most lattice-based encryption schemes in use today, including the schemes standardized by NIST in 2024 (ML-KEM, derived from Kyber).
A cryptosystem has two halves: security (an eavesdropper learns nothing about the plaintext) and correctness (the legitimate receiver recovers the plaintext). This mission is the correctness half of Regev's scheme: Lemma 5.1 of the paper, which converts a tail bound on the noise into a bound on the probability that decryption fails. The source is the published article, Journal of the ACM 56(6), Article 34 (2009). The paper's main theorem, a quantum reduction from lattice problems to LWE, is outside this series.
Fix an integer and let with addition modulo . Fix integers and a probability distribution on . All additions are in , and for .
absZ) is the integer if and otherwise.convPow χ k) is the law of the sum of independent samples from ; is the point mass at .publicKey).encrypt).decrypt, decodeResidue).The outcome distribution outcome n m χ c of a bit is the law of the decrypted bit when all of , , and are drawn as above.
Let and assume that for every ,
Then for each bit ,
the probability being over all the randomness of the protocol. The lemma has no hard-coded parameters: , , , and are arbitrary, and the paper's concrete choice ( prime in , ) is supplied separately by Claim 5.2.
The result. Lemma 5.1 is the interface between the noise distribution and the scheme: any bound on the tails of the convolution powers , , gives a bound on the decryption error, independently of the security analysis. With Claim 5.2 it shows that the paper's parameters decrypt correctly except with negligible probability. The same template (residue equals accumulated noise; small noise rounds correctly) underlies the correctness proofs of essentially every later LWE-based encryption scheme.
Formalizing it. The result is proved in the paper and is elementary; it is not open. As far as is known, no machine-checked statement of Regev's scheme as a probability experiment exists on Prove2Me; related platform items concern a different scheme (a dual-Regev variant with deterministic noise bounds over an even modulus). The mission's contribution is a faithful, reusable definition of the cryptosystem as a probability experiment over all of its randomness, together with a proof of its correctness lemma. The definitions (the distance on , convolution powers of a distribution on , i.i.d. product distributions) are reusable by later missions on the security proof (Claim 5.3, Lemma 5.4) or on other LWE schemes.
The arithmetic is short; the work lies in the probability bookkeeping. The hypothesis controls the law of the noise for each fixed subset size, while the conclusion is about a single experiment in which is random and independent of the errors, and the keys and are random too. The step that needs care is identifying the law of for a fixed with from a product distribution, and then averaging over ; the uniform choices of and must be shown not to affect the residue. A second point is the rounding step: is a cyclic distance on , and the strict inequality is sharp (at the residue is equidistant and decrypts to ), so odd and even and ties must be handled exactly as printed.
[NeZero p] and the hypothesis (the paper defines for , p. 34:14). Primality, part of the paper's parameter choice, is not assumed: Lemma 5.1 does not use it.ZMod p, vectors are Fin n → ZMod p, is a ⬝ᵥ s, bits are Fin 2, and subsets of are Finset (Fin m).PMFs. is defined recursively by binds; the i.i.d. errors use the product PMF with mass ; uniform choices are PMF.uniformOfFintype. The experiment outcome n m χ c draws , then , then , then , all independently.a.val; is natural-number division p / 2; is compared in , since it can be a half-integer.toReal of PMF masses, exact because they are at most ). The form ENNReal.ofReal (1 − δ) < Pr was rejected: for it would add the hypothesis , which the page does not make.Contributions welcome: proofs of the three milestones and the goal; general lemmas on convolution powers and product distributions of PMFs on finite groups.
The two-parameter Poisson–Dirichlet distribution is a law on decreasing sequences with . It describes the ranked frequencies of species in Bayesian nonparametric models (the Pitman–Yor process), the ranked lengths of excursions of Bessel processes and bridges, and the ranked cycle or block sizes in random combinatorial structures. The case is Kingman's one-parameter family , the law of the ranked frequencies in the Ewens sampling formula.
For , Vershik and Shmidt ([67]) and Ignatov ([34]) found a Markov description: the residual fractions form a homogeneous Markov chain, and the law is the -tilt of a stationary chain built from independent ratios. For , Proposition 8 of Pitman and Yor shows that the ratios themselves are independent variables. Theorem 38 of Pitman and Yor (Ann. Probab. 25 (1997) 855–900) unifies both descriptions for the whole two-parameter family.
Timeline. Vershik and Shmidt (1977, 1978, [66, 67]) and Ignatov (1982, [34]) described the size-ordered frequencies through the Markov chain ; Ignatov showed that results of Vervaat and Watterson give the normalizing constant (132). Much of this was known earlier for , the case arising in combinatorics and number theory. Perman, Pitman and Yor (1992, [51]) proved the absolute continuity of with respect to (Proposition 14 here). Pitman and Yor (1997) announced the two-parameter Markov description as Theorem 15 and proved it as Theorem 38 for , quoting the case (Remark 40).
Fix and . The beta distribution () has density on . Let be independent with , and put , . The ranked values of have, by Definition 1, the law ; denotes a probability under which has this law, and its expectation.
From define the ratios (21), the residual fractions (45), and . Conversely, from ratios define
The local time is (24).
The comparison law makes independent with , and is then defined by (125). Constants and functions:
for every nonnegative product measurable ; under both and the sequence is a Markov chain with the same forward transition probabilities, with density
on , , where (140); and the law of is infinitely divisible with
Proposition 8 ( on the ratios), Proposition 14 (the density of relative to ), the moments (30) of , the representation (143) of through the ratios, the finite-dimensional change of measure (144), its limit (145), Proposition 37 (independent ratios give a Markov chain , with co-transition density (128)), the parameter shift (146), and the conditional Laplace transform of given .
The result. Theorem 38 reduces the size-ordered frequencies to a product of independent beta variables, up to a density that depends on alone. Any functional of the ranked frequencies can therefore be computed under a product measure. The Markov property gives the joint density of (Corollary 41), the laws of individual (148), and the asymptotics of and in §7.3 of the paper. Part (iii) identifies the law of under , which determines the density of the largest frequency under .
The formalization. The result has been proved since 1997; none of it is machine-checked. The mission formalizes the paper's own route: absolute continuity (Proposition 14), the beta product structure (Proposition 8), and a limit of finite-dimensional density ratios. It produces reusable statements about real-valued Markov chains defined through conditional laws, and about changes of measure between infinite products. Note that the printed (139) omits the factor ; the formal statement includes it (see Formalization scope).
The finite-dimensional change of measure (144) is an exact computation, but its density degenerates as . Passing to the limit (145) requires identifying the limit of the rescaled densities with , and an almost sure limit of densities does not by itself give the identity of expectations. A second obstacle is that the Markov property of under does not follow from any independence under itself; it is transported from through a density that is a function of only, and the transported kernels must be shown to be the same. Part (iii) needs the Laplace transform of conditioned on , which comes from the Poisson structure of .
Sequences are ℕ → ℝ, 0-based: V ω k is , Yseq v k and YofR r k are . " has law" (HasPD) means that measures of preimages of measurable sets agree with those of the ranked stick-breaking map under an independent beta product (IsStickLaw); ranking counts exceedances with Set.encard. is any probability measure on ℕ → ℝ with independent coordinates of the stated beta laws (IsStarLaw); it is defined directly as a product, never through . The local time is a random variable given with its defining almost sure limit (24). A Markov chain with forward kernels (IsMarkovWith) is stated through the defining identity ; Theorem 38 (ii) asks for one family of Markov kernels serving both laws. The function of (140) is a hypothesis: any function giving the density of under each .
Committed deviations: the goal is the case , the case the paper proves (the case is quoted from [67], [34]); (139) carries the factor that Bayes' rule from (128), (146) and the beta densities produces, and that Corollary 41's confirms; (30) omits its middle expression . Every expectation of a nonnegative quantity is a lower Lebesgue integral, so no identity can hold through the junk value of a non-integrable Bochner integral; no law is written as Measure.map of a possibly non-measurable function; no limit is taken with limUnder; and the parameter range , is a hypothesis of every statement that uses it.
Contributions welcome: the product-measure and beta-density computations behind (144) and (146), the limit passage (145), the Markov property of functions of independent sequences (Proposition 37), and the transfer of a Markov property through a density depending on the first coordinate.
In the periodic-review inventory system with lost sales and a positive lead time , demand that cannot be met from stock is lost rather than backlogged. Unlike the backorder model, whose optimal policy is a base-stock policy depending only on the inventory position, the lost-sales model needs the whole pipeline of outstanding orders as its state, and its optimal policy has no closed form. Exact dynamic programming is impractical beyond small lead times, so practitioners and researchers rely on structural information: monotonicity of the optimal order, and simple bounds that bracket it.
The classical bounds go back to Karlin and Scarf (1958), who studied the case , and Morton (1969), who obtained bounds for general in terms of fractiles of cumulative demand. Zipkin (2008, DOI 10.1287/opre.1070.0482) recovered these bounds inside a unified framework built on a transformed state variable, the partial sums of the pipeline. This mission formalizes that recovery: §4 of the paper, from the closed form of the arriving inventory to Corollary 9.
Timeline. Karlin and Scarf (1958) treat the one-period lead time; Morton (1969) proves the fractile bounds for any and uses the partial-sum state; Nahmias (1979) gives the closed form (7) for the inventory on hand when an order arrives; Zipkin (2008) derives the bounds again by an induction on the re-accounted recursion, together with -convexity results for the original recursion.
Periods are . In each period the order due arrives, a new order is placed, and demand occurs. Demands are independent, identically distributed and nonnegative, with law . The costs are a unit procurement cost , a unit holding cost , a unit lost-sales penalty , and a discount factor ; write .
The state is the vector with , where is the inventory on hand and are the outstanding orders, oldest first. The state space is the cone
After demand and order the state becomes
with the vector of ones. Let be the inventory on hand when the current order arrives, periods later.
The §4 accounting charges to period the expected cost of period , when the order of period is on hand:
The optimal costs satisfy
and the optimal policy is the smallest minimizer of .
Assume and set . Let be the total demand of periods . The fractiles are
Let . The set consists of the policies with for , and, for , and for every .
For every period and every , the smallest optimal order exists and
The goal asserts the bounds as stated by the paper, with the fractiles left as functions of the demand law. It fixes no numerical constants.
The bounds turn a high-dimensional control problem into a box around the decision. The order is limited by the fractile of one-period demand, and also by every partial inventory position against the fractile of -period demand. They justify base-stock-like heuristics for lost-sales systems, restrict the search space in numerical dynamic programming, and are the starting point of the weighted bounds in Corollary 10 of the same paper. Monotonicity of the optimal cost in the pipeline (Theorem 8) is a structural fact used throughout the lost-sales literature.
The results are proved in the literature. To our knowledge none of them is machine-checked. A complete development adds a checked derivation of the classical bounds from first principles. It also adds reusable components: the closed form (7) for lost-sales dynamics, the fractile function for sums of i.i.d. demands, and a finite-horizon dynamic program over a continuum of actions in which the existence of a least minimizer is established rather than assumed.
The bound at the last period (Lemma 6) is a newsvendor-type argument once is written in closed form. Propagating it backwards is harder. The tempting argument is that only adds a cost that grows with , so the optimal order can only shrink. That requires to be nondecreasing in the state, which is not a property of the one-period cost alone. Monotonicity of in turn needs the minimization over to preserve it, and the paper's argument for that uses convexity of in , which the paper derives from -convexity of the original recursion. Even Lemma 7, the last-period case, is proved on the page only for , through a convex-order comparison of the arriving inventory; the general case is asserted to be similar. The existence of a minimizer at every stage also has to be established, since the action set is unbounded and the value functions are defined as infima.
The Lean development lives in the namespace ZipkinLostSales.Bounds. The conventions are these.
fB M 0 is , gB M k is , and fB M (k+1) is . By stationarity, "for all " becomes "for all ", and is , where .Fin L → ℝ, indexed from 0, with the paper's convention . The fractiles are indexed by Fin (L+1). "Nondecreasing in " is monotonicity on for the componentwise order.IsLeast), following the tie-breaking rule on p. 938. Its existence is part of the goal, Lemma 6, and Theorem 8. The least minimizer is not defined as the sInf of the set of minimizers: that sInf is when the set is empty, and always lies in , so that encoding would make the goal trivially true.sInf. Under the assumptions the set is nonempty and bounded below, and the infimum is attained. is the sum of coordinates of independent demands.Assumptions. The paper states , nonnegative independent demand, and . Three readings are added: demand has finite mean, which makes finite; "unit cost" and "discount rate" are read as and ; and "the are independent" with stationary data is read as i.i.d. with one law. may be negative.A sorry-free check shows that the assumptions are jointly satisfiable, with , demand , , and . There , and the least optimal last-period order at is .
A complete development needs:
The closed form (7) and the fractile lemmas are reusable for other lost-sales and newsvendor missions. Proofs of the milestones in any order are welcome, as are auxiliary lemmas on measurability and integrability of the value functions.
Biometric readings, physical unclonable functions and typed passphrases share two defects as cryptographic keys: they are not uniformly distributed, and they are never reproduced exactly. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; preprint arXiv:cs/0602007v4) introduced the secure sketch to handle the second defect without destroying what entropy the secret has. A secure sketch publishes a string from which any reading close to the original recovers the original exactly, while the original keeps a guaranteed amount of min-entropy given . Many sources of noise are not substitutions but insertions and deletions: keystroke sequences, sequenced DNA, and any reading whose alignment drifts. For these the relevant distance is the edit distance, and §7 of the paper gives a secure sketch for it.
This mission formalizes that construction: Theorem 7.5 (p. 27), together with the results it is assembled from, PinSketch for set difference (Theorem 6.3, p. 23, with the BCH decoding argument of Appendix E) and the shingling embedding (Lemma 7.3, p. 25), glued by Lemma 4.7 (p. 15).
All logarithms are base 2. A random variable is identified with its distribution. The min-entropy of is , and the average min-entropy of given is .
Let be a set with an integer-valued distance . An average-case -secure sketch is a pair of randomized procedures such that whenever , and for every pair with . The difference is the entropy loss.
Three spaces occur.
A -shingle of a string is a length- consecutive substring, and the -shingling is the set of all of them. A map is a -biometric embedding with recovery information if it maps distance to distance , takes at most values, and is determined by .
For every finite alphabet with letters, all with and every real , there is an average-case secure sketch
Theorem 7.5 gives a secure sketch for the edit metric whose entropy loss is, for a good choice of , about (p. 26). This is sublinear in for up to nearly linear, and for large it improves on the low-distortion embedding approach of §7.1. Combined with a strong extractor it yields fuzzy extractors for edit distance (Theorem 7.4). PinSketch is itself the standard set-difference sketch, and Lemma 4.7 is a general transfer principle between metrics.
All results here are proved in the paper. None has a machine-checked proof that we know of. A complete development would also formalize a fragment of BCH decoding over , the syndrome-uniqueness theorem for binary BCH codes, and a combinatorial lemma on how insertions and deletions act on shingle sets. Each is reusable outside this mission.
There are two hard steps.
The first is Lemma 6.2. That a low-weight word is determined by power sums is a statement about Vandermonde systems in characteristic 2, where the even power sums carry no new information. Newton's identities, the usual characteristic-zero route from power sums to elementary symmetric functions, fail there because they divide by integers that vanish in characteristic 2. The paper argues through the error-locator and error-evaluator polynomials instead.
The second is the distance clause of Lemma 7.3. An edit path between two strings of length passes through strings of other lengths, so a per-step bound on the shingle sets must hold for strings of every length, including lengths below .
The entropy statements involve average min-entropy over arbitrary auxiliary variables, and each needs the chain-rule bound of Lemma 2.2(b) in average-case form.
PMFs, and randomized procedures are kernels M → PMF S. The auxiliary variable of every average-case statement ranges over every ι : Type, not only finite types. Average min-entropy uses the joint form above. "Min-entropy " means , and is real.K of characteristic 2, and its degree is renamed because denotes min-entropy. Appendix E's large field is this K, distinct from §7's alphabet . Only binary words are formalized, as subsets (Finset Kˣ); the -ary generality of Lemma E.1 is not.MasekPaterson.Shared.editDist with cost 1 per insertion or deletion and 2 per replacement, which equals the insertion/deletion count.Nat.clog 2 (F ^ c + 1).Contributions are welcome on any milestone. The BCH part (Appendix E, Lemma 6.2) and the shingling part (Lemma 7.3) are independent.
The random difference equation
describes the stationary state of the affine recursion driven by independent copies of a random pair . It appears wherever a quantity is multiplied by a random factor and then receives a random increment: the discounted value of a stream of random cash flows (a perpetuity), the stationary volatility of ARCH and GARCH models in financial econometrics (de Haan, Resnick, Rootzén and de Vries 1989), random walks in random environment, and the stationary laws of random coefficient autoregressions. In all of these, the question that matters for risk is the size of the tail .
Timeline:
Let be a pair of real random variables with joint law on . No independence between and and no sign condition on either is assumed. A probability law on is a law for satisfying (1.1) if the law of equals when has law and is independent of .
A law on is arithmetic if it is concentrated on a lattice for some , and nonarithmetic otherwise. For , the conditions of Lemma 2.2 on are
and that the conditional law of given is nonarithmetic. Under them
With and , the constants of Theorem 4.1 are, when a.s.,
and otherwise , where has the stationary law and is independent of .
Assume the conditions of Lemma 2.2 and . Then there is a unique law for satisfying (1.1); the expectations defining are finite; and
with as above. Finally
In the order the proof uses them:
The result. Theorem 4.1 identifies the tail exponent of the stationary solution as the root of , which depends on alone, and expresses the tail constants as expectations under the stationary law. The constants yield the bounds of Corollary 4.3 and closed forms when is an integer (Corollaries 4.4, 4.5). The dichotomy between a.s. (different left and right constants) and (equal constants) is visible only through these formulas. The positivity criterion tells when the power tail is really there: it fails exactly when the recursion has a deterministic fixed point . Tail estimates for GARCH processes, perpetuities in insurance mathematics and random walks in random environment are applications of this statement.
Formalizing it. The theorem has been proved since 1973 and in the present form since 1991; it is open only as a formalization. No machine-checked proof of Kesten's theorem, of the implicit renewal theorem, or of the underlying nonarithmetic key renewal theorem on the whole line is known to this mission. The work consists of formalizing Goldie's proof, which assembles the implicit renewal theorem with moment estimates, a maximal inequality and a Cramér–Lundberg-type lower bound for a random walk with negative drift.
The obvious argument is to write and estimate the tail of each term. It fails because makes every term contribute tails of the same order , and the sum of infinitely many such contributions is exactly what has to be computed; termwise bounds give the right exponent at best, not the limit or the constant. A second natural idea, applying the renewal theorem directly to , needs integrability of a tail difference that is not evident, because is infinite whenever ; the moment differences must be controlled without either term being integrable. The positivity half is a separate problem: the formula for is a difference of two infinite-looking quantities, and showing it is positive requires a lower bound on the tail that does not come from the formula.
Everything is stated in terms of laws. The joint law of is a probability measure on (first coordinate , second ); a law for satisfying (1.1) is a probability measure on that equals the image of under , and uniqueness is among all probability measures on , with no moment restriction. Expectations involving and are integrals against , which is what makes independent of . The conditions of Lemma 2.2 are stated for the law of , with and as lower Lebesgue integrals and the conditional law of taken given . "" is the limit statement , which the paper prescribes and which includes . Milestones on sequences use independent copies on an arbitrary probability space carrying them, stored 0-based.
The statement does not reduce to a trivial one: the ratio form (undefined when ), existence of some fixed point without uniqueness, the positivity criterion as a one-way implication, and tail limits asserted for an arbitrary random variable rather than for the stationary law are all excluded. One correction to the source is built in: Lemma 9.4's (9.17) is printed as an equality, which fails for independent identically distributed non-degenerate , ; the inequality the proof establishes is stated.
A complete development needs: convolution and image measures of products on ; the key renewal theorem on the whole line for nonarithmetic laws with positive mean (the content of the first mission of this series); existence and uniqueness for contractive random affine maps; Lévy-type maximal inequalities; and ladder-height estimates for random walks with negative drift whose steps may equal . The renewal-theoretic and random-walk components are reusable well beyond this mission. Contributions of any milestone, and of supporting lemmas such as the moment bounds for perpetuities, are welcome.
Distributionally robust optimization replaces the expected loss of a statistical model by its worst case over all distributions close to the data distribution . When closeness is measured by an -divergence ball of fixed radius , the robust risk upper-bounds the risk of every subpopulation of that has sufficiently large probability, so a model with small robust risk performs uniformly well across latent subgroups. This is the program of J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization (arXiv:1810.08750; Ann. Statist. 49 (2021), doi:10.1214/20-AOS2004).
The robust risk is itself a statistical functional. It is estimated by plugging in the empirical distribution, and the paper shows (its Theorem 2) that for the Cressie–Read family of divergences with parameter the plug-in estimate concentrates at rate , with . For small (heavy protection against distribution shift) is large and this rate is far slower than the parametric . This mission formalizes the paper's answer to whether the slow rate is an artefact of the plug-in estimator or intrinsic: its Theorem 3, a minimax lower bound valid for every estimator.
Fix and write . The Cressie–Read function is
For a probability measure , a real random variable and a radius , the robust risk is
the supremum of over distributions with likelihood ratio and Cressie–Read divergence at most .
Write
Fix and let be the set of all distributions on the two points ; each is determined by its mass at . An estimator is any function of a sample drawn i.i.d. from . The minimax risk of estimating the robust risk is
The total variation distance between two product laws on the finite set is , and denotes the Kullback–Leibler divergence.
For every ,
The first branch is of order , the second of order . The page prints in the first branch; the target uses (see Formalization scope).
Theorem 3 shows that the rate of the paper's concentration bound for the plug-in robust risk cannot be improved by any estimator, even when the data take only two values. For the robust risk is therefore intrinsically harder to estimate than a mean: its value depends on how much mass puts on rare large values, and rare events are observed rarely. The same phenomenon drives the paper's lower bounds for minimizing the robust risk (its Section 5.2), which are not part of this mission.
The result is proved in the paper; no machine-checked version of it or of Lemma 12 is known. Formalizing it produces a verified two-point analysis of the Cressie–Read robust risk (Lemma 12 and its primal formula), which is reusable for any lower bound or worked example involving -divergence balls, and a verified finite-sample Le Cam two-point bound for estimating a functional of a distribution on two points. It also corrects a constant in the first branch of the printed statement.
The lower bound needs two distributions on that are statistically close yet have well-separated robust risks. Both requirements must be quantitative and must hold simultaneously at the stated constants. The robust risk is a supremum over an infinite-dimensional set of likelihood ratios, so the separation needs exact control of that supremum for two-point laws: an exact value above the threshold , and matching upper and lower bounds below it. For mass near the separation is linear in , while for small mass it is of order , which is where the slow rate comes from. Closeness requires the KL divergence of each pair to be at most , and the two branches need different perturbations. A naive bound on the robust risk by or by the mean gives no separation at all.
The Lean development lives in the namespace UniformDRO.LowerBound. Its conventions are:
HighDimStat.Minimax.minimaxRisk.BanditAlgorithm.bernoulliRelativeEntropy, always evaluated with a second argument in , where it is the true divergence.Real.rpow. The primal formula is stated for , where its negative powers are finite.The goal is the lower bound on the minimax risk (16) over all estimators and all laws on . It does not mention the two hypotheses, , total variation or KL divergence, so it cannot be satisfied by a statement about a particular pair of laws or a particular estimator.
Contributions are welcome at every level: proofs of Lemma 12 through the primal formula or through the dual representation of the robust risk, a general finite-space Le Cam lemma, and tensorization of KL and Pinsker for finite products, which are reusable beyond this mission.
Support vector machines classify observations by choosing a real-valued function from a reproducing kernel Hilbert space and using its sign as the predicted label. The Gaussian kernel is widely used because it gives a flexible class of functions, but that flexibility alone does not explain how quickly classification error approaches the best possible error as the training sample grows. Steinwart and Scovel's 2007 paper identifies distributional conditions under which a Gaussian-kernel SVM achieves a polynomial, and sometimes nearly linear, excess-risk rate. The conditions describe both ambiguity in the labels and the location of data relative to the decision boundary.
The article's result is already proved mathematically. This mission asks for machine-checked statements and proofs of its finite-geometric-exponent, no-offset rate and selected supporting results. It uses arXiv:0708.1838v1, the electronic reprint of the Annals of Statistics article. Its printed page number equals its PDF page number throughout; all page references below use those numbers.
Let be the closed unit ball of , where , and let the label set be . A distribution on has input marginal and a measurable regression function . In the Lean representation, and one version of are carried explicitly; the joint law gives conditional masses and to the two labels. Classification predicts , with . Write for its error probability and for the smallest such risk over measurable decision functions.
The hinge loss is . The Gaussian kernel with parameter is , and is its restricted RKHS. Given a sample of size , an SVM without offset minimizes over that space. The approximation error is the infimum of the corresponding population objective minus the unrestricted Bayes hinge risk; equation (6) uses that unrestricted baseline.
Two assumptions describe the distribution. It has Tsybakov noise exponent if, for sufficiently small , for some . To define geometric noise exponent , partition according to whether is below, above, or equal to . The distance goes from a point in either strict class to the opposite strict class together with the equal-probability class. The geometric condition is
These are Definitions 2.2 and 2.3 and equation (7) of the paper.
The goal is the finite-, no-offset clause of Theorem 2.8. With the paper's two-case exponent , set and . For every , one constant works uniformly for and :
Here is outer probability, and the statement applies to every empirical minimizer. The formula for is in the first case, , and otherwise; the paper's limiting convention specifies .
Three milestones record results used on this path. Theorem 2.1 bounds empirical covering numbers of Gaussian RKHS balls, uniformly in and the sample. Lemma 4.1 locates balls of radius inside the corresponding enlarged decision class. Theorem 2.7 bounds the approximation error by
where depends only on dimension. Their exact source text and page positions appear in the milestone list.
Theorem 2.8 gives a quantitative guarantee for classification risk, rather than only convergence of the regularized hinge objective. The rate responds to both the label-noise exponent and the concentration of input mass near the decision boundary. In the regimes discussed after the theorem, the exponent can approach one; the paper's Remark 2.9 compares it with the benchmark.
Formalizing this result adds a concrete Gaussian RKHS norm compatible with a kernel parameter that changes with , an explicit binary-law model, extended-valued risks and covering numbers, and source-indexed bounds on approximation and complexity. Those objects can be reused in later SVM and kernel-learning statements. The paper's argument is a published proof; the Lean theorem files here are open proof obligations, while the definition files have compiled bodies. No claim of a machine-checked proof of the rate is made.
It is not enough to combine a general consistency theorem with the noise assumptions. The kernel parameter grows with sample size, so the relevant hypothesis class changes with ; a complexity estimate for one fixed class gives no uniform rate. Geometric noise controls approximation error, while Tsybakov noise controls a different fluctuation quantity, and neither by itself supplies the stated exponent. The probability statement also concerns an event defined by empirical minimizers, whose measurability the source deliberately avoids by using outer probability. These are the points at which a direct fixed-class or ordinary-probability statement would fail to match Theorem 2.8.
Lean represents functions on all of but uses only their restrictions to . The joint distribution is built from a probability marginal and a fixed measurable . This makes the paper's choice of regression-function version explicit. The Gaussian RKHS squared norm is the supremum over finite normalized kernel-section combinations; it is outside the RKHS. A covering number is the least positive finite cardinality of a cover with centers in the ambient empirical function space, or if there is no such cover. Hinge and classification risks are extended nonnegative integrals, and Bayes risks range over measurable functions.
The assumptions and give the divisions and powers their intended domains. For , the small- noise bound uses zero on the right, as in the source convention. The paper leaves distance to an empty set unstated; this mission pins . With the infinite-distance convention, Lemma 4.1 and Theorem 2.7 fail for a one-class regression function. The proof display (25) has a volume-factor slip in high dimension; Theorem 2.7 is stated with its printed conclusion, and the issue is recorded in the moderation notes. The goal event includes existence of an empirical minimizer, a fact stated in the paper's setup, and quantifies over every minimizer. This excludes a vacuous SVM predicate. The constant is chosen before and .
The clauses for and an SVM with offset are outside this mission. The separate series mission addresses the implication from an envelope assumption to geometric noise. Further contributions toward the §5 empirical-process estimates, §6 variance estimates, and §7 shrinking and general-rate theorems are welcome; they are not asserted as milestones in this draft.
The multiarmed bandit problem asks how to allocate a single resource, one play at a time, among several alternative projects whose states evolve only when they are worked on. It models the scheduling of jobs on a single machine, the design of sequential clinical trials and many problems of research planning. Gittins and Jones showed that it is optimal to play, at each time, a project of greatest Gittins index, a number computed from that project alone (Gittins and Jones 1974; Gittins 1979).
In practice the Gittins index policy is often replaced by a heuristic: indices are computed approximately, or a policy is constrained by operational rules. A practitioner then needs to know how much value is lost. R. Weber's paper On the Gittins index for multiarmed bandits (Ann. Appl. Probab. 1992) gives a short proof of the index theorem through prevailing charges, and in its Section 5 derives from it two suboptimality bounds. This mission formalizes the second of them, Theorem 3, which bounds the loss of an arbitrary policy using Gittins indices only.
Timeline. Gittins and Jones (1974) and Gittins (1979) prove optimality of the index policy by an interchange argument; Whittle (1980) gives a proof by retirement options; Glazebrook (1982) bounds the suboptimality of policies in terms of Gittins indices, the bound Weber calls "usually weaker than (6)"; Glazebrook (1990) gives the prevailing-charge bound that is Weber's Theorem 2; Weber (1992) proves the index theorem by prevailing charges and states Theorems 2–4.
There are bandit processes. Bandit has a state in a state space ; at each epoch the gambler plays one bandit , receives a reward with mean , the state of bandit moves according to a Markov transition kernel , and the states of all other bandits are unchanged. Rewards are nonnegative and uniformly bounded, and is a discount factor. A policy chooses , possibly at random, as a function of everything observed so far. Its value from the initial state vector is the expected total-discounted reward
The fair charge of a state is the largest ratio of expected discounted reward to expected discounted time that a stopping time of a single bandit started at can achieve,
and Weber's Gittins index is . A Gittins index policy plays, at every epoch, a bandit with the greatest index, ties broken arbitrarily. Theorem 1 of the paper, already formalized on Prove2Me as BanditAlgorithm.gittins_index_theorem, states that every Gittins index policy maximizes .
The model, the fair charge and the Gittins index policy are the published GittinsIndex definitions of Shuze Chen, and the history truncation used to write round expectations is from Harry_Xu's GittinsTerminalPotential.
For a Gittins index policy , every policy and every initial state vector ,
The right-hand side is computed along the trajectory of alone: in each epoch it charges the gap between the greatest index and the index of the bandit actually plays.
The proof compares, for each , two policies built from : , identical to before time and a Gittins index policy from on, and , identical to up to and including time , which then continues playing until its fair charge drops below its value at time and is a Gittins index policy thereafter.
The result. Theorem 3 turns any per-epoch guarantee about the index of the bandit played into a guarantee on value. If a policy always plays a bandit whose Gittins index is within of the greatest, it loses at most ; this is the form in which index heuristics, approximate index computations and constrained index policies are analysed. The open Prove2Me goal AllocationIndices.eps_index_policy_near_optimal (Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices, Theorem 4.18, after Glazebrook 1982) is a bound of this kind for -index policies and follows from (7); it is a separate item and is not part of this mission. Unlike Theorem 2 of the same paper, the bound (7) involves only Gittins indices, not prevailing charges or rewards.
Formalizing it. Theorem 3 is proved in the paper; no machine-checked proof exists. The mission produces a formal statement of the bound on top of the published Markov bandit model and Theorem 1, together with the two intermediate statements of Weber's proof, which have uses of their own: optimality of switching to the index policy after any finite prefix of play is the dynamic-programming form of the index theorem.
The informal proof is half a page, and its key sentence is that the difference of the charges paid by and at any later time is never more than the gap at time . Making it rigorous requires the value-to-go of a history-dependent randomized policy after a fixed time, the fact that both policies from time on are fair games in which expected discounted reward equals expected discounted charge, and a pathwise comparison of two interleavings of charge sequences. The naive reading, that loses only the single epoch , is wrong: playing at time commits the policy to a whole run of , and the bound accounts for the entire run through the factor . Telescoping (8) over also needs as , which rests on bounded rewards and .
The Lean development uses the published BanditAlgorithm model, in which all bandits share one state space (a standard Borel space), one kernel and one reward ; Weber's bandits with different state spaces are encoded by taking the disjoint union. Time is 0-indexed in both. The committed readings of the paper's phrases are:
IsGittinsIndexPolicy; it is not assumed to be built from .weberIndex), and (8) is written with (gittinsIndex) divided by , as on the page.IsSwitchToGittinsAt, IsRunThenGittinsAt), and (8) is stated for every pair of policies satisfying them. "Identical to for times less than " is rounds ; "plays at time " and "identical through time " are rounds . "Drops below" is strict.Using the fair charge in place of in (7) would make the bound false by the factor ; dropping the measurability of would let the expectation degenerate to and make the bound claim that every policy is optimal. Neither is the statement posed here, and a constant-index or one-armed instance, where both sides vanish, only checks that the hypotheses are satisfiable.
Theorem 1 is referenced, not posed. Theorem 2 (the prevailing-charge bound) and Theorem 4 (submodularity of the optimal value in the set of bandits) are missions 1 and 3 of this series; this mission does not depend on them. Weber's definition of an index consistent policy (p. 1028) is not formalized here: the proof of (8) needs the fair-game property in the form of Remark 2 (continue while the fair charge exceeds the prevailing charge), which differs from the definition's "initial value" after an interruption. Contributions welcome: a measurable greatest-index selection, value-to-go decompositions for history-dependent policies, and the fair-game identity for index-consistent play are reusable beyond this mission.
A firm with one product may face several customer classes in each selling interval. When stock is scarce, it must decide which outstanding demands to satisfy and how much inventory to carry into later intervals. When new stock can be bought at several dates, the rationing choice also changes the value of future purchasing opportunities. Topkis studied these linked decisions in a nonstationary model with class-dependent shortage penalties and a finite number of ordering periods. His Theorem 4 identifies conditions under which a policy computed from each period's myopic cost is optimal in the full multiperiod problem Topkis 1968.
The result belongs to a line of work on critical-level policies: choose a stock target and order up to it if current stock is lower. Here the target can be computed one period at a time despite the possibility of future purchases and the separate question of how to ration stock among demand classes. The paper attributes a related myopic policy result to Veinott and explains that its own setting allows a more general rationing policy than the special zero-rationing-level case discussed there Topkis 1968, pp. 175–176. This mission formalizes Topkis's multiperiod statement, including its ordering and rationing conclusions.
There are ordering periods, numbered through . Period has a unit purchase cost . It contains selling intervals, numbered backward: interval is first and interval is last. Within an interval, a random nonnegative demand vector has one component for each of customer classes. The vectors in distinct intervals and periods are independent and each class has a finite mean. At the start of an interval the demand is observed. A decision then selects how much of each class's outstanding demand to leave unsatisfied. The remaining physical stock incurs a holding cost, and each unsatisfied unit incurs a class-specific penalty. Unsatisfied demand is either carried entirely to the next interval or lost entirely, according to the interval. Penalties are nonnegative and rise with class index, so class has the highest shortage penalty Topkis 1968, pp. 162–163, 174.
Let be net stock before ordering at the start of period : physical stock minus outstanding backlogs. The order must clear the backlog, so the post-order stock satisfies . After period , a further unit can be purchased for , while unused stock can be salvaged for revenue . The terminal cost is . Working backward, is the optimal continuation cost, including the period- ordering decision. The actual period cost includes the later continuation value , and equation (19) reads
The single-period cost uses the same demand, holding costs and rationing choices in period , but replaces the later continuation value by the linear terminal charge . A myopic level is any minimum of on ; it is if no such minimum exists. Thus the level need not be the smallest minimum when several stock levels tie Topkis 1968, pp. 174–175.
Suppose and the selected myopic levels are nondecreasing from period onward:
Then , and ordering to minimizes over all feasible post-order levels . If and the stock at the start of period is at most , the optimal rationing policy during that period is the optimal policy for its single-period problem, calculated with terminal costs and Topkis 1968, Theorem 4.
The milestones are the paper's regularity claim for and , existence of an actual optimal order-up-to level, finiteness of , the shape of around an optimal level, and the comparison in equation (20). Together these specify the route from the general dynamic program to the myopic target.
Theorem 4 gives a checkable sufficient condition for replacing a multiperiod ordering computation with a sequence of single-period cost minimizations. It also identifies when the rationing decisions can be obtained from the same single-period model. The stock bound in its rationing clause matters: outside that range, future costs may alter which class demands should be filled now. The result therefore describes both the simplification and its operational domain Topkis 1968, pp. 175–176.
Topkis proved the theorem in 1968; the task here is to produce machine-checked definitions and proofs of that known result. The definitions of feasible rationing, backward value functions, myopic costs and order-up-to levels will also support comparisons with other finite-horizon inventory models. The §1 model is duplicated locally while the four missions for this paper are drafted in parallel, then intended for consolidation into a shared interface.
Convexity alone gives an order-up-to form for the actual cost , but it does not identify its minimizing level with a minimum of the simpler cost . The continuation value depends on all later ordering and rationing decisions. When some unsatisfied demand is lost, the end-of-period net stock can depend on the within-period rationing choice as well. The core issue is therefore to control the difference between the actual and myopic objectives in the stock range relevant to period Topkis 1968, pp. 174–176. A statement restricted to a preselected rationing rule would miss the theorem's claim about optimality among all feasible decisions.
Classes are indexed by Fin n; the largest index is the highest penalty class. Intervals and ordering periods use natural numbers with explicit bounds, and intervals retain the paper's backward numbering. Stock, penalties and costs are real. A period's demand vector has a probability law on real vectors supported on the nonnegative orthant, with every coordinate integrable. The §1 dynamic program uses real infima for feasible rationing choices and Bochner integrals for demand expectations. The multiperiod value uses the nonnegative post-order domain in (19). Its defining infimum is intended to be finite under the paper's assumptions; the regularity and attainment milestones expose the facts that rule out Lean's default value for an unbounded infimum. These functions are used only at , with period costs at .
The multiperiod standing assumptions require , , and at least one interval per period, matching the paper’s positive counts.
Holding costs and the appropriate terminal costs satisfy the convexity and continuity assumptions of §1. Within each period, backlog multipliers equal or . The terminal procurement cost is nonnegative and salvage revenue does not exceed it. Assumption (D′) is encoded as an eventually positive lower bound on the extended-real right derivative of . The §1 terminal functions used in the period assumptions are the linear functions required by the single-period comparison; their regularity adds no independent restriction. Independence across intervals and periods is built into successive expectations. The goal separately assumes and monotonicity of the selected myopic levels only from through .
The formal target compares the actual and single-period sets of optimal rationing decisions at every interval and at every nonnegative state with stock at most . The stock bound and the full feasible set prevent the claim from becoming a result about a handpicked policy. Contributions to the backward recursion, convexity and attainment facts, and the comparison of these two decision sets are all part of this mission.
The assignment problem asks for a one-to-one matching of agents to tasks that minimizes the total cost. It is one of the basic problems of combinatorial optimization and is solved in polynomial time by the Hungarian method. Its random version, in which the costs are independent random variables, is a standard model for the typical behavior of optimization problems on random inputs, and it has been studied in probability, operations research and statistical physics.
Timeline:
This mission is Chapter 10 of Talagrand's article.
Fix and two sets and of cardinal . An assignment is a one-to-one map from onto . Given a cost matrix , the cost of is . In the random problem the costs are , independent and uniformly distributed on , and the optimal cost is the random variable
A median of is any real with and .
The argument uses digraphs. A digraph is a subset , and for the set of neighbors is . For , is -expanding if for every
For the threshold digraph is : it keeps only the cheap edges.
There is a universal constant such that for , every median of and every ,
The constant is left unspecified, as in the paper.
The expected value of is of the same order as a single cost, yet is a function of independent variables. A generic bounded-difference bound in all coordinates gives no useful concentration at this scale. Theorem 10.5 shows that the fluctuations are at most of order , and by the remark after the theorem, so is the standard deviation of . The chapter is a worked example of how a concentration inequality in product spaces is combined with a combinatorial localization argument, the reduction to small costs, and that pattern recurs in the study of random combinatorial optimization problems.
Status: the theorem and its lemmas are proved in the paper. As far as a search of the platform shows, none of them has a machine-checked proof. The two posed statements of Theorem 4.1.1 on the platform (finite-alphabet form) are the concentration inequality the proof calls on; formalizing this chapter adds the combinatorics of expanding digraphs, the random-graph estimate Proposition 10.3 and the final assembly.
The naive approach applies a concentration inequality directly to as a function of the costs, each of which can change by up to . That loses all control, because the variance proxy grows with the number of coordinates. The central step is to show that, with high probability, an optimal assignment only uses costs of order . This requires the cycle structure of Lemma 10.1, and it requires showing that the sparse random digraph has expansion uniformly over all subsets of , whose number is exponential in . Proposition 10.3 has to beat that union bound, and its proof covers only one of the two expansion conditions in detail; the condition (10.2) for large sets is "left to the reader". The final step combines the truncation with Theorem 4.1.1 and a careful choice of parameters for the two ranges of .
The Lean development lives in the namespace TalagrandConc.Assignment and commits to the following conventions:
Fin N, assignments are Equiv.Perm (Fin N), and is optCost, a Finset.inf' over all permutations (no junk value).Fin N × Fin N → ℝ with costLaw N, the product of Lebesgue measure restricted to . The coordinates are the .Set.ncard on the finite type Fin N. -expansion includes as part of the definition.ℝ≥0∞, and is truncated subtraction there.A cycle of length would satisfy Lemma 10.1 vacuously. The formal statement therefore requires , which rules out that trivializing reading. Similarly, Theorem 10.5 fixes one constant for all ; a depending on would make the bound empty.
Infrastructure: the product of uniform laws on a finite index set, iterated expansion arguments for bipartite digraphs, a lower-tail Chernoff bound for independent events, and the union bound over subsets are reusable beyond this mission. Theorem 4.1.1 of the paper is posed elsewhere on the platform and is not restated here. The bound (8.1.1) used in Step 2 of the proof belongs to another chapter of the series. Contributions of proofs of any milestone, or of intermediate displayed estimates such as (10.5), (10.6) and (10.9), are welcome.
Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order , but the variance is unknown, so the bound cannot be evaluated from data.
Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).
For a vector of reals, the sample mean and sample variance are
Let be a probability distribution on a set , and a class of hypotheses (loss functions) . For , its risk is and its variance is , with . For a sample , and are and of the vector .
The complexity of enters through the growth function. For let , and let be the least number of sup-norm -balls centred in that cover . Then
For , sample variance penalization selects
With it is empirical risk minimization.
Fix , , and any . With probability at least in ,
The constants are the paper's. The goal is stated for an arbitrary comparator , so it covers an optimal one when one exists.
In the order of the proof:
Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as ; for a finite class does not depend on and the rate is . The paper gives a two-hypothesis example where empirical risk minimization cannot beat order (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.
All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a -normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.
Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for itself with the right dependence on , and is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.
The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.
Conventions:
i : Fin n.Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in " have laws giving zero mass outside .VarianceRegularization.Expansion.empMean. is a local sampleVar with the normalization. is Mathlib's variance.Metric.coveringNumber (closed balls, centres in the set, values in ).Added hypotheses and repaired statements, each disclosed in the item:
Ruled-out trivializations:
A complete development needs the following:
The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.
Controlled queues are the standard testing ground for Markov decision processes with infinitely many states: the state is a queue length, which is unbounded, and the holding cost grows with it. The classical theory of the average cost criterion (Ross, Applied Probability Models with Optimization Applications, 1970) produces an optimal stationary policy only when the relative discounted values are uniformly bounded, a condition that fails for almost every queue with unbounded holding costs. Linn I. Sennott's paper Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs (Operations Research 37(4):626–633, 1989, doi:10.1287/opre.37.4.626) replaced that boundedness by one-sided conditions that are checked in practice by a monotonicity argument and a single test function. Her conditions became the standard tool for queueing control and are the basis of Chapter 7 of her book Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999).
Timeline:
A Markov decision chain has states ; in state a finite nonempty set of actions; a cost ; and transition probabilities . A policy may depend on the whole history and may randomize; a stationary policy chooses in state . For , is the expected total -discounted cost from and , possibly infinite. The average cost of is
A stationary policy is average cost optimal if there is a finite constant with for every policy and every state .
The queue with variable service rates (Example 2). Time is slotted; is the probability of arrivals in a slot, independently across slots. The state is the number of customers at the beginning of a slot. When the queue is nonempty the server chooses one of finitely many decision variables and serves at rate , so that the customer in service leaves during the slot with probability ; there is no decision in state . From state the next state is with probability (), and from it is with probability . The cost structure: ; a polynomial of degree , nonnegative and increasing on ; and for . The arrival moments are and .
If , then
and
with the optimal average cost, , and bounded below.
Proposition 8 states that a queue in which at least one service rate exceeds the mean arrival rate has an average cost optimal stationary policy for holding costs of any polynomial growth, as long as the matching moment of the arrival distribution is finite. Bounded-cost results do not cover this case, which is the one used in practice. The general Theorem behind it is the standard vanishing discount theorem for countable-state models with unbounded costs; the Markov chain test of Propositions 4–5 and the Corollary reduces its hypotheses to a drift inequality for one policy.
All results of the paper are proved on paper. None is formalized: the platform has Sennott's discounted theory (Propositions 1–3, proved) and, as open statements, the book version of the Theorem (SennottDP.SEN.thm_7_2_3_sen_acoi), its existence part in a compact-action model (ArapostathisAC.SennottACOI.theorem_5_9), and the first half of Lemma A1 (SennottDP.SEN.lemma_7_2_1_acoi_bound). This mission states the paper's own version, with all conclusions of the Theorem, and its application to a concrete queue, which no platform item states.
The obvious route takes a limit of along a sequence and passes to the limit in the discount optimality equation. With unbounded costs and unbounded the sum is an infinite series of terms that need not converge uniformly, so the limit of the sums is not the sum of the limits. Only an inequality survives (Fatou's lemma, which needs the lower bound of Assumption 2), and the equation needs the integrable upper bound of Assumption 3*. For the queue, the hypotheses are not visible from the model: they come from a monotonicity property of and a Lyapunov drift computation whose leading term, , has to dominate a cost polynomial of the same degree.
The model is the published Markov decision chain of Sennott (1999), SennottDP.Discounted.MDC ℕ Act, with its policies, discounted costs and value functions, and the published average cost SennottDP.SEN.avgCost; Markov chains, steady state probabilities and first passage costs are the published SennottDP.MarkovCost objects. Conventions:
The second half of the goal is not "there exist and satisfying (6)": a pair solving (6) alone carries no optimality content, so the goal ties to the optimal average cost and and requires bounded below. The Theorem's milestones are stated for every limit point given by the Lemma, not for some stationary policy. The hypotheses of the goal are satisfiable (two-point arrivals , , one rate , , ), so the goal is not vacuous.
A complete development needs a discrete Tauberian inequality (already proved on the platform), Fatou's lemma for series, a compactness argument on , first passage identities and a Foster–Lyapunov criterion for positive recurrence. The Markov chain criteria (Proposition 4, the Corollary) and the Theorem are reusable for every countable-state queueing control model. Proofs of any milestone, and alternative arguments, are welcome.
Periodic-review inventory systems with lost sales and a positive replenishment lead time are a basic model of retail and spare-parts operations: demand that cannot be met from stock is lost, and an order placed today arrives periods later. Even with a known demand distribution the optimal policy depends on the whole vector of outstanding orders and is intractable for long lead times, so practice and theory fall back on base-stock (order-up-to) policies, which are asymptotically optimal as the lost-sales penalty grows relative to the holding cost (Huh, Janakiraman, Muckstadt and Rusmevichientong, Management Science 2009).
Computing the best base-stock level still requires the demand distribution. In many settings the distribution is unknown and, worse, demand is censored: the manager records sales, , and never sees the demand lost to a stockout. The paper behind this mission, Huh, Janakiraman, Muckstadt and Rusmevichientong, An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand (working paper of February 8, 2007; published in Mathematics of Operations Research 2009, DOI 10.1287/moor.1080.0367), gives an algorithm that learns the optimal base-stock level from sales data alone and bounds its regret against the best base-stock policy. It extended the zero-lead-time adaptive newsvendor analyses (e.g. Huh and Rusmevichientong, Math. Oper. Res. 2009) to positive lead times, where the inventory process is a Markov chain on .
Demands are i.i.d. copies of a nonnegative, continuous random variable with and distribution function . The inventory vector in period is
the outstanding orders and the on-hand inventory ; its inventory position is . Under the order-up-to- policy the manager orders , demand is realized, and
A period with on-hand inventory costs, in expectation, , with holding cost and lost-sales penalty . The long-run average cost of level is
and denotes a level minimizing it over . Write .
The algorithm runs in cycles of length ; . Cycle uses a fixed level . From sales data it computes a sample-path derivative by a recursion over the last periods, forms a gradient estimate from the last period of the cycle, and sets with . The inventory is carried over between cycles. The regret after cycles is
Under Assumption 1 ( and ) and infinite support of , for and , with and ,
with . At this is .
Lemma 5 (tail of ), Lemma 6 (the inventory position falls to ), Theorem 7 (existence, independence of the start, convexity and differentiability of , and existence of with ), Theorem 11 (projected stochastic gradient descent with biased gradients), Lemmas 12 and 13 (sums over cycles of length ), Lemma 14 (the regret from ) and Lemma 15 (the transient regret ).
The theorem gives a nonparametric, sales-only policy whose average cost approaches that of the best base-stock policy at an explicit polynomial rate, uniformly over demand distributions satisfying Assumption 1. Its ingredients are reusable: an explicit geometric ergodicity rate for the lost-sales base-stock chain, convexity of the long-run base-stock cost in , and a regret bound for projected gradient descent whose gradients are biased by Markov dependence.
The result is published; to our knowledge none of it has been machine-checked. The mission formalizes the regret bound, which requires Markov-chain ergodicity on a continuous state space, long-run averages, and stochastic approximation with biased gradients. It also repairs the printed constants: Theorem 10 and Lemma 15 are false as printed (see Formalization scope), and the formal statements make the dependence on explicit.
The obvious route treats the cycle's last-period derivative as an unbiased gradient of and applies standard online convex optimization. That fails: the estimate is computed from a Markov chain started at whatever state the previous cycle left, so it is biased, and the bias decays only as the chain mixes. Controlling the bias requires an explicit mixing rate for a chain on whose state includes the derivative process, uniformly over the levels in and over starting positions above . The ergodicity argument uses a coalescing demand pattern, which exists only when ; without that condition the chain need not be ergodic. A second obstacle is that the objective is defined as a long-run average, so its convexity and differentiability in must be established before any gradient argument applies.
Everything is stated in Lean 4 with Mathlib. The inventory vector is a pair (pipeline Fin (τ-1) → ℝ, newest order first; on-hand ℝ). Lean periods are -based (Lean period is the paper's ); cycles are numbered from . Demand is a sequence on a probability space that is i.i.d., nonnegative, integrable, with and an atomless law; infinite support is for all ; , . The long-run cost is a limsup of Cesàro averages from the empty start (Theorem 7 shows it is a limit from every start), and is any minimizer over . The algorithm is a deterministic function of the demand path; the sample derivative is the recursion the algorithm computes, not a derivative. Integrability of every expectation follows from boundedness of the inventory and is not assumed.
Corrections, all disclosed in the items: Theorem 10 carries instead of on the term, because the printed bound fails for , , , where the right side is and . Lemma 15 carries and . Lemma 14 keeps its printed constant; its proof appears to use the ergodicity theorem one period early. Theorem 11 is stated on an interval with the bias taken conditionally on the history. Lemmas 5 and 6 are stated for infinite support only.
A goal that bounds the regret by alone (costs at the steady state of ), or that lets the levels be any sequence in , is not the theorem: the regret here uses the realized inventory of the algorithm. Lean's conventions and of a nonpositive number cannot trivialize the bound, because infinite support and give . The source is the authors' working paper of February 8, 2007, whose printed page numbers equal the PDF's.
Not yet stated: Theorem 3 and Lemma 4 (ergodicity rate), Theorem 8 and Lemma 9 (bias bounds), Theorem 1 (sample derivatives). They need the joint chain and are welcome as contributions, as are the general pieces: geometric ergodicity via coalescence, and the biased projected-gradient bound.
A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.
The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.
Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).
At round , the outcome is for wet and for dry. The forecaster selects a probability from the finite grid , where is a positive integer. A forecast is represented by the binary probability vector ; the second coordinate is the forecast chance of rain. The forecaster chooses with probability . The Brier loss of that possible forecast is .
After rounds, counts the realized forecasts equal to , and is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is
A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score , in which the realized indicator that was chosen is replaced by its conditional probability . Its weighted count is , and its weighted wet frequency is when the denominator is positive.
For grid points and , the pairwise regret is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing by on rounds weighted by . The algorithm chooses its next distribution so that the regret flow out of each equals the flow into :
These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.
The target is Theorem 1: for every , choose and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies
The time after which the inequality holds may depend on the forecaster, Nature, and . The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.
The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on . Theorem 3's last constant is written as and the corollary's horizon as ; the printed constants are inconsistent with the paper's grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.
The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.
The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.
The weighted score is controlled by quantities known from the chosen mixtures, while depends on the actual random draws. A direct deterministic bound on therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.
The Lean model uses binary outcomes, grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index : the paper's in round is the regret over the preceding indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.
The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map is injective for . The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing by would change the claim.
Every theorem requiring the grid has the explicit condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency ; nonnegative weights make its numerator zero as well. At horizon , the weighted calibration score is . The probability event is measured with the history law's outer measure in . Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.
Retailers of seasonal goods, home builders selling out a development, and airlines and cruise lines selling promotional fares all face the same operational question: inventory is fixed, the selling season is finite, and the price can be changed only rarely. Menu costs, advertising commitments and customer goodwill often restrict a seller to a single price change. The question is then when to change the price, and, if both a lower and a higher price are available, in which direction.
Feng and Gallego (Management Science 41(8), 1995) answered this for Poisson demand. Their §4 treats a single markdown (Theorem 1) and a single markup (Theorem 2). This mission formalizes their §5, the markup-or-markdown problem: the seller starts at a middle price and has one opportunity to move either down or up. The paper shows that the optimal policy is again described by time thresholds that depend only on the remaining stock, now two per stock level. The paper builds on the deterministic and fluid analysis of Gallego and van Ryzin (1994), where arbitrarily many price changes are allowed, and is the starting point of a literature on limited-price-change revenue management surveyed by Bitran and Caldentey (2003).
There are three prices . At price demand is a Poisson process of intensity , and at of intensity , with
all prices and intensities positive. Lowering the price raises both the sales rate and the revenue rate. Salvage value is zero. Note that in this section is the lower price; the initial price is .
A seller with units and time-to-go sells at and may switch once, to or to . Write for the demand process at and for that at .
where is the set of stopping times of the history of with and almost surely.
Under the paper's assumption for every , there are strictly increasing sequences , with
such that , where for and otherwise. The excess equals on and on . Each solves
with and . The thresholds are and .
Theorem 3 says that the two-directional problem has the same simple structure as the one-directional ones. With units left and time-to-go , the seller marks down at once when falls below , marks up at once when exceeds , and otherwise keeps the price. Because the thresholds increase with the stock, the policy reduces to a table of numbers, which the paper computes for a housing example (Table 5). The theorem also quantifies the value of flexibility: in that example, allowing either direction adds about $1,500 over the markdown-only policy and about $7,000 over the markup-only policy.
Lemma 3 and the verification Lemma 1 are reusable beyond this mission. Lemma 3 is a sign-change property of differences of Poisson tail sums, of the kind that drives threshold results in revenue management. Lemma 1 is a sufficient condition for the value of an optimal stopping problem driven by a Poisson process. The paper's results are proved with pen and paper only; none of them has a machine-checked proof. The formalization adds a precise statement of Lemma 1, whose printed hypotheses are insufficient (see the scope section), and an explicit record of which threshold facts Theorem 3 depends on.
The value is the supremum over stopping times of a continuous-time process, and the obvious approach, dynamic programming over the stock, needs the value one stock level down. The thresholds at stock are defined through , so the structure must be propagated from one stock level to the next, and several properties have to propagate together. One must know that again has a single sign change, which requires to be increasing beyond . One must also know that is positive up to and eventually negative, so that is finite, and that . These facts concern three different price pairs at once: , and . A direct comparison of with the two one-directional value functions fails, because the optimal direction itself depends on the stock and the time-to-go. The verification step needs a pathwise fundamental theorem of calculus for the Poisson-driven process, which is where the regularity hypothesis on matters.
QueueingFundamentals_Foundations_ArrivalProcess. The rate enters through the hypothesis IsExpInterarrivals P lam T, and enters only through its law: the sum is written through its Poisson law. is the class of real-valued stopping times of the σ-algebras generated by the counts , , with and almost surely.HasDerivAt. Threshold sequences are indexed from . Every infimum is a real sInf paired with the nonemptiness of its set. , , , and the thresholds are existentially quantified and tied together by the theorem's equations, so the existential determines the paper's objects. The page's assumption is a hypothesis of the goal, as on the page.An airline may offer a low promotional fare while seats remain available, then raise the fare as departure approaches. The choice is dynamic: a sale changes both the number of seats left and the benefit of waiting. The same decision appears for hotel rooms and theater seats. Feng and Gallego study a policy with two fixed prices and at most one price change, while allowing the switching time to depend on actual sales rather than a calendar date chosen in advance. Their 1995 paper proves that this adaptive problem has an inventory-dependent threshold rule. This mission isolates the markup case, in which the second price is higher than the first.
The two-price restriction has a practical role. A seller may know the fare classes it can offer while still needing to decide when to close the promotional class. The result identifies a sequence of time thresholds that can be computed for the chosen price pair. It is therefore a structural claim about an optimal policy, not a choice of numerical prices or a claim that two prices optimize over every possible price menu.
There are items and units of time-to-go. At price , sales requests follow a Poisson counting process with rate . Each request sells one item while stock remains. The paper assumes that demand falls as price rises and that the lower price has the higher revenue rate. Thus the markup case has
The salvage value at the end of the horizon is zero. A fixed switch at time charges first and afterwards. Its expected revenue, denoted , is
The two counts in the last term are independent, so their sum has Poisson mean . This is the expression in §3 of the paper. In particular, is the revenue from increasing the price immediately.
An admissible switching time uses only the history of sales at ; it lies between zero and and cannot wait past stock exhaustion. The optimal value is the supremum of expected revenue over these stopping times. The stopping decision may react to sales before the change, but it cannot anticipate future requests. This distinction matters because a deterministic switch time generally has less information than an adaptive one.
The goal is Theorem 2 on pp. 1382–1383. Define the switching function
There are thresholds with , and is increasing. A continuation premium gives the value
For , below and is zero at or above it; . The function satisfies and the differential equation , where . The remaining thresholds are the first nonnegative zero of and the first positive zero of :
The milestones reproduce equation (17), the markup half of Lemma 2, and Lemma 1. Together they identify the Poisson derivative identity, the sign change of , and the verification criterion used to relate a candidate value to optimal stopping. The paper proves the mathematical result; the mission asks for machine-checked proofs of these formal statements.
The threshold sequence tells a seller when increasing the price immediately is optimal, conditional on the stock still available. The value formula also gives the benefit of continuing at the promotional price when time-to-go lies below the threshold. The statement preserves the paper's weaker word “increasing” for : it asserts monotonicity and does not require strict monotonicity of either sequence. The full theorem includes the recursive equations for and , so a proof of a threshold-shaped region alone would leave part of the source result unformalized.
Formalization would add a reusable optimal-stopping model built from a Poisson arrival process, a fixed-switch revenue function, and a verification lemma. The arrival process already has a published definition; the switching model and the theorem statements here are new drafts. The theorem is established in the 1995 article, while its Lean proof remains to be supplied.
The immediate-switch comparison has a single sign change, but the optimal decision also depends on revenue already earned and on the value of unsold stock after each possible sale. For , the relevant forcing term is , so the sign of alone does not locate the optimal switching threshold. A direct fixed-time comparison likewise does not establish optimality among stopping times that react to observed sales. These are the main obstacles the formal proof must address.
The Lean model uses natural-number stock, nonnegative real time, positive real prices and rates, and an imported counting process built from independent exponential interarrival times. A rate is attached to each price. The history of the first process defines the stopping-time class; the second process enters through its Poisson law after a switch. The supremum ranges over admissible stopping times, and the payoff is bounded and measurable under the stated process law. The definition writes sales before switching as , equal almost surely to for admissible times. The probability-measure assumption is explicit, though the exponential interarrival law entails it.
Lean assigns a default value to an empty real infimum. The theorem explicitly asserts that each defining zero set for , , and is nonempty; it also keeps in the definition of , since . Continuity of at zero connects its boundary value to its differential equation. Lemma 1 includes its missing initial, zero-stock, obstacle, and local-Lipschitz assumptions, all required by its printed proof. The paper's word “bounded” in Lemma 2 is retained in the milestone quotation but replaced by the positive lower bound it uses; is unbounded as stock grows. These choices are recorded for review in the moderation notes.
The goal derives optimality from the demand and price assumptions. It does not assume the verification conditions, the sign change, or the revenue identity as premises. Contributions to the Poisson tail calculus, stopping-time measurability and boundedness, threshold zero sets, and verification argument are within scope and can be reused in related finite-inventory pricing models.
Given a reference probability distribution and a set of probability distributions, the minimum discrimination information problem asks for the member of closest to in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations , and the classical answer is that the minimizer is an exponential family member, with density with respect to .
That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the .
Timeline:
All distributions (PD's) live on one measurable space . The I-divergence of from is
where is the density of with respect to ; it takes values in and vanishes only for . The variation distance is for any PD dominating both. If is a convex set of PD's containing some with , a with
is the I-projection of on .
Fix real-valued measurable functions on . For (Euclidean -space) the moment set is the set of PD's with , . Further:
If is open in , then for every point of the interior of the I-projection of on exists and
for some constant and some .
Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.
The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).
The obvious argument fails at the first step: the moment set is convex but not closed in variation when the are unbounded, since is not continuous in variation. A minimizing sequence therefore converges in variation to some (as in Theorem 2.1), but nothing places in : mass can escape to where is large. Ruling this out needs quantitative control of , which in turn requires knowing the form of before knowing is feasible; the interplay with the convexity of and the openness of is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.
Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions , , .Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. is allowed.sInf over a possibly empty set.A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) ), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.