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.
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?
Online learning and stochastic learning ask different questions. An online learner faces an arbitrary sequence of loss functions and is judged by its regret: the excess of its cumulative loss over that of the best fixed hypothesis in hindsight. A stochastic learner receives independent samples from an unknown distribution and is judged by the risk of a single hypothesis it outputs. Regret bounds hold without any probabilistic assumption, so they are strong guarantees; risk bounds are what statistical learning and stochastic optimization actually need.
The online-to-batch conversion connects the two: run any online learner on losses built from i.i.d. samples and output either the average of its predictions or one prediction chosen at random. The expected excess risk of the output is then at most the expected regret divided by the number of rounds. A general form of the conversion is due to Cesa-Bianchi, Conconi and Gentile (IEEE Trans. Inf. Theory 2004). Shalev-Shwartz's survey (Found. Trends Mach. Learn. 2011) states it in expectation, in Vapnik's general setting of learning, as Theorem 5.1 and Corollary 5.2 (§5, pp. 186–189). Every stochastic-gradient analysis that goes "regret bound, then online-to-batch" rests on this statement.
Fix a dimension and a hypothesis class . Examples range over a measurable space and are drawn from a probability distribution on , which the learner does not know. A cost measures how badly hypothesis does on example , and the risk of is
This is Vapnik's general setting of learning (Definition 5.1); supervised classification, regression and stochastic convex optimization are special cases.
The conversion draws independently from and runs an online learner on the losses . Its prediction in round , , may depend only on . The output is either the average or the randomized choice , with uniform on the rounds and independent of the sample.
For every comparator , under the conditions of Theorem 5.1,
for the randomized output, and for the averaged output when and are convex. The right side is the expected regret divided by . The statement contains no constant: it is an exact reduction, valid for every online learner.
Corollary 5.2 makes every regret bound a risk bound. Combined with the regret of online gradient descent or online mirror descent, it gives the excess-risk rate of stochastic gradient methods for convex Lipschitz problems; combined with logarithmic regret for strongly convex losses, it gives rates. The survey's own "Stochastic Online Mirror Descent" box (p. 189) is exactly this composition.
The result is proved in the paper. What this mission adds is a machine-checked version in a measure-theoretic model with honest non-anticipation and a genuine model of the randomized output. The platform has a related statement, Mohri, Rostamizadeh and Talwalkar's Theorem 8.15 (FoundationsML.OnlineLearning.online_to_batch_conversion), which is a high-probability bound for bounded convex losses in supervised learning; it is a different statement and neither implies the other. The expectation form here is the one stochastic-optimization arguments use.
The result is short on paper; the formal content is the conditional-expectation step. The prediction is a random variable built from , while is a fresh draw, so must be computed by integrating out first, which means a Fubini–Tonelli argument on a product of copies of split into the past, the present and the future of round . The first idea, that has the same law as for a fixed , is wrong: is random. The identity also fails as soon as may look at (take a minimizer of ), so the argument must use the information structure, not only the marginal laws. The averaging part additionally needs Jensen's inequality for and the measurability of as a function of the hypothesis.
EuclideanSpace ℝ (Fin d) with a set, because averaging needs a vector space. Rounds are numbered , and .ψ : Fin T → Ψ under Measure.pi (fun _ => Q), with Q a probability measure: independent draws from .A t : (Fin t → Ψ) → ℝ^d of measurable maps with values in , so non-anticipation holds by typing: . The learner may read the examples, not only the losses; this class contains the paper's learners, so the statements are at least as strong.Fin T. The expectation over is not replaced by the average over rounds (that replacement is the first line of the proof).Infrastructure needed: Tonelli/Fubini on finite products split at a coordinate (Mathlib's Measure.pi), measurability of parametric integrals, and Jensen's inequality for a convex function of a finite average. The round- identity is reusable for any non-anticipating stochastic process; contributions of proofs of any milestone are welcome.
A monotone disjunction over Boolean variables is a rule of the form . Learning such a rule online — predicting the label of each example before it is revealed and paying one unit per wrong prediction — is the basic test case for learning when only a few of many features matter. Littlestone's Winnow algorithm (Littlestone 1988) learns a -literal disjunction with mistakes, while additive algorithms such as the Perceptron need a number of mistakes that grows linearly in on the same problem. Kivinen and Warmuth (1997) placed this gap inside a general theory of multiplicative versus additive updates. Shalev-Shwartz's survey (2011) derives Winnow as a special case of Online Mirror Descent with an unnormalized entropy regularizer, and obtains its mistake bound from a general local-norm regret bound. This mission formalizes that derivation.
Throughout, labels are and instances are . For with , the hypothesis is the disjunction of the variables with . A weight vector errs on when .
Winnow with parameter starts from . On round it receives , predicts , and receives . If it sets for every ; otherwise . The set collects the rounds on which it errs. On those rounds the surrogate loss is the hinge loss , and on all other rounds.
Unnormalized Exponentiated Gradient with parameters , run on linear losses , keeps , where . Winnow is this algorithm with and on , otherwise.
Online Mirror Descent (OMD) with link function predicts . Its analysis uses the Fenchel conjugate of a regularizer on a set , and the Bregman divergence .
For , and every with ,
and if for all , the run with satisfies
with equality at a minimizer of . 2. Theorem 2.23: if for all , then for all
together with its specialization to . 3. (3.3): for Winnow. 4. (3.4): for every round.
The theorem gives a mistake bound for learning sparse disjunctions that is logarithmic in the number of irrelevant features, against the of the Perceptron run on the same surrogate (p. 173). The first inequality also covers non-separable data: the bound degrades by , the total hinge violation of the best disjunction. The milestones are general and carry weight beyond Winnow. Lemma 2.20 is the standard duality form of the OMD regret bound. Theorem 2.23 is a local-norm bound that also allows negative losses down to .
All four results are proved on paper. To our knowledge none has a machine-checked proof, in Lean or elsewhere. This mission produces such proofs for the survey's own route: OMD duality, then unnormalized EG, then Winnow.
The obvious route bounds Winnow directly with a potential function, but the survey's statement sits at the end of a chain. The chain needs Fenchel–Young with an attained supremum, a telescoping identity for the conjugate, and the inequality for . It also needs a reduction in which the surrogate losses depend on the algorithm's own error set . Since is defined after the run, the subgradient inequality must be argued for exactly these losses. The bound uses that is Boolean and that ; for fractional or for it fails. Solving (3.3) and (3.4) for needs .
Vectors are Fin d → ℝ with explicit sums ; Lemma 2.20 is stated in an arbitrary real Hilbert space. Rounds are numbered in place of . Instances, labels and comparators carry the hypotheses , , , . is the natural logarithm, and through Real.log 0 = 0.
Erratum corrected. The Winnow box on p. 173 prints the update , and the proof on p. 174 uses . With that sign the algorithm demotes on a false negative, and Theorem 3.10 is false. Take , , , , and , on every round. The margin condition holds, and errs on round 1. The printed update only shrinks , so every round is an error, and exceeds . On an error round the hinge surrogate has gradient at . The mission therefore formalizes the update (Littlestone's Winnow) and on . With this update the run above errs once. The milestone texts are quoted verbatim, with the printed sign.
Implicit hypotheses made explicit.
Conventions.
The bounds carry no and no constant is instantiated. A trivializing formalization is ruled out: is the run's own surrogate, not a free function, and the conjunct quantifies over the weights.
Infrastructure needed: conjugates and the Fenchel–Young inequality on a subtype, telescoping sums, elementary exponential inequalities, and the case analysis on -valued data. Lemma 2.20 and Theorem 2.23 are reusable for other OMD and EG analyses. Lemma 2.20 is also stated in the companion mission on normalized EG. Proofs of any milestone, and alternative routes to the goal, are welcome. Excluded: the Perceptron comparison (p. 173), and Theorem 3.9 (Perceptron), which is already proved on the platform.
Many optimization problems in shape analysis, computer vision, numerical linear algebra and statistics have a nonlinear search space: a sphere, a Stiefel or Grassmann manifold, a space of curves modulo reparametrization. Projecting iterates of a Euclidean method back onto the constraint set loses the geometry, so one designs methods that move along the manifold itself. Riemannian line-search methods do this by replacing the update with for a retraction , and by carrying old search directions to the new tangent space with a transport.
Nonlinear conjugate gradient (NCG) methods are a natural candidate on manifolds: they need only first derivatives and store one previous direction. In the Euclidean case, Al-Baali showed in 1985 that the Fletcher–Reeves method with strong Wolfe step lengths and satisfies (doi:10.1093/imanum/5.1.121); Nocedal and Wright give the standard textbook proof (Lemma 5.6 and Theorem 5.7 in Numerical Optimization). Ring and Wirth (doi:10.1137/11082885X, SIAM J. Optim. 2012) transfer this analysis to Riemannian manifolds, possibly infinite-dimensional, which is the setting of their application to shape spaces. The mission formalizes that transfer.
is a smooth manifold modelled on a real Hilbert space , with a Riemannian metric on each tangent space and norm . For , is its differential, a continuous linear functional on with dual norm , and the gradient is its Riesz representative, .
A retraction is a family of smooth maps with and . Its transport is .
A run of Algorithm 1 consists of points , directions and steps with . With , the Wolfe conditions at are
and the strong Wolfe conditions replace (1b) by
The angle between and is given by .
The Fletcher–Reeves direction is
For a non-terminating Fletcher–Reeves run with strong Wolfe steps and , if the transport is non-expansive on the search directions, , is bounded below, and the pull-backs are Lipschitz continuously differentiable on with a uniform constant, then
Proposition 15 guarantees that Riemannian Fletcher–Reeves, with any retraction whose transport does not enlarge the search direction, cannot stall at a positive gradient level: some subsequence of the gradient norms tends to zero. Together with strict convexity in the sense of the paper's Proposition 4 this gives convergence of the iterates to the minimizer, and it justifies the use of the method on the shape spaces of the paper's §4. The hypothesis on the transport is the only new ingredient compared with the Euclidean theorem, and the paper's Remark 7 notes that convergence can no longer be guaranteed without it.
The result is proved in the paper. As far as is known, neither Zoutendijk's theorem on a manifold nor the Fletcher–Reeves convergence theorem has a machine-checked proof; Euclidean versions of both appear elsewhere on the platform, but the Riemannian statements, with retraction, transport and tangent-space-dependent norms, are new. The mission produces the line-search interface on a Riemannian manifold (retraction, transport, Wolfe conditions) in a form reusable by other Riemannian methods.
Each search direction is built from a vector in a different tangent space. The transported direction lives in , and only the step equation identifies it with a vector of ; norms, inner products and differentials all depend on the base point, so every Euclidean manipulation has to be carried through that identification. Zoutendijk's theorem has to connect two different descriptions of the same step: the curvature condition (1b) is stated with the differential of at the new point applied to the transported direction, while the Lipschitz hypothesis concerns the one-variable pull-back . They agree only because the transport is the derivative of the retraction, and the agreement is a chain rule for manifold derivatives, which has to be established in Mathlib's mfderiv framework for maps out of a tangent space. The growth bound cannot use ; it needs the non-expansiveness hypothesis exactly where the Euclidean argument uses the identity.
The manifold is a Mathlib manifold modelled on a real Hilbert space E, with Mathlib's RiemannianBundle on its tangent spaces; tangent-space norms and inner products are the Riemannian ones and is mfderiv. Geodesic completeness, separability, the distance and the Levi-Civita connection, standing assumptions of the paper, are not used by any statement and are dropped. The gradient is given as a field with its Riesz property. One retraction family is used for every step (the paper allows a different retraction at each step), the steps are positive, and indices start at .
The following readings are explicit:
Summable.The transport in the conclusion and in the Fletcher–Reeves update is the derivative of the retraction, not an arbitrary linear map; with an arbitrary map, condition (1b) would no longer be a statement about the pull-back , and Zoutendijk's theorem would fail. A run predicate that no sequence satisfies would make the goal vacuous; the one-dimensional run , , , , , satisfies every hypothesis.
The paper's other main result, R-linear convergence of Riemannian BFGS (Proposition 10), is a separate mission, and its superlinear-rate results (Propositions 5, 7, 8, 12, Corollary 13), which require parallel transport and the exponential map, are out of scope. Contributions welcome: proofs of the chain rule identities for retractions (reusable for any Riemannian line search), of Zoutendijk's theorem, and of the milestones in order.
A directed polymer in a random environment is a random up-right lattice path whose law is reweighted by random site weights. Its free energy, the logarithm of the partition function, is believed to belong to the Kardar–Parisi–Zhang (KPZ) universality class: for a path of length of order , the free energy fluctuates on the scale and the path wanders on the scale . For zero-temperature analogues (last-passage percolation with exponential or geometric weights) these exponents were established through exact formulas from random matrix theory (Johansson 2000) and later through a probabilistic coupling argument based on the Burke property of queues (Balázs–Cator–Seppäläinen 2006).
For directed polymers at positive temperature no model with the KPZ exponents was known until Seppäläinen (arXiv:0911.2446, Ann. Probab. 2012) introduced the log-gamma polymer, whose weights are reciprocals of gamma variables, and proved that its free energy has variance of order in the characteristic direction. The model has since become a basic exactly solvable polymer:
The present mission formalizes the 2009 variance theorem, which needs neither of the later exact formulas.
Sites are and . A weight configuration assigns a positive number to each site. On the axes, and for are the boundary weights, and , , are the bulk weights.
An up-right path from to is a sequence whose steps are or . The partition function is
the weight of the origin excluded, . The quenched polymer measure gives the path probability , and the annealed measure is its average over the environment. The exit points and are the numbers of initial steps the path takes along the -axis and along the -axis.
Assumption (2.4). Fix . The weights are independent with
Let and be the digamma and trigamma functions. The characteristic direction is . For a real scaling parameter and a constant , the endpoint satisfies
There are constants and , depending on , such that under (2.4) and (2.6)
The upper bound runs through the Burke property and the variance identity:
The lower bound runs through partition-function comparisons:
The result. Theorem 2.1 was the first proof of the KPZ fluctuation exponent for a directed polymer at positive temperature. Its upper bound also yields a strong law of large numbers for (2.7) and, with Theorem 3.3, a central limit theorem off the characteristic direction (Corollary 2.2). The exit-point estimates of Sections 4 and 5 give the path fluctuation exponent (Theorem 2.3) and are reused for the polymer without boundaries and the point-to-line polymer (Theorems 2.4–2.6).
Formalizing it. The theorem has been proved since 2009; no formal proof of it in a proof assistant is known. A formalization checks a proof with many interacting estimates and two corrected slips (below). The definitions made here (the lattice-path partition function, the inverse-gamma environment, the recursion (3.2), exit points, quenched and annealed measures) are the base for later missions on Theorems 2.3–2.7 of the same paper. Lemma 3.2 contains a gamma-distribution characterization (Lukacs' theorem) of independent interest.
The obvious route to a variance bound, a martingale decomposition of over the independent weights, gives only , i.e. order ; it cannot see the cancellation that produces . The order is specific to the characteristic direction: off it, satisfies a central limit theorem with variance of larger order (Corollary 2.2), so any argument must use the exact relation between the boundary parameters and the endpoint . The upper bound requires controlling the annealed exit point at the scale , with tail estimates whose constants are uniform in the parameters. The lower bound is a separate statement: the path must not exit an axis at distance from the origin with non-vanishing probability, which no upper-bound estimate implies.
Source: arXiv:0911.2446v4 (26 Aug 2015, revised version); its printed page numbers equal the PDF's. All declarations are in the namespace LogGammaPolymer.Variance.
ℕ × ℕ; a path is a step sequence with a fixed number of east steps; is a finite sum over these paths with the starting weight excluded. The environment Env θ μ P bundles one weight family Y : ℕ × ℕ → Ω → ℝ, measurability, mutual independence of every weight off the origin, and the three laws as images under equal to Mathlib's gammaMeasure (shape, rate ). Positivity of the weights is not assumed pointwise in the probabilistic statements; it holds almost surely. The deterministic lemmas (3.1, 5.1, 5.4) are stated for every weight function positive off the origin.variance, and every upper bound or identity also asserts (or integrability of the averaged quantity), so that the junk value of variance and of the Bochner integral cannot satisfy it.Type), the environment, and . Upper limits in are stated as "for every there is with the bound for ". The compact-set uniformity of Lemmas 4.1, 4.3 and (4.32) is formalized. The remark after Theorem 2.1 on uniform constants is not.A formalization in which includes the origin's weight, the laws are not exactly the inverse gammas with shapes and rate , independence is dropped, is allowed, or the constants depend on the environment or on does not state Theorem 2.1.
Needed infrastructure: gamma–beta algebra and a Lukacs-type characterization, independence of finite families built by the recursion (3.2), differentiation of expectations in the shape parameter, and moment bounds for sums of i.i.d. variables. All of these are reusable beyond this mission. Proofs of any milestone, and of supporting lemmas such as (3.3)–(3.4), are welcome.
City logistics often moves goods in two stages: large trucks bring freight from a central depot to a few intermediate satellites, and small vehicles distribute it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) is the basic optimization model of such systems; it contains the capacitated location-routing problem as a special case. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) gave an exact method that solved benchmark instances out of reach for earlier algorithms.
Their method does not attack the whole problem at once. It enumerates configurations, sets of first-level (depot–satellite) routes, discards most of them with cheap tests, and solves a second-level problem only for the survivors. The correctness of the method rests on two facts stated in §5 of the paper: the problem decomposes exactly over configurations (Eq. (26)), and the pruning tests of Propositions 1 and 2 never discard the configuration of a solution better than the incumbent. This mission formalizes those facts.
An instance has a depot , satellites and customers , a symmetric cost on the edges (with the fixed vehicle costs folded in), positive integer demands with total , first-level vehicles of capacity , second-level vehicles of capacity at satellite with a global limit , satellite capacities and handling costs .
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the length of the closed walk. A second-level route leaves satellite , visits a set of customers of total demand and returns; its cost is the walk length plus . Formulation chooses binary , and integer deliveries minimizing subject to: each customer on exactly one used second-level route; at most used routes at and in total; load at at most ; at most first-level routes; the deliveries to equal the load leaving ; each used first-level route carries at most . Its optimal value is , when infeasible.
The set of configurations is
For , , and . Problem is with the first-level routes fixed to : second-level routes only at satellites of , real deliveries for , and . Its value is when infeasible.
The bounds of §5.1 use multipliers , , and marginal costs satisfying the penalty system (12), for every route of satellite :
Let be a real number and a feasible solution of of cost less than , with configuration . Then and
Eq. (26) is what makes the method exact: once every configuration that can carry a solution better than the incumbent is examined, the best is the optimum. Propositions 1 and 2 are what make it fast: they remove configurations from before any second-level problem is solved. If a pruning test discarded the configuration of a cheaper solution, the method would return a suboptimal value and still report it as optimal; the formal statements rule this out for every instance, not just the benchmark ones. The capacity constraints (33) play the same role inside : a cut that removed a feasible solution would make the bound invalid.
The paper's proofs are in an electronic companion; none of these statements has been machine-checked before, and none is on the platform. The formalization also records exactly what the tests need: positive demands, integral vehicle counts, and the sign conditions on the multipliers, and nothing about the optimality of the incumbent.
Most statements are elementary counting and Lagrangean weak-duality arguments over finite index sets. The work lies in the bookkeeping between two formulations with different index sets: sums over all satellites, only over , and a solution of one must be turned into a solution of the other. One step is not elementary: has integer deliveries and real ones, so the inequality in (26) needs an integral delivery plan from a fractional one. That is an integrality property of a bipartite transportation problem (routes to satellites, integral capacities and demands), which no counting argument gives.
Satellites and customers are Fin ns and Fin nc, 0-based. The route families and are arbitrary finite families of elementary routes with costs computed along the closed walk; the paper uses all such routes, so every statement here is a generalization. Demands are positive integers; the triangle inequality is not assumed. Binary variables are Bool; optimal values are infima in EReal, with ⊤ for an infeasible problem. A configuration is a Finset of route indices. The penalties are any , , and satisfying (12), not only those producing the paper's bound LD1. Ceilings of and are natural-number ceilings of rationals; those in Proposition 2 are integer ceilings of reals.
The goal departs from the printed proposition in three disclosed ways. Only necessity is stated: the "if" direction is false, because (b)–(e) ignore the satellite capacities . Condition (a), , is omitted: it holds for some optimal solution, not every one (its split-delivery analogue is posed, and open, on the platform as SplitDeliveryVRPTW.Known.exists_optimal_split_customers; it is not reused here). "An optimal solution" becomes "a feasible solution of cost below ", the property the paper's own justification uses. Proposition 2 is stated with as a hypothesis; the paper's computation of by problem (27)–(32) is not formalized, because (32) forces positive deliveries that does not require. The goal is not trivialized by an infeasible hypothesis: feasible solutions of exist on small instances, and a toy instance was checked in Lean.
A complete development needs finite-sum manipulations, Lagrangean weak duality for (12), and, for (26), integrality of bipartite transportation polytopes, which is reusable well beyond this mission. Proofs of any milestone, and a general transportation-integrality lemma, are welcome.
Single-leg capacity allocation under customer choice is the basic dynamic problem of revenue management: a firm holds a fixed stock of a perishable resource (seats on a flight leg, rooms on a night), and in every period of a finite selling horizon it decides which products (fare classes) to offer to the arriving customer. Talluri and van Ryzin (Management Science, 2004) showed that under a multinomial logit (MNL) choice model with known parameters, the optimal assortment in every period is revenue-ordered and shrinks as capacity becomes scarcer ("nesting by fare order"), which is what justifies the protection levels and bid prices used in practice.
The MNL parameters are estimated from data and are never known exactly. Rusmevichientong and Topaloglu (Operations Research, 2012) study the robust version, in which an adversary picks the parameters of each period from an uncertainty set after seeing the offered assortment, following the robust Markov decision process framework of Iyengar (Mathematics of Operations Research, 2005). Their Section 4 shows that the structure of the known-parameter problem survives: the value function is concave in capacity, the optimal assortment is a revenue threshold set, and it grows with remaining capacity and, when uncertainty does not shrink, over time. This mission formalizes those results.
There are products with revenues . An MNL parameter vector is ; offered the assortment , a customer buys product with probability
and nothing with probability . The expected revenue is .
Static problem (Section 3). For a compact nonempty uncertainty set ,
and is an optimal assortment of smallest cardinality.
Dynamic problem (Section 4). Periods each bring one customer, whose parameter vector lies in a compact nonempty . A purchase consumes one unit of capacity. The value function , the maximum worst-case revenue from period on with units of capacity, satisfies
for , with and . The marginal value of capacity is , and is a maximizer of the right-hand side of smallest cardinality.
For every and , and, in the second part, every with :
The result. Theorems 4.1–4.3 say that robustness costs nothing structurally: the robust policy is still a nested threshold policy, so it can be implemented with the protection levels or bid-price controls already in use, and it can be computed by examining at most revenue-ordered assortments per state instead of . Theorem 4.3 gives the operational content: with less inventory, offer fewer, higher-revenue products; nearer the end of the season (when the uncertainty sets are nested), offer more.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a checked robust finite-horizon dynamic program over finite action sets with compact adversary sets, the reduction of each Bellman step to a static max–min problem with shifted revenues, and checked concavity and time-monotonicity arguments that are reusable for other single-resource problems. The known-parameter analogues for general regular choice models and for the Markov chain choice model are separate drafts on the platform (RevenueOrdered.Nesting.*, MarkovChainChoice.SingleResource.*); they have no uncertainty set and are not used here.
The obvious route to concavity, an induction on in which is a maximum of concave functions, fails: a maximum of concave functions is not concave, and here each candidate assortment is evaluated by a minimum over , and the worst-case parameter vector changes with the capacity level, so the known-parameter argument cannot be reused term by term. Any induction on also has to handle the boundary , where the Bellman equation does not apply and only is given. Every step involving a minimum must use that the minimum over a compact set is attained, and translating a minimum by a constant must be justified rather than assumed.
Fin n (Lean index is product ). A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 . is the published ChoiceCDLP.MNL.mnlObjective. Minima over uncertainty sets are real infima (sInf), equal to the attained minima under the standing hypotheses; maxima are Finset.sup' over all assortments.V t, , is compact, nonempty and contained in (IsUncertaintySeq); the static results assume the same of V. The paper writes "" in Theorem 3.2 and Corollary 3.5; this is read as , compact.RobustMNL.Dynamic, the companion mission on Section 3 of the same paper, identically up to namespace.Randomized coordinate descent updates one block of variables per iteration, chosen at random. For problems whose dimension makes even one full gradient expensive (the "huge-scale" problems of the title, such as sparse least squares or truss topology design), a coordinate step can cost a tiny fraction of a gradient step. Nesterov's paper (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362) gave the first global complexity bounds for such methods with non-uniform sampling, and it is the reference point for the later literature on randomized block methods (Richtárik and Takáč 2014, Lu and Xiao 2015, Allen-Zhu et al. 2016).
The first results of the paper (Theorem 1, the subject of a companion mission) bound the expected objective value after k iterations. An expected bound does not say what happens in a single run. This mission formalizes the paper's answer to that question in §3: by running the method on a slightly regularized objective, one run returns an ε-solution with any prescribed probability β, after a number of iterations that grows only logarithmically in 1/(1 − β).
The variable space is a product of blocks; a point has blocks , and is the point whose -th block is and whose other blocks vanish. In this mission each block carries a Euclidean norm with (3.4), and the whole space carries
The objective is convex and differentiable, has a minimizer with value , and its partial gradients are Lipschitz along their own block with constants (2.2): . Write .
The method RCDM (2.6) draws, independently at each step, block with probability and replaces by , where is a maximizer of (1.8). The quantity is the expectation of over the first draws.
The level-set radius is , and for the regularized objective is
It has block constants , so RCDM applied to samples block with probability and steps with .
For , , and
the point produced by RCDM on satisfies
Theorem 4 turns an in-expectation guarantee into a single-run guarantee with an explicit, non-asymptotic iteration count. Its dependence on the confidence level is logarithmic, so very high confidence costs little; and the count replaces the largest eigenvalue of the Hessian, which governs the full gradient method, by the trace-type quantity , which for sparse problems makes groups of coordinate steps competitive with one gradient step. Theorem 2 is the linear-rate result for strongly convex objectives that later analyses of randomized block methods take as their starting point.
The results are proved in the paper. None of them is formalized in the block setting. The scalar Euclidean case of Theorem 2 is proved on Prove2Me as ConvexOptAlg.CoordDescent.theorem_6_8 (Bubeck, Theorem 6.8), and the bound (3.2), for a -strongly convex in any norm, is proved as ConvexOptAlg.CoordDescent.lemma_6_9. This mission adds block variables with general norms (Theorem 2), the regularization constants, the gradient-norm bound, and the high-probability statement itself, which has no formalized counterpart.
The obvious argument fails. Theorem 2 controls the expected suboptimality of , not of , and Markov's inequality applied to does not reach accuracy ε: and differ by an amount comparable to ε, and the contraction factor itself depends on μ. Relating the run on to the original problem requires the global Lipschitz constant of in , which for is the weighted co-coercivity statement of Lemma 2 of the paper and is not a consequence of (2.2) alone without convexity. The constants of (3.11) are exact, including the factor 2 and the ½, so no estimate may lose a constant. Finally, the iterates depend on all previous draws, so even the finite-sum expectations need a careful account of linearity and of conditioning on the last draw.
Blocks E of finite-dimensional real spaces E i indexed by Fin n (0-based for the paper's 1, …, n). Euclidean blocks (3.4) are inner-product spaces, with absorbed into the inner product; Theorem 2 is stated for arbitrary normed blocks. The dual norm of a block is the operator norm of a functional.Fin k → Fin n; expectations and probabilities are finite sums weighted by . No measure theory is involved.Contributions are welcome on the probabilistic bookkeeping for expect (normalization, linearity, conditioning on the last draw, Jensen for a concave function), which is reusable by every mission of this series; on Lemma 2 of the paper in the block setting; and on the milestones in the stated order.
A retailer that orders stock months before the selling season carries inventory risk: its profit depends on a demand it cannot observe when it commits. For many goods that demand moves with a quantity traded on financial markets: sales of housing-related products with an interest-rate or construction index, sales of fashion or luxury goods with a stock index, sales of commodity-intensive products with a commodity price. V. Gaur and S. Seshadri, Hedging Inventory Risk Through Market Instruments (MSOM 7(2), 2005), ask what such a firm gains by trading in that market, and how the trade interacts with the ordering decision.
Their analysis has two halves. When demand is perfectly correlated with the asset price, the newsvendor payoff can be replicated by a portfolio of the asset and call options, and inventory risk can be removed completely (§2). When demand is only partially correlated, the hedge is imperfect, and the question becomes whether a decision maker with a concave utility still benefits from hedging, and whether hedging changes the order quantity (§3.2). This mission formalizes the first of these two questions in the partially correlated model: Proposition 5, which says that a small fair hedge never lowers expected utility at the margin. A companion mission of the same series treats Proposition 7, on the order quantity.
A firm orders units now at unit cost , sells at price at a future time , and salvages leftovers at . The demand is
where is the time- price of a traded asset and is a forecast error, independent of , with and (§3, p. 107). Write . The paper's standing assumptions (§2, p. 106) are , , and , where is the risk-free rate.
After scaling all cash flows by (p. 110) the firm's terminal wealth without hedging is
with and the scaled initial wealth plus . In these units reads and .
A hedge is a portfolio with time- payoff and time-0 price . The paper requires it to be a fair gamble, (12), and to be an increasing function of (p. 111). If the firm shorts units of the hedge, its wealth is
and a decision maker with utility evaluates it by .
In Lean, the law of is a probability measure ν on ℝ, the law of is a probability measure G on ℝ, the hedge is X_T = φ S_T for a function φ : ℝ → ℝ, the forward price is one real x0r, and every expectation is an integral against the product measure ν.prod G. The definitions file provides unhedgedPayoff, hedgedPayoff and expUtil.
For any concave and differentiable utility function , and any fixed order quantity ,
The Lean statement asserts that the two-sided derivative exists at and is nonnegative.
Proposition 5 is the paper's answer to "should a risk-averse newsvendor hedge at all?": with any concave utility and any order quantity, a small short position in a fair hedge that rises with the asset price weakly increases expected utility. It needs no assumption on the shape of the utility beyond concavity, no sign of , and no assumption on the law of the forecast error beyond independence. It is the starting point for the paper's later results on the optimal hedge (Proposition 4) and on how hedging raises the optimal order (Propositions 6 and 7), and it is a clean instance of a general principle in operations-finance: a fair bet that is negatively correlated with marginal utility is worth taking at the margin.
The result is proved in the paper in a few lines. What this mission adds is a machine-checked version with every regularity condition explicit: the paper differentiates under the expectation and multiplies expectations without stating when this is legitimate, and conditions on informally. To the best of a search of the Prove2Me catalog, neither the result nor the two steps of its proof (an integral version of Chebyshev's covariance inequality for monotone functions, and differentiation of a concave expected utility under the integral sign) is formalized there.
The obvious argument has two analytic gaps. First, exchanging with the expectation needs a dominating function, and the only integrability available is at finitely many values of , for both signs of . Second, " is a decreasing function of " is false as a statement about the pair : depends on too. The covariance step is Chebyshev's inequality for the function and the function , which needs independence (Fubini on the product measure) and has to cope with the conditional expectation being finite only almost everywhere. Neither nor the hedge payoff is bounded.
The Lean development commits to the following conventions.
ν (law of ) and G (law of ) on ℝ; independence is the product measure ν.prod G. The standing assumptions and are hypotheses (∫ e, e ∂G = 0, MemLp id 2 G).φ : ℝ → ℝ, monotone (nondecreasing, reading the paper's "increasing" weakly), measurable and ν-integrable; the fair-gamble condition (12) is ∫ s, φ s ∂ν = x0r. The paper's further remark that is piecewise continuous and a.e. differentiable is not needed and not imposed.u : ℝ → ℝ with ConcaveOn ℝ Set.univ u and Differentiable ℝ u, exactly "concave and differentiable"; no monotonicity of is assumed.A statement of the form 0 ≤ deriv (fun α => expUtil …) 0 would be trivially true whenever the derivative fails to exist (Lean's deriv returns 0 there); the goal instead asserts HasDerivAt with a value D and 0 ≤ D. The hypotheses are satisfiable with a non-constant hedge: a sorry-free check uses , uniform on , uniform on and .
Infrastructure that a complete proof needs, reusable beyond this mission: Chebyshev's integral (covariance) inequality for two monotone functions of a real random variable; differentiation under the integral sign for concave integrands with integrability at three points; Fubini-based conditioning on one coordinate of a product measure. Contributions of these general lemmas as separate theorems are welcome. The source PDF is a scan of the published article.
In a time-inconsistent control problem, a control that is optimal when planned at time stops being optimal when the problem is re-solved at a later time. Two sources of time inconsistency are common in finance and economics. One is a variance term in the objective, as in continuous-time Markowitz mean–variance portfolio selection (Zhou–Li 2000; Basak–Chabakauri 2010). The other is a state-dependent target, as in Björk–Murgoci–Zhou 2014. Dynamic programming does not apply. A standard response is to look for an equilibrium: a control that no planner at any time can improve by an infinitesimal deviation on .
Hu, Jin and Zhou define open-loop equilibria for a general stochastic linear–quadratic (LQ) problem with both sources of time inconsistency. They give a sufficient condition through a flow of forward–backward SDEs, which is the subject of mission I of this series. This mission covers §4 of the paper: the scalar-state case with deterministic coefficients, where the equilibrium is computed explicitly from a system of coupled Riccati equations. Mission III covers §5, the mean–variance application with random coefficients.
On a probability space carrying a standard -dimensional Brownian motion with its filtration , the state is scalar () and the control takes values in :
The coefficients are deterministic functions on : , , , and symmetric. are bounded, are square integrable, , , and . At time , in state , the planner evaluates
where . The third term (the variance-like term) and the fourth term (which depends on ) make the problem time-inconsistent. A control with state is an equilibrium (Definition 2.1) if, for every and every -measurable square-integrable , the spike satisfies
With , and , the coupled Riccati system (4.9) for deterministic is
Given , a linear ODE (4.8) determines with . The candidate equilibrium is the linear feedback (4.4)
Suppose and one of three cases holds:
Then
and, for every solution of (4.8), the closed-loop equation of (4.4) has a solution, and the feedback control along every closed-loop state is an equilibrium.
The theorem gives an equilibrium in closed form, as a linear feedback of the current state with deterministic gains. That makes the equilibrium computable and comparable with the classical, time-consistent LQ regulator. Setting recovers a standard LQ problem, but (4.9) differs from the classical Riccati equation even then: it is a nonsymmetric coupled system (footnote 2, p. 10), and the cases (i)–(iii) are the conditions under which it is solvable. The mean–variance results of §5 (mission III) follow the same pattern.
The result is proved in the paper; to our knowledge it has not been formalized. A formal proof needs global existence for a nonlinear, nonautonomous ODE system with Carathéodory coefficients, obtained by truncation and a priori bounds. It also needs linear SDEs with bounded feedback, Itô calculus for products of deterministic and Itô processes, and the sufficient condition of mission I. Uniqueness in case (iii) is claimed by Theorem 4.4 but not proved in Theorem 4.3; it is part of the goal.
The system (4.9) is quadratic in . Its solutions can blow up in finite time, and can degenerate when changes sign. Picard–Lindelöf therefore gives only local solutions, and a global solution needs a priori bounds and , with and independent of the truncation level. Those bounds are where the case hypotheses enter. In the stochastic half, the equilibrium property is not proved by computing directly. It requires checking that the explicit candidate meets the flow-of-FBSDE sufficient condition, and the flow carries a parameter and the conditional expectations for every .
The general model (data, standing assumptions, states, conditional cost, spike, equilibrium) is stated for arbitrary and instantiated at through toData. It is built on the published substrate Peng1990_SMP_Stochastic (Brownian motion, natural filtration, , Itô integrals, SDE solutions). The formalization commits to the following choices.
The goal's conclusion is Definition 2.1 itself; it does not mention , or (3.4). Existence of the closed-loop state is asserted, not assumed. A formalization that assumes existence, or that replaces equilibrium by condition (3.4), is a different and weaker theorem.
Theorem 3.3 (the sufficient condition) is not posed here. Under the shared model it is mission I's goal at . Contributions are welcome on the ODE layer (truncation, comparison and Gronwall bounds for Carathéodory systems), on linear SDEs with bounded feedback, and on the Itô product rule. These parts are reusable well beyond this paper.
Many optimization problems in shape analysis, computer vision, numerical linear algebra and statistics have a feasible set that is not a vector space but a Riemannian manifold: spaces of curves modulo reparametrization, the Stiefel and Grassmann manifolds, fixed-rank matrices. On such a set the classical recipe "add a multiple of the search direction to the iterate" is not available, and line-search methods replace it by a retraction, a map that follows a tangent direction back onto the manifold (Absil, Mahony, Sepulchre 2008).
Quasi-Newton methods are the most widely used line-search methods in the Euclidean setting, and BFGS is the most popular of them. Transferring BFGS to a manifold raises a specific problem: the Hessian approximation lives on the tangent space at , while the next one must live on the tangent space at , so a vector transport between tangent spaces enters the update.
Timeline:
Let be a smooth manifold modelled on a real Hilbert space , with a Riemannian inner product and norm on each tangent space . For , is its differential, a functional on with dual norm .
A retraction is a family of smooth maps with and . Write , a function on the vector space , with derivatives and .
Algorithm 1 produces iterates . The step satisfies the Wolfe conditions with :
The BFGS direction solves for a bounded bilinear form on . With and , the next form is defined on through an invertible linear map :
The analysis uses the angle and the Rayleigh quotient .
Assume:
Then there is with
The rate is not specified: the goal asserts only R-linear convergence, the shape of the result.
The result. Proposition 10 is a global convergence guarantee for a quasi-Newton method on manifolds, with no restriction to a neighbourhood of the minimizer and no finite-dimensionality. It applies to Riemannian shape spaces of curves, where the paper's numerical experiments take place. The paper's superlinear-rate theory (Proposition 12, Corollary 13) starts from this linear rate.
Formalizing it. The result is proved on paper but has not been machine-checked. A formal proof also checks the delicate points of the infinite-dimensional argument, in particular the use of traces and Fredholm determinants of trace-class perturbations of the identity. The statement as printed needs a correction: the printed bound fails at , and the formal goal bounds , as the appendix's own final display does.
The Euclidean proof idea of bounding the eigenvalues of uniformly does not work for BFGS: those eigenvalues are not uniformly controlled. The Byrd–Nocedal argument replaces them by trace and determinant estimates, which show that a fixed fraction of the iterations have well-conditioned angles. In infinite dimensions the trace and the determinant of do not exist. One must work with , which is trace class, and with the Fredholm determinant, and show that isometric transports leave these quantities invariant. That invariance is exactly where the isometry hypothesis enters. Lemma 9 is also not a finite-dimensional triviality: positive definiteness of does not give coercivity, and a separate compactness-free argument is needed.
The manifold is a Mathlib ChartedSpace E M, with a complete real inner-product space, IsManifold 𝓘(ℝ, E) ∞ M, and a RiemannianBundle on TangentSpace 𝓘(ℝ, E). Every norm on a tangent space is the Riemannian one. is mfderiv, read as a functional on , and its norm is the operator norm.
Committed conventions and explicit readings:
A trivializing formalization is ruled out on three fronts. A sorry-free check on , with , and , shows that the run hypotheses are satisfiable. Every quotient in a statement has a positive denominator along such a run. The rate is quantified after the run and before .
Infrastructure that a complete development needs, and that is reusable beyond this mission:
The last item is absent from Mathlib, and contributions toward it are welcome. The paper's other main result, convergence of Fletcher–Reeves conjugate gradients (Proposition 15), is a separate mission. The superlinear-rate results (Lemma 6, Propositions 5, 7, 8, 12, Corollaries 11, 13) and the numerical §4 are out of scope.
A prophet inequality compares a gambler who sees independent random rewards one at a time, and must accept or reject each on arrival, with a prophet who sees all rewards in advance. The classical inequality of Krengel, Sucheston and Garling (1977–78, as cited in the paper) says that when only one reward may be kept, a single threshold rule earns at least half of , and Samuel-Cahn (1984) showed that the threshold can be chosen as a median. Such statements are the analytical core of sequential posted-price mechanisms: Hajiaghayi, Kleinberg and Sandholm (2007) observed that threshold rules are truthful online auctions, and Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices approximate the optimal Bayesian revenue in many settings, with prophet inequalities for the feasibility constraint as the key technique.
When several items may be accepted subject to a combinatorial constraint, the natural constraints in this application are matroids (for example, at most items, or at most one item per group) and intersections of matroids (for example, bipartite matchings, which are intersections of two partition matroids). Kleinberg and Weinberg (STOC 2012) proved that for every matroid there is an online algorithm with expected payoff at least half of the expected maximum-weight basis, and that for the intersection of matroids the summed version of the same algorithm earns at least of the expected optimum. This mission formalizes the second result.
Timeline:
A finite ground set carries matroids with independent sets and closure operators . A set is feasible if it lies in . Each element has a random weight ; the weights are independent and has law . For a set , , , and .
An online weight-adaptive adversary reveals the elements one at a time; it chooses the -th element after learning , but without knowing or any other unrevealed weight. A threshold algorithm offers a threshold computed from what has been revealed and from the set already selected, and selects exactly when and .
The algorithm of the paper uses a ghost sample , an independent copy of . Let be a -maximum feasible set. For a set and each , is a set of maximum -weight with and , and . Put and . For a parameter , the summed thresholds are
and the algorithm of §4.2 uses . An algorithm has -balanced thresholds (Definition 3) if, for every input sequence with selected set and every disjoint from with ,
For every , all matroids on , all laws on with finite means, and every online weight-adaptive adversary, the algorithm of §4.2 with selects a set with
For this is the factor-2 matroid prophet inequality.
If a threshold algorithm has -balanced thresholds for some , then against every online weight-adaptive adversary
Proposition 2 for each matroid ; the identity between the two forms of ; properties (13) and (14) for the summed thresholds; the identities (20)–(21); and the inequalities (23)–(24) of Appendix A. Together with Proposition 3 these give the goal.
The bound gives a posted-price style selection rule for any feasibility constraint that is an intersection of matroids, with a guarantee depending only on ; the paper's §5 shows that a ratio of order is necessary. Section 6 of the paper turns the result into sequential posted-price mechanisms for multi-dimensional mechanism design, and that application needs the guarantee against the online weight-adaptive adversary, not only against a fixed order. The reduction "balanced thresholds imply an approximation" (Proposition 3) is reusable for other threshold constructions.
The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a formal proof of the guarantee, with the probabilistic part (the ghost-sample argument against an adaptive adversary) and the combinatorial part (the per-matroid exchange inequality) as separate milestones. The paper justifies the per-matroid use of Proposition 2 in one paragraph; because maximizes over the intersection rather than over , the description of as a maximum-weight basis of a contraction (Lemma 2 in the single-matroid case) does not apply verbatim, and the formal proof of that milestone is not a copy of the paper's single-matroid argument.
Two steps do not follow from routine bookkeeping. First, the inequality (23) compares the gambler's surplus, collected along an order that the adversary adapts to the realized weights, with the ghost sample's surplus on the random set . The index revealed at step is itself random, so the step "the weight of the element offered next is distributed as its ghost weight" has to be justified for an adaptively chosen index under a product measure; it fails for an adversary that may look at unrevealed weights. Second, the paper obtains (14) by applying the single-matroid Proposition 2 to each , but its proof of Proposition 2 describes as a maximum-weight basis of a contraction, which uses that is optimal for the matroid in question. Here is optimal only for the intersection , so the obvious transfer of the single-matroid argument does not go through as written and the per-matroid statement needs its own proof.
The ground set is a Fintype; the matroids are Mathlib's Matroid α, indexed by Fin p, each with ground set Set.univ; sets are Finset α. Weights are functions α → ℝ, the weight law is Measure.pi F, and every theorem assumes each F x is a probability measure with F x (Iio 0) = 0 and a finite mean. Expectations are Bochner integrals; under these assumptions every integrand is integrable. Ties in the maximizers and are broken by a fixed rule that does not depend on the weights. is taken disjoint from . The threshold on infeasible steps is a feasibility test in the selection rule. Adversaries and generic threshold rules are deterministic, see only revealed weights, and are measurable in them; randomized adversaries are mixtures of deterministic ones. Generic thresholds in Proposition 3, (23) and (24) are non-negative, as in the paper's .
The goal fixes the thresholds to the summed thresholds of §4.2 with , computed from the ghost-sample objects. A version in which the thresholds are free parameters assumed to satisfy (13)–(14) would be Proposition 3 itself and is ruled out; conversely, Proposition 3 does not mention the §4.2 thresholds.
A complete development needs: elementary facts about maximizers over finite families; matroid exchange properties (a bijective exchange between equal-size independent sets, available in Schrijver's book but not in Mathlib); submodularity of weighted-rank-type functions; and the independence argument for adaptively chosen indices under a product measure. The last two are reusable beyond this mission, as is Proposition 3. Proofs of individual milestones and of these auxiliary facts are welcome.
Many large optimization problems arising in machine learning, statistics and network analysis have so many variables that computing a single full gradient is already expensive, while a single partial derivative, or a gradient with respect to a small block of variables, is cheap. Coordinate descent methods exploit this: at each iteration they update one block of variables only. They are among the oldest methods of numerical optimization, but for a long time their worst-case efficiency was not understood, because deterministic rules for choosing the next coordinate (cyclic order, greedy choice) are hard to analyse globally.
Nesterov (2010/2012) showed that choosing the coordinate at random, with probabilities tied to the coordinate-wise Lipschitz constants of the gradient, yields clean global complexity bounds. This paper started the modern theory of randomized coordinate descent, which was then extended to composite objectives, parallel and accelerated variants, and became a standard tool for huge-scale problems. This mission formalizes the first of its results: the expected sublinear rate of the basic method RCDM (Theorem 1 of the CORE Discussion Paper 2010/2).
The variable is split into blocks, . Write for the -th block and for the point whose -th block is and whose other blocks vanish. Each block space carries a norm with dual norm .
The objective is convex and differentiable, and its set of minimizers is nonempty and bounded; is its optimal value. The partial gradient is the -th block of the gradient. The gradient is coordinate-wise Lipschitz with constants :
for all , and .
For a linear functional , is any maximizer of . The optimal coordinate step is . For let and . The method RCDM starts at and, for , draws independently with and sets . Its expected objective value is , the expectation over the draws .
The weighted norms are and , and the size of the initial level set is
For every ,
The statement holds for every real , every choice of the vectors , and every block decomposition with arbitrary block norms. With (uniform sampling) it reads .
Theorem 1 is the first global efficiency estimate for a coordinate descent method on general smooth convex functions. Its constant is governed by , an average of the coordinate Lipschitz constants, rather than by the global Lipschitz constant of the gradient; for and Euclidean blocks this makes the method competitive with the full-gradient method even when partial derivatives are not cheap, and much faster when they are. The later results of the paper (linear convergence under strong convexity, high-probability bounds, the constrained and accelerated variants, adaptive Lipschitz estimates) reuse the objects and the one-step estimates of this mission.
The result is proved in the paper; nothing in it is open. As far as we know it has not been machine-checked. The platform contains a related item, ConvexOptAlg.CoordDescent.theorem_6_7 (Bubeck's monograph, Theorem 6.7, open), which treats scalar Euclidean coordinates, , and the weaker factor ; together with its proved one-step lemmas (thm_6_7_coord_step, thm_6_7_expected_decrease) it covers the special case of milestones 3 and 5. This mission states the result in the paper's generality: arbitrary blocks and block norms, non-Euclidean dual norms through , every real , and the constant .
The bound is a statement about an expectation, not about individual runs: the recursion on needs Jensen's inequality, , and the fact that every run stays in the initial level set, so that controls along every path. Lemma 2 is the step that links the coordinate-wise condition (2.2) to the weighted full gradient, and it is easy to misjudge: it is false without convexity, since on satisfies (2.2) with arbitrarily small constants. The non-Euclidean block norms add a layer of convex analysis (the dual norm, the vector and its identities) on top of the probabilistic bookkeeping.
Blocks E of finite-dimensional real normed spaces; indices are 0-based. The norm Lean puts on the product is never used; statements use only the block norms and the weighted norms (2.7).E i →L[ℝ] ℝ; the partial gradient is the derivative of composed with the inclusion of block .IsSharpSelection); all results quantify over every selection.Contributions welcome: proofs of the one-step estimates (2.3), (2.4), (2.13), which need a block mean-value argument and the convex analysis of ; Lemma 2, which needs the convex conjugate argument of its proof; and the final summation argument. The block encoding and the identities for are reusable for every other mission of this paper.
Mean–variance portfolio selection (Markowitz, 1952) trades off the expected terminal wealth of an investor against its variance. In a dynamic setting the problem is time-inconsistent: the variance is not a conditional expectation of a function of terminal wealth, so the dynamic-programming principle fails, and a strategy that is optimal when computed at time is no longer optimal when re-evaluated at a later time. A standard response is to treat the investor at each time as a separate player and to look for a subgame-perfect equilibrium strategy, which no future self wishes to deviate from locally (Björk–Murgoci, Ekeland–Lazrak, and others).
Hu, Jin and Zhou (arXiv:1111.0818v1; SIAM J. Control Optim. 50(3), 2012) define open-loop equilibria for a general class of time-inconsistent stochastic linear–quadratic (LQ) problems and characterize them through a flow of forward–backward SDEs. Their §5 applies this to mean–variance investment in a complete market with a random risk premium, where the weight on expected wealth depends on current wealth (a state-dependent risk aversion, motivated in Björk–Murgoci–Zhou, 2014). Earlier equilibrium results for mean–variance investment (Basak–Chabakauri, 2010; Björk–Murgoci–Zhou) work with deterministic or Markovian coefficients and within feedback classes.
This mission is the third of a series on the paper. Mission I formalizes the general sufficient condition (Theorem 3.2); Mission II treats deterministic coefficients and coupled Riccati equations (Theorem 4.4). This mission targets the explicit mean–variance equilibrium of Theorem 5.4.
Fix a horizon and a probability space carrying a standard -dimensional Brownian motion with its filtration ; write . The market has a deterministic bounded interest rate and a progressively measurable, essentially bounded risk premium with values in . A strategy is a progressively measurable with (the class ); the wealth under solves
At time , with current wealth , the investor's cost is
This is the case of the paper's general LQ problem, with , , , , , ; the mission states it that way. For , and an -measurable square-integrable , the spike perturbs on a short window. A strategy with wealth is an equilibrium (Definition 2.1) if, for all such and ,
The equilibrium is built from , , and two backward SDEs: an indefinite stochastic Riccati equation for ,
and a linear BSDE (5.13) for whose coefficients involve and . A process gives a BMO martingale if for all stopping times .
If solves (5.8) with bounded and , and solves (5.13) with bounded, then
is an equilibrium: the closed-loop wealth exists, and for every closed-loop wealth the strategy satisfies Definition 2.1.
Theorem 5.4 gives the equilibrium of a time-inconsistent mean–variance investor in closed form, linear in current wealth, for a random risk premium. With a deterministic premium it reduces to explicit formulas (§5.4), and for it recovers the equilibrium of Basak–Chabakauri and Björk–Murgoci; for it differs from the feedback equilibrium of Björk–Murgoci–Zhou, which shows that open-loop and feedback equilibria are different notions. The random premium is what makes and the feedback gain unbounded.
The result is proved in the paper; nothing here is formalized elsewhere. The mission produces machine-checked statements of the equilibrium, of solvability of the Riccati-type BSDE (5.8), and of the integrability of a linear SDE with BMO-type coefficients, on the platform's published stochastic-calculus substrate. The definition of BMO martingales and the encoding of open-loop equilibria are reusable beyond this paper.
The verification step that most readers try first, plugging into the wealth equation and applying standard SDE estimates, fails: the gain is unbounded, because is only BMO, so the closed-loop SDE is linear with non-Lipschitz-bounded random coefficients and neither existence of the wealth nor follows from standard theory (Proposition 5.3). The BSDE (5.8) has a driver with quadratic growth in and a singular factor ; it is not covered by the standard theory of stochastic Riccati equations and its solution must be bounded away from zero for the feedback to make sense. Uniqueness in (5.8) and solvability of (5.13) rely on BMO-martingale and change-of-measure facts (Kazamaki) that are not in Mathlib. Finally, the equilibrium property is a statement about every and every perturbation, and the sufficient condition (Theorem 3.3) needs the limit behaviour of conditional expectations as .
Everything is built on the published definition Peng1990_SMP_Stochastic (Brownian motion, , Itô integrals, SDEs and BSDEs as relations). The general LQ model, the spike, the conditional cost and Definition 2.1 are in Model; the adjoint equation on , and condition (3.4) in Adjoint; the market, , , BMO, (5.8), (5.13) and (5.14) in Market. Conventions the statements commit to:
The goal does not assume the BMO properties of and (they are conclusions of Propositions 5.1–5.2), does not assume deterministic or (that is the special case of §5.4), and keeps , ; a formalization that assumes any of these, or that admits the junk value on a non-null set, proves a different theorem. Theorem 3.3, the sufficient condition used in the last line of the proof, is the case of Mission I's goal and is not restated here. Welcome contributions: a BMO and Girsanov library on the Peng substrate, existence for quadratic BSDEs, and a proof of the sufficient condition.
Manufacturers routinely share rolling schedules with their suppliers: each period the buyer commits to a purchase for the current period and issues non-binding estimates for future periods, then revises those estimates as the horizon rolls forward. Unconstrained revisions push forecast risk upstream and are a recognized source of the bullwhip effect. A quantity flexibility (QF) contract bounds how far each estimate may move between consecutive issues, giving the supplier a guarantee in exchange for a commitment to cover any order within the bounds. Tsay and Lovejoy (MSOM 1(2), 1999) model a chain of firms linked by QF contracts and ask how a firm in the middle of the chain, the flex node, should translate the schedules it receives into the schedules it issues. Their answer is the Minimum Commitment (MC) policy, justified by Proposition 1: MC solves the node's open-loop planning problem and never breaks either contract.
This mission formalizes Proposition 1. A companion mission (Quantity Flexibility Contracts and Supply Chain Performance 1) formalizes Proposition 2, on when MC keeps zero inventory.
Periods are . In period the node receives from its customer a release schedule : is bought now, estimates the purchase in period . The node issues to its supplier a replenishment schedule of the same form. Its ending stock is .
The contracts carry parameters and (): output parameters with the customer and input parameters with the supplier. The incremental revision (IR) constraints are, for all and ,
The cumulative parameters are and , so . A convex cost , minimized at , is charged on ending stock.
At period , with , and known, the open-loop program (F-OLFC) chooses and the planned purchases , , to minimize subject to the stock balance (17), coverage (18), the input IR constraints (19) between and , and the cumulative bounds (20).
The MC policy computes and projected inventories by one recursion on : ,
In Lean: QFParams, Acum, Ωcum, IROut, IRIn, mcStep, run, inv, sched, projInvAt (module Model) and stock, Feasible, RelaxedFeasible, objective, lbar, pStar (module FOLFC).
For an MC run from with , against any customer schedules obeying (6), and any convex minimized at zero:
and for every the schedule , with suitable planned purchases, is feasible for (F-OLFC) at period and attains its minimum.
Proposition 1 is what makes MC a well-defined operating rule for an intermediate firm: whatever the customer does within its contract, the node can serve it from stock and its own revisions stay within the supplier's contract, so the chain of contracts composes. Proposition 2 and the paper's simulation study of how flexibility propagates along a supply chain (§§5–6) both assume the node uses MC, and rely on Proposition 1 for that choice being both feasible and myopically optimal.
The paper's optimality argument is sketched: the relaxed solution is attributed to "a straightforward application of Kuhn–Tucker conditions" with details in an unpublished thesis, the equivalence of (32) with (21)–(23) is omitted, and Lemma 1's proof is replaced by intuition. A machine-checked proof supplies these steps. To our knowledge no part of this paper has been formalized before. The mission also fixes the statement: the printed range of (19) makes the optimality claim false, and the claim needs a start of the run that the paper leaves implicit.
The obvious argument treats (F-OLFC) as a lot-sizing problem with minimum lot sizes and observes that the greedy purchases (30) are optimal. That only solves the relaxation. The difficulty is that MC is not stated through (30): it is a recursion on the replenishment schedule with a positive part in the projected inventory, and one has to show that the MC schedule can carry the greedy purchases within the upper bounds of (19) and (20). Those bounds can bind, and whether they do depends on the previous period's schedule, so the optimality claim is not a one-period statement: it needs an induction over the run, through Lemma 1 and the customer's IR constraints. The admissibility half needs the same induction, with the nonnegativity of the schedules carried along.
All quantities are real numbers. Parameters are sequences ℕ → ℝ whose index is unused; schedules are infinite sequences, and the MC recursion runs over all . (6) and (7) are written with replaced by . The standing assumptions , () are hypotheses. is any convex function with for all ; no strict convexity, differentiability or monotonicity is assumed.
The run starts from an arbitrary state (run period ); the MC policy acts from period . The following departures from the printed statement are disclosed:
(F-OLFC) ranges over all real schedules and purchases; the only MC-specific object in the goal is the candidate schedule. Optimality is stated as "feasible, and no feasible point has a smaller objective", never as an infimum, so an infeasible program cannot make it vacuous. The MC step is literally (21)–(23), with the carried-over term and the positive part; a run that sets or drops the max is a different policy.
Infrastructure: the model and (F-OLFC) are self-contained over Mathlib (Finset.prod, ConvexOn). Proofs of the three milestones, and of the monotonicity of a convex function minimized at zero on , are welcome as separate contributions.
In distributed computing, many graph problems (minimum spanning tree, shortest paths, connectivity checks) are solved by processors that sit at the vertices of the input network and communicate only along its edges. When every edge can carry only a few bits per round, the number of rounds an algorithm needs can be far larger than the network's diameter. Understanding by how much is the central question of the CONGEST (here: B) model of Peleg's monograph Distributed Computing: A Locality-Sensitive Approach (SIAM, 2000).
Das Sarma, Holzer, Kor, Korman, Nanongkai, Pandurangan, Peleg and Wattenhofer (SIAM J. Comput. 41 (2012) 1235–1265) proved round lower bounds for a long list of verification problems (is a given subgraph a spanning tree, a cut, a Hamiltonian cycle, …) and for approximating optimization problems such as the minimum spanning tree and shortest paths. Every one of those bounds goes through a single reduction, the Simulation Theorem (Theorem 3.1), which transfers lower bounds from two-party communication complexity to distributed algorithms.
Timeline:
A B-model network is an undirected graph whose vertices are processors with unbounded local computation. Computation proceeds in synchronous rounds; in each round, every vertex sends a message of bits along each incident edge in each direction, then updates its local state from its old state and the messages it received. Two vertices and hold inputs ; all other vertices start without input. A public-coin randomized algorithm additionally lets all vertices read a shared random string. It computes with -error in rounds if, for every , both and output after round with probability at least . is the least such .
In the communication complexity model, Alice holds , Bob holds , one bit is sent per round, and both must output . is the least number of bits of an -error public-coin protocol.
The network consists of paths with vertices each, a complete -ary tree of depth with vertices at level , and spoke edges joining each leaf to on every path. The inputs sit at the two extreme leaves, and . The -right set consists of all path vertices at positions , the leaves with , and their ancestors; the -left set is the mirror image, and , . denotes the vector of states of the vertices of at the end of round .
If a public-coin algorithm on computes with -error in rounds and
then some public-coin two-party protocol computes with -error using at most
The theorem turns any lower bound , such as those for set disjointness and equality, into a round lower bound on : an algorithm with rounds forces . Choosing the parameters gives the paper's bounds of order rounds for verification and approximation problems (§§4–7), and the same reduction underlies a large body of later CONGEST lower bounds.
The result has been proved since 2011. A machine-checked version would provide the first formal model of synchronous bandwidth-limited message passing and of public-coin two-party protocols on the platform, together with a verified reduction between them. No formalization of the theorem, of the B model, or of two-party communication protocols is known to exist in Mathlib or on the platform.
The informal proof is short; the work lies in making the information flow precise. The naive simulation, in which Alice simulates the vertices near and Bob those near , fails because the cut between the two halves contains path edges plus the spokes, and can be large: sending every message across it costs bits per round. The argument must instead let both parties' simulated regions shrink by one path position per round, so that the only messages crossing into Bob's region come from tree vertices with children each. Making this rigorous requires a careful accounting of which vertices belong to , which edges leave , and why the functions that update the configurations do not depend on the other party's input.
(Fin Γ × Fin (d^p)) ⊕ Σ ℓ : Fin (p+1), Fin (d^ℓ); paths are numbered from . The children of are , . are Finsets defined for every , with the paper's special case at . The nodes require .Fin B → Bool) on every directed edge in every round. Optional or variable-length messages would let silence carry information and make the theorem false (e.g. at ).PMF on an arbitrary type, shared by all vertices (resp. both parties); -error requires both outputs to be correct on the same random string, and .sInf, which would be on an empty set; the goal is stated for every algorithm.Contributions welcome: proofs of the milestones, and reusable infrastructure for executions of message-passing algorithms (locality lemmas such as Observation 3.3 hold on any graph).
Assortment optimization asks which subset of products a firm should offer when customers choose among the offered products, or leave without buying. It underlies shelf-space planning in retail, the choice of which fare classes to keep open in airline revenue management, and the selection of items shown on a web page. The multinomial logit (MNL) model is the standard choice model in this literature: when the model parameters are known, the optimal assortment is revenue-ordered, that is, it consists of the products with the highest revenues (Talluri and van Ryzin, 2004; Gallego et al., 2004; Liu and van Ryzin, 2008), so only candidate assortments need to be compared instead of .
In practice the parameters of the choice model are estimated from limited data. Rusmevichientong and Topaloglu (Operations Research, 2012) take a robust view: the parameters are only known to lie in an uncertainty set, and the firm maximizes its worst-case expected revenue. Their main structural result is that the revenue-ordered structure survives this uncertainty, whatever the uncertainty set. This mission formalizes that result and the comparative statics the paper derives from it.
There are products, , and product earns revenue . A customer's choice is governed by a parameter vector (all components strictly positive): is the weight of the no-purchase option and the preference weight of product . When the assortment is offered, the customer buys product with probability
and buys nothing with the remaining probability. The expected revenue of is
The parameters are unknown and lie in an uncertainty set , which is compact and nonempty. The Robust Logit problem maximizes the worst-case expected revenue:
Among the optimal assortments, is one with the smallest cardinality. For a single parameter vector , write and ; this is the classical problem with known parameters. Finally, for , and are the same quantities when every revenue is replaced by .
Equivalently: an assortment is optimal with smallest cardinality if and only if it is the set of products whose revenue strictly exceeds the optimal worst-case revenue. When this set is for some .
Milestones 3–6 are consequences of the goal on the same definitions.
Theorem 3.2 reduces the robust problem, a max–min over assortments and a possibly infinite parameter set, to at most revenue-ordered candidates, each requiring one worst-case evaluation . Applied to a singleton it also reproves the classical revenue-ordered optimality under known MNL parameters, together with the exact tie-breaking description. Corollary 3.5 and Theorem 3.6 say that more uncertainty calls for a larger assortment, and that the robust assortment is the largest assortment optimal for some parameter in ; Theorem 3.7 compares assortments when all revenues shift by a constant, which the paper uses in Section 4 to show that robust dynamic assortments grow with remaining capacity and over time.
The results are proved in the paper; none of them has a machine-checked proof on Prove2Me. The platform has ChoiceCDLP.MNL.top_ranked_optimal (from Liu and van Ryzin, 2008), a statement about top-ranked offer sets for known MNL weights, which is a different statement without uncertainty or tie-breaking. A formal development here gives a checked version of the robust structure theorem stated for arbitrary real revenues, the generality in which the dynamic part of the paper uses it.
The obvious argument fails at the max–min. For known parameters, Lemma 3.1 immediately shows that a product should be added exactly when its revenue beats the current expected revenue; but under uncertainty the minimizing parameter vector changes with the assortment, so one cannot compare and at a single worst-case . The argument has to establish a strict improvement uniformly over and then pass to the minimum, which is where compactness enters: a pointwise strict inequality survives the minimum only because it is attained. The tie-breaking rule is equally essential: a product with can be added to an optimal assortment without changing its worst-case value, so without the smallest-cardinality rule the characterization is false.
Products are Fin n, so Lean index stands for the paper's product . A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 and p.2 i the weight of product ; IsPos p expresses . The expected revenue is the published definition ChoiceCDLP.MNL.mnlObjective. The worst case is a real infimum (sInf), and is a maximum over all subsets of products. is encoded as the predicate IsSmallestOptimal V r S (optimal, and of cardinality at most that of every optimal assortment), not as a choice function, so every statement about is asserted for every optimal assortment of smallest cardinality. and are the same objects for the revenue vector , which is exact since is at those revenues.
Standing assumptions and departures from the page:
The infimum is meaningful only under the standing assumptions (on an empty set it is ), which is why they appear as hypotheses of every statement. A complete development needs continuity of on positive vectors and attainment of minima on compact sets, both available in Mathlib, and finite maxima over Finset (Finset (Fin n)). The lemmas about (milestones 1–2) are reusable for any MNL model. Proofs of any milestone, and alternative proofs of the goal, are welcome.
The source is the authors' manuscript of 20 Sep 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's page numbers, and all page citations refer to it.
A differential variational inequality (DVI) couples an ordinary differential equation with a finite-dimensional variational inequality whose solution enters the dynamics as a control. Contact mechanics with friction, electrical circuits with diodes, dynamic traffic equilibria, hybrid engineering systems and the continuous-time limits of Nash games all have this form. Pang and Stewart's survey (Math. Program. 113, 2008; author's version hal-01366027) set up a common framework for these models and studied the most direct numerical method: the Euler-type time-stepping scheme, which replaces the time derivative by a difference quotient and solves one static variational inequality per time step.
For the scheme to converge, its iterates must exist and be bounded uniformly as the step goes to zero. Section 7 of the paper proves convergence once such bounds are available (Theorem 7.1). Section 8 supplies them for a class of DVIs in which the algebraic part is not affine: the constraint set is a cone and the VI map is a strongly monotone composite. This mission formalizes that section.
Fix , and dimensions . The data are , , , a map and a set . For ,
The initial-value DVI (6.2) is , , .
With and , the time-stepping scheme (7.2) starts at and computes, for ,
The standing assumptions are:
Choosing orthonormal bases of and of , the map is strongly monotone with some modulus (8.7).
Let be a closed convex cone, (A), (B), (D), (C′), and (E) hold. There is such that for every with and every the scheme has a unique run, and for all small
These are the hypotheses (7.5)–(7.6) of the convergence theorem of §7.
A companion item states Proposition 8.1, the derivative form of (D).
Theorem 8.1 is one of the two routes in the paper to convergence of the time-stepping scheme. The other (Theorem 7.4) needs a linear-growth property of the VI solutions that holds for affine or coercive problems; Theorem 8.1 replaces it by structural assumptions on that cover nonlinear complementarity systems on cones, including the case that yields the initial-value differential complementarity problem (Corollary 8.1). Combined with Theorem 7.1(a), it shows that the Euler trajectories have uniformly convergent subsequences whose limits are weak solutions of the DVI, and so gives existence of weak solutions constructively.
The paper's results are proved on paper but, as far as a search of Mathlib and the platform shows, no part of DVI theory is formalized. The formalization also settles a printed error: the bound (8.10) of Proposition 8.3 carries a factor that its proof does not justify, and the printed statement is false (a one-dimensional counterexample is recorded on the milestone). The milestone states the bound the proof does give; (8.14) and Theorem 8.1 are unaffected.
The obvious argument fails at the multiplier bound. The VI map is strongly monotone, but only with modulus of order , so the solution of each step is bounded only by times the data. This loss is harmless for existence and uniqueness but would destroy the uniform bounds (7.5). Recovering an bound requires separating the components of in , where is blind and only the order- monotonicity of helps, from the components in , where itself is strongly monotone; condition (E) and the cone structure of are what allow the two parts to be tested separately. A second difficulty is that (7.6) needs a Lipschitz bound on with a constant that does not blow up as .
EuclideanSpace ℝ (Fin k); matrices are continuous linear maps; is the adjoint; is the published definition SolodovSvaiterVI.Alg21.viSol Φ K.The development needs: existence for strongly monotone (coercive) VIs on closed convex sets; the implicit-function argument for the -equation of a step; orthogonal decompositions along ; and discrete Gronwall estimates. The VI existence result and the decomposition lemmas are reusable beyond this mission. Proofs of any milestone, and of the existence theorem for strongly monotone VIs as a separate theorem, are welcome.
Networks of coupled oscillators model generators in an electric power grid, pacemaker cells, Josephson junction arrays and many other systems in which units with their own rhythm interact through their phase differences. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012, doi:10.1137/110851584) show that, after a singular-perturbation reduction, the transient-stability question for a lossy power network with non-uniform generators becomes a synchronization question for a non-uniform Kuramoto model: oscillators with different damping coefficients, different natural frequencies, an arbitrary coupling graph and phase shifts induced by line losses.
This mission concerns the cleanest regime of that model: lossless coupling and natural frequencies proportional to the damping. There the oscillators do more than agree on a frequency; they agree on a phase. For the classic Kuramoto model (Kuramoto, 1975) with identical frequencies, phase synchronization from inside an open half-circle was obtained by consensus methods for nonlinear coupled systems (Lin, Francis and Maggiore, 2007) and by Jadbabaie, Motee and Barahona (2004). Theorem V.10 of Dörfler–Bullo extends this to non-uniform damping, directed coupling with a globally reachable node, and gives an explicit worst-case rate for symmetric coupling. The proof rests on the contraction theory of time-varying consensus protocols (Moreau, 2004).
There are oscillators. Oscillator has a phase on the circle, a damping coefficient and a natural frequency . Oscillators interact through coupling weights (, with ) and phase shifts . The non-uniform Kuramoto model (8) is
The weights define a directed graph with an edge from to whenever ; a globally reachable node is a node to which every node has a directed path. For the closed arc set is the set of configurations whose angles all lie in a closed arc of length .
This mission assumes zero phase shifts, , and proportional frequencies, for all . The phases synchronize exponentially to a trajectory when there are and with for all and .
For the rate, is the Laplacian of a weight array, is its second-smallest eigenvalue (the algebraic connectivity) when , , , , and .
For every solution with , :
Theorem V.10 gives phase synchronization of non-uniform oscillators from every initial configuration inside an open half-circle, for directed coupling graphs that need only a globally reachable node, and identifies the limit phase: anywhere in the initial range in general, the damping-weighted mean under symmetric coupling. The rate separates three effects: graph connectivity (), initial phase cohesiveness () and non-uniformity of the damping (, ). For the classic Kuramoto model the statements reduce to known results ([19] and [33] of the paper).
The result is proved in the paper; no machine-checked proof is known. A formal proof needs a Dini-derivative argument for the maximum of finitely many smooth functions along an ODE, a contraction theorem for linear time-varying consensus with positive, bounded weights on a graph with a globally reachable node, and a Courant–Fischer bound on the weighted disagreement. Each is a reusable piece of infrastructure for networked control and synchronization.
The obvious argument linearizes: , so the model looks like linear consensus. That only holds near the diagonal; from an arc of length close to the effective weights come close to zero and depend on the state, so neither a fixed Laplacian nor a local linearization covers the claimed region. One needs first that the arc never grows, which is a statement about a non-smooth function (the arc length) along trajectories, and then exponential convergence of a consensus protocol whose weights are time-varying and, for directed graphs, non-symmetric, so there is no quadratic Lyapunov function in general. For the explicit rate the disagreement vector is orthogonal to , not to , and the angle between the two hyperplanes has to be controlled.
Angles are represented by real lifts ; the vector field is -periodic in each coordinate, so solutions on the torus are projections of solutions on . is encoded as for all on the initial lift, and every conclusion (invariance, , , the weighted mean, the convergence bounds) refers to that lift and the same continuous lifted trajectory, which is at least as strong as the statement on the torus. A solution is a curve on whose derivative within equals the vector field at every ; statements quantify over every such curve. The model is stated with the paper's general field and hypotheses , ( arbitrary, not set to zero).
Conventions and corrections, each disclosed in the item's Formalization Note:
AlonMilman.PropertyT.lambda1 applied to the symmetric Laplacian.Exponential convergence requires a rate ; a statement with or with a solution predicate that no curve satisfies would be trivial. The synchronous trajectory satisfies the solution predicate, so the hypotheses are satisfiable.
Infrastructure welcome beyond this mission: upper Dini derivatives and comparison lemmas for maxima of differentiable functions, exponential stability of linear time-varying consensus (Moreau's theorem), and Laplacian ordering for entrywise-dominated weights.
A real number is normal in base when every block of base- digits occurs in its expansion with limiting frequency , exactly as it would in a sequence of independent uniformly random digits. It is normal (absolutely normal) when it is normal in every base . Whether the classical constants of analysis, above all , are normal is one of the oldest open questions linking number theory and probability: it asks whether a number defined by geometry has digits that are statistically indistinguishable from random ones.
Timeline.
Large-scale digit computations of are statistically consistent with normality. No base is known in which is normal, and it is not even known that any particular digit occurs infinitely often in its decimal expansion.
A digit sequence is a function ; is the first digit after the point. A word is a finite list of naturals. For , the occurrence count is the number of positions with for every . Overlapping occurrences each count.
The sequence is normal in base (IsNormalSeq b s) if, for every word with all entries ,
The -th base- digit of a real after the point is
The real is normal in base (IsNormalReal b x) if is normal in base . Two remarks:
This is the conjecture in its standard form, normality in every base. The base-ten case is the special case .
None are listed. No decomposition of this problem into intermediate statements is known that would be a faithful attack path, and the mission does not invent one. Proposals for intermediate targets are welcome in the discussion; see the contributions listed under Formalization scope.
The known theorems of the subject (Champernowne's constructions, the Copeland–Erdős theorem, Borel's theorem) concern numbers built to be normal or almost every number; they are not steps toward and are kept in the separate mission Explicit normal numbers: Champernowne and Copeland–Erdős.
A proof that is normal in base would give every finite digit pattern a definite limiting frequency in its expansion. It would be the first normality result for a classical constant not built to be normal. Every known normal number is constructed digit by digit (Champernowne, Copeland–Erdős, Sierpiński, Becher–Figueira) or shown to exist by a measure argument (Borel). Even the base-2 case would settle the Bailey–Crandall programme for .
Formalization status. The goal is open mathematics. The definitions it is stated with are published and are shared with the mission Explicit normal numbers: Champernowne and Copeland–Erdős, where Champernowne's theorems and the Copeland–Erdős theorem have machine-checked proofs.
The constructive results all prove normality from the digit-by-digit description of the number. In particular, the Copeland–Erdős block criterion needs the expansion to be an explicit concatenation of blocks. has no such description. Its known series (Machin-type formulas, BBP) give digits as values of exponential sums, and no known method controls the joint distribution of long digit blocks of such values.
Borel's theorem does not help: it only says that the exceptional set is null, and gives no criterion for deciding whether a given number lies in it. Neither high-precision digit statistics nor irrationality measures for imply normality.
All declarations live in the namespace Normal and use the definition bundle Normal_Core:
count, IsNormalSeq, digit, IsNormalReal;ofDigits b s ;flatten, digitsBE, concatDigits;Committed conventions:
The definitions agree with Borel's, and the mission does not admit a trivialising reading. A real number is not normal merely because it is irrational, and the empty word imposes only the trivial condition.
The bundle also contains a verbatim copy of the integer-arithmetic definition IsNormal from xiangyazi24/agafonov; its equivalence with IsNormalSeq is proved on the platform (Normal.isNormalSeq_iff_isNormal), so results stated in either form transfer.
Welcome contributions:
A real number is normal in base when every block of base- digits occurs in its expansion with limiting frequency , as it would in a sequence of independent uniformly random digits. Borel introduced the notion in 1909 and proved that almost every real number is normal in every base, by an argument that produces no example. This mission collects the two classical papers that do produce examples: Champernowne's construction of and the theorem of Copeland and Erdős, which shows that the concatenation of any sufficiently dense increasing sequence of integers, the primes included, is normal.
Timeline.
A digit sequence is a function ; is the first digit after the point. A word is a finite list of naturals. For , the occurrence count is the number of positions with for every ; overlapping occurrences each count.
The sequence is normal in base (IsNormalSeq b s) if, for every word with all entries ,
The -th base- digit of a real after the point is , and is normal in base (IsNormalReal b x) if is normal in base . The integer part of plays no role; for a rational with two expansions the floor selects the one not ending in repeated 's.
If is an increasing sequence of positive integers such that, for every , the number of exceeds for all large , then the digit sequence obtained by writing the base- expansions of one after another is normal in base . A machine-checked proof is on the platform.
These are the standard examples of explicitly given normal numbers, and the Copeland–Erdős block argument is the model for most later constructions. The mission also fixes a definition of normality for real numbers together with the transfer from digit sequences to reals, which other work on normal numbers can import.
All declarations live in the namespace Normal and use the definition bundle Normal_Core: count, IsNormalSeq, digit, IsNormalReal; ofDigits b s ; the concatenation operators flatten, digitsBE, concatDigits; the Champernowne and Copeland–Erdős constants.
Conventions: digits are read after the point with the floor convention above; frequencies are limits of real quotients; words of every length with entries are quantified; results for real numbers are stated for bases by hypothesis.
The proofs are imported from the repository xiangyazi24/normal and verified by the platform. Their auxiliary lemmas are published on the platform as dependencies of the milestones and are not listed as items of this mission.
The open question whether is normal is a separate mission and is not approached by the methods here, which rely on the number being given as an explicit concatenation of blocks.
Many problems in machine learning and statistics minimize an average of smooth losses, one per training example: regularized least squares, logistic regression, and other forms of empirical risk minimization. Two classical families of methods attack such finite sums. The full gradient method evaluates all component gradients per iteration and converges linearly for strongly convex objectives, but each iteration costs gradient evaluations. The stochastic gradient method evaluates a single component gradient per iteration, so its iterations are cheap, but it converges only sublinearly, at rate , even under strong convexity.
Le Roux, Schmidt and Bach (arXiv:1202.6258, NIPS 2012) introduced the stochastic average gradient (SAG) method, which keeps a table of the most recently evaluated gradient of every component and moves along their average. It evaluates one component gradient per iteration, like the stochastic gradient method, and the paper proves that it nevertheless converges linearly in expectation. SAG was among the first of the variance-reduced incremental methods; SAGA (Defazio, Bach & Lacoste-Julien, 2014), SVRG (Johnson & Zhang, 2013) and their accelerated variants followed. Its predecessor, the incremental aggregated gradient method of Blatt, Hero & Gauchman (2007), selects the components cyclically and had a linear rate only for strongly convex quadratics, without an explicit constant.
This mission covers the paper's first main result, Proposition 1, which uses the step size . The second result, Proposition 2, for the larger step size , is a separate mission of this series.
Let and minimize
Each is convex and differentiable, and its gradient is Lipschitz continuous with constant : for all . The average is strongly convex with constant : the function is convex. Then has a unique minimizer . The gradient variance at the optimum is .
The SAG iteration with step size maintains a state . Starting from and the zero table , for an index is drawn uniformly from , independently of the past, and
The table is refreshed before the iterate moves, so uses the new gradient. Expectations are over the indices only; the data are fixed.
With the constant step size , for every ,
The constants are those printed in the paper.
The proof tracks a quadratic Lyapunov function with and an explicit block matrix (p. 19). The milestones, in the order the proof uses them, are:
Proposition 1 gives a linear rate for a method whose per-iteration cost does not depend on . Measured in passes through the data, its rate per pass is comparable to the full gradient method's, while each pass of SAG touches every component only once on average. The bound depends on the initial point only through and on the data only through , which is zero when every component is minimized at .
The result is proved in the paper and has been widely re-derived, but it has no machine-checked proof that this mission is aware of. A formalization would be the first verified linear-rate theorem for SAG. Lemma 1 is an exact identity, valid for every quadratic Lyapunov function of the same block form, and is reused verbatim in the proof of Proposition 2. Milestones 2, 3 and 7 are general facts (co-coercivity, completing the square, a Schur-complement domination) that recur throughout the analysis of incremental methods.
The iterate alone is not a Markov chain: its evolution depends on the stale gradients in the table, so neither nor decreases in expectation from one step to the next. The obvious first idea, bounding in terms of as for the stochastic gradient method, fails because the cross terms between the table error and the iterate error have no sign. The analysis must therefore control the table and the iterate jointly, through a function of the whole state ; the exact expected one-step change of a general quadratic form in (Lemma 1) is the computation everything else rests on, and it requires careful bookkeeping of block matrices.
is EuclideanSpace ℝ (Fin p) and the components are indexed by Fin n with . The components and their gradients are both given, tied by HasGradientAt; each is convex (§A.1, p. 13), which the proof's co-coercivity step needs; and are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. Strong convexity is stated literally as on p. 5, as convexity of . The point is any minimizer of ; uniqueness and are consequences. The restriction used in the proof is not assumed, since it follows from the hypotheses when .
The SAG state is a pair (table, iterate); SAG.SmallStep.step refreshes the table entry and then moves the iterate, and SAG.SmallStep.runFrom applies the steps for a given index sequence. The goal starts from the zero table and fixes the step size . The expectation is SAGA.Convex.expectIdx n k, the uniform average over all index sequences, which is exactly the law of independent uniform indices; a conditional expectation given is the average over the next index from an arbitrary current state. Block matrices are families of blocks (continuous linear maps), and Lemma 1 makes explicit the symmetry of and and the identity that its proof uses. The domination is stated for every : the page's closing remark "for " is stronger than its own computation needs.
The goal bounds the average over all index sequences; a bound for each fixed sequence would be false, and a bound for one sequence would be a different, weaker statement. Proposition 1 is not to be formalized with a free step size, an arbitrary initial table, or a variance quantity other than at : each of these changes the constant .
Needed infrastructure: algebra of finite sums of inner products over block families, the tower property for the uniform average over index sequences, co-coercivity of convex smooth functions (published on the platform as ConvexOptAlg.SmoothGD.eq_3_6), and strong-convexity monotonicity of the gradient. Proofs of individual milestones are welcome, as are alternative proofs of the goal that bypass the Lyapunov function.
Many problems in machine learning are finite-sum problems: minimize the average of loss functions, one per training example,
Two classical methods sit at opposite ends. Full gradient (FG) descent evaluates all gradients per iteration and converges linearly on strongly convex problems, at a cost proportional to per step. Stochastic gradient (SG) descent evaluates one gradient per iteration, independent of , but its error decreases only sublinearly, as .
Le Roux, Schmidt and Bach (arXiv:1202.6258, NIPS 2012) introduced the stochastic average gradient (SAG) method, which keeps the one-gradient-per-iteration cost of SG and attains a linear rate, as FG does. SAG was the first method of this kind and started the line of variance-reduced methods (SVRG, SAGA, Katyusha) that are now standard for finite sums.
The paper has two convergence results. This mission formalizes the second one, Proposition 2: when the number of examples is at least , SAG with the larger step size reduces the expected suboptimality by a constant factor per pass through the data, independently of the conditioning of the problem. Proposition 1 (step size , any ) is the subject of a separate mission.
Let with . The standing assumptions (p. 5, §3, and p. 13, §A.1) are:
Write and , the variance of the gradients at the optimum.
SAG. The state is : a table of stored gradients and an iterate . At iteration an index is drawn uniformly from , independently of the past, and
Warm start. Proposition 2 is about a specific run. The first iterations are stochastic gradient steps from with . SAG is then started from the average , with all set to and step size .
Lyapunov function. For parameters and , the proof uses
at , , .
If , the warm-started run satisfies, for every ,
The constant is the paper's own; the goal fixes it as printed.
In the order the proof uses them:
The result. Proposition 2 gives a rate per pass through the data, , that depends on neither nor once . On p. 6 the paper compares it with the FG rate and the accelerated FG rate . With , , , SAG iterations contract by at the cost of one FG iteration, while FG contracts by and accelerated FG by . The SG warm start replaces a constant proportional to by one of order , so the bound also captures the behaviour of the early iterations.
Formalizing it. The paper's proof is complete, and a machine-checked proof is new; no SAG statement exists on the platform. A formalization would check the paper's long appendix computation (pp. 23–29: a Lyapunov argument with completing the square on block vectors) and fix its slips: on p. 30 the proof writes , where its own Step 2 gives the factor , and the bracket that follows matches . Lemma 1 is shared with Proposition 1, and the SG bound of §A.3 is a standalone result (after Bach and Moulines, 2011).
The obvious approach does not work. SAG's update direction is a biased estimate of : the stored gradients were computed at old iterates. So the usual SG argument, an unbiased step followed by a bound on , breaks down. The proof instead tracks the joint state through a Lyapunov function that couples the table and the iterate, and it needs a function-value term to handle the large step . The one-step bound (pp. 24–28) is an inequality between quadratic forms in . It holds only after completing the square in the block, and it closes only under ; the margin there is small (). The domination step similarly minimizes over .
EuclideanSpace ℝ (Fin p), and the components are indexed by Fin n. and are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg.SAG.LargeStep.Assumptions. Strong convexity is stated in the paper's form: is convex. Each is convex (§A.1), and gradients are tied to the functions by HasGradientAt.Fin k → Fin n, weighted uniformly (SAGA.Convex.expectIdx), which is the law of independent uniform draws. A conditional expectation given is the average over the indices of one step from an arbitrary fixed state.hybrid draws indices. The SG phase uses the first , index is drawn and unused, and SAG uses the last , from with . The SG step sizes are .hybrid. Every hypothesis is satisfiable: , , , , .ConvexOptAlg.SmoothGD.eq_3_6) are reusable beyond this mission.Transient stability of a power grid asks whether the generators of the network return to synchronous operation after a large disturbance such as a fault or a line trip. In the classical network-reduced model the rotor angles obey second-order swing equations, and stability certificates usually come from energy functions evaluated numerically. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) relate this problem to a first-order system of coupled phase oscillators, the non-uniform Kuramoto model, and derive purely algebraic conditions on the network parameters under which the oscillators synchronize. Such conditions read as "the network connectivity dominates non-uniformity, losses and lack of phase cohesiveness" and are checked from the data alone, without simulation.
The paper gives two such sufficient conditions. This mission formalizes the second, Theorem V.5, which measures connectivity by the algebraic connectivity of the lossless coupling and therefore applies to sparse (connected, not necessarily complete) networks. A companion mission treats Theorem V.3, the condition for complete graphs.
Timeline. For the classical Kuramoto model, Jadbabaie, Motee and Barahona (ACC, 2004) and Chopra and Spong (IEEE TAC, 2009) analysed synchronization with the Lyapunov function , and Chopra and Spong proved frequency synchronization under cohesive phases. Dörfler and Bullo (2009–2012) extended the analysis to non-uniform time constants , phase shifts and non-complete graphs, using a weighted Lyapunov function.
There are oscillators with phases , time constants , natural frequencies , coupling weights and phase shifts (), with . The non-uniform Kuramoto model is
In this mission , and its non-zero entries induce a connected graph.
If , then
Lemma V.8 (the identity (36) that replaces by ), Lemma V.9 (a quadratic-form bound by ), the sinc estimate and the bound on the lossy coupling (p. 25), the Lyapunov-derivative bound (37), the sandwich bounds (39) on , the existence and uniqueness of from the analysis of (41), and the eventual entry of every trajectory into .
The condition is checkable from network data: of a weighted Laplacian, two vector norms and the extreme time constants. It applies to sparse networks, where the complete-graph condition of Theorem V.3 does not, and specializes for classical Kuramoto oscillators to (Remark V.7). Through the singular-perturbation argument of Section IV, conditions of this kind certify transient stability of the network-reduced power system.
The result is proved in the paper; no machine-checked version is known. A formalization fixes several points the printed text leaves loose: the norm is written on p. 23 with a double sum that counts each pair twice; the chain defining on p. 25 is printed with its inequalities reversed; and "reaches " holds only asymptotically. The formal statements make each of these precise.
The obvious Lyapunov function, , has a sign-indefinite derivative as soon as the differ, because the coupling is not symmetric. The weighted function restores a symmetric structure, but only through the non-obvious identity (36). After that, the sinusoidal coupling has to be bounded below by a quadratic form on a set where the phase differences stay below , the lossy coupling has to be bounded above uniformly in the state, and the resulting ultimate-boundedness argument has to be run with sublevel sets of , which are ellipsoids rather than balls of unless all coincide. The constants , , come from this mismatch, and the passage from sublevel sets back to balls is the most delicate step.
The prophet inequality of optimal stopping compares a gambler, who sees independent non-negative random values one at a time and must accept or reject each on arrival, with a prophet who sees them all in advance. Krengel, Sucheston and Garling showed that the gambler can secure , and Samuel-Cahn showed that a single threshold suffices. Since Hajiaghayi, Kleinberg and Sandholm (2007) and Chawla, Hartline, Malec and Sivan (2010), prophet inequalities have served as the approximation guarantees of sequential posted-price mechanisms: an online selection rule with a prophet guarantee turns into a truthful mechanism with a revenue guarantee.
The natural multi-choice generalization lets the gambler accept a set of elements, subject to a feasibility constraint. Kleinberg and Weinberg, Matroid Prophet Inequalities (STOC 2012, arXiv:1201.4764), proved that when the feasible sets are the independent sets of a matroid, the factor is still achievable, by an explicit threshold rule, and even when the order of arrival is chosen adaptively by an adversary.
Timeline:
Let be a finite ground set and a matroid; is its family of independent sets. For each a distribution on is given; the weights are independent with , and . Let and .
An online weight-adaptive adversary reveals the elements one at a time: it picks knowing but not . An online algorithm maintains a selected set and, when arrives with its weight, irrevocably accepts or rejects it, keeping independent. A threshold rule offers a threshold computed from the revealed prefix (and when ) and accepts iff .
The algorithm of the paper uses a ghost sample: an independent copy of the weights. Let be a -maximum-weight basis. For an independent set , among the partitions with and a basis, , denote one maximizing . The algorithm (9) sets
For every matroid on a finite ground set, every family of distributions on with finite means, and every online weight-adaptive adversary, the set selected by the algorithm (9) satisfies
The goal is stated for the paper's own algorithm, which is stronger than the existence statement of §3.
earns . 2. The identity behind (9) = (10), and the telescoping identity (Property (2) for ). 3. Lemma 1 (bijective basis exchange, and its weighted form), Lemma 2 ( is a maximum-weight basis of the contraction ), Lemma 3 ( is submodular on subsets of an independent set). 4. Inequalities (11) and (12), and Proposition 2:
pointwise in ; then Property (3) with for the thresholds (9).
The theorem gives the optimal constant: already for a rank-one matroid (choose one element) no online algorithm beats . It covers every matroid with one algorithm, including uniform, partition, graphic and transversal matroids, which model capacity, unit-demand and spanning-tree constraints. Through the reduction of Chawla et al., the paper derives from it order-oblivious posted-price mechanisms that are 2-approximations to the optimal revenue in single-parameter settings with matroid feasibility and, through the adaptive adversary, in multi-dimensional unit-demand settings (§6 of the paper). The decomposition through -balanced thresholds is reused in the paper for intersections of matroids, with factor .
The result has been proved since 2012; it has not been formalized. The mission produces a machine-checked development of the model (online adaptive adversaries, threshold rules, the ghost-sample expectations), of the general reduction (Proposition 1), and of the matroid facts the algorithm relies on, notably the bijective exchange lemma (Schrijver, Corollary 39.12a), which is not in Mathlib.
The obvious argument fixes the order of arrival and compares the algorithm with the prophet item by item. It fails here because the order is chosen adaptively from the revealed weights, so the set of elements still to come is random and correlated with the past. The proof must instead compare the algorithm's realized selection with a ghost optimum built from an independent sample, and bound the value the algorithm forgoes by the value the ghost optimum could still add, . The step that needs matroid structure is Property (3): the total threshold offered to any set that could still be added must be at most half of . The thresholds were computed along the history , not at the final , so the bound requires the submodularity of (Lemma 3) and a weight-dominating exchange between and in the contraction . Neither holds for general downward-closed families.
Fintype α; the matroid is Mathlib's Matroid α with ground set Set.univ; sets are Finset α; contraction is Matroid.contract.F : α → Measure ℝ, probability measures with F x (Set.Iio 0) = 0 (support in ) and Integrable id (F x) (finite means). The weight law is Measure.pi F, and every expectation is a Bochner integral over it. Finite means make , and the integrands of the thresholds integrable, so no expectation is a junk value.The goal fixes the thresholds by (9) through , and the ghost expectation; a statement in which the thresholds are free parameters assumed to satisfy (2)–(3) would be Proposition 1 and is not the goal.
Contributions are welcome at every level: the measurability of the online run, the exchange lemma for Mathlib matroids, the greedy characterization of maximum-weight bases of a contraction, and the probabilistic core (7) of Proposition 1. The matroid lemmas are reusable beyond this mission, in particular by the matroid-intersection mission of the same paper.
Random time changes occur when a process is observed on an operational clock rather than calendar time. In queueing models, for example, an arrival-count path may be evaluated at an evolving service clock. A functional limit theorem for the outer path and another for the clock are useful together only when evaluating one path at the times supplied by the other preserves convergence. Ward Whitt's 1980 paper studies several path operations with this question in mind; composition is its first main operation. The issue is specific to paths with jumps, because a small shift of the clock can move an evaluation across a jump.
Let be nonempty intervals of real time, with , and let be a complete separable metric space. The càdlàg path space consists of paths that are right continuous and have left limits on . Its subspace contains the continuous paths. The nondecreasing clock space consists of càdlàg real-valued paths on that are nondecreasing and take their values in . Its subspace contains the continuous, strictly increasing clocks. For and , composition is the path on .
Convergence uses the Skorohod topology. On a compact interval , let be the increasing homeomorphisms of and let . With denoting uniform distance, Whitt's metric is
Thus close paths may have nearby jumps at different times, provided an increasing time change aligns them. On a general interval, convergence is checked on compact subintervals whose endpoints are continuity points of the limit or endpoints of the full interval. Whitt gives this definition in §2, then gives , , and in §3. All subsets carry relative topologies and products carry product topologies.
For in and in , the first milestone states
The path-space definition and the two preparatory milestones are a small-oscillation partition for a càdlàg path, cited by Whitt from Billingsley, and Whitt's Lemma 2.2, which relates convergence on a compact interval to convergence on the two pieces made by splitting it at a continuity point.
The second case, and the combined goal, also allow the outer limit path to jump. Let mean the endpoints of that belong to . The corrected target is
The goal includes both cases for simultaneously varying and . The endpoint condition is vacuous for an endpoint excluded from . It is part of the strictly increasing clock case only; it imposes no extra restriction when the outer limit path is continuous.
This theorem supplies a precise condition for carrying two path limits through a random time transformation. In particular, the assertion includes convergence of the composed paths as elements of a càdlàg space, not merely convergence of their values at individual times. The distinction matters at jumps: pointwise convergence does not control the placement or ordering of nearby jumps. The result is a deterministic continuity statement that can be paired with probabilistic mapping theorems when the corresponding random paths are available.
Whitt proved the composition theorem in 1980, subject to the endpoint issue described below. The formalization work here is to construct its path-space interface in Lean, state the corrected continuity theorem with every domain condition visible, and eventually replace the open sorry proofs with checked proofs. The interface can also support the paper's later results on reflection, first passage, and time reversal; those results are separate missions. No proof of this mission's goal is claimed yet.
The tempting argument is to use separate continuity of and and then substitute into the first convergence. That argument loses control of evaluations near a jump of . A time change may align a jump of with the corresponding jump of , while the clock may cross those times differently. Continuity of the outer limit path removes that difficulty in one case; in the other, the clock must be continuous and strictly increasing. The source explicitly shows that composition is not continuous on all of (§3, p. 75).
The endpoints impose a further obstruction because increasing homeomorphisms of a closed time interval fix its endpoints. Bauer's Remark on p. 75 observes a failure at the right endpoint. There is a symmetric failure at the left endpoint, so the statement here includes both. This is a correction to the printed theorem, not a new claim that the uncorrected theorem is true.
Paths are represented as total functions , with only values on the named interval used. The domain assumptions OrdConnected and Nonempty express nonempty real intervals. The outer interval is also required to have nonempty interior: the formal convergence predicate checks only compact intervals with , so on a one-point it imposes nothing, and the case would fail for constant outer paths with different values. A clock's range condition is explicit, as is nondecreasingness for every prelimit clock. Membership of all paths in the relevant càdlàg spaces is part of the convergence predicates. The output predicate likewise requires every composition and its limit to be càdlàg. This rules out the trivialization in which one merely proves convergence of selected point evaluations or assumes the compositions already have the conclusion's path-space properties.
The compact uniform distance and the infimum over time changes take values in . They use the actual metric on , not a real supremum with a default value on an unbounded set. A time change is a total function whose restriction to the compact interval is continuous, strictly increasing, and onto. Continuity at a time means continuity relative to the path's interval. The general-interval convergence predicate checks the compact intervals specified by Whitt and requires each sequence member to belong to . The theorem is written as sequential continuity; Whitt's spaces are metrizable, making that equivalent to topological continuity. The real-valued clock space uses the relative topology inherited from real-valued càdlàg paths.
The endpoint correction is exact in the Lean statement. At the right endpoint, take , , for , and . Then is zero while . At the left endpoint, take , , , , and . The outer paths converge in on , but the compositions disagree at . Both examples show why continuity of at the image of every included endpoint is required in the case.
The development needs the càdlàg definition, metric and convergence predicates, compact restriction lemma, and the finite oscillation partition. Their definitions and lemmas are reusable for other functionals on path spaces. Contributions that prove the milestones and goal under the stated hypotheses are welcome. This mission does not formalize the Borel measurability or probability-measure machinery discussed elsewhere in Whitt's paper; Theorem 3.1 itself is a deterministic continuity claim.