Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Banks, insurers and planners who optimize under uncertainty need a single number that measures how bad the bad outcomes of an uncertain profit are. The value-at-risk, a quantile of the profit distribution, is the regulatory standard but ignores how far the worst outcomes fall below it and is not concave. The average value-at-risk (also called conditional value-at-risk, tail value-at-risk or expected shortfall) averages the worst -fraction of outcomes instead. It is concave, isotonic with respect to second-order stochastic dominance, and, through the minimization formula of Rockafellar and Uryasev (2000), it turns risk-averse stochastic programs into linear or convex programs. It is also the building block of most other version-independent risk functionals: distortion and Kusuoka representations write them as mixtures of average values-at-risk.
The axiomatic view goes back to Artzner, Delbaen, Eber and Heath (1999); the treatment of distributions with atoms, where several plausible definitions disagree, is due to Acerbi and Tasche (2002) and Rockafellar and Uryasev (2002). This mission follows Section 2.2.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, doi:10.1142/6478), pp. 48–58, together with Proposition 2.74 on p. 109.
All outcomes are profit variables: larger values are better. Let be a probability space and an integrable real random variable with distribution function and left-continuous quantile function
For the average value-at-risk is the lower-tail average
so that , and the average value-at-risk deviation is . When jumps at , the two levels
satisfy . Write and . Second-order stochastic dominance means for every nondecreasing concave for which both expectations exist; , are comonotone if for all .
In the Lean development, in the namespace RiskFunctionals.AVaR, these objects are distributionFunction, quantileFunction (both of the law P.map Y), averageValueAtRisk P Y α, avarDeviation P Y α, alphaPlus, alphaMinus, SSD and Comonotone.
For integrable and :
and, if is finite,
The goal is the conjunction of the five parts, stated as printed. is finite for every , and for exactly when is essentially bounded above; parts 3–5 presuppose it. At with not essentially bounded above, the attainment claim of part 1 is false (see Beyond the paper), so the goal as printed is expected to be disprovable there.
A strengthened variant of Proposition 2.37 drops the hypothesis that is nonconstant: for every average value-at-risk equals , and the book's argument never uses the hypothesis.
Two corrected variants address the endpoint . For integrable but not essentially bounded above (for instance exponential), for every , so the maximum in (2.19) is not attained; likewise for every , so the minimum in (2.112) is not attained. The corrected Theorem 2.34 asserts part 1 only when is finite, and the corrected Proposition 2.74 adds the same hypothesis; both leave everything else unchanged.
Theorem 2.34 is the toolkit through which the average value-at-risk is used. Representation 1 makes it the optimal value of a one-dimensional concave maximization, which is how it enters stochastic programs and the newsboy-type models of Examples 2.39–2.40. Representation 2 exhibits it as an infimum of linear functionals over an explicit dual set, which yields concavity, -Lipschitz continuity and the link to the general dual representation of acceptability functionals. Representations 3–5 are the computational formulas for discrete distributions, where the naive "average of the outcomes below the quantile" is wrong. Proposition 2.36 shows that the family characterizes second-order dominance, and Proposition 2.74 identifies the deviation as a minimal-loss functional.
The results are classical and proved in the literature. What the mission adds is a machine-checked version in the book's conventions: profit variables, the lower tail, the left-continuous quantile, the dual set in with bound , and general distributions with atoms. The platform holds related results in other conventions: the Rockafellar–Uryasev minimization formula for loss functions and upper tails, an open loss-side dual representation on , and expected-shortfall properties on finite state spaces; none states these representations for profit variables on a general probability space.
Everything happens where has an atom at . A proof that pretends is continuous, so that , covers none of the cases the theorem was written for: the optimal dual variable must put a fractional weight on the event , and representations 4 and 5 differ from each other precisely by the jump. Passing between integrals over , integrals against the law, and Lebesgue integrals of the quantile function over needs the quantile transform for arbitrary distributions. The endpoint is genuinely different: there may be infinite and the maximum in (2.19) and the minimum in (2.112) are then not attained: the book's statements fail there, and the corrected variants carry the finiteness condition.
A random variable is a measurable, integrable on a probability space; is computed from the law of and so depends only on its distribution. The quantile function is real-valued; wherever it is evaluated at a point , the statement assumes for some . Maxima and minima are stated as attained greatest and least elements of the value sets, never as bare suprema or infima. In the dual representation ranges over measurable functions with and almost surely. Conditional expectations given an event are integrals against the conditional probability measure; when the event is null its coefficient is as well. The limit at is taken in the extended reals, since may be .
A trivializing formalization is ruled out: writing (2.19) or (2.20) with sSup/sInf and no attainment, or using an upper-tail, loss-side conditional value-at-risk in place of the book's lower-tail functional, would change or empty the statement; neither is done.
Contributions welcome: the quantile transform for general laws, the change of variables between , the law and , and the Rockafellar–Uryasev argument are reusable across the rest of this series (Kusuoka and distortion representations, nested average value-at-risk).
Risk measures used in portfolio optimization, insurance pricing and regulation are almost always law invariant: they assign a number to a random profit that depends only on its distribution, not on the scenario in which each outcome occurs. Kusuoka (Kusuoka 2001) showed that on a non-atomic space every law-invariant coherent risk measure is the worst case, over a family of weightings, of mixtures of one elementary functional, the average value-at-risk (also called conditional value-at-risk or expected shortfall). This reduces the design and the computation of law-invariant risk measures to the choice of a set of probability measures on the interval of confidence levels, and it underlies the use of the average value-at-risk as the building block of spectral and distortion risk measures.
This mission formalizes the version of Kusuoka's theorem proved in G. Ch. Pflug and W. Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, §2.2.4, Theorem 2.45), stated for acceptability functionals of profit variables on , , together with the coupling and realization results its proof uses and a worked example from the same section.
Let be a probability space. It is non-atomic if no measurable set with has only subsets of probability or . Fix and the conjugate exponent , ; is the space of real random variables with finite -th moment (identified when equal almost surely) and its dual, paired by .
For with distribution function , the quantile function is , , and the average value-at-risk at level is the lower-tail average
The book uses profit variables, so larger values are better and averages the worst -fraction of outcomes; .
A real valued is an acceptability functional if it is translation equivariant, (A1), concave (A2), and monotone, a.s. (A3). It is version-independent if whenever and have the same distribution. A dual representation is
and is version-independent if equally distributed are both or neither in , with . Theorem 2.45 adds the conditions (C1) , (C2) every is non-negative, (C3) every has .
Under (C1), (C2) and (C3) there is a family of probability measures on , fixed independently of , such that for every
and in general with an additional penalty and in the second integral.
The result. The Kusuoka representation says that the average values-at-risk are the extreme points of law-invariant acceptability: any such functional is determined by a set of mixing measures on the confidence levels. Consequences used in the rest of the book and in the literature include the identification of comonotone additive functionals with single mixtures (Choquet representations), explicit representations of mean–deviation functionals such as (2.41), and the reduction of optimization problems with law-invariant risk constraints to families of average value-at-risk constraints. The statement for , rather than for bounded variables, is what makes it applicable to models with unbounded returns.
Formalizing it. The theorem is proved in the book and in the literature; it has not been machine-checked. Formalizing it requires infrastructure that is reusable beyond this mission: the quantile function and the average value-at-risk on , the realization of a prescribed joint law on an arbitrary non-atomic probability space, and the Hardy–Littlewood-type rearrangement inequality behind the antimonotone coupling. Related platform results are in other conventions: a distortion functional of losses on as a single mixture of average values-at-risk (MultistageStochastic.distortion_avar_mixture, proved) and Schmeidler's comonotonic characterization on finite uniform spaces (RiskUncSets.Distortion.theorem_4_1, open). Neither covers the infimum over a family, profit variables, or .
The obvious argument is to write each as a mixing measure directly. This fails because depends on the joint law of , not on the two marginals; the infimum must first be reduced to antimonotone couplings, which requires (a) that every coupling of the two marginals can be realized on the given space without leaving , using version-independence of both and and non-atomicity, and (b) the extremal property of the antimonotone coupling for products of an and an variable, where quantile functions may be unbounded at both ends. The passage from to a mixing measure is a Stieltjes integration by parts on that must handle a point mass at , and the integrability of , which tends to the essential infimum of (possibly ) as . Non-atomicity cannot be dropped: the book's Counterexample on p. 63 is a version-independent functional on a two-point space without representation (2.37).
Probability spaces are (Ω, ℱ, P) with IsProbabilityMeasure P; non-atomicity is the book's notion (no atoms), which is stronger than Mathlib's NoAtoms. Random variables are elements of Lp ℝ p P with 1 ≤ p, p ≠ ⊤, and dual variables elements of Lp ℝ q P with p.HolderConjugate q. The quantile function is the left-continuous inverse of the book's (1.3), evaluated only on or inside integrals over ; is the lower-tail average (2.15), not the upper-tail loss CVaR. Version-independence is "equal laws give equal values" (IdentDistrib). Every infimum is stated as a greatest lower bound in (IsGLB), which forces the indexing set to be nonempty and bounded below; measures on are measures on with no mass outside . The family is quantified before : a family allowed to depend on would reduce (2.37) to matching the single number by some mixture, a much weaker statement, and that reading is excluded. Each representation also asserts that every integrand is integrable against every measure of the family, so that no integral can take Lean's default value .
Beyond the paper. Two variant items accompany the goal. kusuoka_representation_strong ([Strengthened]) drops (C2) and (C3): for a real valued acceptability functional they follow from (A1), (A3) and the dual representation, since for every forces (constants) and (scaled indicators). kusuoka_representation_probe ([Sharpness probe]) drops non-atomicity; it is expected to be false by the p. 63 Counterexample, and a disproof is the sought outcome. The printed proof of Theorem 2.45(iii) has a sign gap (it derives ); the statements (iii) and (iv) are kept as printed.
Contributions welcome: the quantile transform and realization of joint laws on non-atomic spaces, the rearrangement inequality on , and the integration-by-parts construction of the mixing measure, each of which can be submitted as a separate lemma.
A risk measure that returns a single number answers the question "how acceptable is this random profit, seen from today?". Multi-period decision problems — portfolio rebalancing, insurance reserves, stochastic programs on scenario trees — need the same question asked at every later date, given the information available then. The answer is no longer a number but a random variable measurable with respect to the information available at that date. Section 2.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific, 2007, doi:10.1142/6478), sets up these conditional acceptability mappings axiomatically and gives them a dual representation modelled on the defining relation of the conditional expectation. The conditional average value-at-risk defined there is the building block of the nested risk measures used in multi-stage stochastic optimization (Chapter 3 of the same book), and of the time-consistent risk measures of Ruszczyński and Shapiro (doi:10.1287/moor.1060.0204) and Detlefsen and Scandolo (doi:10.1007/s00780-005-0159-6).
Let be a probability space and a sub--field, the observable information. Fix and let be its conjugate exponent, . Put and , the subspace of classes with an -measurable version. Random variables equal almost surely are identified, and every (in)equality between them holds almost surely. Variables are profits: larger is better.
A map is a conditional acceptability mapping if for all
It is positively homogeneous if for , and upper semicontinuous if, for every , the real functional is upper semicontinuous on . For and the dual function is
For and , the conditional average value-at-risk is a class in such that, for every ,
When is trivial it reduces to the lower-tail average of the left-continuous quantile function of .
For an upper semicontinuous conditional acceptability mapping , every and every ,
and if is positively homogeneous then takes only the values (on ) and (off ), and
Further items of the section, stated faithfully but not milestones:
Theorem 2.51 says that a conditional acceptability mapping is determined by the family of real concave functionals , and that each of these is an infimum of expectations under densities whose conditional expectation is . It turns the axioms (CA1)–(CA3) into a computable object: a dual set, one per observable event, which is what stochastic programs with conditional risk constraints actually optimize over. The converse direction (Theorem 2.52 and Example 2.53) is how the book manufactures conditional versions of the average value-at-risk and of other dual-representable functionals, and Proposition 2.57 lists the properties used later when these mappings are nested over a tree.
None of these results is formalized. Mathlib has conditional expectation, spaces, Hölder
duality and the Hahn–Banach separation theorem, but no Fenchel–Moreau theorem on and no
conditional risk mappings. Prove2Me poses, as an open problem, Ruszczyński and Shapiro's
representation of lower semicontinuous conditional risk mappings
(CondRiskMap.Repr.theorem_1); it is stated pointwise in on abstract paired spaces with
loss variables, not in the integrated form over events used here. Two of the printed statements are false as stated, and the mission
records this: see Beyond the paper below.
The obvious route to (2.45) applies the Fenchel–Moreau theorem to and then shows that the dual function is off the constraint set. The first step needs the biconjugation theorem for concave upper semicontinuous real functionals on , with the dual identified as , for every including where the dual is ; none of this is in Mathlib. The second step must handle the constraint as an equality of conditional expectations, not of expectations. For Theorem 2.52 the natural argument builds a measure on from the infimum and takes its Radon–Nikodym derivative; the additivity of that set function is exactly what fails for general .
is Lp ℝ p P with 1 ≤ p, p ≠ ∞, and is Mathlib's subspace
lpMeas ℝ ℝ m p P of classes a.e. equal to an m-measurable function, where m ≤ mΩ is
; the dual exponent is given by p.HolderConjugate q. Pointwise axioms are almost
sure. is Mathlib's P[Z|m]. Every infimum, and the dual function
, is computed in EReal, so an empty constraint set gives , an unbounded one
, and no infimum has a junk value; the difference always has a
real first term. Upper semicontinuity is that of the real functionals indexed by ,
as the book defines it — reading it as upper semicontinuity of the map into , or
replacing the infimum by an unconstrained one over all of , would change the theorem. The
conditional is a predicate on classes in , never a construction:
its existence is a stated result, not an assumption. Profits, not losses: the lower tail is
averaged. Version-independence (Definition 2.55, used in Proposition 2.57(i)) is stated
pointwise: the conditional is almost surely one fixed function of the
conditional distribution function of (2.56), for every .
Needed infrastructure: the Fenchel–Moreau theorem on , the – duality pairing, and Radon–Nikodym on a sub--field. All three are reusable well beyond this mission.
Beyond the paper. Two corrected variants are posed beside the faithful statements. Theorem 2.52, corrected (findings F1, F2) adds that is bounded in and closed under pasting along ; without pasting, on makes the right side of (2.50) non-additive in , and without boundedness with makes it . Proposition 2.57, corrected (finding F3) replaces the second inequality of (2.58), , which fails on two equally likely points with , trivial, full and , by . Disproofs of the faithful Theorem 2.52 and of the faithful Proposition 2.57 are welcome contributions, as are proofs of the variants.
Risk functionals assign a number to an uncertain profit and are used as objectives and constraints in portfolio selection, insurance and energy planning. Since the axiomatization of coherent risk measures by Artzner, Delbaen, Eber and Heath (Math. Finance 1999), the standard way to understand such a functional is through a dual representation: the functional is written as a worst case of expectations under a family of probability densities, penalized by a convex or concave function of the density. Föllmer and Schied (Finance Stoch. 2002) and Ruszczyński and Shapiro (Math. Oper. Res. 2006) established this representation for convex risk measures on and on paired spaces. Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007), develop the same theory on the profit side, for acceptability functionals (larger is better) and deviation risk functionals, on spaces. Section 2.2 of their book recognizes these functionals by their dual representations. This mission formalizes that section and the conjugate duality of Appendix B it rests on.
Let be a non-atomic probability space: no measurable with has every measurable subset of probability or (the book assumes this throughout). Fix and with . Write and , paired by
A functional is a map ; constants are constant random variables. An acceptability functional satisfies
Positive homogeneity (A4) is for , and strictness (A5) is . A deviation risk functional satisfies (D1) , (D2) convexity, and (D3) . The acceptance set of is , and a set defines .
The concave conjugate and the convex conjugate are
and . A convex-type is proper if everywhere and somewhere; a concave-type is proper if is.
A proper upper semicontinuous acceptability functional satisfies, for every ,
and conversely, a functional represented in this form by any proper functional in place of is upper semicontinuous and satisfies (A1)–(A3). Up to semicontinuity, acceptability functionals are exactly the penalized infima of expectations under probability densities.
Further items, not milestones: the first sentence of Theorem B.1 ( is the largest l.s.c. convex minorant of a proper ) and the deviation half of Corollary 2.32, representation (2.12), each stated as printed.
The corollary is the profit-side, form of the dual representation of convex risk measures. It turns a property of a functional into a constraint on its dual domain. Translation equivariance becomes the requirement that the densities have mean one, and monotonicity becomes the requirement that they be nonnegative. This is how later chapters of the book compute with the average value-at-risk, distortion functionals and multi-period functionals: each is specified by its supergradient set. A machine-checked version gives these computations a common, verified foundation.
The results are classical and proved on paper; none is formalized in this form. The platform holds a loss-side analogue on abstract paired spaces with signed-measure duals (ConvexRiskFn.Dual.theorem_2_2) and a Fenchel–Moreau theorem in the same setting (ConvexRiskFn.Dual.theorem_2_1). Neither states the /, profit-side, density-constrained representation (2.11). Formalizing the chapter also checks its statements: three printed statements are false as written, and the mission poses a corrected form beside each faithful one.
Representation (2.11) needs the Fenchel–Moreau theorem in infinite dimension, for an extended-real concave functional, on with dual . That requires Hahn–Banach separation of a closed convex hypograph and the identification of the dual of , and Mathlib provides only parts of the latter. Upper semicontinuity in the norm topology must be converted to weak semicontinuity, and the value must be handled throughout. Example 2.28 of the book shows that dropping upper semicontinuity breaks the representation, so the hypothesis cannot be avoided. The restriction of the infimum to densities with , is a separate step: one must show that every other has . The first sentence of Theorem B.1 fails as printed when has no continuous affine minorant, so the natural "largest l.s.c. convex minorant" route to the biconjugate needs care.
Functionals are EReal-valued maps on Mathlib's Lp ℝ p P, with p ≠ ⊤, [Fact (1 ≤ p)] and [p.HolderConjugate q]. The pairing is the Bochner integral of , integrable by Hölder's inequality. Conjugates are EReal suprema and infima over the whole space, so they are never a junk default. (A2), (D2) and (A4) are written as the book's inequalities in EReal, where . Non-atomicity is the book's atom definition, which is stronger than Mathlib's NoAtoms. Semicontinuity is for the norm topology. "Proper" follows the concave or convex notion of Appendix B. The book's abstract dual pair is instantiated as with , the example it gives itself.
A trivializing formalization would take the infimum in (2.11) over all of (Fenchel–Moreau alone), or replace by a real-valued function and so discard the values that encode the constraints. The goal does neither: the infimum ranges over the densities, and is the EReal conjugate.
Beyond the paper. There are three variants, each a corrected statement beside its faithful one:
deviation_representation_corrected (F1): (2.12) prints where is meant. For and , , but gives .fenchel_moreau_largest_corrected (F2): Theorem B.1's first sentence needs . For on , is not the largest l.s.c. convex minorant.acceptabilityOfSet_properties_corrected (F3): Proposition 2.27(i) needs a monotone (a closed set built from line segments gives but ), and (v) holds only for ().A complete development needs Fenchel–Moreau for extended-real functionals on , the duality for , and coupling constructions on non-atomic spaces for version independence. All of these are reusable well beyond risk theory. Contributions of any of these pieces, or proofs of the corrected variants, are welcome.
A switch or wireless network can have several queues ready for service while its hardware permits only certain combinations to be served together. A scheduler must choose a feasible combination repeatedly as new packets arrive. The question is whether this local sequence of decisions keeps the queue process stable whenever the arrival rates fit within the network's service capacity. Kelly and Yudovina formulate this question for finite service schedules and independent Poisson arrivals in §7.8 of Stochastic Networks.
MaxWeight scheduling gives larger queues greater influence over the choice of schedule. An exponent controls how strongly queue length affects priority. The chapter's target is a stability guarantee for every positive exponent, rather than a guarantee confined to the familiar linear weighting. The supplied Lecture Notes PDF states this as Theorem 7.13, printed page 180, and develops supporting analytic questions in Appendix D.
Let be a finite nonempty set of queues. A schedule is a vector describing how many packets each queue can serve in one time slot. The feasible schedule family is finite and nonempty. It is downward closed: reducing any schedule coordinate leaves a feasible schedule. This includes the possibility of unused service when a selected queue has fewer packets than the schedule permits.
The admissible region is
It describes arrival rates dominated by an average of feasible schedules. The interior used here is the ordinary interior in .
Fix . At queue vector , a schedule is drawn from a fixed probability distribution supported on the maximizers of . New arrivals in the slot are independent Poisson variables of means , independent of the scheduling randomization and the past. The next queue vector is
These laws specify a homogeneous Markov chain on the countable state space . They follow the general model in §7.8 and the explicit empty-queue convention in Example D.4, printed page 213.
The goal is Theorem 7.13: for , the MaxWeight- queue chain is positive recurrent. In return-time notation,
This retains every positive value of and the full queue process.
Three supporting targets are selected from the same supplied source. Proposition D.1 states the Foster–Lyapunov criterion for an irreducible countable chain and an arbitrary finite exception set. A nonnegative function with drift at most outside that set and at most inside it yields finite expected return to the set from every starting state and positive recurrence.
Exercise 7.18 concerns the weighted drift
It asks for constants and finite such that
Exercise D.1(3) asks for finite moments of , where is a finite service bound and is Poisson, and for the tail term
to tend to zero as for fixed . The source locations are printed pages 210–211, 182, and 214–215 respectively.
The recurrence conclusion concerns repeated operation over an unlimited number of slots. It asserts a finite mean return time to each queue state under the specified policy. It does not require an explicit formula for the stationary distribution, nor does it prescribe a numerical delay guarantee. The result therefore identifies a capacity regime in which this queue-based scheduling rule is stable, while leaving performance within that regime as a separate question.
The formalization contribution is the connection between a concrete random scheduling transition law and recurrence on an infinite state space. Its reusable components include the capacity region of finite schedules, capped-service queue transitions, extended return expectations, and the Poisson envelope estimates. The textbook presents the theorem as an established result with a proof sketch. The theorem items here are statements awaiting proofs; compilation verifies their Lean syntax and types, not their mathematical proofs.
Negative drift by itself is insufficient for the recurrence conclusion. The distinctions between negative drift, drift bounded away from zero, and control of upward increments matter in the chapter's discussion, printed pages 180–181. Arbitrary positive real exponents also require attention at empty queues and to unbounded Poisson arrivals.
The sketch's equality between actual departures and a chosen schedule fails when a positive queue is shorter than the proposed service. This is a proof gap, not a counterexample to the stability theorem. Appendix D additionally switches between conditioning on the full vector and conditioning on one coordinate in (D.5). Those conditional expectations need not agree for coupled schedules. The selected statements retain actual capped departures and avoid relying on that ambiguous display. Completing the analytic link to the goal remains part of the proof task.
Queue and schedule coordinates are natural numbers, rates are nonnegative real numbers, and the exponent is an arbitrary positive real. The schedule family is a finite set of vectors. Random tie rules are stationary probability kernels supported on the maximizing schedules; the source specifies no particular distribution among ties. The norm in Exercise 7.18 is made Euclidean explicitly. Constants there are chosen before the queue vector is quantified, so they cannot depend on the current state or time.
Return times are represented by extended nonnegative sums of survival probabilities. Consequently, an event of never returning has infinite expected cost. Real drift sums have explicit absolute-integrability conditions. In the queue drift and Poisson moment items, integrability is a conclusion, not an assumed substitute for analysis. The Poisson tail term is an unconditional tail integral, including when its conditioning event would have probability zero.
No selected statement contains an unspecified term or a high-probability claim; there are therefore no numerical asymptotic constants to instantiate. Exercise D.1 is included only through its explicitly numbered part (3). The remaining parts, (D.5), congestion-control optimization results, and the switch-specific matching example are outside this mission's theorem list. No variants are posed.
Stability is not defined as negative drift, and the goal is not restricted to or a finite truncation of the queue space. Mathlib supplies probability mass functions, product measures, Poisson laws, real powers, and topology. The local definitions supply the scheduling and recurrence interfaces needed to state the targets.
ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a; correspondence with a particular published printing has not been verified.Stations sharing a communication channel must decide when to transmit. If nearby stations transmit together, their signals may interfere; if they all wait, capacity is wasted. A central scheduler can coordinate activity, but distributed access assigns decisions to individual stations. The mathematical question is whether simple random local decisions can supply all the service combinations that the interference constraints permit. This mission concerns the idealized continuous-time model in Section 5.4 of Kelly and Yudovina, Stochastic Networks, using the supplied Lecture Notes PDF.
The model isolates a capacity question from implementation issues. Stations sense active neighbors immediately, so collisions do not occur. Transmission durations and attempt clocks are exponential. The question concerns the equilibrium activity of this process for fixed parameters. Delayed sensing, packet queues, and parameter adaptation require additional results and are outside the theorem's claim.
An interference graph is a finite simple undirected graph whose vertices are stations. An edge means that its two endpoints cannot transmit together. Write for the station set and for the set of binary activity vectors satisfying this restriction. The value means that station is transmitting. The all-zero vector is always feasible.
Each station has a finite real parameter . An active station stops transmitting at rate . An inactive station starts at rate when all its neighbors are inactive. These transitions define a continuous-time Markov chain on . Its generator is , with negative total outgoing rates on the diagonal, and its transition matrices are for .
A distribution on feasible schedules offers mean activity at station . The capacity region includes every nonnegative arrival vector that some such distribution can dominate:
This definition permits arbitrary distributions on feasible schedules. The random-access process produces a much more specific family, indexed by one real number per station.
Equation (5.8) identifies the stationary distribution of the specified chain:
The goal is Theorem 5.17, printed page 126 of the supplied PDF. Every arrival vector in the ordinary interior of has strictly smaller coordinates than the equilibrium service vector for some finite parameters:
Three Appendix C milestones supply the accompanying optimization statements. For a convex objective and componentwise convex constraint map on a convex set , Theorem C.7 asserts convexity of the extended value function . Theorem C.3 supplies a nonvertical support at an interior point of its finite-value domain. Theorem C.4 states the equivalence between such support and the strong Lagrangian principle for equality constraints, with
The faithful C.4 statement is retained without an unprinted finiteness hypothesis. Its infinite-value defect and the separately labelled correction are described below. The goal itself retains the source's strict service inequalities.
The capacity theorem says that the exponential random-access family does not leave a gap inside the region attainable by arbitrary mixtures of independent schedules. It provides a service margin in every coordinate at once. Its quantifiers allow the parameters to depend on the graph and arrival vector, but require every parameter to remain a finite real number. The theorem does not provide a uniform parameter bound as the arrival vector approaches the boundary.
The known mathematical result is attributed to Jiang and Walrand in the supplied source. The formalization target is a checked statement of that result and its supporting mathematical interfaces. The proposal's theorem declarations remain proof tasks. The finite exclusion process, its invariant law, and the distinction between feasible schedule mixtures and exponential-family marginals are reusable in later work on scheduling. The extended-value optimization layer can also support problems unrelated to communication networks.
Normalizing positive exponential weights only constructs a probability distribution. It does not establish that the distribution is invariant under the given dynamics, nor that its marginal vectors cover every strictly feasible demand. Changing one station's parameter changes the other stations' equilibrium opportunities through interference. Coordinatewise scalar tuning therefore does not settle simultaneous coverage.
The optimization statements require care at infeasible and unbounded problems. A real-valued infimum with a default value would conceal these cases. In particular, the literal C.4 equivalence fails for an empty domain: both primal and Lagrangian infima are , but no finite-height hyperplane touches that value. This is an issue with the unrestricted statement, not a new hypothesis for the capacity theorem.
Stations are indexed by Fin d, and activity coordinates by Fin 2. Simple graphs enforce symmetry and exclude self-interference. A decidability instance is computational bookkeeping for a finite adjacency relation. The empty station set is permitted: it has one empty schedule, and the service conclusion has no coordinates. For one station the mean activity is . All normalizing sums are finite and strictly positive because the empty schedule contributes weight one.
Interior means ambient Euclidean interior. Arrival vectors in the closed region alone are insufficient: at the one-station boundary demand , no finite parameter supplies service greater than one. Finding F1 records this sharpness example; no extra sharpness item is posed.
The CTMC is represented by its finite generator and matrix-exponential transition semigroup. Its stationary-law theorem asserts invariance for every nonnegative time. Optimization infima use EReal, so infeasibility gives and unboundedness below gives . Convexity is expressed through the real epigraph; supporting affine functions have real heights and slopes. Slack elimination in (C.2) preserves the inequality . No asymptotic constants or failure probabilities require instantiation in these targets.
Beyond the paper. The single corrected variant of C.4 adds exactly that is finite. Finding F2 gives the empty-domain counterexample to the unrestricted equivalence and the supporting argument for the correction. The original remains the milestone anchor. Findings F3 and F4 separately record the slack-multiplier sign error on printed page 209 and the word “maximized” in the minimization argument on printed page 127; neither changes the goal or creates a variant.
The definitions have concrete mathematical bodies without proof placeholders. The theorem types expose their defining formulas for independent auditing, and use Mathlib's finite sums, graph types, topology, convexity, extended reals, and matrix exponential. A formulation that assumes the desired service vector or proves only normalization would not capture this mission.
Food-borne outbreaks are traced slowly: when contaminated produce reaches shelves, the source is often unknown for weeks, and retailers recall everything. Traceability technology (for example blockchain ledgers) identifies the contaminated source at once, so only its units are discarded. Regulators and large retailers have pushed for it, and the intuitive view is that every member of the chain gains. Dong, Jiang & Xu (Management Science, 2022) show in a three-tier pricing game that this is not so: the chain's most powerful member, the retailer, can earn less in equilibrium with traceability than without it. The reversal happens for an explicit interval of retail prices, under an explicit condition on the primitives.
A retailer sells units at an exogenous retail price . She buys them at a wholesale price from one tier-1 supplier, who buys one unit at a procurement price from each of tier-2 suppliers (farms). Each farm produces at unit cost and is contaminated independently with probability , or if it exerts a risk-reduction effort at cost , where and . Assumption 1 of the paper is . A farm's survival probability is with effort and without.
Tier-1 earns (expected units sold) and the retailer (expected units sold); expected units sold are in Case N and in Case T. The retailer chooses , tier-1 then , and the farms then choose effort simultaneously. The solution concept is subgame-perfect Nash equilibrium (SPNE) with the paper's selection rules: the Pareto-dominant tier-2 equilibrium is played; an indifferent farm exerts effort; an indifferent tier-1 or retailer induces effort; an agent with zero profit still trades.
The paper solves both games in closed form. With , the effort thresholds of the retail price are
and the retailer's profit on the relevant branches (Tables EC.1–EC.2) is , and , with and . The paper's Definition 1:
DEFINITION 1 (BREAK POINT CRITERION). The Break Point Criterion (BPC) is satisfied if traceability adoption decreases the retailer's equilibrium profit when the retail price is at the effort threshold with traceability, i.e., .
Under the standing assumptions and BPC there exist with
such that both games have an SPNE at every retail price, and for all SPNE , at ,
where , are the retailer's equilibrium profits.
In proof order: Lemma 1 (tier-2 equilibrium, Case N, p. 9); Lemma 2 (tier-1's optimal price, Case N, p. 10); Proposition 1 (SPNE, Case N, p. 11); Lemma 3, Lemma 4 (Case T, p. 13); Proposition 2 (SPNE, Case T, p. 14); Lemma 5 (BPC implies and , p. 21).
The variant proposition_3_strong adds strict increase with traceability on
, where , and equality on
.
Proposition 3 is the paper's headline result (Abstract, p. 1): removing the cascade threat does not make every member better off, and the losses concentrate on retail prices around the traceability effort threshold . It underlies the paper's later welfare discussion (Observation 1, Proposition 4), where every member is worse off on part of the interval, and the policy point that adoption may need subsidies or contract adjustments.
The result is proved in the paper, partly in sketch form; none of it is formalized. A formal development produces the first fully specified multi-tier pricing-and-effort game on the platform: an -player effort game with a selection rule, two nested best-response problems with tie rules, and subgame-perfect equilibrium as a predicate, together with a welfare comparison stated on equilibria rather than on formulas.
Each step is elementary, but the equilibrium has to be established, not assumed. The tier-2 stage is an -player game in Case N whose equilibria above can be multiple (a stag hunt), so the selection rule matters. Tier-1 and the retailer optimize a margin whose effect on effort is a step function of the price; their maxima are attained only because the thresholds are closed and the tie rules settle the boundary, and they must be identified among all real prices. The final comparison is between two piecewise-linear functions with different breakpoints in the two cost branches. The paper prints no proof of Lemma 5, Lemma 4 or Proposition 2, and Proposition 3's printed proof is a short sketch that treats the high-cost branch as "similar".
Everything lives in the namespace FoodTrace.Adoption (definition module
Def_FoodTrace_Adoption_Model). Conventions:
Params = (n, ρ, ρe, e, cp); Standing collects , ,
, , , and Assumption 1. The implicit hypotheses
, , , are made explicit.Bool per farm; profiles are Fin n → Bool, with no symmetry built in.none with profit 0; prices range over all of .cpLow, is cpBar.The retailer's profit in the goal is her payoff at an SPNE of the game, not the closed forms of Tables EC.1–EC.2; the goal asserts the existence of SPNE in both games at every retail price, so the comparison over all equilibria is not vacuous; and BPC is satisfiable (the Figure 4 instance , , , gives ).
Beyond the paper. One variant is posed beside the faithful goal: proposition_3_strong
(strengthened, finding F2), the exact sign pattern above. Evidence: a four-region comparison of
the equilibrium profits, confirmed at 1.87 million sampled retail prices on 18,820 random BPC
instances in both cost branches.
Needed infrastructure: finite products and sums over Fin n, real inequalities with powers, and
case analysis on Option. The equilibrium layer (selection, best responses with tie rules, SPNE as
a predicate) is reusable for other sequential supply-chain games. Proofs of the stage results
(Lemmas 1–4, Propositions 1–2) and of Lemma 5 are welcome as independent contributions.
Food delivery platforms such as Uber Eats, DoorDash and Meituan let a restaurant serve customers who never enter it, but they also charge those customers a delivery fee and share the restaurant's kitchen with its walk-in trade. Whether the platform helps or hurts the restaurant is a question restaurant owners, platforms and regulators all ask. Chen, Hu and Wang (Management Science, 2022) answer it in a stylized game: a restaurant whose kitchen is a queue, a platform that sets a fee, and two kinds of customers who decide where to eat by comparing expected waiting costs. Their first main result, Proposition 1, describes how the equilibrium changes as more customers become able to order through the platform: below a critical mass nothing changes for the restaurant, and at the critical mass the restaurant abruptly turns into a delivery-only kitchen. The analysis builds on the unobservable-queue joining games of Edelson and Hilderbrand (1975) and Hassin and Haviv (2003).
A kitchen serves meals at rate . At total joining rate the expected wait for food is . A meal is worth to a customer. Walk-in customers pay the food price and incur waiting cost rate ; food-delivery customers pay plus the delivery fee and incur the smaller waiting cost rate . Their expected utilities are
and balking gives . Tech-savvy customers arrive at rate and may walk in, use delivery or balk; traditional customers arrive at rate and may walk in or balk. The delivery-worker pool is unlimited and costless.
A customers' equilibrium under is a profile of joining rates with in which every option used by a positive rate is a best reply at , and an arrival stream that does not fully join is no better off joining. Ties between delivery and walking in at go to delivery. The game has three stages. The restaurant sets . The platform then sets to maximize . Finally customers play an equilibrium. The restaurant maximizes , where . A subgame-perfect equilibrium (SPE) combines a customers' equilibrium after every , a best-response fee after every , and an optimal price . Its outcome is , , , , , and the social welfare , the total surplus of all stakeholders.
Assume , , , . There is such that for every there are and an SPE for every whose outcome, viewed as a function of , satisfies the following. With if and otherwise:
The thresholds are existential, as printed. The milestones pin them to the values the proof constructs: is the root of in , , is the smallest root of , and has a closed form (Online Appendix p. 23).
The paper's own chain (Online Appendix C.1): Lemma C.2 (customers' equilibrium), Proposition C.3 (platform's best response), Corollary C.2 (restaurant's profit curve), Lemmas C.6–C.8 (the three profit curves, their maxima and intersections), Proposition C.4 (restaurant's optimal price), and Corollaries C.3–C.4 (platform profit and welfare in equilibrium). "We have Proposition 1 from Proposition C.4, Corollary C.3 and Corollary C.4."
The result separates two regimes. In the delivery-irrelevant regime, more tech-savvy customers only change who eats at the restaurant; the price and the throughput are fixed while the platform's profit and welfare grow. Past the critical mass , the restaurant raises its price and serves only delivery customers, and the platform's profit and social welfare drop. This is the basis of the paper's answer to "friend or foe" and of its later analysis of revenue-sharing contracts that restore coordination (Proposition 2, not part of this mission).
The paper's proof is a long chain of case analyses over piecewise-defined profit functions, spread over 22 pages of appendix. A machine-checked version settles every boundary case. Reading the proof closely has already turned up several (findings F1–F9): ties in the restaurant's optimum at and at ; table rows that are wrong outside their derived price range; an implicit hypothesis ; the degenerate case ; a tie rule that needs a precise reading; and a boundary error in Lemma C.7(3). The definitions of the queue-joining equilibrium and the three-stage Stackelberg game can be reused for other platform and queueing games. None of this has been formalized before.
The equilibrium is defined by optimality conditions, so each stage needs an existence-and-characterization argument, not a formula check. The customers' stage has mixed strategies with three utility comparisons and a tie rule. The platform's profit is piecewise in , with branches that switch depending on and on whether . The restaurant's profit is the upper envelope of three curves whose maxima must be compared through the cubic defining and a quartic-type equation defining . The obvious approach, substituting the tables, fails at the boundaries. At and at the restaurant has two optimal prices with different platform profits, so "the" equilibrium price is not unique. The jump statements are therefore about a particular equilibrium selection and about one-sided limits.
All objects live in FoodDeliv.Decentral, with one definitions file, FoodDeliv_Decentral_Model. Conventions:
Beyond the paper. No variant items are posed. The findings file records the evidence for each deviation above.
Contributions welcome: proofs of the milestones in any order; existence of customers' equilibria for every under the tie rule; reusable lemmas on unimodal functions, cubic roots and one-sided limits of piecewise functions.
An adjustable decision is a rule that responds to information revealed after an optimization problem is specified. In production planning, for example, a later quantity may depend on observed demand, while an earlier commitment must remain constant. A robust counterpart requires the resulting decisions to satisfy the constraints for every realization in a prescribed uncertainty set. The information available to each decision is part of the model: observing one linear combination of uncertain data does not permit a policy to use all the data coordinates.
Quadratic rules provide a finite family of responses with more flexibility than affine rules. The resulting robust constraints still quantify over infinitely many uncertain realizations. This mission concerns the case in which that infinite family has an exact finite semidefinite representation: fixed recourse and ellipsoidal uncertainty, as stated in Corollary 14.3.8 of Ben-Tal, El Ghaoui and Nemirovski. The result is about optimization over the selected quadratic rules; it makes no claim that these rules attain the best value among all possible responses.
Let denote the uncertain data and let
The uncertain linear problem has decision variables and constraint rows:
All four data functions are affine in . For variable , a specified matrix determines its observations. A quadratic decision rule has the form
The optimization variables are the coefficients and an objective threshold . The matrices are fixed data. The coefficient matrices are unrestricted: using full arrays retains every quadratic polynomial, with harmless redundancy in their skew-symmetric parts. If , the policy is constant.
Fixed recourse means that whenever , both and column are independent of . Coefficients of nonadjustable variables may still be uncertain. This is Definition 14.3.1, printed p. 371, including the condition on the objective. Robust epigraph feasibility means that and hold for every .
The supporting geometric target is Lemma 14.3.7, printed p. 384. The quadratic lift of is the symmetric matrix with top-left entry zero, first column , and lower-right block . Its ordinary convex hull is compact and satisfies
The goal is Corollary 14.3.8. For every policy coefficient vector and threshold, robust epigraph feasibility is equivalent to feasibility of the explicit SDP after adding one nonnegative multiplier for each constraint row and one for the objective row. If the signed slack in row is written , its matrix constraint is
The model defines these coefficients directly from the original data and the observation matrices. The theorem also asserts that the matrices depend affinely on the SDP decision vector. There are matrix constraints of order , and
scalar decision variables. With , the bound and the corresponding dense matrix coefficient bound make the polynomial-size conclusion explicit.
The equivalence retains every original policy coefficient and objective threshold. It therefore preserves the entire robust feasible epigraph, including instances with no feasible policy and optimization problems whose values are unbounded. The goal also states equality of attainable thresholds and preservation of minimizers for the same linear objective in the finite SDP. It does not assume that either problem has a minimizer. Equality of a pair of real-valued infima would express less information and could conceal degenerate cases.
The mathematical results are established in the textbook. This mission supplies open Lean theorem statements for their formal verification and concrete definitions for their objects. The homogeneous S-lemma and the inhomogeneous S-procedure are already Proved on Prove2Me and are retained as references. The moment-hull identity and the complete quadratic-policy representation are the new targets. Their definition layer can also support work on polynomial policies and other lifted uncertainty sets.
Checking a quadratic constraint on an ellipsoid is a global requirement. Evaluating it at a finite collection of sample points does not establish the required universal inequality. Likewise, the image of a convex uncertainty set under the quadratic lift is generally not convex. The target must identify its whole convex hull, including compactness and boundary points.
The formalization must also preserve information restrictions through every matrix coefficient. Full observation cannot replace , even if the resulting semidefinite program is easier to describe. The objective has uncertain affine data and participates in the same robust requirement as the constraints. These issues distinguish the complete statement from a single quadratic inequality or a result that assumes all coefficient columns are certain.
All spaces and matrices are finite dimensional over the reals. The code uses finite functions for coordinates, but defines the uncertainty set through a sum of squares, so the norm is Euclidean. Matrix indices have a distinguished first coordinate. The unshifted lift has zero there; the positive-semidefinite moment block has one. Positive semidefiniteness also enforces symmetry of the moment matrix.
The model, uncertainty set, policy evaluation, original robust epigraph, and proposed SDP constraints are separate concrete definitions. Neither feasibility equivalence nor the moment-hull identity is assumed in the definitions. The theorem quantifies over every finite dimension, including zero; an empty observation list produces a constant policy. No division by a dimension or a policy-dependent denominator occurs.
The polynomial-size statement concerns the explicit real SDP representation, as in the book. It does not add a machine model or a bit-complexity theorem for an SDP solver. The formalization uses full quadratic coefficient arrays, so its stated counts need not be minimal. The bound includes all these redundant coefficients. There are no optional variants in this mission. The recorded sharpness observation about explains why its injectivity is retained in the compactness theorem.
An inventory manager chooses replenishment orders before knowing all future demand. Orders made today affect both the stock available tomorrow and the cost of later decisions. A flexible commitment contract adds another consideration: deviations from previously announced orders can incur penalties. The uncertainty therefore concerns a sequence of observations, and the object being optimized is a sequence of decision rules. Chapter 15 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization uses this setting to compare the cost of unrestricted adaptive policies with the cost of affine policies.
For such a comparison, an exact benchmark matters. Evaluating a policy against every trajectory in a continuous uncertainty set can require infinitely many constraints. The chapter's Lemma 15.2.1 identifies a class of problems whose optimal value is preserved by restricting uncertainty to finitely many extreme scenarios. This mission formalizes that general lemma, which the book applies to inventory management, rather than the numerical experiments or a particular contract data set.
A history at stage is the tuple , where each observation is a real vector of dimension . A policy specifies a real decision vector of dimension for every possible history. Dependence only on observations already available is called nonanticipativity. Two full trajectories with identical observed prefixes necessarily produce the same decision at that stage.
There are decision stages and uncertainty sets . All data except the observations are fixed. Linear maps and vectors impose the initial and linking inequalities
Vector inequalities hold coordinatewise. The term uses the whole observed prefix. A fixed real bound restricts the infinity norm of each decision at stages . The terminal decision still appears in the last linking constraint, but the printed norm restriction does not cover it.
Each decision incurs a stage cost . The costs are lower semicontinuous convex functions with polyhedral effective domains. A cost may be outside its domain; within the domain it is finite. Polyhedrality of the domain does not require the cost itself to be piecewise linear. The total cost includes all stages.
Write for the infimum of all real bounds for which some policy satisfies the preceding constraints and
For nonempty polytopes , the target is the complete value equality in Lemma 15.2.1, printed p. 430:
Here denotes the set of extreme points of . Both sides optimize over unrestricted nonanticipative policies. The target does not restrict those policies to affine rules, assert that every fixed policy has its worst cost at an extreme trajectory, or assert attainment of the optimum. The source states this lemma without a local numbered proof sequence, so the mission has one goal and its concrete model definitions, with no additional milestone chain.
For interval uncertainty, the extreme observations are interval endpoints. The book uses this consequence to replace a box of demand trajectories by a finite scenario set. It then describes a finite optimization problem whose decisions must agree whenever their available information agrees. These are exact comparisons of optimal values for the specified models, not estimates of sampling error. The number of scenarios can still grow exponentially with the horizon, as the chapter discusses on printed pp. 430–432 of the source.
The formalization makes the policy information pattern, terminal-stage treatment, and extended-value convention explicit. These details are useful beyond the inventory application because the lemma permits arbitrary compatible linear constraints and convex stage costs. The current artifacts state the known textbook result in Lean; a successful statement build is not a proof of the lemma. The reusable definitions are concrete and contain no unproved mathematical assertions.
The uncertainty set is a product, but decisions at different stages are connected by constraints. A decision chosen for one trajectory cannot be chosen independently of another trajectory sharing the same history. Consequently, a statement about a single convex function on a polytope does not by itself express the multistage result. The target must retain the order of policy choice and universal quantification over trajectories, the complete cost sum, and the information available at each decision.
The final stage introduces a separate boundary issue: its cost and feasibility constraints remain present even though the printed bound stops one stage earlier. Omitting the final cost or extending the bound would change the problem. Degenerate and infeasible instances also require a value convention that does not assign them an arbitrary real number.
Lean represents observations and decisions by finite real coordinate spaces, with dimensions allowed to vary by stage. Histories are finite dependent tuples; a policy's argument type contains exactly the observed prefix. Linear maps represent the book's matrices, including maps from stacked histories. Nonempty polytopes are convex hulls of nonempty finite sets, allowing singletons and lower-dimensional polytopes. The cost-domain predicate uses finitely many nonstrict matrix inequalities.
The extended optimal value is an EReal infimum of achievable real objective bounds. An empty set of bounds gives , while bounds unbounded below give . No subtraction of infinities occurs. Regular costs exclude , so the finite sum in the objective has no mixed-infinity ambiguity. The definition does not assume feasibility, boundedness below, or attainment. Zero horizon and zero-dimensional coordinate spaces follow the same displayed formulas.
Formalization Note No singleton assumption is placed on , and no measurability, continuity, or affine restriction is imposed on policies. The theorem expands its concrete model for independent auditing. A Lean type check verifies agreement with the separately named reusable definitions. The required mathematical infrastructure includes convex hulls, extreme points, lower semicontinuity, finite linear algebra, and extended-real order. Completion requires a proof of the stated value equality with precisely these hypotheses.
Regression and classification fit a parameter vector to observed data. When measurements can vary within a prescribed set, a fit judged only at the nominal observations need not control its loss on the possible data. A worst-case loss constraint requires the loss bound to hold for every admissible matrix of measurements. Such a requirement can contain infinitely many inequalities even when the parameter vector has finitely many coordinates. Chapter 12 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (2009) identifies structural assumptions under which this requirement has an exact finite convex representation.
This mission concerns the representation in Theorem 12.2.5. Its application is to robust fitting problems whose uncertainty support function separates into a feature-dependent factor and the infinity norm of a residual-space vector. The result applies to both symmetric losses, such as norms of regression residuals, and asymmetric losses formed from positive residual parts.
Let be positive integers. The nominal data matrix has one column per measurement and one row per feature. For a parameter vector , its residual vector is . A fixed matrix describes the structure of permitted perturbations, and a nonnegative scalar controls their size. The uncertain data matrices are
where is convex, compact, and contains zero. No independence of its columns is imposed.
The loss function is finite and convex. Assumption L requires one of two forms: for every , or for every . Absolute value and positive part act coordinatewise. The function is convex and nondecreasing in every coordinate on the nonnegative orthant. The choice of form is global, rather than chosen separately at each residual.
Assumption A specifies the support of in every rank-one direction:
Here is finite, nonnegative, convex, and positively homogeneous, and is a norm. The goal uses . These are the standing objects and assumptions of Section 12.2, printed pages 311–319 of the source.
For any real threshold , the goal is the exact equivalence
if and only if there exists a real satisfying
The goal also states convexity in of the scalar functions on the left of these constraints. There are shifted-loss inequalities and one amplitude inequality.
The numbered supporting targets preserve the source's identities. Equation 12.2.11 gives the Fenchel biconjugate representation of a finite convex loss. Equation 12.2.12 equates the worst-case realized loss with its conjugate expression involving the support of . Equation 12.2.15 replaces that support by its factorization under Assumption A. Equation 12.2.18 equates the resulting worst-case loss with a maximum over the dual unit ball:
The maxima in these identities are required to be attained. The Fenchel representation itself uses the source's supremum notation.
Theorem 12.2.5 replaces a constraint over a continuum of data matrices with finitely many evaluations of the original loss and the uncertainty gauge. It retains the dependence of uncertainty on the fitted parameter through . Consequently, the representation describes exactly the robust feasible parameters, including zero uncertainty, rather than merely giving a sufficient condition. Evaluation efficiency remains relative to the supplied loss and gauge, as in the book's tractability discussion.
The mathematical result is established in the textbook. The contribution sought here is a machine-checked formalization of its statement and supporting identities. The general finite-dimensional Fenchel biconjugacy theorem already has a proved platform item and is reused as the first milestone; the other three identities and the capstone are open theorem statements in this draft.
The central issue is relating uncertainty in a matrix to uncertainty in the residual vector while preserving exactness. A uniform bound on individual matrix entries does not by itself express Assumption A. Conjugate functions also need extended values: replacing an infinite conjugate by a real default would change the optimization problem. Establishing equality of optimal values alone is insufficient for identities written with maxima; their attainment is part of the targets. The zero-amplitude case must agree with the nominal loss throughout.
Vectors use finite-dimensional real Euclidean spaces and matrices have explicitly ordered feature and measurement indices. Coordinates use Fin m, so the first coordinate is indexed by zero. The infinity norm in the goal is taken on the plain coordinate function; it is not the Euclidean norm of the residual vector. The statements include both signs for every coordinate.
The published fenchelConjugate and fenchelBiconjugate definitions are reused. Conjugate objectives take values in EReal. Every claimed maximum is expressed using IsGreatest at a common finite real value, so existence, boundedness, equality, and attainment remain visible. The inner support supremum in Equation 12.2.12 is real-valued and ranges over a nonempty compact image. The dual unit ball in Equation 12.2.18 is represented directly by for all .
All hypotheses about the loss, gauge, norm, and uncertainty set are explicit in each new theorem. None assumes the desired finite reformulation. Assumption L is retained despite the recorded observation that a weaker loss hypothesis suffices for the mathematical equivalence. There are no variant targets. A computational cost model and an optimization algorithm are outside this formalization; the explicit finite formulas and their convexity are the representation being formalized. Reusable work includes finite-dimensional conjugacy, compact support maximization, and dual-norm geometry.
A linear constraint can fail when its coefficients vary. In an engineering or planning model, requiring it to hold for every imaginable realization may exclude useful decisions, while checking it only at an average realization may give little control over failure. A chance constraint specifies an acceptable probability of violation. Chapter 2 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization studies deterministic convex conditions that guarantee this probabilistic requirement for a single uncertain linear inequality.
The chapter distinguishes a guarantee from an exact description of chance feasibility. Its robust constraints are safe approximations: satisfying them guarantees reliability, but a reliable decision need not satisfy them. The goal here concerns how known bounds on the perturbations can be incorporated into such an approximation without losing an explicit convex representation.
A decision is a vector . The deterministic data are vectors and scalars . Define the residual coordinates by , including the nominal coordinate . A realized perturbation satisfies the constraint exactly when
For a probability law and a tolerance , chance feasibility means that the strict reverse inequality has probability at most . Robust feasibility over a deterministic set means that the displayed inequality holds for every .
The perturbation coordinates are independent measurable real random variables. Their moment-generating functions obey the two-sided bound
where and . These are the book's assumptions P.1–2. The goal additionally assumes almost-sure support bounds , with finite endpoints satisfying . No positive lower bound on is imposed.
Write , , and . The general safety statement, Proposition 2.4.1, asserts that
Its feasible set is convex. Proposition 2.4.2 states the tail bound at every nonnegative safety level :
Theorem 2.4.3 identifies the first deterministic inequality with robust feasibility over the moment uncertainty set
The capstone is Theorem 2.4.4. Let be the intersection of with the support box . Then is robust feasible over if and only if there exist extended residual vectors satisfying
This system is convex in its decision and auxiliary variables. Every feasible triple has violation probability at most . The theorem includes both the deterministic equivalence and the probabilistic guarantee, as on printed page 48.
Two supporting targets retain the chapter's bounded mean-zero specialization. Proposition 2.3.1 gives the tail estimate for independent mean-zero perturbations in . Proposition 2.3.3 identifies robustness over the intersection of the unit box and a Euclidean ball with its lifted conic system and establishes the corresponding chance guarantee. These are supporting statements from the source, not replacements for the general capstone.
The capstone connects a deterministic set of allowed perturbations with a stochastic model specified through moment bounds and support information. It gives a finite convex system whose feasible decisions satisfy the requested reliability level for every law meeting those assumptions. The statement does not require choosing a particular parametric distribution or estimating a probability separately for every decision.
These are known textbook results. The formalization targets are their Lean statements and eventual machine-checked proofs, including zero scales and boundary feasibility. The reusable content comprises finite-dimensional uncertainty sets, explicit exponential-moment hypotheses, and the relationship between lifted convex constraints and strict-event probabilities. The present authoring pass leaves the six theorem proofs open; compilation checks their types, not their truth.
The exact robust representation includes equality cases in the endpoint order and permits degenerate ellipsoids. A formulation restricted to positive scales or strict interior intersections would omit cases of the stated theorem. The chance guarantee must also include the boundary of the explicit safe set; it cannot be replaced by a condition requiring an additional strict margin.
The printed proofs have local discrepancies recorded in the mission findings: the proof of Proposition 2.4.2 omits a sum and invokes an open-interval risk bound at its excluded endpoint when the safety level is zero, the first line of the goal's proof uses a different radius, and the limiting argument on page 50 asserts a zero limit that fails for strictly feasible residuals. These findings concern the proofs, not counterexamples to the theorem statements. The goal retains the printed constants and hypotheses.
The namespace is RobustOpt2009.ScalarChance. Vectors use real-valued functions on Fin L; the nominal coordinate is a separate real component. All Euclidean lengths are explicit square roots of sums of squares, avoiding the default function-space sup norm. Probability is evaluated under a probability measure, and all random coordinates are measurable. The exponential-moment definition includes integrability, preventing nonintegrable Bochner integrals from supplying default zero values.
Scaled coordinates implement the book's zero-denominator convention: a zero scale forces zero displacement. Robust feasibility is a universal inequality, so no empty or unbounded real supremum is used. The exponential-certificate set, its topological closure, and the perturbation uncertainty set remain separate concrete objects. No definition assumes the desired equivalence or tail bound. Finite sums include the zero-dimensional case, where the statements reduce to their deterministic or empty-event versions.
Further work consists of proving the stated concentration, convexity, and exact representation claims using these definitions and Mathlib's probability and finite-dimensional analysis. No variants are posed in this chapter.
An optimization model can require a linear inequality to hold with high probability when its coefficients are random. Such a chance constraint controls the probability of violation, but its feasible set need not be convex or easy to describe. A conservative convex approximation can make the requirement usable within a larger optimization model. Chapter 4 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization studies when such approximations also have a robust interpretation: the inequality must hold for every perturbation in a deterministic uncertainty set.
The target here is the chapter's Bernstein construction. It starts from information about the joint exponential moments of a random vector, rather than a fixed list of scenarios. Its conclusion identifies exactly the uncertainty set associated with the conservative approximation. Exactness concerns the relationship between that approximation and robust feasibility; the approximation is still only a sufficient condition for the original chance constraint.
Let have probability distribution on . A coefficient vector is a pair , where and . The requirement is
The violation event is strict. Equality in the underlying linear inequality therefore counts as feasible. The parameter controls the permitted probability of failure.
A logarithmic moment-generating majorant is a finite convex function satisfying and
These are Assumption Q.1. They concern the joint distribution; independence of the coordinates is not required. Assumption Q.2 provides an affine conjugate representation
where is linear, , and is convex and lower semicontinuous. Every real sublevel set of is bounded. Allowing permits restrictions on the effective domain without changing the ambient space.
The goal is Theorem 4.2.5, printed pp. 85–86 of the book. Define the coefficient sets independently by
Define the auxiliary sublevel set and its affine image by
The theorem says that is nonempty, convex, and compact and that
It also retains the displayed perspective characterization and its probabilistic consequence:
and this condition implies the original chance constraint.
Four source-numbered milestones accompany the goal. Lemma B.1.1 identifies the closure of a homogenized convex sublevel set with the zero sublevel set of its perspective infimum, including finiteness and convexity of that function. Proposition 4.2.2 characterizes the Bernstein approximation and asserts its normal safety. Proposition 4.2.3 gives bounded sublevel sets for an affine conjugate representation whose linear map has trivial kernel. Theorem B.1.2 gives the general robust representation under its directional-limit assumption. Each statement retains its source hypotheses and all conclusion clauses.
The chapter's result gives a deterministic meaning to a probabilistic sufficient condition. An uncertainty set chosen through the conjugate data describes precisely the same coefficient constraints as the Bernstein approximation. This connects the probability model to robust linear feasibility while preserving the distinction between a guarantee and an exact description of the original chance-feasible set.
The formalization supplies separate, concrete definitions for the probability condition, the coefficient cone, and the perturbation set. That separation makes the equality in the main result a substantive theorem. The appendix statements also expose reusable finite-dimensional convex analysis, including perspective values, closed cones, and affine images of extended-real sublevel sets. These are known mathematical results from the book; the current draft consists of type-checked statements awaiting Lean proofs. A successful statement build is not a proof of any of these assertions.
Closure and optimization at a boundary are central issues. The perspective infimum ranges over strictly positive scales, but its value may be approached only as the scale tends to zero. Replacing the infimum condition by the existence of one feasible scale would change the target. Similarly, an extended-real function can impose a proper effective domain, so a formalization restricted to everywhere-finite penalties would omit cases covered by the theorem.
The general appendix theorem includes a directional limit below a specified level. That limit can be negative infinity, including in the application to the chapter's coefficient variable. Requiring a finite real limit would exclude the intended application. Probability expressions also require attention to the strict violation event and to the meaning of an expectation when exponential moments diverge.
Finite-dimensional real spaces are represented by functions on Fin n, with the standard topology. Coefficients are pairs , so coefficient feasibility and perturbation membership have different types. The linear map is explicit and its affine translation is applied before taking the pairing. No independence, Gaussian distribution, bounded support, or injectivity assumption is added to the goal. Injectivity belongs only to Proposition 4.2.3 and its variant.
Formalization Note Infima and suprema are computed in the complete extended-real lattice. The penalty's negative-infinity value is explicitly excluded where the source uses . Convexity is expressed by the real epigraph and lower semicontinuity by closed real sublevels. Q.1 uses the equivalent bound on the nonnegative integral of the exponential, avoiding a default real-integral value on nonintegrable inputs. The uncertainty set is the actual affine image of the specified sublevel set, not an assumed certificate for robust feasibility.
Beyond the paper. One additional target strengthens Proposition 4.2.3 by removing only lower semicontinuity. Finding F1 records that finite bounds in the positive and negative coordinate directions, together with injectivity, already bound each sublevel set. The faithful proposition retains lower semicontinuity and remains the milestone. This strengthening does not change the goal or remove the topological assumptions needed for compactness elsewhere.
A resource constraint can remain useful even when an exceptional disturbance makes exact satisfaction impractical. In such cases the model needs to distinguish the disturbances against which feasibility is mandatory from those for which a controlled violation is acceptable. Ordinary robust optimization specifies a set of perturbations and requires the constraint to hold everywhere in that set. It does not itself describe what happens outside that set. Chapter 3 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization introduces a quantitative way to make this distinction for uncertain linear inequalities.
The object of this mission is the globalized robust counterpart of a single scalar inequality. Its tolerance is proportional to distance from a normal uncertainty range, with a prescribed restriction on admissible displacement directions. The goal is Proposition 3.2.1, which characterizes this global requirement by two ordinary robust inequalities. The result is a known theorem of the book; the target here is its faithful Lean formalization.
Let be a decision vector. The data consist of vectors and scalars . A perturbation vector determines the inequality
The normal range is a nonempty closed convex subset of . A closed convex cone containing zero describes the possible directions of departure. The physically possible range is the sum
Here denotes the book's ; remains the number of perturbation coordinates. A fixed norm measures displacement. These are the perturbation-structure assumptions (G.a–c) on printed page 68 of the source.
For a physically possible perturbation, its constrained distance from the normal range is
The displacement restriction is part of the definition. The admissible set of displacement lengths is nonempty when and is bounded below by zero. Thus the distance has a finite real value on precisely the domain where the counterpart uses it.
A nonnegative real parameter is the global sensitivity. Global robustness requires the residual of the uncertain inequality to be at most for every physically possible perturbation. This is Definition 3.1.1 and equation (3.1.4) of the book.
Write the residual and its directional part as
The goal is the complete equivalence of Proposition 3.2.1, printed page 69:
Both right-hand requirements are universal inequalities. The nominal coefficients occur in the first and do not occur in the second. The directional condition includes the zero direction and every direction on the boundary of the unit ball.
There are no separate supporting theorem milestones in this mission. The numbered Chapter 1 representation results discussed after the proposition describe applications of its conclusion. They are not intermediate targets needed to state this capstone.
The equivalence distinguishes feasibility throughout the normal range from control of how the residual varies along admissible directions. As explained in Remark 3.2.2 of the book, it brings the globalized counterpart into contact with representation results for ordinary robust constraints. The proposition itself remains valid without a boundedness assumption on the normal range and without choosing a special shape such as a box or ellipsoid.
The formalization fixes the exact relationship between the domain of the distance and the quantifiers in the counterpart. It also makes the treatment of the cone and the norm explicit. These conventions are useful when subsequent developments specialize the model. The mission asks for a proof of the displayed equivalence; finite reformulations for particular uncertainty geometries and the chapter's antenna-array application are outside this target.
The constrained distance cannot generally be replaced by ordinary distance to . That substitution changes which normal points are eligible when evaluating a disturbance. The normal range can also be unbounded, so compactness of is not available as a standing assumption. A formal proof must handle the domain of the infimum and the full directional quantification with these features intact.
The parameter may be zero. In that case the globalized condition requires exact feasibility throughout , as noted after Definition 3.1.1 in the source. The cone may consist only of zero, and the relevant displacement can have zero norm. None of these cases is excluded by a positivity assumption added for convenience.
All coefficients and sensitivities are real. Decision and perturbation vectors use the finite coordinate types Fin n and Fin L; their zero-based indexing is a relabeling of the source sums. The nominal coefficients are separate parameters. The goal writes the coordinate sums and constrained infimum explicitly, using only Mathlib objects, so its meaning does not depend on an unpublished definition from another chapter.
An arbitrary norm is represented by Mathlib's real seminorm type together with definiteness: implies . Closedness uses the usual topology on finite-dimensional real coordinate space. Convexity of both sets, nonemptiness of , membership of zero in , and closure of under nonnegative scaling are explicit hypotheses. The global robustness condition is the distance inequality itself, not a definition chosen to assume its desired characterization.
The real infimum is used only over a nonempty set of nonnegative lengths. Its value on an empty set is not used by the theorem. Zero coordinate dimensions are permitted with empty sums interpreted as zero. The faithful goal retains convexity of ; the separately recorded observation that it is unnecessary does not alter this statement. The remaining formal work concerns this exact equivalence, using finite sums, convex sets, seminorms, topology and real infima from Mathlib.
Unitary representations turn symmetries into operators on Hilbert spaces. For ordinary locally compact groups, the associated group -algebra lets one study these operators through a single algebraic object. A Lie supergroup adds odd infinitesimal symmetries to an ordinary Lie group. Its unitary representations must respect both the group action and those odd operators. Neeb and Salmasian construct a -algebra that captures this combined structure Neeb–Salmasian 2015. The representation correspondence is the point at which their construction becomes useful: a representation of retains precisely the data of a unitary supergroup representation.
The paper subsequently uses this bridge to discuss direct integral decompositions through the -algebra. This mission concerns the bridge itself, Theorem 6.4. Its input is not a special connected or nilpotent group: the paper works with an arbitrary finite-dimensional Lie supergroup. The later CCR results in §7 add hypotheses and are outside this mission.
A finite-dimensional Lie supergroup is a pair . Here is a real Lie group and is a real Lie superalgebra. Its even part is the Lie algebra of . The group acts smoothly on the superalgebra by an adjoint action whose even restriction is the derivative of conjugation; differentiation of the action recovers the superbracket. These are the conditions of Definition 2.1, including the finite-dimensional convention stated just after it.
A unitary representation consists of a graded complex Hilbert space , a strongly continuous unitary action of preserving that grading, and a real-linear superalgebra action on the space of smooth orbit vectors. On even elements, equals the derived group action. On odd elements, is symmetric, and the odd action transforms under through the adjoint action. This is Definition 2.3, including its parity and bracket requirements.
The paper adjoins a parity element and writes . A test function on this group is a pair of smooth, compactly supported complex functions on . Using the complex universal enveloping algebra, the authors form an algebraic crossed product . A word and a test function act in each unitary representation by the bounded operator . The norm of an algebraic element is the supremum of the norms of these represented operators; completion after quotienting its zero seminorm gives the non-unital -algebra §§3–4.
A star representation of on is nondegenerate when the span of its image applied to is dense. A morphism between two unitary supergroup representations is a bounded, even, complex-linear operator intertwining both their -actions and their -actions on smooth vectors. A morphism between -algebra representations intertwines every element of .
The first targets are the uniform bound of Proposition 3.2 and the smoothness statement of Proposition 5.1. For each word and test pair , the same constant works for every unitary representation:
The left multiplier orbit is smooth for every . The construction from a nondegenerate representation also identifies its smooth vectors with the represented algebraic core, as in Lemma 6.2. These are the analytic steps named in the milestone list.
The goal is Theorem 6.4. Propositions 6.1 and 6.3 give mutually inverse assignments on objects, and Theorem 6.4 retains the same intertwiners:
Thus each unitary representation yields exactly one nondegenerate representation agreeing on every generator, each nondegenerate representation comes from exactly one unitary supergroup representation, and a bounded operator intertwines one pair exactly when it intertwines the other. The goal includes all three clauses.
The result lets questions about unitary Lie supergroup representations be transferred to a -algebra without losing the odd infinitesimal action or the morphisms. In the paper, this is the foundation for the later direct integral discussion and CCR criteria. Without the equivalence, properties of would have no stated connection to decomposition of unitary supergroup representations §7.
The mathematical result is proved in the cited paper; the local Lean declarations are open statements. A complete formal development would add machine-checked proofs for the uniform operator bounds, the algebra and multiplier facts, reconstruction of the odd action, and the categorical equivalence. The reusable parts include smooth-vector actions, integrated test-function operators, and a universal bounded family of representations.
The odd infinitesimal operators are defined on , not automatically as bounded operators on all of . Integrating against a test function supplies smooth vectors, but it does not by itself give a bound for an arbitrary word in the odd and even operators that is uniform over every representation. That uniformity is needed to construct one -norm. In the reverse direction, a nondegenerate representation of first gives bounded operators; recovering the derived action on precisely the smooth core requires the multiplier and smoothness statements. An object-level bijection alone would still miss the paper's assertion about intertwiners.
Lean models as a finite-dimensional smooth real Lie group, with its Mathlib group Lie algebra and a finite-dimensional real normed space. The superbracket and odd adjoint action are fields of a Harish–Chandra pair. Smoothness uses , not analyticity. The group is neither assumed connected nor second countable. A left Haar measure is fixed. The Hilbert spaces quantified in the mission belong to Type; the index of all such unitary representations belongs to Type 1.
The test space is encoded as pairs of functions, and the enveloping-algebra elements needed here as finite words. is the closed non-unital star subalgebra of the bounded product of operator algebras generated by their representation families. This uses all Type-small unitary representations; the paper takes unitary-equivalence classes of cyclic ones, which yield the same norm through its Remark 2.5. The algebra depends only on and Haar measure, and acts on itself. This rules out a choice of algebra or an off-domain operator value that would make the correspondence automatic.
The published smooth-orbit and vector-integral definitions from van Dijk–Neeb–Salmasian–Zellner are reused. Completing this mission calls for the Dixmier–Malliavin factorization, Gårding smoothing, bounded operator estimates, non-unital -algebra representations and multiplier actions. Contributions proving those general tools or the source-labelled milestones are within scope. The generator family is represented through vectors rather than an operator-norm Bochner integral, whose measurability is unavailable for a merely strongly continuous representation.
The relative entropy of entanglement measures how distinguishable a multipartite quantum state is from all fully separable states. In finite dimensions it is a standard entanglement measure, but infinite-dimensional systems raise a basic analytical problem: the measure may take the value , and finite-rank approximations do not automatically control its behavior at a limit state. Shirokov's analysis identifies a broad class of states at which the direct relative entropy of entanglement is finite and lower semicontinuous. The result applies when all but possibly one marginal state satisfy the FA-property, a spectral condition that includes useful finite-entropy states without requiring finite-dimensional Hilbert spaces.
The paper relates the direct measure to a universal extension formed from local finite-rank compressions. This mission isolates the part of Theorem 2 A) and the source results needed to reach it. A later paper by Lami and Shirokov addresses more general global lower semicontinuity questions using a different operator model and hypotheses; its statements are related work, not imports into this mission. Shirokov, §4.3; Lami–Shirokov.
There are parties , with separable Hilbert spaces . A state is a positive trace-class operator with trace one on their joint system. Its marginal is obtained by tracing out every party except . A product state is a tensor product of one state per party. The set of fully separable states is the trace-norm closed convex hull of product states. Closure matters in infinite dimension: restricting to finite convex combinations would change the infimum below. Shirokov, pp. 10–11, (26).
Write for Lindblad's quantum relative entropy, including the trace correction for unnormalized positive operators and the value on support failure. The direct relative entropy of entanglement is
The von Neumann entropy and are extended nonnegative real quantities in natural-logarithm units. A state has the FA-property when its eigenvalues admit nonnegative numbers with and . In particular, the FA-property implies finite entropy. The set consists of joint states with the FA-property on at least marginals. Shirokov, pp. 2, 4, 14, (1), (34).
For each party, a finite-rank orthogonal projector compresses the joint state. The universal extension takes the supremum of the homogeneous values of all such local compressions. A compressed positive operator with trace is valued as ; the zero operator has value zero. Local spectral projectors built from the marginals define the approximation used in Theorem 1. Shirokov, pp. 7, 12–13, (17), (31).
For , . For every sequence of states in trace norm,
The sequence itself may lie anywhere in the full state space. This is the sequential lower semicontinuity assertion (35), together with finiteness, in Theorem 2 A).
The milestones, in attack order, are: the FA entropy consequence (p. 4); the pure-state separable comparison of Lemma 3; the -convexity of (first sentence of Theorem 2 E)); the upper bound (28) by any marginal entropies,
the concavity-defect bound (27), ; membership of in ; the -class assertion of Theorem 1; the relative-entropy inequality of Lemma 1 for positive maps with trace-preserving sum; the comparison ; lower semicontinuity of ; and the equality on (Theorem 2 B)). These are claims made in the paper, with the portions outside the route explicitly scoped in the item descriptions. Shirokov, pp. 4, 8, 11, 13–15, 20, 25.
The theorem gives a stable finite value of at every state in : approximating sequences cannot converge there while hiding a smaller limiting value. This matters when infinite-dimensional states are approximated by finite-rank or energy-constrained states, because pointwise convergence of operators alone does not control an extended-valued entanglement measure. The equality with also identifies the direct measure with a globally lower semicontinuous construction on the stated domain. Shirokov, Theorem 2 and discussion in §4.3.
The mathematical result is proved in the source paper. The formalization work is to express its spectral FA condition, multipartite partial traces, trace-norm separability, finite-rank compression, homogeneous extension, and extended-real inequalities in Lean, then prove the milestones and goal. The published P01 definition already supplies von Neumann entropy and Lindblad relative entropy; the propositions in this mission are open Lean statements, not machine-checked proofs. This shared infrastructure can support other infinite-dimensional quantum information results involving separability and marginal entropies.
A direct argument from the infimum defining cannot simply exchange that infimum with a state limit: the separable comparison state that nearly minimizes at one point need not remain useful along a convergent sequence. Infinite values also make real-valued continuity bounds insufficient. The paper's theorem therefore has to coordinate a finite-entropy estimate on marginals with control of local finite-rank approximations and a lower semicontinuous extension. The approximation estimate is uniform over a class of functions, with the rank threshold and error sequence chosen before the function. Shirokov, Theorem 1 and proof of Theorem 2 A).
Each is represented as for a countable basis index type. Parties are indexed by , and the joint basis uses their dependent Cartesian product. The state topology is the trace-norm topology of the published P33 state structure. Entropy, relative entropy, and take values in ; no real-valued surrogate replaces an infinite value. The FA-property requires an actual orthonormal eigenbasis tied to the state's coefficients. Its partition sum is computed in , so divergence cannot default to zero. The definition of says at least FA marginals and does not impose FA on the sequence in the goal.
The class is represented with a finite set of FA parties in place of the first parties, reflecting the paper's relabeling symmetry. Within that class, is converted to a real number only on the finite-entropy domain. The universal extension uses all finite orthonormal local families and the homogeneous convention for compressed positive operators. The setting also defines countable separable decompositions, finite-rank projectors, the spectral approximation relation, binary entropy in nats, and positive linear maps on the trace class. The proviso of (27) that "all the involved quantities are finite" (p. 11) is stated as finiteness of at the two mixed states. These definitions and the cited P01/P33 libraries are the reusable work. A definition of FA that every state satisfies, a separable set without trace closure, or a real that discards would trivialize or alter the target.
The paper also states a regularized case. It is outside this mission: its proof in version 2 invokes propositions by broken “??” references that are absent from the source. The hatted-class and -class portions of Theorem 1, the regularized equality in Theorem 2 B), and the entanglement-monotone part of the universal-extension bullet are likewise outside these milestones. Contributions proving the stated Lean milestones, improving the common operator definitions, and then proving the goal are welcome.
A firm that can lower its unit production cost must usually spend money before it sells anything. That payment improves the margin on future sales but leaves less cash to fund production. If the firm borrows the shortfall, the investment can therefore change both its operating return and the cost of financing. Tanrisever, Joglekar, Erzurumlu and Lévesque (2021) study this tension in a two-stage model of a capital-constrained producer facing uncertain demand. Their Proposition 4 asks when the producer gains more from the investment in a market with bankruptcy costs than in a frictionless capital market.
The question matters for a production decision made before demand is known. A cost reduction may permit a larger production quantity and increase the return on each sale. It may also reduce the size and risk of the required loan, although paying for the investment consumes capital first. The paper isolates these effects so that the sign of the financing contribution can be examined separately from the direct operating gain. This mission covers that analytic comparison in §3 of the published paper, not its later numerical experiments or uncertain-investment extension.
The firm sells each unit for . It chooses a nonnegative production quantity before demand is realized; demand is uniform on with . Revenue is . The firm starts with unit production cost and capital . It may invest to reduce unit cost by , where is cost reduction per dollar. Its post-investment cost and capital are and . Without investment, the corresponding pair remains . These are the objects introduced on p. 91 of the paper.
For a generic cost-capital pair , production requires an external loan when . A competitive bank lends the shortfall and chooses a face value so that its expected receipt equals the loan principal. If sales revenue falls below the face value, the firm defaults; the bank recovers revenue less a proportion lost to bankruptcy, where . The bank's zero-profit equation is equation (2), and Assumptions 2–3 require the adjusted face value to be below and the face value to be below . A self-financed quantity has no loan. The firm's expected bankruptcy cost is the expected lost proportion of revenue in default. Its expected operating profit before the investment payment is
An equilibrium production quantity is any feasible that maximizes over every feasible nonnegative quantity. The mission compares equilibria for and at the same , then repeats the comparison at . Ties, if any, are allowed. The investment's net benefit is invested operating profit minus minus noninvested operating profit. The model and profit definition follow equations (1)–(4) on p. 92 of the paper.
The paper separates the net benefit into an operational effect , independent of , and a friction effect :
Here compares the perfect-market operating profits. Proposition 2 gives in the positive-margin regime. Proposition 3 defines by four integrals of the marginal rate of return and marginal cost of external funds . In particular, is an explicit quantity derived from the two production and financing curves; it is not defined from the difference between and . These formulas appear on pp. 93–95 of the paper.
The goal is Proposition 4. For any positive , at equilibrium quantities under friction and at their perfect-market counterparts, it states
The milestone list follows the paper's supporting claims: competitive pricing of the loan, properties of bankruptcy cost and marginal financing cost, the equilibrium equations, the positive operational effect, the area description of profit, and the decomposition of . Each claim is stated over the same model. The goal makes no assertion that every parameter choice produces a positive friction effect; it identifies the consequence when the integral in equation (8) is positive.
A positive means the investment's change to production and financing improves its value relative to a perfect capital market. Proposition 4 turns that model-specific sign into a comparison of two net benefits, each evaluated at its own equilibrium quantities. Without the financing calculation, the direct reduction in unit cost alone says only that the operational effect is positive; it does not determine how market frictions change the investment's value. The distinction is the paper's contribution in §3 Tanrisever et al. (2021).
The result is proved in the published paper; its proofs are assigned there to Online Appendix A, which is not included in this mission's canonical PDF. This formalization sets up an open Lean proof problem for that known result. It also gives reusable, explicit definitions for competitive zero-profit loan pricing under uniform demand, proportional bankruptcy loss, feasible production, and equilibrium profit. Those definitions can support later formalizations of the paper's threshold and comparative-statics results. The local proposal contains statements and compiled definitions, while the milestone theorems and goal remain proof obligations.
The comparison in Proposition 4 depends on an identity between two descriptions of profit. Equation (4) defines profit through expected revenue and the bankruptcy-cost expectation. Figures 2–3 and equation (8) express the same quantities through areas under marginal curves. Identifying the area with the expected-profit expression requires control of the loan face value as production varies and of the transition between borrowing and self-financed production. Merely subtracting the two profit formulas does not yield equation (8). The equilibrium quantity is also chosen over feasible production quantities determined by the bank's lending restrictions, so a stationary marginal equation needs justification as an equilibrium characterization. These are the main obligations represented by the earlier milestones.
Lean uses real-valued parameters and a normalized interval integral, , for every expectation under . The parameter record holds ; a standing predicate requires their stated positivity, , and . The friction proportion remains a variable in . Quantities are nonnegative with no imposed upper bound. Lending feasibility enforces Assumptions 2–3; self-financed quantities require no loan. Equilibrium quantities are hypotheses quantified over all feasible competitors, avoiding a default-valued supremum or a manufactured maximizer.
Two conventions are stated explicitly. First, is added for Propositions 2–4: with , the first upper limit in the paper's equation (8) can be negative, and its displayed implication fails. Second, and where . On the positive-loan branch, is the lower closed-form root of the bank's equation (2), and agrees with the printed formula. The paper usually assumes capital is insufficient for production; this proposal also allows self-financed production, with the convention disclosed in the statements. The definition of is the four-integral equation (8), rather than , and expected profit remains equation (4), rather than an area definition.
The development needs interval integration, real square roots and derivatives, convexity, and optimization over feasible real quantities from Mathlib. The definitions and theorems use the main text of the published article; proofs in its online appendices and the later numerical and stochastic extensions are outside the present scope.
A quantum repeater is judged by how much it beats direct transmission over a point-to-point link. The natural yardsticks are the two-way assisted capacities of the link's channel : the quantum capacity and the secret-key capacity , the best rates of entanglement and key that two parties can obtain over many uses of when unlimited two-way classical communication and local operations are free. Computing them exactly for a given channel is rare, because it requires a lower and an upper bound that meet.
Pirandola and Laurenza (arXiv:1512.04945v2, 2016) obtain such matching bounds for a family of channels. The lower bound is the coherent information of the channel (with its reverse version), which is achievable by the hashing protocol. The upper bound is the entanglement flux , the relative entropy of entanglement of the channel's Choi matrix, which bounds for channels that can be simulated by teleportation. For the qudit dephasing channel the two bounds coincide, which gives (Eqs. (20) and (95)). This mission formalizes that coincidence.
Fix a dimension and the computational basis of a qudit. Let and let be the generalized phase operator, . For a dephasing probability define the binomial weights
and the qudit dephasing channel, given by its Kraus operators,
Write and (with ) for its Shannon entropy.
The Choi matrix of a map on matrices is , where . The first tensor factor is the reference , the second the channel output . With the von Neumann entropy :
The paper's candidate separable state is .
For every and :
The lower and the upper bound on the two-way capacities therefore meet. The statement keeps and free and asserts exact values, not numerical constants.
The result. The coincidence of the two bounds pins down and of the qudit dephasing channel for every and , which gives the repeaterless benchmark for any qudit link dominated by dephasing. At it recovers the qubit dephasing benchmark of the same paper (Eq. (75), with , which the binary entropy does not see). Combined with the operational facts the paper imports (the hashing inequality and the bound of by the flux for teleportation-covariant channels), it yields the capacity formula (95).
Formalizing it. The paper's computation is complete but terse. The formalization makes three implicit points explicit: the support of the Choi matrix lies inside the support of the rank- state (so is taken on its support); the claim of " non-zero eigenvalues" in (91) fails at , while the entropy identity does not; and (45) needs trace preservation as well as unitality. The results are proved in the paper and, as far as the platform's catalogue shows, formalized nowhere. Eq. (68) and Eq. (45) are reusable lemmas about arbitrary states and unital channels.
The calculation on the page is short; the difficulty lies in what it leaves to the reader. The entropy identity (91) asks for the spectrum of a matrix that is not diagonal in the computational basis, while the von Neumann entropy is defined through the matrix functional calculus, so "diagonalizing" has to be made precise. The state has rank in dimension : the relative entropy against it is finite only because of a support inclusion the paper does not mention, and a computation that ignores the kernel of does not establish the value. The upper bound needs to be separable in the sense of the infimum, a finite convex combination of product density matrices, not merely diagonal. Finally, the coherent information is a difference of entropies of a partial trace and of the full Choi matrix; equating it to requires both that the output marginal is maximally mixed and the entropy identity (91).
Qudit indices are Fin d, with (and [NeZero d] where an instance needs it); is real with . is a matrix power, , and the channel is the published QAlgorithms.krausApply of the Kraus family . The Choi matrix is the published QAlgorithms.idTensorSuperop applied to maximallyEntangledProjector d (entries on ), the reference being the first factor of Fin d × Fin d. Entropies are in bits with : QAlgorithms.vnEntropy for states and a local Shannon entropy for the weights. The partial traces are QAlgorithms.traceLeft (over the reference) and QAlgorithms.traceRight (over the output). The relative entropy and are the published relativeEntropyBits and relativeEntanglement (Umegaki entropy divided by , off support, infimum over IsSeparableDensity, values in ). The real bound is embedded with ENNReal.ofReal; since , nothing is lost.
None of the defined quantities is given by its closed form: the Choi matrix is computed from the channel, is the infimum over all separable states (not or an infimum over diagonal states), and is defined from partial traces, not as . This rules out the trivializing formalization in which a milestone or the goal holds by definition. The bound alone holds for every state; the goal's bound is .
The operational capacities and of Eq. (95) are not formalized. They are defined over adaptive LOCC protocols with private-state targets, which have no substrate on the platform. The paper also does not prove the two bridges from them to the bounds: it imports (Eq. (2), from Pirandola et al.) and the hashing inequality (from Devetak and Winter). For the same reason, the reverse inequality is not stated, since the paper obtains it only through the hashing bound. Teleportation stretching, convexity of the flux, the bosonic Gaussian channels and the erasure channel are outside this mission.
Contributions are welcome at every level: the spectrum of circulant blocks, the support calculus of the Umegaki entropy, and the separable decomposition of diagonal states are all reusable beyond this mission.
A Gittins index assigns a number to an uncertain arm in a discounted bandit problem. The index converts a sequential choice, where an agent may keep gathering information or retire, into a tax threshold for playing the arm. Computing it generally requires an optimal stopping calculation. A Bayesian upper confidence bound, by comparison, is a quantile of the posterior distribution and is directly available for a Gaussian posterior. Russo's note asks how closely these two quantities agree when the agent is patient and the discount factor approaches one. The answer is an asymptotic identity for a Gaussian arm, not a finite-discount formula. Russo, 2019, pp. 1–3.
The note places its result alongside work on computational approximations of Gittins indices and finite-horizon index policies, but aims at the conceptual relationship with Bayesian confidence bounds. It appeared as an arXiv preprint in 2019; this mission follows that version's theorem numbering and formulas. A later journal publication appeared in Operations Research in 2021, but its numbering is not used here.
One arm has an unknown quality . The prior distribution is Gaussian, , where and . Playing the arm at time yields , where the observation noises are independent Gaussian variables of mean zero and variance . After observing , the posterior is . Its mean and variance follow the Gaussian update (1) of Russo, p. 2. In particular, .
For each play, the agent pays a tax . The agent may retire, receiving zero thereafter. At discount factor , an admissible retirement time uses only the rewards observed through the current time. Its discounted payoff includes the play at : . The value is the supremum of the expected payoff over these retirement times. The Gittins index is the supremum of taxes for which the value is nonnegative. These are the stopping-time value and fair-tax definition in equations (2)–(3) of Russo, p. 2.
Write and for the distribution function and density of , and . Thus is the prior's upper -quantile, with .
The goal is Theorem 1, p. 3, for each fixed prior mean, positive prior variance, and positive observation-noise variance:
The remainder is an additive quantity tending to zero; the claim does not assert equality at any fixed discount factor. The paper reduces the general prior to a standardized one. Its intermediate targets are the normal-quantile asymptotic, explicit bounds on , an upper bound obtained from noiseless information, and a matching lower bound from an admissible exploration policy. They appear as the mission's milestones, along with the posterior identities the lower bound uses. Russo, pp. 3–6.
The theorem identifies the limiting tax threshold with a familiar statistical quantile. It explains why a Bayesian upper confidence bound can approximate the Gittins priority of an arm when the effective horizon is large. It does not state that a quantile policy is exactly optimal at a fixed horizon or discount factor, and the paper's limitations section notes that significant observation noise relative to the horizon can make exploration costly. Russo, pp. 3, 7.
For a formal development, the reusable pieces are a Gaussian stopping-time model, the fair-tax index, the normal tail and positive-part estimates, and posterior update identities. The asymptotic theorem is proved in the source paper but has no machine-checked proof in this mission. Its local Lean statement is a target with sorry; the same applies to the milestone theorems. The definitions and a small sanity lemma compile in the pinned environment. Contributions that establish the source's stated bounds, their probabilistic prerequisites, or the final asymptotic reduction are relevant.
The direct idea of replacing the index by a posterior quantile at each fixed does not establish the theorem. The index optimizes over retirement times that adapt to noisy observations. A decision maker who sees without noise has a larger value, so the resulting expression supplies an upper bound, but it does not give a lower bound for the original information structure. The paper's matching lower estimate uses an actual reward-adapted policy and tracks both the cost of initial sampling and the benefit of later commitment. The two estimates must agree to an additive , not merely at their leading order. Russo, §§3.3–3.4, pp. 4–7.
Lean uses the canonical probability space : the first coordinate is , and the second is the independent noise sequence. The model measure is the Gaussian prior times an infinite product of Gaussian noise laws. The reward history at time generates . An admissible -valued stopping time has ; means never retire. The stopped reward is a countable sum. The index is the supremum of the nonnegative-value tax set. Only the discount domain is used in fixed-discount statements; limits approach one from below. Variances are nonnegative reals at the Mathlib Gaussian interface, with strict positivity assumed in the theorem statements. The paper suppresses in the index notation; Lean keeps it explicit and arbitrary.
The value is defined from the stopping problem and the index from the fair-tax set. Retirement decisions depend on observed rewards only; giving them access to would change the target. The posterior variance uses in its closed form, correcting a printed error in (1). Lemma 3's limit is , and Lemma 7 uses in its little-o scale; their printed versions are inconsistent with the surrounding derivations. The natural-language item notes identify these corrections. Russo, pp. 2, 4, 6, 9.
Measurements of long quantum spin chains can have outcomes far from their typical values. A large-deviation principle quantifies how quickly the probability of such outcomes decreases with the number of sites. In a classical lattice system this is a standard way to describe rare macroscopic fluctuations; in a quantum chain, observables on overlapping sets of sites generally fail to commute, which makes the corresponding probability laws harder to analyze. Ogata's 2008 paper establishes a full principle for the energy density of any translation-invariant finite-range interaction in a -finitely correlated state. Its introduction explains that earlier spin-chain results covered upper bounds or more restricted observables and states, while the lower bound for general observables remained the substantial issue. Ogata, pp. 2–4
The finitely correlated class includes local states generated from finite auxiliary memory. It is large enough to include mixtures and periodic behavior, so a theorem restricted to a primitive transfer map would miss part of Ogata's statement. This mission targets the printed Theorem 1.2 in its full scope. Ogata, p. 4
At each site let be the algebra of complex matrices. On sites , the local algebra is the -fold tensor product, represented as matrices whose rows and columns are spin configurations. A finite-range translation-invariant interaction assigns a Hermitian operator to each finite set of sites , with the same term on translated sets and with when the diameter of exceeds a fixed range. Its finite-volume Hamiltonian is
The sum includes the scalar term associated with the empty set. The interaction need not be nearest-neighbor and may have a term on any finite pattern within its range. Ogata, pp. 2–3
A -finitely correlated state is specified by a finite-dimensional auxiliary algebra , a unital completely positive map , and a faithful stationary state on . Iterating gives a compatible local state on sites. The probability measure is the spectral distribution of in : for a Borel set , it assigns the state weight of the spectral projection corresponding to . These local restrictions determine the distributions used in the theorem. Ogata, pp. 3–4
The goal is a good rate function : is lower semicontinuous and each set is compact for finite . For every closed and open in , Theorem 1.2 asserts
One rate function serves both inequalities and every eligible set. The statement asserts existence, without imposing a formula for or a primitivity condition on the auxiliary map. Ogata, pp. 3–4
The milestone list includes the paper's Gärtner–Ellis theorem, the spectral-law exponential-moment identity behind equation (1), the two-sided order estimate (15) for a gapped auxiliary map, the regrouping of consecutive sites into one site, under which the same state is generated by the -th iterate of the transfer map and , and the differentiable limiting pressure under condition (14). In the last target, the pressure is the limit of for every real . These are narrower claims with separate hypotheses; none replaces the full goal. Ogata, pp. 4–5, 12–15
The theorem gives an exponential-scale description of the energy-density distribution for all translation-invariant finite-range interactions in this state class. The upper bound controls probability on closed sets; the lower bound supplies the matching guarantee for open sets. Compact sublevel sets prevent low-rate mass from escaping to infinity. The result is already proved in Ogata's paper; the remaining work here is a machine-checked development of the statement and its supporting mathematics. Ogata, Theorem 1.2
Formalizing the finite-dimensional transfer construction, its spectral measures, and an extended-valued LDP vocabulary would also make these objects available for later spin-chain results. The goal itself is not currently accompanied by a machine-checked proof in this mission. The Gärtner–Ellis and auxiliary-map statements are likewise proof targets, not asserted as solved Lean facts.
The exponential of a sum of overlapping local interaction terms cannot generally be factored into independent one-site contributions. Even when an auxiliary transfer map has a spectral gap and yields a differentiable limiting pressure, that argument does not directly cover every finitely correlated state. A mixture can have a limiting log moment generating function with a corner; the resulting rate function can be nonconvex. Ogata's printed Lemma 4.1 reduces to special components but omits the separate mixture step needed to recover the unrestricted theorem. The goal retains the theorem's printed hypotheses, while the condition-(14) milestone records precisely the restricted pressure claim. Ogata, pp. 12–15
The Lean model uses finite matrices for local algebras. A nonempty finite site basis represents , with site 1 indexed by 0. An interaction stores one Hermitian term for each support anchored at its least site; all translates that fit in appear in the Hamiltonian. The scalar empty-set term is retained. The auxiliary algebra is represented by a full matrix algebra ; finite-dimensional -algebra data have an equivalent full-matrix representation for the generated local states. Stationarity is written in the primal trace form. The recursive local state places the first site's matrix in the outermost application of .
The spectral law is formed from the eigenvalues and spectral weights of the actual Hamiltonian. It is not supplied as an arbitrary sequence of measures. The theorem uses no ergodicity, spectral-gap, or condition-(14) binder, and both LDP bounds range over every closed or open subset of . Logarithms of probabilities take values in the extended reals, with ; sequence limits are at , so the placeholder value at is immaterial. Nonnegative lower integrals represent exponential moments. In the restricted pressure milestone, the real logarithm applies to a positive state expectation. These choices also rule out a vacuous proof based on a zero measure, a moment represented by a non-integrable Bochner integral, or a rate function unrelated to the spectral law.
Reusable contributions include finite-dimensional spectral-law lemmas, positivity and stationarity facts for completely positive maps, good-rate-function and LDP lemmas on , and the Gärtner–Ellis result. The full theorem additionally needs a treatment of non-ergodic finite mixtures and periodic components that preserves both large-deviation bounds.
Optical quantum communication commonly encodes information in continuous variables such as the position and momentum quadratures of a light mode. Gaussian states and Gaussian operations are attractive in this setting because phase shifters, squeezers, beam splitters, and homodyne measurements are standard optical tools. Transmission through a lossy or noisy line can also be modeled by a Gaussian channel. The practical question is whether adding vacuum modes and Gaussian encoding and decoding can protect a signal against such a channel. Niset, Fiurášek, and Cerf (2008) give a negative answer for the code class defined in their Fig. 1.
The result sits after the early impossibility results for distilling Gaussian entanglement with Gaussian operations, including Giedke and Cirac (2002). Those results concern shared states and allowed local operations. The 2008 paper asks the channel-coding question directly: whether a finite Gaussian code can make a fixed single-mode Gaussian channel less damaging to entanglement. It introduces a scalar, entanglement degradation, to state the answer for every single-mode Gaussian channel in one inequality.
A single optical mode has two real quadratures, and . For modes, the order is . A state has a real covariance matrix recording its second moments in this order. The vacuum covariance matrix is the identity . A Gaussian channel on one mode is described at the covariance level by two real matrices and :
Here is the added noise. Complete positivity imposes symmetry and a matrix positivity condition on ; in particular, it gives . A Gaussian unitary changes covariances by a symplectic matrix , satisfying for the canonical symplectic form . Displacements affect first moments only and therefore play no role in these covariance formulas.
The code uses a positive integer . The input occupies mode zero in the formalization; the other modes are vacuum ancillas. A Gaussian encoding unitary acts on all modes, then the same channel acts independently once on each mode, and a Gaussian decoding unitary acts on all modes. Only the first output mode is retained. This defines an effective single-mode channel with matrices . The ancillas contribute noise to even before the channel uses are counted.
For a channel , the paper defines its degradation by
The intended value is when the denominator vanishes: the quotient is then interpreted as infinite and is saturated by the minimum. This quantity is related to the entanglement remaining when acts on one half of a two-mode squeezed vacuum as the squeezing grows. The paper measures that entanglement through the smallest symplectic eigenvalue after partial transpose and the logarithmic negativity .
The mission goal is the theorem on page 3, equation (11): for every completely positive single-mode Gaussian channel and every finite code of the stated form,
This is the assertion that the code cannot lower the channel's entanglement degradation. It includes , singular channels, and channels with negative determinant . No numerical performance constant or bound on the number of modes is fixed.
The milestones record the paper's channel-noise constraint (2), the fact that the code produces a Gaussian channel, the local matrix normal forms used in Lemma 2, the asymptotic calculations (8) and (10), the entanglement-breaking case, and Lemma 2 itself. Lemma 2 characterizes the degradation through the limiting squared eigenvalue and, when finite, gives . The milestones retain the paper's distinction between positive, negative, and zero determinant regimes.
The theorem rules out a specific and broad way of improving Gaussian transmission: adding any finite number of vacuum ancillas and using Gaussian unitaries before and after independent uses of a fixed channel cannot improve this intrinsic entanglement measure. The paper applies this conclusion to attenuation, amplification, and classical-noise channels, showing how an apparent reduction in one channel parameter can be offset by increased noise. It also relates degradation to an upper bound on quantum capacity, though that further bound is outside this mission. Niset, Fiurášek, and Cerf (2008)
The paper's theorem is proved in the mathematical literature; the goal here is a machine-checked statement and, eventually, a proof in the covariance-matrix representation. The published covariance layer already supplies symplectic forms, two-mode squeezed covariances, partial transpose, and an intrinsic ; this mission adds the channel and code definitions required to state the no-go theorem. Those definitions can be reused for other single-mode Gaussian-channel questions. A complete proof still needs substantial results connecting codes, Gaussian operations, and entanglement behavior; a compiled sorry statement alone does not establish the theorem.
One might try to compare before and after the code. That scalar does not track the code: encoding mixes signal and vacuum modes, each copy of the channel adds noise, decoding mixes the modes again, and discarding modes changes both and . Neither determinant separately gives the desired inequality. The boundary also defeats a direct real-valued transcription of the printed quotient. The asymptotic entanglement formulas cross several determinant regimes, with different normal forms and a separate entanglement-breaking case. The central challenge is to retain the physical meaning of all these cases in one theorem over arbitrary finite codes.
Lean uses real matrices indexed by interleaved mode and quadrature coordinates. The published QAlgorithms_Papers_Independent_Frontier30_P13 layer provides ModeQuadrature, phaseJ, squeezedCM, partial transpose, and the intrinsic smallest symplectic eigenvalue lambdaMin; QAlgorithms_Papers_Independent_Dependency50_P10 provides entrywise complexification. A channel is required to satisfy the Gaussian complete-positivity matrix inequality. Encoders and decoders satisfy . The code uses the same on every one of its modes, with , and includes the vacuum covariance on every ancillary mode. Gaussian unitaries enter through their symplectic matrices; their displacement parts do not affect covariances.
The definition of explicitly saturates at when , avoiding Lean's zero value for division by zero. The squeezed input uses and . The eigenvalue is the intrinsic lambdaMin, not an unguarded square-root expression. Logarithmic negativity uses the natural logarithm; its finite limit statement assumes , while the degradation statement still covers . The infinite-squeezing output is represented by limits of finite- covariances and entanglement quantities.
The code's vacuum term, all noise blocks, the symplectic equation, and the guarded degradation are essential to the target; dropping any of them would change the question. Lemma 1's teleportation equivalence and the external Gaussian no-distillation theorem are not formalized here. Their faithful treatment would require operational Gaussian states, measurements, and protocols beyond the covariance model. Contributions establishing those interfaces, proving the stated matrix milestones, or connecting the two layers are welcome.
Quantum circuits whose gates respect a global symmetry are a standard model for quantum simulation, for symmetry-protected quantum computing, and for the study of conserved quantities in quantum dynamics. For SU(d) symmetry on qudits, the unitaries that commute with every are, by Schur–Weyl duality, exactly the unitaries in the linear span of the qudit permutations. A natural question is whether every such unitary can be built from local symmetric gates, as happens without symmetry, where 2-qudit gates are universal.
Marvian, Liu and Hulse (arXiv:2105.12877) show that for the answer is no, and that the obstruction appears as conservation laws. Unitaries generated by 2-local SU(d)-invariant gates conserve quantities that general SU(d)-invariant unitaries change. The paper gives two families of such laws. The first, Theorem 1 (the law, from a symmetry of the swap Hamiltonians), is a separate result of the paper and is not part of this mission. The second, Theorem 2, is the target here. It comes from a correspondence between a subspace of the qudits and a system of free fermions.
Timeline: Marvian (Nature Physics 18, 283, 2022) showed that symmetry together with locality restricts the realizable unitaries in general, with examples for U(1) and SU(2) symmetry. For qubits with SU(2) symmetry, the constraints restrict only relative phases between sectors of inequivalent irreducible representations (p. 3 of the present paper). The present paper (arXiv:2105.12877, v2 January 2022) treats SU(d) with , where constraints beyond relative phases appear. The connection to Marin's 2007 description of the Lie algebra generated by transpositions (J. Algebra 310, 742) is discussed on p. 9.
Consider qudits with Hilbert space and computational basis , .
For , the vector antisymmetrizes the levels over the first qudits with weight (Eq. (40)). The subspace is the span of all permutations of these vectors (Eq. (42)), and is the orthogonal projector onto it.
For an operator on one qudit, is acting on qudit . Let . The map sends an operator on the qudits to the matrix
(Eqs. (49), (51)). On the fermionic side there are sites, creation operators , the vacuum , and the fermionic swap (Eq. (28)). Its single-particle counterpart is on (Eq. (33)). The map sends to (Eq. (41)).
For every , every density operator on qudits and every positive integer ,
The statement holds for all and . Its content is the case : the case holds for every SU(d)-invariant unitary (Eq. (55)).
Theorem 2 gives an infinite family of polynomial invariants of the state, for . Together these fix the spectrum of , so every Rényi entropy of the single-particle density operator is conserved. Already for the law is violated by SU(d)-invariant Hamiltonians with 3-local terms (p. 11 and §IV D). This shows that, for , 2-local SU(d)-invariant gates are not universal among SU(d)-invariant unitaries, even up to relative phases, and that 3-local interactions can be detected from the dynamics of . For the laws hold for all SU(2)-invariant unitaries.
The result is proved in the paper. As far as a search of the platform shows, it has not been formalized. A formalization adds machine-checked versions of the qudit–fermion correspondence of §IV B, including the isometry and the intertwining relation (44), and of the free-fermion form of the swap dynamics. These are statements about finite-dimensional matrices, so the whole development stays inside Mathlib's linear algebra.
The obvious route is to show that each generator acts on by conjugation with an unitary, and then to induct over products. The difficulty is the generator step. The definition (51) of involves the projector onto a span of antisymmetrized vectors, and nothing in (51) shows directly why conjugating by should conjugate by . The covariance becomes visible only after is identified with fermionic Fock sectors, where the swap becomes a quadratic, particle-number-preserving Hamiltonian. That identification needs care with the signs of the fermionic creation operators and with the ordering of products. A second obstacle is the characterization of the generators (Eq. (5)). It rests on the commutant of being spanned by and the swap, a Schur–Weyl statement for two qudits that Mathlib does not provide.
Operators on the qudits are matrices indexed by Fin n → Fin d, with sites and levels 0-based and [NeZero d] assumed so that exists. Fock-space operators are matrices indexed by Finset (Fin n), the set of occupied sites. The creation operator uses the Jordan–Wigner sign , the encoding of the public definition QAlgorithms_Papers_Independent_Next46_P23, copied rather than imported.
The following conventions are fixed:
EuclideanSpace ℂ (Fin n → Fin d).QAlgorithms.Entanglement.IsCompletelyPositive.The following trivializing formalizations are ruled out:
A complete development needs:
Finset Fock space;The Fock-space and permutation-operator lemmas can be reused for other qudit–fermion and Schur–Weyl statements. Contributions welcome: proofs of any milestone, and lemma-level infrastructure on the Fock space.
In the fluid queuing model (Vickrey's model) of flows over time, a continuum of infinitesimal particles travels from a source to a sink through a network whose arcs have capacities and transit times. Each particle picks a route that minimizes its own arrival time, and a dynamic equilibrium (a Nash flow over time) is a flow in which no particle can arrive earlier by deviating. Dynamic equilibria are a basic model of congestion in road traffic and communication networks.
Koch and Skutella (2011) showed that the derivatives of a dynamic equilibrium are normalized thin flows with resetting, and Cominetti, Correa and Larré (2015) proved that such thin flows always exist, which gives existence of equilibria. Computing a thin flow, however, was known to be efficient only in the two extreme cases where no arc or every arc is resetting. Kaiser (2022) casts thin flows as a linear complementarity problem, studies how they depend on the flow value, and shows that on two-terminal series-parallel networks the whole family of thin flows, for all flow values at once, can be computed in polynomial time. The key quantitative fact behind that algorithm is a bound on the number of breakpoints of the thin-flow labels as a function of the flow value. This mission formalizes that bound and the chain of results it rests on.
A network is a finite directed multigraph with vertex set , arc set and two vertices . It is a shortest path graph if is acyclic and every vertex is reachable from . Fix a set of resetting arcs and capacities . A static –-flow of value is a vector on the arcs that is conserved at every vertex other than and has net outflow at .
Along an arc a label is propagated by
Labels correspond to the flow if for every and on every arc with ; such an is a normalized thin flow with resetting (Definition 4).
The label function maps each flow value to the corresponding labels, with label at , of a normalized thin flow of value . A breakpoint of is a value around which some component of is not affine.
A two-terminal series-parallel multigraph is built from single arcs by series composition (sink of glued to source of ) and parallel composition (sources glued, sinks glued).
For a two-terminal series-parallel multigraph , any and any capacities : the label function exists, is continuous on , has finitely many breakpoints, and
The milestones follow the paper's proof path.
The bound is what makes the recursive computation of along a series-parallel decomposition run in time polynomial in the size of the network. Each composition step is linear in the number of pieces, and Theorem 31 keeps the number of pieces linear in . Combined with the paper's §5, the result computes dynamic equilibria in series-parallel networks for piecewise constant, and more generally right-monotone, inflow rates. For general graphs the complexity of computing a thin flow with resetting is open: the problem lies in PPAD, and no polynomial algorithm is known. The bound is attained already for a single non-resetting arc, whose label at is .
The results are proved in the paper. None of them has been formalized: there is no machine-checked theory of flows over time, thin flows or directed series-parallel graphs. A formalization adds three things. It gives a checked LCP formulation of thin flows, which is reusable for any equilibrium computation in this model. It gives a checked parametric analysis (existence, uniqueness, monotonicity and piecewise linearity of the labels). And it gives a complete account of the counting argument for parallel composition, which the paper extends from the sink's label to the whole label vector only in outline ("Repeating the counting more carefully…").
Existence (Theorem 13) is not elementary. It combines a principal-minor computation for a block matrix with a theorem from LCP theory: a -matrix whose LCP has only the trivial solution at zero data has a solution for every right-hand side. Mathlib has neither. Piecewise linearity (Proposition 17) likewise uses that solution sets of an LCP are finite unions of polyhedra.
The breakpoint count is subtle in the parallel case. Splitting the flow between the two parts is generally not unique, so is not simply a composition of and . The proof constructs a piecewise linear selection of the split and counts where its pieces can change. A tempting shortcut is to bound only the breakpoints of the sink's label . That is weaker than what is claimed, which is a bound for the entire label vector.
Net) with arc types and tail/head maps, so parallel arcs are first-class.Finset of arcs and capacities are real with .IsLeast, never sInf.T.toNet of terms T : SPTerm built from arc, series and par. Every member of Definition 28's class is isomorphic to such a graph, and all quantities here are isomorphism-invariant.Set.encard in Lemmas 29–30 and with Set.ncard plus finiteness in the goal.A complete development needs:
The LCP layer and the network and series-parallel layer are reusable beyond this mission. Contributions to either are welcome, as are proofs of the elementary milestones (Lemma 7, Lemma 11, Theorem 14, Corollary 15) independently of the rest.
The walled Brauer algebra is the centralizer algebra of mixed Schur–Weyl duality: for it acts on the mixed tensor space of and commutes with , and for it plays the same role for the general linear supergroup . Its representation theory has been studied through cellular structures and blocks (Cox–De Visscher–Doty–Martin 2008), Khovanov arc algebras (Brundan–Stroppel 2012) and cyclotomic quotients (Sartori–Stroppel 2015).
For the group algebra of the symmetric group there is a classical description of the center: it consists of the symmetric polynomials in the Jucys–Murphy elements (Jucys 1974, Murphy 1983). Jung and Kim (arXiv:1508.06469v2) prove the walled analogue: when is semisimple, its center is generated by the supersymmetric polynomials in its Jucys–Murphy elements. This mission formalizes that theorem and the chain of results leading to it.
Timeline. Jucys (1974) and Murphy (1981, 1983) describe the center of through Jucys–Murphy elements. Stembridge (1985) characterizes supersymmetric polynomials and shows that the power sums generate them. Cox, De Visscher, Doty and Martin (2008) give the cellular structure of , its blocks in characteristic zero and a semisimplicity criterion. Brundan and Stroppel (2012) prove that the central element (essentially ) acts on cell modules by a content sum. Jung and Kim (2015, revised 2017) prove the generation theorem for all supersymmetric polynomials.
Fix integers and . An -walled Brauer diagram is a pairing of vertices, on top and on the bottom, with a wall between positions and , such that vertical edges do not cross the wall and horizontal edges do. is the complex vector space with these diagrams as basis; two diagrams are multiplied by stacking them and replacing each closed loop by a factor .
For vertices on the same side of the wall, is the diagram of the transposition of and . For , is the diagram with a top arc and a bottom arc joining and and all other vertices joined straight down. The Jucys–Murphy elements (Definition 2.1) are
A polynomial is supersymmetric (Definition 2.8) if it is symmetric in the and in the separately, and the substitution produces a polynomial independent of . Examples are the power sums . Write for the supersymmetric polynomials and for the substitution , .
The cell modules are indexed by bipartitions with , , ; this set is . The set equals except when and , where is removed; it indexes the simple modules. The content vector lists the contents of , then zeros, then the contents of shifted by .
Both inclusions are asserted. The goal fixes no constants; the hypothesis holds for all but finitely many (Proposition 1.1).
The theorem gives an explicit generating set for the center of a semisimple walled Brauer algebra, parallel to the symmetric-group case. Its consequences in the paper include a description of the Gelfand–Zetlin subalgebra and formulas for primitive idempotents (§4), an alternative proof of the block classification of Cox et al. (§5), and, via the same method, the center of the quantized walled Brauer algebra (§6). Corollary 2.9 alone, valid for every , provides a supply of central elements whose action on each cell module is computed by Corollary 3.3.
The theorem is proved in the paper; no part of it is formalized. A formalization would supply machine-checked Jucys–Murphy relations for a diagram algebra built on a published, generic encoding of walled Brauer diagrams, a Lean development of supersymmetric polynomials (including Stembridge's theorem, absent from Mathlib), and a reusable dimension count for centers of semisimple algebras in terms of simple modules.
The inclusion of the supersymmetric polynomials in the center (Corollary 2.9) reduces to diagram relations plus Stembridge's theorem; the latter is a nontrivial statement about polynomial rings, with no counterpart in Mathlib. The reverse inclusion is the harder half. A central element is not visibly a polynomial in the : the argument must show that enough linearly independent central elements of the form exist, which requires computing their scalars on every cell module (an explicit cellular computation involving the arc elements ), separating all content vectors (where semisimplicity enters through the criterion of Cox et al.), and comparing with , which needs Wedderburn–Artin together with the classification of simple modules. Separation genuinely fails outside the semisimple range, so no argument independent of can work.
The algebra, diagrams, cell modules , the index sets (CellIndex) and (Label) and contents are the published definitions WalledBrauer_Blocks_{Diagram, Algebra, ModuleTheory, Partitions, CellModules}, used as references. New definitions are in WalledBrauer.Center.Setting. Conventions:
Fin (r + s)); the paper's is jm δ ⟨k-1, _⟩.MvPolynomial (Fin r ⊕ Fin s) ℂ. The evaluation is defined monomial by monomial in increasing vertex order, without assuming that the commute; it is never routed through a commutative subalgebra.IsSemisimpleRing, the center is Subalgebra.center ℂ, "generate" is Algebra.adjoin ℂ. In Proposition 1.1, is real.Supersymmetry is defined intrinsically on polynomials, never through the algebra, so neither inclusion of the goal holds by definition; stating only or only as the goal is excluded.
Proofs of any milestone are welcome, as are reusable developments of supersymmetric polynomials (Stembridge's theorem, elementary supersymmetric polynomials) and of the center of a split semisimple algebra.
Statistical decision theory compares two experiments by asking which one is more useful: one experiment is deficient with respect to another if, in every decision problem, it achieves nearly the same payoff. The randomization criterion turns this operational comparison into a structural one: an experiment is -deficient exactly when a Markov kernel (a randomization) maps the better experiment to within of the worse one in -distance. Its exact case, the Blackwell–Sherman–Stein theorem, is a standard tool in statistics and economics, and the approximate version is the basis of Le Cam's theory of comparison of experiments (Strasser 1985; Torgersen 1991).
Quantum information asks the same question for quantum devices: when can one channel be simulated from another by further processing, and how is that detected by tasks? A short timeline of the results this mission builds on:
This mission formalizes the central result of the last paper: the randomization theorem for post-processings of channels (Theorem 3, p. 15).
All spaces are finite-dimensional. A Hilbert space is with its standard basis and is the algebra of complex matrices. A C-algebra* is a block-diagonal algebra with ; full matrix algebras and the diagonal (classical) algebras are the extreme cases. is the set of density matrices in .
is the real space of Hermitian linear maps from to , paired with by , where is the trace of a map on matrices.
An admissible family of positive cones (Definition 1) assigns a closed convex cone of Hermitian maps to every pair of spaces, with , and . Here , and are the positive, completely positive and entanglement-breaking maps. Examples are , , and the -positive maps. Restricted to algebras, is a cone in , and is the dual of under the pairing. A -channel is a trace-preserving element of ; they form . is the replacement map .
The two norms on are
where and are the orders of and . For , is the usual diamond norm.
Given channels and , a decision algebra , decision rules and payoff maps , is -post-processing deficient with respect to , written , if every payoff achievable from is achievable from up to (Definition 3).
For the following are equivalent:
Moreover, if , then (all decision algebras) iff .
Lemma 1 (trace property of ); identity (1); (proof of Lemma 2); (p. 8); Corollary 8 (ii) for ; the dual formula (4) for ; Corollary 8 (iii) for channels; and Lemma 4, monotonicity of both norms under channels.
Theorem 3 says that a channel is approximately worse than another in every post-processing decision task exactly when every post-processing of the better channel can be approximated, in the (-)diamond norm, by a post-processing of the worse one. It contains the classical randomization criterion (classical algebras, ) and Matsumoto's quantum criterion (cq-channels, ) as special cases. Through the Moreover clause, it reduces deficiency over all decision algebras to a single one, the output algebra. Because is arbitrary, the same statement covers positive, -positive and completely positive simulation.
The paper gives complete proofs, and the result is not open. No machine-checked version of it, of the base-section norms, or of admissible cone families exists on the platform or in Mathlib. A complete development gives a reusable, Mathlib-only layer for Hermitian maps between block algebras, their trace pairing, cone families, and the diamond norm defined relative to a cone; and a formal proof of a quantum decision-theoretic equivalence that relies on a minimax theorem.
The equivalence (i)⇔(ii) and the implication (iv)⇒(i) are short once the norm duality is available: Corollary 8 (ii) and (iii), which identify norms of positive elements and differences of channels with suprema of payoffs. Formalizing those duality statements is the first obstacle. They rest on the appendix theory of base sections, including the fact (Theorem 8) that and are dual norms, which uses an extension theorem for positive functionals and closedness of the cones.
The step (iii)⇒(iv) is where the argument cannot be done pointwise. Condition (iii) gives, for each payoff separately, a decision rule depending on ; condition (iv) needs one that works for all at once. Exchanging the two quantifiers requires a minimax theorem on the compact convex sets (the unit ball of ) and , followed by formula (4). Compactness of needs closedness of .
All definitions are in one module, ChannelRandomization.PostProc.Setting, and depend only on Mathlib.
sInf/sSup. Their sets are nonempty and bounded when the dimensions are positive, and in dimension 0 both sides of every statement are 0.List.TFAE) together with the Moreover clause. "" means that the identity of lies in for every .The structure of admissible families is not vacuous: the positive maps form an instance, constructed sorry-free in a separate verification file. A formalization that defines the norms by the supremum formulas, fixes , drops the closedness of the cones, or restricts the decision algebra to one kind proves a different statement and does not count.
Out of scope are the pre-processing theorem (Theorem 5, whose proof the paper omits as "practically the same as the proof of Theorem 3"), the cq- and qc-channel specializations of §3.2.1–3.2.3, the pointwise deficiency results, and the Choi-matrix formula of Theorem 1.
Contributions are welcome at every level: proofs of the milestones, a general Lean theory of base sections and their norms (Theorem 8, Corollary 8 in abstract form) that would serve other ordered-vector-space arguments, and alternative proofs of (iii)⇒(iv) using Mathlib's minimax theorem.