Missions · Prove2Me

Completed

On properties of the space of quantum states and their application to construction of entanglement monotonesResearch Paper

Motivation

We consider two properties of the set of quantum states as a convex topological space and some their implications concerning the notions of a convex hull and of a convex roof of a function defined on a subset of quantum states. By using these results we analyze two infinite-dimensional versions (discrete and continuous) of the convex roof construction of entanglement monotones, which is widely used in finite dimensions. It is shown that the discrete version may be 'false' in the sense that the resulting functions may not possess the main property of entanglement monotones while the continuous version can be considered as a 'true' generalized convex roof construction. We give several examples of entanglement monotones produced by this construction. In particular, we consider an infinite-dimensional generalization of the notion of Entanglement of Formation and study its properties.

This mission is the statement-level formalization of On properties of the space of quantum states and their application to construction of entanglement monotones (arXiv:0804.1515v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Discrete Jensen inequality for upper-bounded extended costs (Proposition A-1: discrete Jensen inequality, PDF p. 31). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

55 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 2 (A-1, A-2, B, C, D): generalized convex-roof construction: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, MeanEnergy, EnergySublevel, TensorSubadditivity, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Proposition 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Proposition 2: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Lemma 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Lemma 2: QuantumState. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Proposition 3: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Proposition 4: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 2: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Proposition 5: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Proposition 6: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 3: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 4: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Theorem 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Lemma 3: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Lemma 4: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 5: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexRoof, MuConvexRoof, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 6: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 7: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Proposition 7: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, MeanEnergy, EnergySublevel, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Proposition 8: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 9: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RelativeEntropy, SpectralExponent, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Corollary 8: continuity on a fixed-marginal fibre: Printed statement requires correction: The stated separability assumptions do not ensure a purification in K. The reverse implication is false for one-dimensional K with an infinite-entropy marginal. A dimension or purification hypothesis is missing; do not silently add it. (source-ambiguity)
Lemma A-1: posterior expected-cost lower semicontinuity: TraceClass, QuantumState, Instrument, PosteriorStates. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§2.1: convexity fails to imply countable/integral convexity: QuantumState, OperatorRank. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 1: entropy separates finite/countable hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 2: σ/µ hull separation and Jensen failure: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, HilbertTensor, SeparableState, PureProductStates, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 3: µ hull versus convex closure: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
After Corollary 1: exact Jensen criterion: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Remark 1: σ roofs fail increasing convergence: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, SeparableState, PureProductStates, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Remark 2(1): decreasing convergence of µ hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Remark 2(2): decreasing convergence of µ roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Unnumbered analogue of Corollary 4 for µ roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Remark 3: automatic linear growth: QuantumState, EnergySublevel, AffineGrowth. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 4: output Rényi convex-closure limit: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 4, (18): equality at finite output entropy: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, MeanEnergy, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 4: continuous Rényi hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 4: uniform limit and constrained Holevo capacity: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, HolevoCapacity, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§4.1: existence of tensor regularization: HilbertTensor, TensorSubadditivity, EntanglementRegularization, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§4.1: global discontinuity of entropy-normalized measures: HilbertTensor, QuantumState, Entropy, PartialTrace, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Remark 6: discrete convex-roof counterexample: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, MixedStateIndicator, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 5: continuous power-purity monotones: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, PowerPurityCost, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 6: Rényi roofs and energy continuity: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RenyiEntropy, MeanEnergy, PartitionFunction, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§5.1: discrete/continuous EoF comparison and lower semicontinuity criterion: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§5.1: local truncations if the roofs differ: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, LocalTruncation, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§5.1: EoF stability under LOCC approaching identity: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§5.2: bounded continuous EoF approximations: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RankEntropyApproximation, OperatorRank, MeanEnergy, PartitionFunction, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§5.3: continuous local families: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§6: extension to stable µ-compact convex sets: GeneralBarycenterSpace, MuCompact, StableConvexSet, CountableExtremeGeneration, MuConvexRoof, SigmaConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Example 5 final sentence: claimed indicator supremum: Printed statement requires correction: The claimed supremum contradicts the printed generating cost on a pure Bell state: it is 2, not indicator value 1. No unique corrected formula is supplied. Retain the valid continuous family result independently and defer this sentence. (source-ambiguity)
§2.3: pure-state roofs as hulls of the +∞ extension: Printed statement requires correction: The unqualified +∞ extension need not be semibounded, while the source defines both hulls only for semibounded functions. For an upper-bounded pure-state f taking −∞ at one pure state, its extension takes both −∞ and +∞; a mixture charging that pure state and a mixed state has an undefined extended cost. The lower-bounded version used in the proof is meaningful, but does not settle the printed arbitrary-semibounded assertion. (source-ambiguity)
§2.2: greatest σ-convex minorant: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§2.3: greatest σ-convex extension: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
Remark 6 continuation: pathology of unequal roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, MuConvexity, SigmaConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
§5.2: properties of rank-constrained entropy approximants: Entropy, QuantumState, Ensemble, OperatorRank, RankEntropyApproximation. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)

Selected references

On properties of the space of quantum states and their application to construction of entanglement monotones, arXiv:0804.1515v4, https://arxiv.org/abs/0804.1515v4

4 thms2 active usersReviewed

Quantum Information·Captain: Goku

Attainability and lower semi-continuity of the relative entropy of entanglement, and variations on the themeResearch Paper

Motivation

The relative entropy of entanglement $E_R$ is defined as the distance of a multi-partite quantum state from the set of separable states as measured by the quantum relative entropy. We show that this optimisation is always achieved, i.e. any state admits a closest separable state, even in infinite dimensions; also, $E_R$ is everywhere lower semi-continuous. We use this to derive a dual variational expression for $E_R$ in terms of an external supremum instead of infimum. These results, which seem to have gone unnoticed so far, hold not only for the relative entropy of entanglement and its multi-partite generalisations, but also for many other similar resource quantifiers, such as the relative entropy of non-Gaussianity, of non-classicality, of Wigner negativity $\unicode{8212}$ more generally, all relative entropy distances from the sets of states with non-negative $\lambda$ -quasi-probability distribution. The crucial hypothesis underpinning all these applications is the weak*-closedness of the cone generated by free states, and for this reason the techniques we develop involve a bouquet of classical results from functional analysis. We complement our analysis by giving explicit and asymptotically tight continuity estimates for $E_R$ and closely related quantities in the presence of an energy constraint.

This mission is the statement-level formalization of Attainability and lower semi-continuity of the relative entropy of entanglement, and variations on the theme (arXiv:2105.08091v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (seed): attainability, lower semicontinuity, compactness and uniqueness (Theorem 5 (seed): attainability, lower semicontinuity, compactness and uniqueness, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

29 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 9: dual variational formula for resource relative entropy: support-compressed exponential and log-partition (hard)
Lemma 11: Gibbs variational formula without faithfulness: log-partition at singular and zero positive trace-class operators (hard)
Lemma 13: duality for a weak*-compact convex subnormalised set: support-compressed log-partition and extended inner supremum (hard)
Remark 14: Petz dual formula without faithfulness: nonfaithful Petz log-partition functional (hard)
Corollary 20: bipartite relative entropy of entanglement: completed bipartite state space, closed-hull separability and log-partition (hard)
Corollary 22: weak*-closed cones for partition separability: partition-indexed completed tensor products and closed-hull pi-separability (hard)
Corollary 23: multipartite relative entropy of partition entanglement: multipartite pi-separable distance and log-partition (hard)
Lemma 24: weak*-closed PPT cone: partial transposition T(H_A tensor H_B) to B(H_A tensor H_B) (hard)
Corollary 25: relative entropy of NPT entanglement: PPT state space, extended distance and log-partition (hard)
Lemma 30: photon-number attenuation preserves lambda positivity: concrete Weyl representation, lambda-positive states and number attenuation (hard)
Corollary 31: weak*-closed lambda-positive cone: lambda-positive cone on the actual m-mode Hilbert space (hard)
Corollary 32: relative entropy of lambda negativity: lambda-positive distance and support-compressed dual formula (hard)
Lemma 33 (cited): quantum Darmois–Skitovich characterisation as printed: a corrected quantum Darmois-Skitovich statement and unitary beam splitter (source-ambiguity)
Lemma 34: weak*-closed cone of Gaussian states: all displaced m-mode Gaussian states as actual trace-class states (hard)
Corollary 35: attainability and lower semicontinuity of non-Gaussianity: Gaussian-state set, Gaussification and moment-defined entropy identity (hard)
Unnumbered consequence after Corollary 35: entropy of Gaussification: actual Gaussification on the finite-number-energy state set (hard)
Unnumbered result (124): finite-local-dimension continuity bounds: six bipartite entanglement measures and tensor-power regularizations (hard)
Proposition 36: bipartite energy continuity estimates (125),(127): all six resource measures, energy moduli and oscillator specialization (hard)
Proposition 36: generic-G asymptotic-tightness clause: a valid hypothesis set for generic-G asymptotic tightness (source-ambiguity)
Remark 37: faithfulness of the bipartite continuity modulus: the source-admissible G and actual generalized-inverse continuity modulus (hard)
Corollary 38: uniform and asymptotic continuity of six bipartite measures: six bipartite measures on correlated n-copy states and additive energy (hard)
Unnumbered multipartite entropy upper bounds (149),(150), proved in Appendix C: multipartite marginals and extended local entropy upper bounds (hard)
Unnumbered result (151): finite-dimensional multipartite continuity: partition separability, one unrestricted final factor and singleton-only regularization (hard)
Proposition 39: multipartite energy continuity estimates (155)–(157): multipartite energy budgets and the complete three continuity moduli (hard)
Proposition 39: asymptotic-tightness clause for m=2: partition-restricted large-energy tightness (source-ambiguity)
Remark 40: faithfulness of multipartite continuity moduli: the actual H[s] entropy capacity and multipartite moduli (hard)
Corollary 41: uniform and asymptotic multipartite continuity: grouped multipartite copies, additive local energies and partition measures (hard)
Lemma 43: infinite-dimensional Lieb three-operator inequality: support-compressed exponential of log A+log B-log C (hard)
Lemma 44: countably decomposable separable approximation to a pure state: actual countable pure-product mixture with all prescribed marginals (hard)

Selected references

Attainability and lower semi-continuity of the relative entropy of entanglement, and variations on the theme, arXiv:2105.08091v3, https://arxiv.org/abs/2105.08091v3

13 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

The Zero Set of a Real Analytic FunctionResearch Paper

Motivation

A brief proof of the statement that the zero-set of a nontrivial real-analytic function in $d$ -dimensional space has zero measure is provided.

This mission is the statement-level formalization of The Zero Set of a Real Analytic Function (arXiv:1512.07276v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A nontrivial real-analytic function has a Lebesgue-null zero set (Proposition 0, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

The Zero Set of a Real Analytic Function, arXiv:1512.07276v1, https://arxiv.org/abs/1512.07276v1

7 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

The optimal unitary dilation for bosonic Gaussian channelsResearch Paper

Motivation

A generic quantum channel can be represented in terms of a unitary interaction between the information-carrying system and a noisy environment. Here, the minimal number of quantum Gaussian environmental modes required to provide a unitary dilation of a multi-mode bosonic Gaussian channel is analyzed both for mixed and pure environment corresponding to the Stinespring representation. In particular, for the case of pure environment we compute this quantity and present an explicit unitary dilation for arbitrary bosonic Gaussian channel. These results considerably simplify the characterization of these continuous-variable maps and can be applied to address some open issues concerning the transmission of information encoded in bosonic systems.

This mission is the statement-level formalization of The optimal unitary dilation for bosonic Gaussian channels (arXiv:1009.1108v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Complex kernel and rank relations for Gaussian channel data (Section II, Eqs.(6)–(10), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

4 results of the paper are not stated yet, because the library lacks an interface they need:

Main result, Eq.(12): Actual multimode Fock Gaussian channel, pure Gaussian environmental density, Gaussian unitary and tensor partial trace (hard)
Section III, Eqs.(16),(29): Actual finite-theta thermal CJ state and Stinespring-induced Gaussian purification (hard)
Section V, Eqs.(48)–(49): Mixed Gaussian environment implementing the full channel on every input (hard)
Section IV, Eqs.(34)–(47), last paragraph: Well-typed universal literal block recipe with an exact-count extension for odd support rank (source-ambiguity)

Selected references

The optimal unitary dilation for bosonic Gaussian channels, arXiv:1009.1108v1, https://arxiv.org/abs/1009.1108v1

6 thms2 active usersReviewed

Quantum Information·Captain: Goku

Comparison of Quantum Channels by SuperchannelsResearch Paper

Motivation

We extend the definition of the conditional min-entropy from bipartite quantum states to bipartite quantum channels. We show that many of the properties of the conditional min-entropy carry over to the extended version, including an operational interpretation as a guessing probability when one of the subsystems is classical. We then show that the extended conditional min-entropy can be used to fully characterize when two bipartite quantum channels are related to each other via a superchannel (also known as supermap or a comb) that is acting on one of the subsystems. This relation is a pre-order that extends the definition of "quantum majorization" from bipartite states to bipartite channels, and can also be characterized with semidefinite programming. As a special case, our characterization provides necessary and sufficient conditions for when a set of quantum channels is related to another set of channels via a single superchannel. We discuss the applications of our results to channel discrimination, and to resource theories of quantum processes. Along the way we study channel divergences, entropy functions of quantum channels, and noise models of superchannels, including random unitary superchannels, and doubly-stochastic superchannels. For the latter we give a physical meaning as being completely-uniformity preserving.

This mission is the statement-level formalization of Comparison of Quantum Channels by Superchannels (arXiv:1808.02607v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum majorization of channels by all paired entropy tests (Theorem 7, continued p.19, PDF p. 18). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

Comparison of Quantum Channels by Superchannels, arXiv:1808.02607v3, https://arxiv.org/abs/1808.02607v3

25 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

A Primal-Dual Smoothing Framework for Max-Structured Non-Convex Optimization: The Framework Returns an ε-Near-Stationary Point Within an Explicit Number of IterationsResearch Paper

Motivation

Many problems in robust optimization, adversarial learning, distributionally robust learning and min-max games have the max-structured form

\min_{x\in\mathcal X}\ q(x):=f(x)+r(x),\qquad f(x):=\max_{y\in\mathcal Y}\ \Phi(x,y)-g(y),

where $\Phi$ is smooth in $x$ but not convex, and concave in $y$ . The function $f$ is neither smooth nor convex, so gradient methods do not apply directly and convex duality does not close the problem. The standard target is then a near-stationary point: a point close to its own proximal point. In Hilbert spaces this notion and the matching algorithms are well developed (Davis and Drusvyatskiy 2019, doi:10.1137/18M1178244; Thekumparampil et al. 2019, arXiv:1907.01543). Many applications, however, live on simplices or spectral sets where the natural norm is $\ell_1$ or a Schatten norm and the natural proximal geometry is a Bregman divergence (entropy, for example).

R. Zhao (Mathematics of Operations Research, 2024; arXiv:2003.04375) gives a primal-dual smoothing framework for this problem in arbitrary finite-dimensional normed spaces. The dual variable is smoothed by a strongly convex function, and the primal problem is handled by an inexact Bregman proximal-point method. This mission formalizes the outer-loop guarantee of that framework: an explicit iteration bound after which the method returns an $\varepsilon$ -near-stationary point.

Setting

Let $\mathbb X$ and $\mathbb Y$ be finite-dimensional real normed spaces with arbitrary norms. Write $\mathcal X\subseteq\mathbb X$ for a nonempty closed convex set, the domain of a convex lower semicontinuous $r$ , and $\mathcal Y\subseteq\mathbb Y$ for a nonempty convex compact set. The function $g$ is convex and continuous on $\mathcal Y$ . $\Phi$ is jointly continuous, $\Phi(x,\cdot)$ is concave, and $\Phi(\cdot,y)$ is differentiable and $\gamma$ -weakly convex on $\mathcal X$ for some $\gamma>0$ :

\Phi(x',y)-\Phi(x,y)-\langle\nabla_x\Phi(x,y),x'-x\rangle\ge-\tfrac\gamma2\|x'-x\|^2 .

A distance generating function $\omega_{\mathcal X}$ is continuous and 1-strongly convex on $\mathcal X$ , and differentiable at every point of $\mathcal X$ with a $\beta_{\mathcal X}$ -Lipschitz gradient ( $\beta_{\mathcal X}\ge1$ ). Its Bregman divergence is $D_{\omega_{\mathcal X}}(x',x)=\omega_{\mathcal X}(x')-\omega_{\mathcal X}(x)-\langle\nabla\omega_{\mathcal X}(x),x'-x\rangle$ . For $0<\lambda<\gamma^{-1}$ , the proximal point $\mathrm{prox}(q,x,\lambda)$ minimizes $Q^\lambda(x';x)=q(x')+\lambda^{-1}D_{\omega_{\mathcal X}}(x',x)$ over $\mathcal X$ . A point $x\in\mathcal X$ is an $\varepsilon$ -NS point if, for some such $\lambda$ , $\|\lambda^{-1}(x-\mathrm{prox}(q,x,\lambda))\|\le\varepsilon/\beta_{\mathcal X}$ .

Dual smoothing: for a 1-strongly convex continuous $\omega_{\mathcal Y}$ on $\mathcal Y$ , set $f_\rho(x)=\max_{y\in\mathcal Y}\Phi(x,y)-g(y)-\rho\,\omega_{\mathcal Y}(y)$ , $q_\rho=f_\rho+r$ , and $R_{\mathcal Y}(\omega_{\mathcal Y})=\sup_{\mathcal Y}|\omega_{\mathcal Y}|$ .

Algorithm 1 fixes $\eta>0$ , $\lambda\in(0,\gamma^{-1})$ and $\rho=2\eta/R_{\mathcal Y}(\omega_{\mathcal Y})$ , and starts from $x_1\in\mathcal X$ . Iteration $k$ finds $x_{k+1}\in\mathcal X$ with $Q^\lambda_\rho(x_{k+1};x_k)\le\min_{\mathcal X}Q^\lambda_\rho(\cdot\,;x_k)+\eta$ , where $Q^\lambda_\rho$ is $Q^\lambda$ with $q_\rho$ in place of $q$ . It stops at the first $K$ with $\|x_{K+1}-x_K\|\le\sqrt{2\eta/(\lambda^{-1}-\gamma)}$ and outputs $x_K$ .

Formalization targets

Goal: Corollary 4.1

For $\lambda\in(0.8\gamma^{-1},\gamma^{-1})$ , $\varepsilon>0$ and $\eta=\varepsilon^2\lambda(1-\gamma\lambda)/(32\beta_{\mathcal X}^2)$ , every run of Algorithm 1 stops at a first index

K\le\left\lceil\frac{32\beta_{\mathcal X}^2(q(x_1)-q^*)}{5\varepsilon^2\lambda(\gamma\lambda-0.8)}\right\rceil+1,

and $x_K$ is an $\varepsilon$ -NS point. Here $q^*$ is the optimal value, or any lower bound of $q$ on $\mathcal X$ .

Milestones

(3.7): $|f_\rho-f|\le\rho R_{\mathcal Y}(\omega_{\mathcal Y})$ on $\mathcal X$ .
$Q^\lambda(\cdot\,;x)$ is $(\lambda^{-1}-\gamma)$ -strongly convex on $\mathcal X$ (p. 13).
$Q^\lambda_\rho(\cdot\,;x)$ is $(\lambda^{-1}-\gamma)$ -strongly convex on $\mathcal X$ (p. 15).
Lemma 4.2: $\|x_K-\mathrm{prox}(q_\rho,x_K,\lambda)\|\le2\sqrt{2\eta/(\lambda^{-1}-\gamma)}$ .
Lemma 4.3: $\|\mathrm{prox}(q_\rho,x,\lambda)-\mathrm{prox}(q,x,\lambda)\|\le2\sqrt{\rho R_{\mathcal Y}(\omega_{\mathcal Y})/(\lambda^{-1}-\gamma)}$ .
Theorem 4.1: with $\eta$ as above, $\|x_K-\mathrm{prox}(q,x_K,\lambda)\|\le\varepsilon\lambda/\beta_{\mathcal X}$ , so $x_K$ is $\varepsilon$ -NS.
Theorem 4.2: termination within $\lceil(q(x_1)-q^*)/((\frac{\gamma\lambda}{1-\gamma\lambda}-4)\eta)\rceil+1$ iterations.

Significance

Corollary 4.1 bounds the number of outer iterations, that is, approximate proximal subproblems, needed to reach an $\varepsilon$ -NS point. The bound is $O(\beta_{\mathcal X}^2(q(x_1)-q^*)/\varepsilon^2)$ for fixed $\gamma\lambda$ , and it holds in any norm. In the paper this count is combined with an accelerated primal-dual solver for each subproblem to obtain the overall gradient complexities (its Corollary 4.2 and Table 1). The paper reports these as the first complexity results for near-stationarity of (1.1) in the non-Hilbertian setting. The outer-loop count is the part of that analysis that does not depend on the inner solver, so it applies to any inner method that meets the $\eta$ -accuracy of Step 2.

The result is proved in the paper. It has no machine-checked proof on Prove2Me or, as far as is known, elsewhere. A formal development would provide reusable infrastructure: strong convexity of Bregman proximal objectives built from weakly convex parts in a general normed space, existence of Bregman proximal points in finite dimension, and the stability of proximal points under uniform perturbation of the objective.

Difficulty

The arithmetic of the final bound is short. The work lies in the analytic facts underneath it, which a Hilbert-space intuition gets wrong. In a general norm $\|\cdot\|^2$ is not smooth and weak convexity cannot be rewritten as convexity of $\Phi+\tfrac\gamma2\|\cdot\|^2$ . Strong convexity of $Q^\lambda$ must therefore come from the gradient inequality and the 1-strong convexity of $\omega_{\mathcal X}$ , passed through a supremum over $\mathcal Y$ . The paper's remark cites only $\lambda^{-1}>\gamma$ and the strong convexity of $\omega_{\mathcal X}$ . The weak convexity of $f$ and the convexity of $r$ are also needed. Existence of the proximal point is not automatic: it requires lower semicontinuity of $f+r$ on the closed set $\mathcal X$ , which comes from compactness of $\mathcal Y$ and joint continuity of $\Phi$ , together with coercivity from strong convexity in finite dimension. Finally, Theorem 4.1 is stated at the termination index, and termination itself (Theorem 4.2) requires $\lambda>0.8\gamma^{-1}$ .

Formalization scope

$\mathbb X,\mathbb Y$ are E, F with NormedAddCommGroup, NormedSpace ℝ and FiniteDimensional ℝ. No inner product is assumed. Gradients are fderiv, dual norms are operator norms on E →L[ℝ] ℝ, and differentiability is assumed at every point of $\mathcal X$ where a gradient is used. Maxima are real suprema over the subtype $\mathcal Y$ . Strong convexity is Mathlib's StrongConvexOn. The proximal point is a predicate IsProx, not a function. Iterates are indexed from 1. A run constrains only the iterations actually executed, those before the first stop. $r$ is real-valued, with values off $\mathcal X$ irrelevant. The optimal value is encoded as any lower bound of $q$ on $\mathcal X$ , and $\eta$ -optimality in Step 2 as a bound against every $x'\in\mathcal X$ . If $R_{\mathcal Y}(\omega_{\mathcal Y})=0$ , Lean sets $\rho=0$ (no smoothing); the paper leaves this case undefined, and all statements remain true. Hypotheses of the paper not used here are omitted, which only strengthens the statements: the Lipschitz bounds (1.2)–(1.3), Assumption 1.3, $\gamma\le L_{xx}$ , essential smoothness and property (i) of the distance generating functions. Lemma 4.3 is stated as (4.12) for $\rho\ge0$ . Theorem 4.1 is stated at a first stopping index, without a termination claim.

Trivializing formalizations are ruled out. The norms are general, not Euclidean. Weak convexity is the gradient inequality (1.4). The suprema are over a nonempty compact $\mathcal Y$ with continuous integrands, so they are finite. Existence of proximal points and termination are conclusions, never hypotheses. $K$ is the first stopping index of a genuine run.

Welcome contributions: the strong convexity of $Q^\lambda$ and $Q^\lambda_\rho$ (milestones 2–3), a general existence lemma for minimizers of strongly convex lower semicontinuous functions on closed convex sets in finite dimension, and the quadratic-growth estimate at a minimizer of a strongly convex function.

Selected references

R. Zhao, A Primal-Dual Smoothing Framework for Max-Structured Non-Convex Optimization, Mathematics of Operations Research, 2024. arXiv:2003.04375v5. https://arxiv.org/abs/2003.04375
D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM J. Optim. 29(1), 2019. https://doi.org/10.1137/18M1178244
K. K. Thekumparampil, P. Jain, P. Netrapalli, S. Oh, Efficient Algorithms for Smooth Minimax Optimization, NeurIPS 2019. https://arxiv.org/abs/1907.01543
Yu. Nesterov, Smooth minimization of non-smooth functions, Math. Program. 103, 2005. https://doi.org/10.1007/s10107-004-0552-5

10 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Brand Spillover as a Marketing Strategy: The Weak-Brand Firm Should Commit to Forgo Brand Spillover if and only if the Supplier Would Otherwise Drop It or the Insourcing Cost Is LowResearch Paper

Motivation

Competing brands often buy their products from the same contract manufacturer (CM). A weaker brand can exploit this. The paper's opening example is the Chinese retailer Netease Yanxuan, which advertises that its goods use "the same materials, the same factories, and the same workers" as international brands such as Adidas, Coach and MUJI. A weak brand that discloses its common supplier in this way borrows part of the leader's reputation. This practice is called brand spillover.

The obvious view is that a weak brand should use any spillover it can get. Wu, Zhang and Zhou (SSRN 3891915, Management Science 2021) show that this view is incomplete. A supplier that serves both brands has to keep the strong brand willing to outsource. If the weak brand's spillover makes that too expensive, the supplier stops serving the weak brand, or it extracts the spillover's value through its prices. The paper's main result, Proposition 4, says when the weak brand is better off committing in advance not to use the spillover. This mission formalizes that result together with the equilibrium analysis it rests on.

Setting

Two firms sell substitutable products. Firm S has brand power $\theta_S = 1$ and Firm W has brand power $\theta_W = \theta < 1$ . With quantities $q_S, q_W$ the market-clearing prices are

p_S = 1 - q_S - q_W,\qquad p_W = \theta_W - q_S - q_W .

Each firm can produce in-house at unit cost $c > 0$ , or buy from the CM, whose own unit cost is normalized to $0$ . A sourcing structure is one of $(O,O)$ , $(O,I)$ , $(I,O)$ , $(I,I)$ : the first letter is Firm S's choice and the second Firm W's, with $O$ for outsourcing and $I$ for insourcing. Brand spillover can occur only under $(O,O)$ . There, if Firm W uses it, its brand power becomes $\theta + \alpha(1-\theta)$ , where $\alpha \in [0,1]$ is the level of brand spillover.

The game has four stages:

Firm W decides whether to commit to not using brand spillover. Committing is equivalent to setting $\alpha = 0$ .
The CM announces wholesale prices $w_S$ and $w_W$ .
The firms choose their sourcing simultaneously.
The firms compete in quantities.

At stage 4 the quantities are the first-order-condition solutions, and each firm's profit is the square of its quantity. At stage 2, for each structure, the CM maximizes its revenue $\sum w_i q_i$ over the outsourcing firms, subject to participation constraints. A constraint says that a firm does at least as well outsourcing at the offered price as deviating to insourcing. The CM then induces the structure with the highest optimal revenue. The standing assumption $\theta \ge \underline\theta = \max\{(2+7c)/7,\ (1+c)/2\}$ keeps Firm W in the market.

The thresholds used below are $c^{oi} = \tfrac13(2-\theta)$ , $c^{oo}_1 = \tfrac12(2\theta - 1 - 3\alpha(1-\theta))$ and $c^{oo}_2 = \tfrac12(1 + \alpha(1-\theta))$ .

Formalization targets

Goal: Proposition 4

Assume $\alpha > 0$ . Let $\Pi_W$ be Firm W's profit at an equilibrium without commitment, and $\Pi^0_W$ its profit at an equilibrium with commitment. If the structure without commitment is $(O,I)$ , then $\Pi_W \le \Pi^0_W$ . Otherwise

\Pi_W < \Pi^0_W \iff c < \theta - \tfrac12 - \alpha + \alpha\theta \iff \alpha < \frac{2\theta - 1 - 2c}{2(1-\theta)} .

Milestones

The quantity stage has a unique Nash equilibrium, with profits $q_i^2$ .
Lemma 1: the CM never induces $(I,I)$ or $(I,O)$ .
Lemma 2: under $(O,I)$ the CM's optimal price is $w^{oi}_S = \min\{c, \tfrac14(2-\theta+c)\}$ .
Lemma 3: under $(O,O)$ the CM's optimal prices are $w^{oo}_S = \min\{c - \tfrac12\alpha(1-\theta), \tfrac12\}$ , and $w^{oo}_W$ given by (2)–(3).
Appendix B: the equilibrium quantities and their signs.
Proposition 2(b): under $(O,O)$ , Firm W's profit decreases in $\alpha$ exactly when $\alpha < (2\theta-2c-1)/(3(1-\theta))$ .
Proposition 3: the equilibrium sourcing structure for every spillover level.
With commitment, the CM always induces $(O,O)$ . Firm W then earns $((2\theta-1-c)/3)^2$ or $((2\theta-1)/6)^2$ .

Significance

Proposition 4 splits the parameter space into three regions. In the first, the supplier would drop the weak brand: it induces $(O,I)$ , and Firm W pays the insourcing cost. In the second, the supplier captures the spillover through a higher wholesale price, and the weak brand loses ground to the strong one. In the third, the spillover pays. The comparative static behind the second region is Proposition 2(b): brand spillover can lower the profit of the firm it benefits. The analysis also identifies when the strong brand is hurt by the weak brand's spillover and should act to prevent it (paper, abstract and §5).

The paper proves the result by hand, and no formal proof exists. A complete development would give machine-checked proofs of:

a four-stage game with participation-constrained pricing;
the closed-form solution of two non-convex price programs;
an equilibrium comparison that holds for every selection when the CM is indifferent between structures.

Formalizing the statements has already found two slips in Proposition 3: a sign in $T_1$ , and a boundary point that the printed case split assigns to the wrong structure.

Difficulty

The CM's feasible sets are not convex. Each participation constraint compares two squared quantities, $q_{\text{out}}^2 \ge q_{\text{in}}^2$ , so it admits two branches: a price below a bound, or a price so high that the quantity changes sign. The paper's proofs treat only the first branch. A complete proof must rule out the other branches as optimal, so maximizing a concave quadratic is not enough.

The goal compares equilibrium outcomes, not formulas. Each side combines an optimal-price problem with a choice between structures. The no-commitment side changes regime along the curves $T_1$ , $T_2$ , $T_3$ , which contain square roots. Firm W's profit has a kink at $c = c^{oo}_1$ .

Formalization scope

Model and its general part. The model is one definitions module, BrandSpillover.Commitment.Model. The profit functions use the referenced general linear Cournot payoff SupplierAudit.Competition.cournotPayoff with substitution parameter $1$ . All quantities and prices are real numbers.
Quantities. The stage-4 quantities are the first-order-condition formulas on $\mathbb R$ and are not clamped at $0$ , as in the paper. Clamping them changes the CM's feasible set and breaks Lemma 3.
Prices. Wholesale prices range over $\mathbb R^2$ , without a sign restriction. The price for a firm that insources is ignored.
Feasibility. The feasible set of each program is the page's set of profit comparisons. It is never replaced by the linear bounds derived in the proofs.
Equilibrium. An equilibrium is a structure whose optimal CM revenue is at least that of every other structure, together with optimal prices for it. Ties are allowed, and the goal holds for every selection.
Standing assumptions. The standing assumptions are $c > 0$ , $\underline\theta \le \theta < 1$ and $\alpha\in[0,1]$ , with the paper's weak inequality $\theta \ge \underline\theta$ . The goal adds $\alpha > 0$ , from p. 17.
Corrections. $T_1$ uses $(1-\theta)^2$ where the page prints $(1+\theta)^2$ . Condition (i) of Proposition 3 includes $c = c^{oo}_1$ . The committed profit is stated for every admissible $c$ , including $c > \tfrac12$ , which the page omits.
Ruled-out shortcut. Substituting the closed-form prices of Lemmas 2–3 into the goal would turn it into a comparison of squares. The goal is therefore stated about equilibrium outcomes of the price programs.
Contributions. Proofs of any milestone are welcome. Lemma 3 and Proposition 3 are the hardest.

Selected references

X. Wu, F. Zhang, Y. Zhou, Brand Spillover as a Marketing Strategy, SSRN preprint 3891915, June 2021; Management Science, 2021. https://ssrn.com/abstract=3891915, https://doi.org/10.1287/mnsc.2021.4165
A. Arya, B. Mittendorf, D. E. M. Sappington, The make-or-buy decision in the presence of a rival: strategic outsourcing to a common supplier, Management Science 54(10), 2008. https://doi.org/10.1287/mnsc.1080.0874
N. Singh, X. Vives, Price and quantity competition in a differentiated duopoly, RAND Journal of Economics 15(4), 1984. https://doi.org/10.2307/2555525

11 thms2 active usersReviewed

Graph Theory Quantum Error Correction Quantum Information·Captain: mikedeng1

Decoding Quantum Tanner Codes: The Parallel Decoder Corrects Every Error of Weight Linear in the Code Length in Logarithmically Many RoundsResearch Paper

Why decoding good quantum LDPC codes matters

Quantum computers must correct errors faster than they accumulate, and quantum low-density parity-check (LDPC) codes are the leading candidates for doing so with little overhead: every check involves a bounded number of qubits, so syndromes can be measured by local circuits. In 2021–2022 the first asymptotically good quantum LDPC codes appeared, with dimension and minimum distance both linear in the code length $n$ : the expander lifted product codes of Panteleev and Kalachev (arXiv:2111.03654) and the quantum Tanner codes of Leverrier and Zémor (arXiv:2202.13641). A code is only useful if errors can be corrected efficiently. Leverrier and Zémor (arXiv:2208.05537) give two decoders for quantum Tanner codes that correct every error of weight up to a constant fraction of $n$ : a sequential one running in linear time, and a parallel decoder running in a logarithmic number of rounds of local updates. This mission is about the parallel decoder.

Timeline:

2021, Panteleev–Kalachev: asymptotically good quantum LDPC codes and locally testable classical codes (arXiv:2111.03654).
2022, Leverrier–Zémor: quantum Tanner codes, a simpler construction on left-right Cayley complexes (arXiv:2202.13641).
2022, Gu–Pattison–Tang, Leverrier–Zémor and Dinur–Hsieh–Lin–Vidick: efficient decoders for linear-distance quantum LDPC codes (arXiv:2206.06557, arXiv:2206.07571, arXiv:2206.07750).
2022, Leverrier–Zémor, Decoding quantum Tanner codes: sequential and parallel decoders up to a constant fraction of $n$ , with a revised parallel analysis in v3 (arXiv:2208.05537v3).

The code and the decoder

Let $G$ be a finite group and $A=A^{-1}$ , $B=B^{-1}\subseteq G$ with $|A|=|B|=\Delta$ . The quadripartite left-right Cayley complex has four copies of $G$ as vertices, $V_{ij}=G\times\{ij\}$ , and one square $\{(g,00),(ag,01),(gb,10),(agb,11)\}$ for every $(g,a,b)\in G\times A\times B$ . The set of squares $Q$ has $n=|G|\Delta^2$ elements, and every vertex $v$ sees its $Q$ -neighbourhood $Q(v)$ as an $A\times B$ array: columns are indexed by $b$ , rows by $a$ . The left Cayley graph $\mathrm{Cay}(G,A)$ and the right Cayley graph $\mathrm{Cay}(G,B)$ are assumed to be non-bipartite Ramanujan graphs: every adjacency eigenvalue other than $\pm\Delta$ has absolute value at most $2\sqrt{\Delta-1}$ .

Two local codes $C_A\subseteq\mathbb F_2^A$ , $C_B\subseteq\mathbb F_2^B$ with $\dim C_A+\dim C_B=\Delta$ are fixed. Write $V_0=V_{00}\cup V_{11}$ and $V_1=V_{01}\cup V_{10}$ . The code $\mathcal C_1\subseteq\mathbb F_2^Q$ consists of the vectors whose view on every $Q(v)$ , $v\in V_1$ , lies in the dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$ : every local view is a sum of a word whose columns are in $C_A$ and a word whose rows are in $C_B$ . $\mathcal C_0$ is defined in the same way on $V_0$ with $C_A^\perp$ , $C_B^\perp$ . The local codes and their duals have distance at least $\delta\Delta$ . Both dual tensor codes are $\kappa$ -product-expanding: every codeword $x$ splits as $x=c+r$ with $|x|\ge\kappa\Delta(\|c\|+\|r\|)$ , where $\|c\|$ counts non-zero columns and $\|r\|$ non-zero rows.

A $\sigma_x$ -type error $e\in\mathbb F_2^Q$ is decoded in three phases. In the preprocessing phase every $v\in V_1$ chooses a minimum-weight local error $\varepsilon_v$ with the local syndrome of $e$ ; the mismatch is $Z=\sum_{v\in V_1}\varepsilon_v$ . The mismatch decomposition writes $Z=\hat C_0+\hat R_0+\hat C_1+\hat R_1$ , with $\hat C_j$ a sum of $C_A$ -columns and $\hat R_i$ a sum of $C_B$ -rows. Postprocessing outputs $\hat e=\sum_{v\in V_{10}}\varepsilon_v+\hat C_0+\hat R_1$ . The parallel decoder (Algorithm 3) runs rounds of four substeps, one for each of $V_{00},V_{01},V_{10},V_{11}$ . In a substep, every vertex $v$ of the current class simultaneously looks for a non-zero local dual tensor codeword $x_v$ on $Q(v)$ with $|\hat Z|-|\hat Z+x_v|\ge|x_v|/2$ , picks one of maximum weight, splits it as $c_v+r_v$ with $\|c_v\|+\|r_v\|$ minimal, and updates $\hat C_j$ , $\hat R_i$ and $\hat Z$ .

Formalization targets

Goal: Theorem 20 (= Theorem 3)

Fix $\varepsilon\in(0,1/6)$ and $\delta,\kappa>0$ . For all $\Delta$ large enough, every error with

|e|<\frac1{2^{12}}\min\Big(\frac{\varepsilon^3}{16},\frac\kappa4\Big)\delta^2\kappa^2\frac n\Delta

is corrected by every run of the parallel decoder. With $\theta=\frac14\big(\frac14-\frac32\varepsilon\big)$ , each round satisfies $|\hat Z_{k+1}|\le(1-\theta)|\hat Z_k|$ , so $\hat Z_k=0$ once $(1-\theta)^k\cdot4|e|<1$ , and then $e+\hat e$ lies in the span $\mathcal C_0^\perp$ of the $\sigma_x$ -generators.

Milestones

Lemma 4 (expander mixing) and Lemma 5: $\lambda(\mathcal G^\square_0),\lambda(\mathcal G^\square_1)\le4\Delta$ .
Lemmas 7, 10, 11, 8 and Theorem 9: the minimum distance, $d_{\min}\ge\delta^2\kappa^2n/(1024\Delta)$ .
Lemmas 14, 15, 16 and Theorem 12: if a minimum decomposition of a non-zero mismatch has few active vertices, some local codeword lowers $|Z|$ by $(1-\varepsilon)|x_v|$ .
Lemma 17: $|Z|\le4|e|$ and $\|Z\|\le4|e|/(\kappa\Delta)$ .
Lemma 19: below $2^{-16}\varepsilon^3\kappa^2\delta^2n/\Delta$ , sequential decoding with parameter $1/2$ never stalls, and switching to $\varepsilon$ still converges.
Lemma 18: if the $\varepsilon$ -sequential decoder converges, one parallel round removes at least $\theta|Z|$ .

Significance

The theorem shows that asymptotically good quantum LDPC codes can be decoded against adversarial errors of linear weight by $O(\log n)$ rounds of local computation, each vertex acting only on its own $Q$ -neighbourhood. This matters for fault tolerance, where decoding latency is a bottleneck. The milestones carry independent value. Theorem 9 is a linear minimum distance bound for quantum Tanner codes in the quadripartite setting. Theorem 12 is the local-to-global "weight reduction" principle on which both decoders rest. Lemmas 4–5 are spectral facts about Cayley graphs and square complexes that are reusable for any expander-based code.

The paper's results are proved, not open; none has been machine-checked. The sequential decoder's correctness (Theorem 13) is posed separately on the platform as an open goal in the mission Decoding quantum Tanner codes (Leverrier, Zemor), which shares this mission's published definitions; this mission does not restate it. Formalizing the present chain would give a complete, checked proof that a parallel decoder exists for good quantum LDPC codes, and would expose the constants. Two printed constants are corrected here (see the scope section), and sharper constants or simpler arguments are welcome.

Difficulty

The obvious argument is to bound the mismatch and its norm, apply Theorem 12 repeatedly, and let all vertices of a class flip at once. That argument fails because parallel flips are not sequential flips. A vertex's best local move against the mismatch at its turn need not be the move a converging sequential run would make, and a round could stall even though a sequential run never does. Lemma 18 resolves this with a virtual sequential run, a partition of its increments into "good" and "bad" ones (Claim 1), and the maximum-weight rule at every vertex. Without that rule the lemma is false. Theorem 12 itself is a counting contradiction. It uses robustness, the expander mixing lemma twice, and two notions of "exceptional" vertices, and it needs $\Delta$ large. Theorem 9 needs the coset-minimization of Lemma 7 before the same counting can start.

Formalization scope

The development builds on the published layers QAlgorithms_Defs_TensorCode and QAlgorithms_Defs_TannerDecoder. These define the complex, $\varphi_v$ , $\mathcal C_0$ , $\mathcal C_1$ , the $\sigma_x$ span, minimum local corrections, the mismatch, Algorithm 2 and the output $\hat e$ . The conventions are:

A vertex $(g,ij)$ is (g, (i, j)) : G × (Bool × Bool), squares are G × A × B, and weights are hammingNorm cast to ℝ.
One new definitions file holds Algorithm 3 (admissible move, parallel choice, substep, round, run), decompositions and their norm, active, exceptional and ordinary vertices, the clustering sets $T$ , stalled and converging sequential decoders, $\mathcal C_1^\perp$ , and the square graphs $\mathcal G^\square_k$ .
" $\Delta$ large enough" is $\exists\Delta_0\,\forall\Delta\ge\Delta_0$ , with $\Delta_0$ depending only on the constants fixed before it.
Only $\sigma_x$ -type errors are treated; the $\sigma_z$ case is symmetric.
Non-bipartiteness of the Cayley graphs (the standing choice of p. 10) is assumed wherever spectral bounds are used.
Theorem 12 assumes $Z\ne0$ and asks for a non-zero $x_v$ .

Corrected constants. Theorem 9 is stated with $1024$ instead of the printed $256$ , because Lemma 8 and the proof's $|x|\ge\frac{\kappa\Delta}2\|x\|$ give $1024$ . The goal's error bound uses $\min(\varepsilon^3/16,\kappa/4)$ instead of $\min(\varepsilon^3/16,\kappa)$ , which is what the corrected distance supports. Both corrected statements are weaker than the printed ones.

No trivialization. Every vertex must flip a maximum-weight admissible move whenever one exists, and runs range over all such choices. "Logarithmic time" is the per-round contraction factor, not mere eventual termination. Validity is membership of $e+\hat e$ in the $\sigma_x$ -generator span, with $\hat e$ the paper's postprocessing output. A formalization that lets vertices idle, drops the maximum-weight rule, or proves only eventual termination does not prove this theorem.

Needed and reusable infrastructure:

spectral graph theory for regular multigraphs (expander mixing, eigenvalues of commuting Cayley adjacencies);
product expansion and local minimality of decompositions;
the combinatorics of the left-right complex (shared rows and columns).

Contributions proving the graph lemmas or Lemma 18, whose proof is pure counting, are especially welcome.

Selected references

A. Leverrier, G. Zémor, Decoding quantum Tanner codes, IEEE Transactions on Information Theory; arXiv:2208.05537v3, 2022. https://arxiv.org/abs/2208.05537
A. Leverrier, G. Zémor, Quantum Tanner codes, FOCS 2022; arXiv:2202.13641. https://arxiv.org/abs/2202.13641
P. Panteleev, G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, STOC 2022; arXiv:2111.03654. https://arxiv.org/abs/2111.03654
S. Gu, C. A. Pattison, E. Tang, An efficient decoder for a linear distance quantum LDPC code, STOC 2023; arXiv:2206.06557. https://arxiv.org/abs/2206.06557
A. Leverrier, G. Zémor, Efficient decoding up to a constant fraction of the code length for asymptotically good quantum codes, SODA 2023; arXiv:2206.07571. https://arxiv.org/abs/2206.07571
I. Dinur, M.-H. Hsieh, T.-C. Lin, T. Vidick, Good quantum LDPC codes with linear time decoders, arXiv:2206.07750, 2022. https://arxiv.org/abs/2206.07750
G. Kalachev, P. Panteleev, Two-sided robustly testable codes, arXiv:2206.09973, 2022. https://arxiv.org/abs/2206.09973

18 thms2 active usersReviewed

Machine Learning Optimization Statistics·Captain: mikedeng1

High-Dimensional Learning Under Approximate Sparsity with Applications to Nonsmooth Estimation and Regularized Neural Networks: Excess-Risk Bounds at S3ONC Solutions of MCP-Regularized M-EstimationResearch Paper

Motivation

High-dimensional statistical learning (HDSL) fits a model with $p$ parameters from $n$ samples when $p$ may far exceed $n$ . The standard guarantees for sparse estimators, such as the Lasso, rest on restricted strong convexity (RSC) or restricted eigenvalue conditions on the empirical risk (Negahban et al., 2012; Loh & Wainwright, 2015). These conditions fail or are hard to verify for many losses that matter in operations research and machine learning: nonsmooth losses, losses of neural networks, and M-estimation problems whose population risk is not strongly convex near any sparse vector.

Liu, Ye and Lee (arXiv:1903.00616v2; Operations Research, 2022) remove RSC entirely. They regularize the empirical risk with a folded concave penalty, the minimax concave penalty (MCP) of Zhang (2010), and analyse not a global minimizer (intractable, since the problem is nonconvex) but any point satisfying a weak second-order stationarity condition. They also replace exact sparsity by approximate sparsity: the best sparse vector need only be $\varepsilon_A$ -optimal for the population risk. Their main result, Theorem 1, gives an excess-risk bound whose sample complexity is poly-logarithmic in $p$ .

Setting

Observations $Z_1, \dots, Z_n$ are i.i.d. copies of a random element $Z$ of a measurable space $\mathcal W$ . A loss $L(\beta, z)$ , with parameter $\beta \in \mathbb R^p$ , defines the population risk $\mathbb L(\beta) = \mathbb E[L(\beta, Z)]$ , assumed finite for every $\beta$ and bounded below, the empirical risk $\mathcal L_n(\beta) = \frac1n\sum_i L(\beta, Z_i)$ , and the regularized objective

\mathcal L_{n,\lambda}(\beta) = \mathcal L_n(\beta) + \sum_{j=1}^p P_\lambda(|\beta_j|), \qquad P_\lambda(\theta) = \int_0^\theta \frac{[a\lambda - t]_+}{a}\,dt,

The standing assumptions are:

smoothness (11): each partial derivative $\partial L/\partial\beta_j$ is $U_L$ -Lipschitz along coordinate $j$ , for almost every $z$ ;
Assumption 3: the centred losses $L(\beta, Z_i) - \mathbb E L(\beta, Z_i)$ are sub-exponential with $\psi_1$ -norm at most $\sigma \ge 1$ on the box $\|\beta\|_\infty \le R$ ;
Assumption 4: $L(\cdot, z)$ is $\mathcal C(z)$ -Lipschitz on the box, where $\mathcal C(Z_i)$ is sub-exponential around its mean ( $\psi_1$ -norm at most $\sigma_L \ge 1$ ) and $\mathbb E\,\mathcal C(Z_i) \le \mathcal C_\mu$ , $\mathcal C_\mu \ge 1$ ;
Assumption 1 (A-sparsity): some $\beta^*_{\varepsilon_A}$ with $\|\beta^*_{\varepsilon_A}\|_\infty \le R$ , $R \ge 1$ , and $s = \|\beta^*_{\varepsilon_A}\|_0 > 1$ nonzero entries satisfies $\mathbb L(\beta^*_{\varepsilon_A}) - \inf_\beta \mathbb L(\beta) \le \varepsilon_A$ . Assumption 2 replaces $\inf_\beta \mathbb L$ by any lower bound $L^*_g$ .

A vector $\hat\beta$ satisfies the S³ONC (significant subspace second-order necessary conditions, Definition 1) at a sample if it is a KKT point of $\mathcal L_{n,\lambda}$ , with subgradients $\kappa_j \in \partial|\hat\beta_j|$ , and $U_L + P''_\lambda(|\hat\beta_j|) \ge 0$ whenever $|\hat\beta_j| \in (0, a\lambda)$ . With $\tilde\zeta = \ln(3eR(\sigma_L + \mathcal C_\mu))$ , Theorem 1 fixes $\lambda = \sqrt{8\sigma/(c a n^{2/3})\,[\ln(n^{2/3}p) + \tilde\zeta]}$ , where $c \in (0, 1/2]$ is the constant of the Bernstein inequality (12).

Formalization targets

Goal: Theorem 1 (p. 18)

For $a < \min\{1/U_L, 1\}$ and any random $\hat\beta$ with $\|\hat\beta\|_\infty \le R$ satisfying the S³ONC almost surely:

(i) if $\mathcal L_{n,\lambda}(\hat\beta) \le \mathcal L_{n,\lambda}(\beta^*_{\varepsilon_A}) + \Gamma$ almost surely and $n > C_3[((\Gamma + \varepsilon_A)/\sigma)^3 + s(\ln(np) + \tilde\zeta)]$ , then with probability at least $1 - 2(p+1)e^{-n/C_3} - 6e^{-n^{1/3}/C_3}$ ,

\mathbb L(\hat\beta) - \inf_\beta \mathbb L(\beta) \le C_3\sigma\Big[\frac{s(\ln(np)+\tilde\zeta)}{n^{2/3}} + \sqrt{\frac{s(\ln(np)+\tilde\zeta)}{n}} + \frac{1}{n^{1/3}}\Big] + C_3\sqrt{\frac{\sigma(\Gamma+\varepsilon_A)}{n^{1/3}}} + \Gamma + \varepsilon_A;

(ii) if $\hat\beta$ is no worse in $\mathcal L_{n,\lambda}$ than a Lasso solution $\hat\beta^{\ell_1}$ , the $\Gamma$ -free bound (22) holds under (21).

$C_3, C_4$ are universal constants. The goal fixes the polynomial rate $n^{-1/3}$ ; the general-rate result is Proposition 1.

Milestones (the paper's proof chain)

Proposition 2: the S³ONC forces $|\hat\beta_j| \notin (0, a\lambda)$ almost surely.
Lemma EC.1: the empirical risk is $(2\sigma_L + \mathcal C_\mu)$ -Lipschitz on the box with high probability.
Proposition 3: uniform deviation of $\mathcal L_n$ from $\mathbb L$ over $\{\|\beta\|_\infty \le R, \|\beta\|_0 \le p'\}$ .
Proposition 4: $\|\hat\beta\|_0 \le p'_u - 1$ with high probability.
Lemma EC.2: comparison of the Lasso solution with $\beta^*_{\varepsilon_A}$ in $\mathcal L_{n,\lambda}$ .
Proposition 5: the joint sparsity and excess-risk events for general $\varrho \in (0, 1/2)$ .
Proposition 1: the excess-risk bounds (16), (18) at S³ONC solutions for general $\varrho$ .

Significance

The theorem shows that second-order stationarity, which first- and second-order methods can certify (the paper's Theorem 2 gives a pseudo-polynomial algorithm), suffices for poly-logarithmic sample complexity in $p$ without convexity or RSC. The paper builds on it for nonsmooth losses through smoothing (Theorem 3) and for regularized neural networks (Theorem 4). The same definitions layer (MCP, S³ONC, A-sparsity) serves those results.

The result is proved on paper, in the electronic companion of the cited preprint. Nothing of it is formalized: the platform has no folded concave penalty, no S³ONC and no excess-risk bound for sparse M-estimation without RSC. This mission provides the definitions, the goal and the proof chain as stated by the authors, with two disclosed adjustments (see Formalization scope).

Difficulty

The obvious argument bounds $\mathcal L_n(\hat\beta) - \mathbb L(\hat\beta)$ uniformly over the box $\|\beta\|_\infty \le R$ and then compares $\hat\beta$ with $\beta^*_{\varepsilon_A}$ . It fails: a covering of a $p$ -dimensional box costs a factor $p$ , not $\ln p$ , in the sample size. The usual repair, RSC, which localizes the estimator near a sparse target, is exactly what the paper does without. $\hat\beta$ is moreover only a stationary point of a nonconvex objective, not a minimizer, so no optimality inequality over the whole space is available. The probabilistic part requires keeping the constants consistent across several union bounds and two Bernstein inequalities, with failure probabilities that must stay summable in the sparsity level. In Lean, an additional obstacle is that suprema over uncountable sparse sets are not obviously measurable.

Formalization scope

Data: an abstract measurable space $\mathcal W$ (its embedding in $\mathbb R^q$ plays no role), independent $Z_i$ with common law $\mu$ . $L(\beta, \cdot)$ is measurable and $\mu$ -integrable for every $\beta$ , and $\mathbb L$ is bounded below, so $\inf_\beta \mathbb L(\beta)$ is a genuine infimum.
Norms: the Euclidean norm is written out (Mathlib's norm on Fin p → ℝ is the sup norm). $\|\cdot\|_{\psi_1}$ is the published Orlicz norm HighDimProb.Concentration.subexponentialNorm, always together with an explicit witness of sub-exponentiality. The paper cites the equivalent moment form; the difference is absorbed by the universal constants.
Bernstein constant: (12) and the analogous bound for $\mathcal C(Z_i)$ used in Lemma EC.1 are hypotheses with their constant $c$ , quantified first. Every universal constant ( $C_1$ – $C_4$ , $\tilde c$ ) comes after $c$ and before every problem object: $p$ , $n$ , the distribution, $L$ , $\hat\beta$ , $\Gamma$ . Remark 1 asserts that such a $c \in (0, 1/2]$ exists; the platform's proved bernstein_weighted supplies one.
Derivatives: the gradient enters through coordinate partial derivatives, which is all (11), (13), (14) use. $P'_\lambda, P''_\lambda$ are derivatives of the literal integral (4).
Probabilities: "with probability at least $1-\delta$ " is an upper bound $\delta$ on the outer measure of the failure set.
Random vectors: $\hat\beta$ and $\hat\beta^{\ell_1}$ are arbitrary measurable maps with the stated almost-sure properties; no statement constructs them.
Corrections: $a < 1$ is added to Theorem 1 and Proposition 1. It is Proposition 5's hypothesis, which their printed proofs invoke. Proposition 4's $\zeta_1(\epsilon)$ prints $\sigma_C$ , and $\sigma_L$ is meant. Theorem 1's $\lambda$ is kept as printed ( $\ln(n^{2/3}p)$ ), although Proposition 1 at $\varrho = 1/3$ uses $\ln(n^{1/3}p)$ .

The trivializing formalizations are ruled out explicitly: constants chosen after the instance, junk values of non-integrable expectations, empty infima or undefined derivatives, the sup norm in place of the Euclidean norm, and an estimator chosen by the theorem.

Welcome contributions: proofs of the milestones in order; a Lean proof that Assumption 3 implies (12), via the published Bernstein inequality; a measurable-selection or outer-measure lemma for suprema over sparse boxes, which is reusable across high-dimensional statistics.

Selected references

H. Liu, Y. Ye, H. Y. Lee, High-dimensional learning under approximate sparsity with applications to nonsmooth estimation and regularized neural networks, Operations Research, 2022; preprint arXiv:1903.00616v2, 2021. https://arxiv.org/abs/1903.00616
C.-H. Zhang, Nearly unbiased variable selection under minimax concave penalty, Annals of Statistics 38(2), 2010. https://arxiv.org/abs/1002.4734
J. Fan, R. Li, Variable selection via nonconcave penalized likelihood and its oracle properties, Journal of the American Statistical Association 96, 2001. https://doi.org/10.1198/016214501753382273
S. N. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers, Statistical Science 27(4), 2012. https://arxiv.org/abs/1010.2731
P.-L. Loh, M. J. Wainwright, Regularized M-estimators with nonconvexity: statistical and algorithmic theory for local optima, Journal of Machine Learning Research 16, 2015. https://arxiv.org/abs/1305.2436
R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027

11 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

On Co-opetitive Supply Partnerships with End-Product Rivals: Information Asymmetry, Dual Sourcing and Supply Market Efficiency: The Equilibrium Wholesale Price and When the VI Buys InformationResearch Paper

Motivation

Firms often buy key components from the very rivals they compete with in the end market. The paper's examples: Lockheed Martin has sourced engine control systems and gearboxes from AgustaWestland, its competitor in national helicopter markets, while avoiding single sourcing from it in markets where it holds an information advantage; vertically integrated generic-drug makers such as Teva supply active ingredients to finishing-only rivals such as Apotex. Such co-opetitive supply relationships raise an informational problem studied in operations management: the buyer's order quantity reveals what the buyer knows about demand, and the supplier, who is also a competitor, can use that signal when setting her own output. The buyer may therefore distort his orders to hide his information, and the supplier may lower her wholesale price to make revealing it worth his while.

S. H. Jung and P. Kouvelis (SSRN 3555184, 2020; published in Manufacturing & Service Operations Management) analyse this trade-off in a stylized model with a single outside supplier as the buyer's alternative. Their main result, Proposition 4, gives the supplier's equilibrium wholesale price in closed form and identifies when she pays an information rent to learn demand and when she prices to keep the buyer from leaving.

Setting

A vertically integrated firm (VI, "she") with production cost normalized to $0$ and a downstream outsourcing firm (DO, "he") compete in quantities. The market-clearing price is $P = 1 - Q + \epsilon$ , where $Q$ is total output and the demand shock $\epsilon$ is $t$ or $-t$ ( $t > 0$ ), each with probability $1/2$ . Only the DO observes $\epsilon$ . Play proceeds in two stages.

The VI offers a unit wholesale price $w_I$ .
The DO orders $Q_{O,1}$ from the VI at $w_I$ and $Q_{O,2}$ from an outside supplier at the unit price $w_A$ . The VI sees $Q_{O,1}$ but not $Q_{O,2}$ , updates her belief about $\epsilon$ , and produces $Q_I$ .

In state $\epsilon$ the VI earns $(1 - (Q_{O,1} + Q_{O,2} + Q_I) + \epsilon)Q_I + w_I Q_{O,1}$ . The paper solves the quantity subgame in closed form. Below the separating/pooling threshold $\bar w_{sep/pool}$ of its equation (3) the DO's order reveals the state (separating quantities, Lemma 1); between $\bar w_{sep/pool}$ and the pooling cap $\bar w_I$ of equation (4) the DO orders the same amount in both states and tops up from the outside supplier in high demand (pooling quantities, Lemma 2); at or above $\bar w_I$ he buys only from the outside supplier (Proposition 1). Averaging the VI's state profit gives $\Pi^s_I(w_I)$ , $\Pi^p_I(w_I)$ and $\Pi^{n*}_I = (3 + 4w_A)^2/100$ , and the VI's objective is equation (6):

\Pi_I(w_I) = \begin{cases}\Pi^s_I(w_I) & w_I \le \bar w_{sep/pool},\\ \Pi^p_I(w_I) & \bar w_{sep/pool} < w_I < \bar w_I,\\ \Pi^{n*}_I & w_I \ge \bar w_I,\end{cases}\qquad w_I^* = \arg\max_{w_I \ge 0}\Pi_I(w_I).

The analysis is carried out under the paper's standing assumptions: $\underline t := 28(4 + 5\sqrt2)/1105 \le t$ and $\underline w := 126(17 - 3\sqrt{34})/(570\sqrt{34} - 15829) < w_A < 1/2 - 5t/7$ . The constant $\bar t \approx 0.4005$ is the nonzero solution of equation (7), $153(\sqrt{5134} - 122)\bar t + 125\sqrt{21\bar t(51\bar t + 52)} = 0$ .

Formalization targets

Goal: Proposition 4

For $\underline t \le t < \bar t$ there is $\bar w_A > 0$ solving $\Pi^s_I(\bar w_{sep/pool}) = \Pi^p_I(\bar w_I)$ such that, for every admissible $w_A$ ,

w_A > \bar w_A \;\Rightarrow\; w_I^* = \bar w_{sep/pool}, \qquad w_A \le \bar w_A \;\Rightarrow\; w_I^* = \bar w_I^{(-)},

and for $t \ge \bar t$ , $w_I^* = \bar w_I^{(-)}$ for every admissible $w_A$ . Here $w_I^* = \bar w_{sep/pool}$ means this price is nonnegative and the unique maximizer of $\Pi_I$ on $w_I \ge 0$ , and $w_I^* = \bar w_I^{(-)}$ means $\sup_{w_I \ge 0}\Pi_I = \Pi^p_I(\bar w_I)$ , approached as $w_I \uparrow \bar w_I$ . The cap itself is excluded; at the crossing $w_A=\bar w_A$ , the separating boundary can attain the same value.

Milestones

Equation (13): $\Pi^p_I$ is a concave quadratic, uniquely maximized over $\mathbb R$ at $(3703 - 4066t - 242w_A)/9204$ .
The proof of Lemma 3: the left limit of $\Pi_I - \Pi^{n*}_I$ at $\bar w_I$ in closed form.
Lemma 3: some $w_I \in [0, \bar w_I)$ gives $\Pi_I(w_I) > \Pi^{n*}_I$ .
Lemma 4: $\Pi^s_I$ is strictly increasing on the separating region.
For $t > 35/92$ , $\bar w_{sep/pool} - \bar{\bar w}_{equal}$ is strictly increasing in $w_A$ , where $\bar{\bar w}_{equal}$ (equation (16)) equates the last separating piece with $\Pi^p_I(\bar w_I)$ .
Its limit as $w_A \uparrow 1/2 - 5t/7$ equals $(153(\sqrt{5134} - 122)t + 125\sqrt{21t(51t + 52)})/5250$ .
The limit itself is positive if and only if $t < \bar t$ .
Lemma 5 (i): for $t < \bar t$ , thresholds $\underline w_A$ , $\bar w_A$ inside the range separate the separating and the pooling outcomes. The pooling value is approached by feasible wholesale prices if its maximizing endpoint is excluded.

Significance

Proposition 4 turns a two-stage signaling game into a two-parameter phase diagram. The VI pays an information rent, by pricing at $\bar w_{sep/pool}$ below the outside price, only when demand uncertainty is low ( $t < \bar t$ ) and the outside market is inefficient ( $w_A > \bar w_A$ ). Otherwise she prices just below the level at which the DO walks away, and the DO conceals his information by pooling and dual sourcing in high demand. The paper builds its welfare comparison (Proposition 5) and its numerical study of the value of the partnership and of information on this characterization.

The result is proved on paper but has no machine-checked proof. The work is explicit real analysis: a piecewise objective with square roots, branch thresholds and a jump, and an optimization over a half-line. The formal statement also records corrections the paper needs (see the scope section), so that a proof checks the intended theorem rather than its typeset version.

Difficulty

$\Pi_I$ is neither concave, monotone nor continuous: the separating piece itself has four sub-branches (the low-demand order hits zero, the DO starts dual sourcing), and $\Pi_I$ jumps down to $\Pi^{n*}_I$ at $\bar w_I$ . A first-order condition on one formula does not work. The comparison of the two candidates, $\Pi^s_I(\bar w_{sep/pool})$ against $\Pi^p_I(\bar w_I)$ , involves nested radicals in $t$ and $w_A$ , and its sign changes along a curve $w_A = \bar w_A(t)$ that has no closed form. The paper locates that curve only through the monotonicity of $\bar w_{sep/pool} - \bar{\bar w}_{equal}$ in $w_A$ and the sign of its boundary limit; establishing both requires polynomial inequalities over a two-dimensional region with irrational coefficients.

Formalization scope

Everything is in $\mathbb R$ ; the parameters are the two reals $t$ and $w_A$ , and the decision variable is $w_I$ . The two-point prior is written out as an average of the two states; no measure theory is used.

The quantity subgame is taken as given. Lemmas 1–2, Definition 1 and Proposition 3 (existence and selection of the Pareto-dominant separating or pooling equilibrium) are not formalized; their closed-form quantities enter (6) as definitions, transcribed as printed. The goal is the VI's first-stage problem over the displayed (6), which is exactly what Proposition 4 is about.
Equation (4) is corrected. The page typesets $\bar w_I$ with the radical over $34(7 - 10t - 14w_A)$ ; the radical belongs over $34$ alone, $\bar w_I = (245 - 350t - 70w_A - 6\sqrt{34}(7 - 10t - 14w_A))/420$ . The typeset form contradicts the paper's own Lemma 3 identity and Table 1, and makes Lemma 3 and Proposition 4 false in part of the region.
Standing assumptions $t \ge \underline t$ , $w_A > \underline w$ (exact value) and $w_A < 1/2 - 5t/7$ are used on the VI optimization statements, including Lemma 3, which the paper states just before introducing $t \ge \underline t$ . Algebraic items such as equation (13) use their stated domains.
$w_I^* = \bar w_I^{(-)}$ is a supremum with a left limit, never an arg max at $\bar w_I$ , where $\Pi_I = \Pi^{n*}_I$ . The domain $w_I \ge 0$ is kept: over all of $\mathbb R$ the pooling quadratic would dominate. Any formalization that builds the answer into the definition of $\Pi_I$ , or replaces the threshold $\bar w_A$ by one outside the parameter range, trivializes the result and is excluded.
Positive parts are max 0, and Real.sqrt radicands are nonnegative wherever they are used. Printed slips in the proofs (a $\bar t$ for $t$ in a limit formula, $\Pi^{S*}_I$ for $\Pi^{p*}_I$ ) are corrected in the Lean and disclosed.

Contributions welcome: proofs of the milestones, which are self-contained real-analysis statements; reusable lemmas on piecewise-defined maximization and one-sided limits of branch functions; and, separately, a formal treatment of the quantity-subgame equilibria of Lemmas 1–2.

Selected references

S. H. Jung, P. Kouvelis, On Co-opetitive Supply Partnerships with End-Product Rivals: Information Asymmetry, Dual Sourcing and Supply Market Efficiency, SSRN preprint 3555184, 2020; Manufacturing & Service Operations Management, 2022. https://ssrn.com/abstract=3555184, https://doi.org/10.1287/msom.2021.0982

10 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Quality Regulation on Two-Sided Platforms: Exclusion, Subsidization, and First-Party Applications: Exclusion Is a Special Case of Subsidization and Is Dominated by ItResearch Paper

Why platform quality rules matter

An application platform can increase average quality by excluding low-quality developers, or it can pay high-quality developers to join. Either choice changes the number of applications, the consumer audience, and the fees the platform can charge. Huang, Lyu, and Xu study these linked effects in a two-sided market with consumers and two developer types. Their SSRN paper, §5.1.1 compares exclusion with a targeted subsidy from the platform's perspective. The comparison matters when a platform must decide whether to restrict entry or use payments to shape the mix of applications.

The paper appeared in Management Science in 2021. This mission uses the 43-page SSRN posting, whose page and equation numbering are the source for every target below. Its online appendices are absent from the held posting, so several closed forms that the paper says are available there cannot be cited as printed appendix statements.

Market and decisions

A two-sided platform serves consumers and application developers. A fraction $\lambda$ of developers are high quality, with application quality $q_h>0$ ; the remaining fraction are low quality, with quality normalized to zero. Write $m$ for the consumer network size, $n$ for the total developer network size, and $n_h,n_l$ for the high- and low-quality developer counts. Their average quality is $\bar q=q_hn_h/n$ when $n>0$ .

Consumers receive base value $w$ , a cross-side benefit $\alpha_c n$ , and a benefit $\beta\bar qn$ from total application quality. The separate average-quality preference $\mu$ is fixed to zero in this mission, matching §5.1. Developer types receive cross-side benefits $\alpha_{dh}m$ and $\alpha_{dl}m$ , while congestion costs them $bn$ . Consumers and developers also face uniformly distributed differentiation costs on $[0,\theta_c]$ and $[0,\theta_d]$ . The platform chooses a developer access fee $p_d$ and a consumer access fee $p_c$ .

Under exclusion, only high-quality developers can enter, so $n=n_h$ and $\bar q^E=q_h$ . Under subsidization, low-quality developers may enter, and the platform pays each high-quality entrant a fixed amount $\gamma\ge0$ . The paper's demand equations determine the network sizes from the fees. The resulting profits are

\Pi^E=p_dn+p_cm-\eta mn,\qquad \Pi^S=p_dn+p_cm-\eta mn-\gamma n_h,

where $\eta mn$ is the platform's operating cost. The model defines an optimum by comparison with every feasible outcome of the same strategy. Thus the goal concerns the platform's choices and induced participation, rather than a comparison of two isolated algebraic formulas.

Formalization targets

The main target is a corrected form of Proposition 4, p. 26. For optimal, interior exclusion and subsidization outcomes in the nonnegative-subsidy regime,

\Pi^{S*}\ge\Pi^{E*},\qquad \bar q^{S*}\le q_h=\bar q^{E*},\qquad m^{S*}>m^{E*},\qquad n^{S*}>n^{E*}.

It also asks for a feasible subsidy outcome that reproduces the optimal exclusion outcome: no low-quality entrant, the same consumer and high-quality developer counts, and the same platform profit. The goal is quantified over outcomes that optimize the original fee-and-participation model.

Five milestones follow the paper's attack path: the reduced exclusion profit in §4.1, p. 12; the exclusion optimum in Proposition 1.1(1), pp. 12–13; the reduced subsidy profit in §4.2, p. 16; the optimal subsidy in Proposition 2.2(1), p. 17; and the replication claim in the discussion following Proposition 4, p. 26. Each milestone carries the statement from the SSRN pages and its page provenance.

What the comparison establishes

Profit dominance would mean that, within the specified parameter regime, a platform with the subsidy option can attain at least the exclusion profit. The quality comparison says this gain may come with a lower average quality, even while the consumer and total developer networks grow. The replication clause gives the strategy comparison a direct interpretation in terms of fees and participation. These are distinct claims: a larger total network need not contain more high-quality developers.

The result is already claimed in the paper, but the printed Proposition 4 contains statements that do not hold as written. A formal proof would establish the corrected result for the exact fee, subsidy, and demand model, and would clarify the required regime and interior conditions. The reusable outputs are the model definitions and the reduced-profit identities; other quality-regulation comparisons could build on them. No machine-checked proof of this proposition is claimed here. The draft Lean theorem is an open target.

Why the target is difficult

The fee choices affect participation on both sides, while quality affects consumer demand and developer payments affect the platform's net revenue. Comparing the two optima therefore requires more than observing that a subsidy can raise high-quality participation. In particular, an unconstrained algebraic optimum for $\gamma$ can be negative, but the actual subsidy strategy requires $\gamma\ge0$ . The paper's claim that exclusion is a special case also has to respect this constraint while keeping the same realized network sizes and profit.

The source's part (3) shows another difficulty: high-quality participation, total developer participation, and developer access fees can move in different directions. Treating those quantities as interchangeable would prove a different and sometimes false comparison.

Formalization scope and corrections

All parameters, fees, network sizes, and profits are real numbers. The Lean model uses the paper's untruncated linear demand equations at $\mu=0$ . Feasibility requires nonnegative consumer and developer counts; it also requires $\gamma\ge0$ , $n_l\ge0$ , and $n_h\ge0$ for subsidization. The high-quality count in consumer demand makes total quality equal to $q_hn_h$ . The composite parameters $\bar\alpha_d,\xi,\xi_1,\rho,t,\tau$ use the coefficients and signs printed in §§3–4.

The standing parameter condition includes $0<\lambda<1$ , $q_h,\theta_c,\theta_d,b,w>0$ , $\alpha_{dl}\le\alpha_{dh}$ , and $\beta\ge0$ ; it puts no extra sign on $\alpha_c$ or $\eta$ . The strict inequalities on $\lambda$ strengthen the source's $\lambda\in[0,1]$ because the exclusion inverse demand divides by $\lambda$ and the comparison requires both developer types. Separate strict-concavity conditions make explicit the paper's joint-concavity assumption and its use of unique optima. The main theorem assumes interior optimal participation and $\alpha_{dh}-\alpha_{dl}\le\beta q_h$ .

That last restriction is needed for the printed profit-dominance claim. For example, $\lambda=1/5$ , $q_h=1/2$ , $\theta_c=\theta_d=1$ , $\alpha_{dh}=1$ , $\alpha_{dl}=0$ , $\alpha_c=b=1/2$ , $\beta=\eta=0$ , and $w=1$ give $\Pi^{S*}=150/551<22/79=\Pi^{E*}$ . The paper's printed part (3) also claims $n_h^{S*}>n^{E*}$ and $p_d^{S*}>p_d^{E*}$ . At its Figure 3 parameters with $\lambda=1/10$ , $n_h^{S*}=247650/27398773<525/52868=n^{E*}$ . At $\lambda=1/4$ , $q_h=1$ , $\theta_c=1$ , $\theta_d=4$ , $\alpha_{dh}=1$ , $\alpha_{dl}=1/2$ , $\alpha_c=3/2$ , $b=2$ , $\beta=1/2$ , $\eta=0$ , and $w=1$ , the subsidy developer fee is $-64/199<-2/7$ , the exclusion fee. The goal therefore states larger total developer and consumer networks and leaves out the false fee comparison.

The goal cannot be discharged by defining profit as its reduced quadratic formula or by merely substituting the reported optimal closed forms: the fee-and-demand definitions and optimality over feasible outcomes remain part of the statement. The development needs real algebra, strict concavity of quadratic objectives, inverse-demand identities, and inequality reasoning at the feasible boundary. The equation identities and basic optimization lemmas are useful contributions beyond this comparison.

Selected references

P. Huang, G. Lyu, and Y. Xu, Quality Regulation on Two-Sided Platforms: Exclusion, Subsidization, and First-Party Applications, Management Science, 2021; SSRN posting 3948778, §§3–5, especially Proposition 4, p. 26 (PDF 27).

7 thms2 active usersReviewed

Completed

Economics Mechanism Design Operations Research·Captain: mikedeng1

On the Futility of Dynamics in Robust Mechanism Design: Minimax Regret Equals T Times the Single-Round Minimax Regret and Repeating a Direct Static Mechanism Is OptimalResearch Paper

Motivation

A seller who faces the same buyer again and again, a firm that contracts repeatedly with a supplier, or a platform that allocates resources to a returning user can adapt its terms over time. The buyer's behaviour reveals information about their preferences, and mechanisms can link rounds through bundles, discounts and promised future utility. When the principal does not know the distribution of the agent's preferences, adapting looks attractive. This is the repeated-interaction setting of the paper.

Balseiro, Kim and Russo ask whether such dynamics help when the principal evaluates a mechanism by its worst-case regret over a set of possible distributions, the robust objective common in dynamic pricing and online learning. Their answer, under two conditions that hold for a broad class of games, is that dynamics are useless. The optimal minimax regret over $T$ rounds is exactly $T$ times the single-round minimax regret restricted to point-mass distributions, and repeating a single-round direct mechanism achieves it. This mission formalizes that reduction (Theorem 1 of the paper).

Setting

A game consists of a set of shocks $\Theta$ , a set of outcomes $\Omega$ with a no-interaction outcome $\emptyset$ , a principal utility $u(\theta,\omega)$ and an agent utility $v(\theta,\omega)$ , with $u(\theta,\emptyset)=v(\theta,\emptyset)=0$ . The agent's shocks $\theta_1,\dots,\theta_T$ are i.i.d. from a distribution $F$ that the agent learns in Round 0 and the principal never sees. The agent observes $\theta_t$ privately at the start of round $t$ .

A dynamic mechanism $A$ fixes report spaces $\mathcal M_0,\dots,\mathcal M_T$ , with a report QUIT in $\mathcal M_0$ . It also fixes decision rules $\omega_t=\pi_t(m_t,h_t,z_t)$ , which depend on the current report, the public history $h_t=(m_{0:t-1},\omega_{1:t-1})$ and a private uniform $z_t$ . Finally it fixes a recommended strategy $\sigma$ , with $m_0=\sigma_0(F,y_0)$ and $m_t=\sigma_t(\theta_t,h^+_t,y_t)$ . Here $h^+_t=(F,\theta_{1:t-1},m_{0:t-1},\omega_{1:t-1})$ is everything the agent knows and $y_t$ is the agent's private uniform. After QUIT every outcome is $\emptyset$ .

The principal utility and agent utility of a strategy $\tilde\sigma$ are the expected sums $\mathbb E[\sum_{t=1}^T u(\theta_t,\omega_t)]$ and $\mathbb E[\sum_{t=1}^T v(\theta_t,\omega_t)]$ . $A$ is incentive compatible (IC) if, for every distribution $F$ on $\Theta$ and every feasible strategy $\tilde\sigma$ , following $\sigma$ gives the agent at least as much as $\tilde\sigma$ . Because QUIT is a deviation, IC contains individual rationality. With $\mathcal A$ the set of IC mechanisms:

\mathrm{OPT}(F,T)=\sup_{A\in\mathcal A}\mathrm{PrincipalUtility}(A,F,T),\qquad \mathrm{Regret}(A,F,T)=\mathrm{OPT}(F,T)-\mathrm{PrincipalUtility}(A,F,T),

\mathrm{Regret}(T)=\inf_{A\in\mathcal A}\ \sup_{F\in\mathcal F}\mathrm{Regret}(A,F,T),

where $\mathcal F$ is the set of distributions the principal guards against.

A direct static mechanism $S^{\times T}$ repeats a single-round rule $\tilde\pi(m,z)$ . The agent reports a shock or PASS (which yields $\emptyset$ ), the rule ignores the history and the round, and the recommended strategy is truthful. $\mathcal S^{\times1}$ is the class of such single-round mechanisms that are IC. Assumption 1 says that $\delta_\theta\in\mathcal F$ for every $\theta$ . Assumption 2 (extreme-point convexity) says that $\mathrm{OPT}(F,T)\le\mathbb E_{\theta\sim F}[\mathrm{OPT}(\delta_\theta,T)]$ for $F\in\mathcal F$ .

Formalization targets

Goal: Theorem 1

Under Assumptions 1 and 2,

\mathrm{Regret}(T)=T\cdot\inf_{S\in\mathcal S^{\times1}}\sup_{\theta\in\Theta}\mathrm{Regret}(S,\delta_\theta,1).

Moreover, an $S$ that is within $\epsilon/T$ of the single-round infimum satisfies $\sup_{F\in\mathcal F}\mathrm{Regret}(S^{\times T},F,T)\le\mathrm{Regret}(T)+\epsilon$ . The multi-round problem has an optimal mechanism if and only if the single-round problem does. No constant is fixed: the statement identifies the value, its near-optimal solutions and the existence of optimal solutions.

Milestones

In proof order:

Proposition 13 (parts 1–2): $\mathrm{OPT}(F,T)\le T\,\bar u(F)$ and $\mathrm{OPT}(\delta_\theta,T)=T\,\bar u(\delta_\theta)$ , where $\bar u$ is the first-best single-round value.
Proposition 1: $\mathrm{OPT}(\delta_\theta,T)=T\cdot\mathrm{OPT}(\delta_\theta,1)$ .
Lemma 4: every IC mechanism yields $S(A)\in\mathcal S^{\times1}$ with T times its point-mass principal utility.
Lemma 2: the lower bound $\sup_F\mathrm{Regret}(A,F,T)\ge T\sup_\theta\mathrm{Regret}(S,\delta_\theta,1)$ .
Claim 1: replicating any round of a deviation as a single-round deviation.
Lemma 5: $S^{\times T}$ is IC, and its value is linear in $T$ .
Lemma 6: the single-round mixture inequality.
Lemma 3: the upper bound $\sup_F\mathrm{Regret}(S^{\times T},F,T)\le T\sup_\theta\mathrm{Regret}(S,\delta_\theta,1)$ .

Significance

Theorem 1 replaces a $T$ -round dynamic mechanism design problem, whose decision variables are history-dependent rules over arbitrary message spaces, by a single-round problem over direct mechanisms and point masses. The single-round problem is often a linear program or is solvable with Myersonian methods. The paper uses this to compute the minimax regret $T/e$ for repeated selling of one good (Proposition 3) and to characterize the optimal mechanism of a principal–agent contract model (Proposition 4). For these games it shows that adaptive learning schemes cannot beat a myopic, non-adaptive mechanism under the minimax-regret criterion.

The result is proved on paper. The Lean statements in this mission compile, but their proofs remain open. A complete development would give a machine-checked model of repeated principal–agent interaction with a fully strategic, forward-looking agent: arbitrary report spaces, private randomization, augmented histories, and IC against all history-dependent deviations. It would also check a revelation-principle-type reduction (Lemma 4) whose informal proof leaves measurability and integrability implicit.

Difficulty

The obvious argument restricts nature to point masses and then "repeats the best single-round mechanism". It fails twice. First, an optimal dynamic mechanism may be IC only because of its dynamics; the lower bound needs a single-round mechanism $S(A)$ whose IC follows from IC of $A$ against deviations that mimic another point mass (Lemma 4). Second, a repeated mechanism must be IC against deviations that condition on the whole past. Showing that one round of such a deviation is itself a single-round deviation (Claim 1) requires the agent to simulate past shocks and the principal's randomness from private noise. Behind both steps sit time-averaged and conditional outcome laws that must be realized as measurable rules of a single uniform.

Formalization scope

The Lean game (FutileDynamics.StaticOpt.Game) gives the shock and outcome spaces, utilities, and no-interaction outcome. The mechanism model (FutileDynamics.StaticOpt.Model) imports it and fixes the following conventions, all disclosed in the items:

$u$ and $v$ are jointly measurable and bounded, so every expectation is a genuine Bochner integral.
$\Theta$ is a standard Borel space and nonempty, and $0<T$ .
Decision rules are jointly measurable. A feasible strategy, recommended or deviating, is jointly measurable in all its arguments, the distribution $F$ (Giry σ-algebra) included.
Rounds are 0-indexed (k : Fin T is round $k+1$ ), and uniforms live on unitInterval.
Every report space is a standard Borel space, so the set of measurable (feasible) deviations is not an artefact of the designer's choice of σ-algebra.
The round report space $\Theta\cup\{\mathrm{PASS}\}$ is Θ × Bool: $(\theta,\mathrm{true})$ reports $\theta$ , and every $(\theta,\mathrm{false})$ is PASS and yields $\emptyset$ . CONTINUE/QUIT is true/false.
$\mathrm{OPT}$ , $\mathrm{Regret}(A,T)$ , $\mathrm{Regret}(T)$ and the single-round value are real suprema and infima over sets that are nonempty (the always- $\emptyset$ mechanism is IC) and bounded.
The paper's $\bar u$ (E-8) is printed as a supremum over $\mathcal S^{\times1}$ , but its proof drops IC. The Lean $\bar u$ ranges over all direct rules (corrected).

The statement admits several trivializing formalizations, and the model rules each out:

$\mathcal A$ restricted to direct or static mechanisms. Here OPT and $\mathrm{Regret}(T)$ quantify over every report-space family.
IC required only against $F\in\mathcal F$ , only against point masses, or only against truthful misreports. Here IC holds against every probability distribution and every feasible history-dependent, randomized deviation, QUIT included.
$\mathcal S^{\times1}$ defined by the IC/IR program (3). Here it is IC in the dynamic sense at horizon 1.

A complete development needs:

trajectories of the interaction as measurable functions of the noise;
Fubini and independence arguments for i.i.d. shocks;
measurable sampling from a distribution on a standard Borel space;
splitting one uniform into countably many.

These pieces are reusable for any repeated-game or dynamic-mechanism formalization. Proofs of the milestones, of the lower and upper bounds, and of auxiliary measurability lemmas are welcome.

Selected references

S. R. Balseiro, A. Kim, D. Russo, On the futility of dynamics in robust mechanism design, Operations Research, 2021; SSRN working paper 3449698 (version of October 5, 2020), the text formalized here. https://doi.org/10.1287/opre.2021.2122 · https://ssrn.com/abstract=3449698

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Preference Elicitation for Participatory Budgeting: Randomized Threshold Approval Votes Achieve Distortion O(log² m)Research Paper

Motivation

In participatory budgeting, residents of a city vote on how to spend part of a public budget on a list of proposed projects, each with a known cost. The practice has been adopted by cities in North America and Europe, including New York City, Chicago, Madrid and Paris, the last two each spending more than 100 million euros through participatory budgets in 2017 (Cabannes, 2004; paper §1). Every deployment must choose a ballot: voters may be asked to approve some projects, to rank them, or to fill a knapsack within the budget. The ballot determines how much information about the residents' preferences reaches the aggregation step, and so how much welfare the chosen set of projects can guarantee.

The implicit utilitarian framework of Procaccia and Rosenschein (2006) makes this question quantitative. Voters are assumed to hold cardinal utilities, which the ballot reveals only partially; the quality of a ballot-plus-aggregation pair is measured by its distortion, the worst-case ratio between the best achievable welfare and the welfare it actually obtains. Benadè, Nath, Procaccia and Shah (Management Science, 2021; AAAI 2017 conference version) apply this lens to participatory budgeting and compare the input formats used in practice. Their main positive result is that threshold approval votes with a randomly drawn threshold reach distortion $O(\log^2 m)$ , against $m$ for a rule that uses no information at all and $\Omega(\sqrt m)$ for any deterministic threshold.

Setting

There are $n$ voters $N=[n]$ and a set $A$ of $m$ alternatives (projects). Alternative $a$ costs $c_a\in[0,1]$ , and the budget is $1$ . Write $c(S)=\sum_{a\in S}c_a$ , and let

\mathcal F_c=\{S\subseteq A:\ c(S)\le 1,\ c(T)>1\text{ for all }S\subsetneq T\subseteq A\}

be the family of inclusion-maximal budget-feasible sets.

Voter $i$ has a utility $v_i(a)\ge 0$ for each alternative, utilities are additive over sets, and they are normalized: $\sum_{a\in A}v_i(a)=1$ . The social welfare of a set is $\mathrm{sw}(S,\vec v)=\sum_{a\in S}\sum_{i\in N}v_i(a)$ .

A threshold approval vote at threshold $t$ is the set $\tau_i=\{a\in A: v_i(a)\ge t\}$ . A randomized threshold rule chooses a threshold $t$ at random and maps the resulting profile $\vec\rho(\vec v,t)=(\tau_1,\dots,\tau_n)$ to a (possibly random) set in $\mathcal F_c$ . In the formalization, a rule is a finite mixture of arms; each arm has a probability, a threshold, and a deterministic aggregation map from approval profiles to $\mathcal F_c$ (ThresholdRule), and its expected welfare is the weighted sum over arms (ThresholdRule.expWelfare). The rule never sees the utilities, only the approval sets. The distortion of a rule is bounded by $D$ when

\max_{T\in\mathcal F_c}\mathrm{sw}(T,\vec v)\ \le\ D\cdot\mathbb E[\mathrm{sw}(\text{rule},\vec v)]\quad\text{for every normalized profile }\vec v,

and the distortion associated with an input format is that of the best rule for it.

Formalization targets

Goal: Theorem 3.5

\exists\,C>0\ \ \forall n,\ \forall A\text{ with }m\ge 2,\ \forall c\in[0,1]^A:\ \exists\text{ rule }R\ \ \forall\vec v,\ \forall T\in\mathcal F_c:\quad \mathrm{sw}(T,\vec v)\le C\log_2^2 m\cdot\mathbb E[\mathrm{sw}(R,\vec v)].

The goal fixes only the shape $O(\log^2 m)$ , with an absolute constant chosen before $n$ , $A$ and the costs, and it covers every $m\ge 2$ .

Milestones

For $m=2^K$ , with $\ell_j=2^{j-1}/m^2$ , $u_j=2^j/m^2$ , $I_j=(\ell_j,u_j]$ , cost buckets $S_j=\{a:c_a\in I_j\}$ ( $S_0$ uses $I_0=[0,1/m^2]$ ) and counts $n^a_j=|\{i:v_i(a)\in I_j\}|$ . In the statements involving $S^*$ , it is an optimal member of $\mathcal F_c$ for the given utility profile (IsWelfareOptimal).

Observation 3.1: some rule has distortion at most $m$ .
Eq. (6): $\sum_{j\ge1}n^a_j\ell_j\le\mathrm{sw}(a,\vec v)\le n/m^2+\sum_{j\ge1}n^a_ju_j$ .
At most $1/u_j$ alternatives from $S_j$ are budget-feasible.
Eq. (7): the same sandwich for $\mathrm{sw}(S^*\cap S_k,\vec v)$ .
Eq. (8): a greedy top set $B_{j,k}\subseteq S_k$ at threshold $\ell_j$ has $\mathrm{sw}(B_{j,k},\vec v)\ge\frac14 n^*_{j,k}u_j$ .
Mechanism A's expected welfare is at least $(\mathrm{sw}(S^*\setminus S_0,\vec v)-n/m)/(16\log^2 m)$ .
Mechanism B: $S_0$ is feasible and covers $S^*\cap S_0$ .
The explicit form for $m=2^K$ : distortion at most $2+16\log^2 m$ .

Significance

The theorem separates randomized from deterministic elicitation: with a fixed threshold no aggregation rule beats $\Omega(\sqrt m)$ (Theorem 3.4 of the paper), while drawing the threshold at random brings the distortion to $O(\log^2 m)$ , close to the $\Omega(\log m/\log\log m)$ lower bound of Theorem 3.6. It is the paper's argument for threshold approval as a practical, low-burden ballot, and it supports the empirical comparison in the paper's §5 between input formats on data from real participatory budgeting elections.

The result is proved in the paper; no machine-checked version is known. A formalization yields a reusable layer for implicit utilitarian voting with budgets (feasible-set families, normalized additive profiles, randomized rules over partial ballots, distortion), on which the paper's other bounds (Theorem 3.3 for rankings, Theorems 3.4 and 3.6 for lower bounds) and the related literature on distortion can be stated. It also makes explicit the reading of distortion under a random threshold that the proof actually uses.

Difficulty

The obvious rule picks the threshold and then funds the most-approved projects greedily. It fails because one threshold cannot serve both high-utility and low-utility voters, and because popular projects may be expensive: approval counts say nothing about costs. Mixing over thresholds alone does not help either; the ratio for a single badly chosen threshold can be of order $m$ . What has to be shown is that one fixed mixture, chosen before any utilities are seen, recovers a $1/O(\log^2 m)$ share of the optimum simultaneously for every profile, despite rounding of utilities into intervals, budget constraints within each cost class, and the loss of everything below the smallest threshold.

Formalization scope

All objects live in PBElicit.RandThresh (definition file PBElicit.RandThresh.Setting). Voters are Fin n; alternatives are a Fintype with $m$ = Fintype.card A. Utilities are real, nonnegative and normalized (IsUtilityProfile); costs satisfy $0\le c_a\le 1$ , which the paper uses when it calls a single alternative budget-feasible. Rules must return sets of $\mathcal F_c$ (IsMaxFeasible); the paper's mechanisms return feasible sets, which are extended to maximal ones. The maximum over $\mathcal F_c$ is stated as "for every $T\in\mathcal F_c$ "; distortion bounds are multiplicative. Logarithms are base $2$ . The milestones take $m=2^K$ , as the paper's proof does; the goal does not.

Distortion is read as the optimum over the total expected welfare (threshold and aggregation together), which is what the proof of Theorem 3.5 bounds; the paper's displayed definition puts the expectation over the threshold outside the ratio. The interval bound (8) is formalized as its outer inequality, because the printed middle step fails when a utility equals a threshold exactly.

The rule is fixed before the utilities, sees only threshold approval votes, and must return an inclusion-maximal feasible set; choosing the rule after the profile (which makes distortion $1$ trivially) is excluded by the quantifier order, and the uniform rule of Observation 3.1 only gives distortion $m$ , so a $C\log^2 m$ bound is a genuine improvement.

Welcome contributions: proofs of the milestones, the reduction from general $m$ to the next power of $2$ , and further results of the paper stated on the same definitions.

Selected references

G. Benadè, S. Nath, A. D. Procaccia, N. Shah, Preference Elicitation for Participatory Budgeting, Management Science, 2021 (AAAI 2017 conference version). https://doi.org/10.1287/mnsc.2020.3666
A. D. Procaccia, J. S. Rosenschein, The Distortion of Cardinal Preferences in Voting, Cooperative Information Agents (CIA), LNCS 4149, pp. 317–331, 2006. https://doi.org/10.1007/11839354_23
I. Caragiannis, A. D. Procaccia, Voting Almost Maximizes Social Welfare Despite Limited Communication, Artificial Intelligence 175(9–10), pp. 1655–1671, 2011. https://doi.org/10.1016/j.artint.2011.03.005
C. Boutilier, I. Caragiannis, S. Haber, T. Lu, A. D. Procaccia, O. Sheffet, Optimal Social Choice Functions: A Utilitarian View, Artificial Intelligence 227, pp. 190–213, 2015. https://doi.org/10.1016/j.artint.2015.06.003
Y. Cabannes, Participatory Budgeting: A Significant Contribution to Participatory Democracy, Environment and Urbanization 16(1), pp. 27–46, 2004. https://doi.org/10.1177/095624780401600104

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Best of Both Worlds: Ex-Ante and Ex-Post Fairness in Resource Allocation: Recursive Probabilistic Serial Is Ex-Ante Envy-Free and Ex-Post Envy-Free up to One GoodResearch Paper

Motivation

Many allocation problems hand out indivisible goods without money: course seats, shifts, donated food, inherited items. An integral allocation of such goods can rarely be envy-free. With one good and two agents, someone always envies. The standard remedies are of two kinds. Randomization restores fairness in expectation: the probabilistic serial rule of Bogomolnaia and Moulin (J. Econ. Theory 2001) yields a fractional allocation that is envy-free and can be implemented as a lottery over integral allocations. Approximation restores fairness after the draw: envy-freeness up to one good (EF1), introduced by Lipton, Markakis, Mossel and Saberi (EC 2004) and named by Budish (J. Political Economy 2011), asks only that any envy disappear once a single good is removed from the envied bundle.

The two remedies pull apart. Giving all goods to one agent chosen uniformly at random is envy-free ex-ante, but after the draw one agent holds everything. Round-robin picking with a uniformly random order is EF1 after every draw, and proportional but not envy-free in expectation (Proposition 2 and Example 1 of the paper). Freeman, Shah and Vaish (arXiv:2005.14122, 2020; with Aziz, Operations Research 2024) ask whether one lottery can be fair in both senses at once. They show that it can, and that the answer depends on how the lottery is built, not only on which fractional allocation it implements.

Setting

There is a finite set $N$ of $n \ge 1$ agents and a finite set $M$ of $m$ goods. Agent $i$ has an additive valuation with values $v_{i,g} \ge 0$ . A fractional allocation is a matrix $X$ with $X_{i,g} \in [0,1]$ the share of good $g$ given to agent $i$ , and $v_i(X_i) = \sum_g X_{i,g} v_{i,g}$ . An integral allocation gives each agent a bundle $A_i \subseteq M$ , with bundles pairwise disjoint, and $v_i(A_i) = \sum_{g \in A_i} v_{i,g}$ . A randomized allocation is a finite lottery $\{(p^k, A^k)\}_k$ over integral allocations. It implements the fractional allocation $\sum_k p^k A^k$ .

$X$ is envy-free (EF) if $v_i(X_i) \ge v_i(X_h)$ for all $i, h$ . An integral allocation $A$ is EF1 if for all $i, h$ with $A_h \neq \emptyset$ some $j \in A_h$ satisfies $v_i(A_i) \ge v_i(A_h \setminus \{j\})$ . A lottery is ex-ante EF if the allocation it implements is EF. It is ex-post EF1 if every allocation it draws is EF1.

The eating protocol $\mathrm{Eating}(M', 1)$ runs for one unit of time on the goods $M'$ , each of mass one. At every moment each agent eats her favorite good among those not yet fully consumed, at rate one. Recursive Probabilistic Serial (Algorithm 1) proceeds in $\lceil m/n \rceil$ stages, starting from $M^1 = M$ . Stage $t$ computes $X^t = \mathrm{Eating}(M^t, 1)$ and decomposes it as $X^t = \sum_k w^{t,k} A^{t,k}$ by the generalized Birkhoff–von Neumann theorem, Theorem 1 of the paper. It then draws $B^t = A^{t,k}$ with probability $w^{t,k}$ and continues on $M^{t+1} = M^t \setminus \bigcup_i B^t_i$ . The final bundles are $B_i = \bigcup_t B^t_i$ .

Formalization targets

Goal: Theorem 2 (p. 11)

For every instance, every way of breaking ties between equally valued goods, and every decomposition rule satisfying the conclusions of Theorem 1,

\text{the lottery of Algorithm 1 is ex-ante envy-free and ex-post EF1.}

Milestones

Theorem 1 (p. 9). A matrix with entries in $[0,1]$ and row and column sums at most $1$ is a convex combination of $0/1$ allocations. Each of their row and column sums is the floor or the ceiling of the corresponding sum of $X$ .
One eating stage (§3.1, p. 9). $\mathrm{Eating}(M', 1)$ satisfies the hypotheses of Theorem 1 and is supported on $M'$ . If $|M'| \ge n$ , every agent eats a total mass of exactly one.
One item per stage (§3.1, p. 9). Every allocation of the decomposition uses only goods of $M'$ . If $|M'| \ge n$ , it gives each agent exactly one good.
Each eating stage is envy-free (proof of Theorem 2, p. 11).
Lemma 1 (p. 11). In iteration $t < \lceil m/n \rceil$ , each agent weakly prefers the good she receives to every good still unallocated.
Lemma 2 (p. 11). Every allocation returned by Algorithm 1 is EF1.
Algorithm 1 returns a randomized allocation (§3.1, p. 9).
The expectation recursion (proof of Theorem 2, p. 11; Algorithm 3, p. 33). The implemented allocation is the first eating stage plus the weighted sum of the allocations implemented on the remaining goods.

Significance

Theorem 2 shows that ex-ante envy-freeness and ex-post EF1 are compatible for additive goods. Algorithm 1 is a constructive witness. The paper builds on this in two directions. A polynomial-time variant (§3.2) computes such a lottery. An impossibility result (Theorem 3) shows that adding ex-post fractional Pareto optimality is too much. The paper also extends the approach to bads and mixed manna (§7), where the natural extension guarantees only ex-post EF2.

The result is proved on paper. No formalization of probabilistic serial, the eating protocol, EF1 of randomized allocations or the rectangular Birkhoff–von Neumann theorem with floor and ceiling bounds is known to us in any proof assistant. Mathlib has the square doubly stochastic case (doublyStochastic_eq_convexHull_permMatrix), and Prove2Me has it as FamousTheorems.birkhoff_von_neumann. This mission asks for a machine-checked proof of Theorem 2 about an explicit definition of the eating protocol and of Algorithm 1.

Difficulty

The proof is short on paper but hides two pieces of continuous-time bookkeeping. First, the eating protocol is a process in time. The stage statements need a description of it in which "agent $i$ ate a positive share of $g$ while $g^*$ was still available" can be stated and checked. Second, the ex-ante argument conditions on the history of earlier draws. Because the decomposition may have exponentially many branches, it has to be turned into an induction over the recursive lottery. The obvious shortcut, proving the result for "the" BvN decomposition of each stage, fails because the decomposition is not unique and the theorem must hold for all of them. Weight-zero terms of a decomposition can violate Lemma 1. They are never drawn, but any argument over the whole support must exclude them explicitly.

Formalization scope

Agents and goods are finite types with decidable equality. The good set $M$ is the whole type of goods, and $n \ge 1$ is [Nonempty N]. Values are real and non-negative. All quantities are in $\mathbb R$ , and $\lceil m/n \rceil$ is Nat.ceil of a real quotient. Integral allocations are bundle maps N → Finset G, and lotteries are finite lists of (probability, allocation) pairs.

The eating protocol is a definition computed event by event. Between events every agent eats a fixed good chosen by a choice rule. The next event comes when the time budget ends or a good being eaten is exhausted. The minimum runs only over goods actually being eaten, so no division by zero occurs. $|M| + 1$ events suffice, and later iterations change nothing. Algorithm 1 is a definition: a recursion over stages producing a lottery over stage histories.

The only free parameters of the goal are the tie-breaking rule, constrained to choose a most valuable available good, and the decomposition rule, constrained to satisfy Theorem 1's conclusions. The eating outcome, the lottery and its support are computed by the definitions, never assumed. A statement taking $X^t$ or the lottery as free variables with envy-freeness as a hypothesis would trivialize the goal and is not this mission.

Conventions that differ from the page:

Ex-post EF1 is over allocations drawn with positive probability.
The without-loss-of-generality assumption that every good is valued positively by some agent is omitted. The proof does not use it, so the goal is stronger.
Theorem 1 is stated as existence, without its running-time clause.
Algorithm 1's printed line 2 initializes $M^0$ , while the loop reads $M^1$ . Its line 8 is a union over all stages inside the loop. Both are read as the intended algorithm, consistent with Algorithm 3 and with the proof of Theorem 2.
Histories are indexed from $0$ .

Not included are Proposition 1, the §3.2 polynomial-time variant, the SD-EF remark after Theorem 2, and §§4–7 (Theorem 3, the group-fairness results, the MNW characterization, bads). A proof of Theorem 1 in this rectangular form, with the floor and ceiling bounds, would be reusable well beyond this mission, for example in other fair-division and assignment results. So would a clean theory of the eating protocol. Contributions to either are welcome.

Selected references

R. Freeman, N. Shah, R. Vaish, Best of Both Worlds: Ex-Ante and Ex-Post Fairness in Resource Allocation, arXiv:2005.14122v1, 2020. https://arxiv.org/abs/2005.14122 (journal version with H. Aziz, Operations Research, 2024).
A. Bogomolnaia, H. Moulin, A New Solution to the Random Assignment Problem, Journal of Economic Theory 100(2), 2001. https://doi.org/10.1006/jeth.2000.2710
R. J. Lipton, E. Markakis, E. Mossel, A. Saberi, On Approximately Fair Allocations of Indivisible Goods, ACM EC 2004. https://doi.org/10.1145/988772.988792
E. Budish, The Combinatorial Assignment Problem: Approximate Competitive Equilibrium from Equal Incomes, Journal of Political Economy 119(6), 2011. https://doi.org/10.1086/664613
E. Budish, Y.-K. Che, F. Kojima, P. Milgrom, Designing Random Allocation Mechanisms: Theory and Applications, American Economic Review 103(2), 2013. https://doi.org/10.1257/aer.103.2.585

10 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Technical Note–A Simple Heuristic Policy for Stochastic Distribution Inventory Systems with Fixed Shipment Costs: An Upper Bound on the Long-Run Average Cost of Modified Echelon (r,Q) PoliciesResearch Paper

Motivation

A one-warehouse, multi-retailer (OWMR) distribution system is the basic model of a supply chain in which a central warehouse buys from an outside supplier and ships to several retail locations. When every shipment carries a fixed cost and a positive lead time, the optimal policy of the stochastic system is unknown, and the classical approach is to search over a structured class of policies and bound its cost. Exact evaluation of even a simple policy is hard, because the warehouse can run out of stock and then the retailers' replenishments interact.

Zhu, Chen, Hu and Yang (SSRN 2921743; Operations Research, 2021, doi:10.1287/opre.2021.2101) study modified echelon $(r,Q)$ policies for continuous-review OWMR systems with Poisson demand. Their central tool is an explicit upper bound on the long-run average cost of any such policy, written as the retailers' single-stage $(r,Q)$ costs, a warehouse term that depends on the retailer policies, and a fixed-cost allowance. Their heuristic policy, its worst-case performance guarantee and its asymptotic optimality (Theorems 2–4 of the paper) are all built on this bound. The single-stage cost functions follow Zheng (1992) and the echelon cost accounting follows Chen and Zheng (1994).

Setting

There are $N\ge1$ retailers, indexed $i=1,\dots,N$ , and one warehouse, indexed $0$ . Retailer $i$ faces Poisson demand of rate $\lambda_i>0$ , independent across retailers, so the warehouse sees Poisson demand of rate $\lambda_0=\sum_i\lambda_i$ . Installation $i$ has a constant lead time $L_i>0$ , a fixed cost $K_i>0$ per shipment, and an echelon holding cost rate $h_i>0$ ; unmet retailer demand is backlogged at rate $p_i>0$ . Write $\bar K=\max_iK_i$ .

A modified echelon $(r,Q)$ policy has reorder levels $r_i$ and order quantities $Q_i>0$ for every installation. When the echelon inventory position $IP_i$ of installation $i$ is at or below $r_i$ and the upstream installation has stock on hand, a shipment raises $IP_i$ as close as possible to $r_i+Q_i$ .

With $D_i\sim\mathrm{Poisson}(\lambda_iL_i)$ the lead-time demand of retailer $i$ , the single-stage holding-and-backlog rate and the single-stage $(r,Q)$ cost are

G_i(y)=\mathbb E\big[h_i(y-D_i)^++(h_0+p_i)(y-D_i)^-\big],\qquad C_i(r_i,Q_i)=\frac{\lambda_iK_i+\int_{r_i}^{r_i+Q_i}G_i(y)\,dy}{Q_i}.

With $G_i(w_i)=\sup_{r_i<z\le r_i+Q_i}G_i(z)$ , $M_j=\max\{G_j(w_j),C_j(r_j,Q_j)\}$ and $S_i=\sum_{j\ne i}(r_j+Q_j)$ , the envelope of Lemma 3 at warehouse echelon level $x$ is

\bar\Gamma_i(x)=\sum_{j\ne i}M_j+\begin{cases}M_i & x-S_i>r_i,\\ \max\{G_i(x-S_i),M_i\} & \text{otherwise},\end{cases}\qquad \bar\Gamma(x)=\max_i\bar\Gamma_i(x).

With $D_0\sim\mathrm{Poisson}(\lambda_0L_0)$ , set $\hat G=\bar\Gamma-\sum_iC_i$ , $\Lambda_0(y)=\mathbb E[h_0(y-D_0)+\hat G(y-D_0)]$ and

\hat C_0(r_0,Q_0)=\frac1{Q_0}\Big[\lambda_0K_0+\int_{r_0}^{r_0+Q_0}\Lambda_0(y)\,dy\Big].

The long-run average system cost is (1) of the paper,

C(r,Q)=\frac1{Q_0}\Big[\lambda_0K_0+\int_{r_0}^{r_0+Q_0}\mathbb E\big[h_0(y-D_0)+\Omega(y)\big]\,dy\Big],

where $\Omega(y)$ is the expected cost rate of all retailers when the warehouse inventory position is $y$ .

Formalization targets

Goal: Theorem 1 (p. 13)

C(r,Q)\le C^U(r,Q)\equiv\sum_{i=1}^NC_i(r_i,Q_i)+\hat C_0(r_0,Q_0)+\frac{\lambda_0\bar K}{Q_0}.

It is stated for every policy, with no assumption on the parameters beyond $Q_i,Q_0>0$ .

Milestones

App. A (3): the per-retailer bound: the charge of retailer $i$ is at most the own-retailer term of $\bar\Gamma_i(x)$ .
Lemma 3: the total retailer charge at a feasible state is at most $\bar\Gamma(x)$ .
App. A (8): $\hat\Gamma(x)\le\bar\Gamma(x)=\hat G(x)+\sum_iC_i$ .
App. A (9): $\Gamma_0(y)\le\Lambda_0(y)+\sum_iC_i$ .
App. A (10): $\frac1{Q_0}[\lambda_0K_0+\int_{r_0}^{r_0+Q_0}\Gamma_0]\le\hat C_0(r_0,Q_0)+\sum_iC_i$ .

Significance

The bound replaces the cost of an $(N+1)$ -installation stochastic system, which has no closed form, by computable retailer costs and a warehouse term. This is what makes the paper's heuristic policy computable and what its performance guarantees compare against: each retailer uses its single-stage optimal $(r_i^*,Q_i^*)$ , and the warehouse minimizes the remaining term. Bounds of this decomposition type are a standard device in multi-echelon inventory theory, and Lemma 3's envelope, which charges each retailer at the lowest inventory position the others can leave it, is the step specific to the distribution setting.

The result is proved in the paper's online appendix. It has not been formalized. A formal development adds to the platform a single-stage $(r,Q)$ cost with Poisson lead-time demand, the echelon envelope of Lemma 3 for general $N$ , and an explicit OWMR cost decomposition, all of which are reusable by later work on distribution systems, including the paper's own performance bounds.

Difficulty

The core is Lemma 3 for general $N$ . Bounding each retailer separately by its worst case $\max\{G_i(w_i),C_i\}$ fails, because a retailer below its reorder level can have a much larger cost rate $G_i(IP_i)$ ; the bound must use that the inventory positions are coupled through the warehouse echelon level. The printed proof is an induction on $N$ whose step needs convexity of a sum in which one term is only bounded by a convex function, so the order of bounding and convexity arguments matters. Convexity and continuity of $G_i$ (a Poisson mixture of piecewise-linear functions) must be established, and every expectation against the Poisson law needs an integrability argument, since the integrands grow linearly.

Formalization scope

All declarations live in the namespace DistribRQ.UpperBound. Retailers are indexed by Fin N with [NeZero N]; the warehouse data $L_0,K_0,h_0,r_0,Q_0$ are separate. The primitives are bundled in Primitives N (all rates and costs positive) and the policy in Policy N (real $r_i,r_0$ ; $Q_i,Q_0>0$ ), following the paper's continuous approximation (p. 7). Poisson expectations are Bochner integrals over $\mathbb N$ against poissonMeasure, evaluated at real arguments $y-n$ . $G_i(w_i)$ is the supremum of $G_i$ over $(r_i,r_i+Q_i]$ , since the paper's $\arg\max$ need not be attained on a half-open interval.

The sample-path model (cycles, shipment intervals, the paper's Lemmas 1–2) has no substrate, so the system is encoded as the paper's proof uses it:

$C(r,Q)$ is (1), with $\Omega$ any interval-integrable function satisfying the bound of p. 12, $\Omega(y)\le\lambda_0\bar K/Q_0+\mathbb E[\hat\Gamma(y-D_0)]$ ; this bound is where Lemmas 1–2 enter and is a hypothesis.
$\hat\Gamma(x)=\int\sum_ic_i(z_i)\,\kappa(x)(dz)$ for any Markov kernel $\kappa$ concentrated on the feasible states of p. A1 ( $z_j\le r_j+Q_j$ ; $\sum_jz_j\le x$ ; and $\sum_jz_j<x$ forces $z_i>r_i$ for all $i$ ), and any measurable, nonnegative admissible charges ( $c_i(z)\le\max\{G_i(z),C_i\}$ for $z>r_i$ , $c_i(z)\le G_i(z)$ for $z\le r_i$ ).
The theorem holds for every such $\kappa$ , $c$ and $\Omega$ , so the real system is an instance.

$\hat\Gamma$ is never a free function bounded by $\bar\Gamma$ , the feasible set keeps the clause for positive warehouse stock, and $G_i$ , $C_i$ , $\Lambda_0$ are computed from the Poisson law rather than taken as parameters; formalizations that relax any of these, or that rely on a junk value of sSup, an integral or a division, trivialize the statement and are not accepted.

Contributions welcome: convexity and continuity of $G_i$ , Poisson integrability lemmas, Lemma 3 for general $N$ , and the averaging steps of App. A (8)–(10).

Selected references

H. Zhu, Y. (F.) Chen, M. Hu, Y. Yang, Technical Note—A Simple Heuristic Policy for Stochastic Distribution Inventory Systems with Fixed Shipment Costs, Operations Research, 2021. SSRN copy of 2020-09-08: https://ssrn.com/abstract=2921743; doi:10.1287/opre.2021.2101.
Y.-S. Zheng, On properties of stochastic inventory systems, Management Science 38(1), 1992. https://doi.org/10.1287/mnsc.38.1.87
F. Chen, Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1994. https://doi.org/10.1287/mnsc.40.11.1426

7 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Optimal Sequential Multi-class Diagnosis: Under Exponential Tilting, Every Reachable Posterior Belief Is a Closed-Form Function of an r-Dimensional Diagnostic Statistic, r = rank(B)Research Paper

Motivation

In sequential multi-class diagnosis, a decision maker observes a system repeatedly, then chooses when to stop and which hidden class to report. Each new observation can improve the diagnosis, but waiting has a cost. A direct dynamic program uses the vector of posterior class probabilities as its state. With $N+1$ possible classes, that state lies in an $N$ -dimensional probability simplex. Wang's model asks when the observed sequence can instead be summarized by fewer coordinates, so that the same posterior can be recovered without retaining a full belief vector as an independent state Wang, §2–§3.

The paper considers class distributions related by exponential tilting. This relationship appears in common one-dimensional distribution families, including the normal, binomial, Poisson, and gamma examples collected in its Table 1 Wang, p. 8. The result targeted here is the belief reconstruction identity of Theorem 1. Later parts of the paper use the reduced statistic in optimality equations and study stopping regions; those results are outside this mission Wang, pp. 12–18.

Setting

The hidden class is $j\in\{0,\ldots,N\}$ . Before observing data, the decision maker has a prior belief $\theta=(\theta_0,\ldots,\theta_N)$ : every component is nonnegative and their sum is one. Conditional on class $j$ , observations $y_1,\ldots,y_t$ are independent and have the same density $f_j$ on the observation space $\mathcal Y$ . Class $0$ supplies a baseline density $f_0$ . The one-step Bayesian operator $\mathcal B$ multiplies each current class weight by that class's likelihood at the new observation and divides by the sum of all weighted likelihoods. Starting at $\Pi_0=\theta$ , the belief $\Pi_t$ is obtained by applying $\mathcal B$ once for each observation in arrival order Wang, pp. 6–7.

In the exponential tilting model, a transformed observation $h(y)\in\mathbb R^p$ and a parameter $\beta_j\in\mathbb R^p$ describe each nonbaseline density:

f_j(y)=f_0(y)\exp\{\beta_{j0}+\beta_j^{\mathsf T}h(y)\},\qquad \beta_{j0}=-\log\int_{\mathcal Y}\exp\{\beta_j^{\mathsf T}h(y)\}f_0(y)\,dy.

Here $j=1,\ldots,N$ . Place the $\beta_j^{\mathsf T}$ in the rows of the diagnostic parameter matrix $\mathbb B$ . Its rank decomposition is $\mathbb B=\mathbb R\mathbb P$ , where $\mathbb R$ has $N$ rows and $r$ linearly independent columns, while $\mathbb P$ has $r$ linearly independent rows and $p$ columns. Thus $r=\operatorname{rank}(\mathbb B)$ . The paper calls $\mathbb R$ the reconstruction matrix and $\mathbb P$ the projection matrix Wang, Definition 1, p. 8.

Formalization targets

Theorem 1: posterior reconstruction

For $t\ge1$ , define the diagnostic statistic $x_t=\mathbb P\big(\sum_{m=1}^t h(y_m)\big)/t\in\mathbb R^r$ . For classes $j=1,\ldots,N$ , the target identity is

\Pi_t(y_1,\ldots,y_t,\theta)_j =\mathcal T_j^t(x_t,\theta) =\frac{\theta_j\exp\{t(\beta_{j0}+e_j\mathbb R x_t)\}} {\theta_0+\sum_{i=1}^{N}\theta_i\exp\{t(\beta_{i0}+e_i\mathbb R x_t)\}}.

The baseline coordinate is $\mathcal T_0^t=1-\sum_{j=1}^{N}\mathcal T_j^t$ . The normalizer appearing in $\mathcal T^t$ is evaluated from the row $e_i\mathbb R\mathbb P$ , as in equation (3), and the theorem identifies it with the model normalizer through $\mathbb B=\mathbb R\mathbb P$ . The target also identifies the set of posteriors reachable after exactly $t$ observations with $\mathcal T^t(\Omega_t,\theta)$ , where $\Omega_t$ is the set of attainable diagnostic statistics. These statements give a precise reading of the paper's claim that reachable beliefs admit an $r$ -coordinate representation Wang, Theorem 1, p. 9; Definition 2, p. 10.

The goal additionally states that the map $x\mapsto\mathcal T^t(x,\theta)$ is injective on $\mathbb R^r$ when every prior component is positive. This is an explicit, qualified reading of the paper's phrase that the dimensionality is equal to $r$ . For discrete observations, the reachable set $\Omega_t$ can be finite, so the phrase cannot always mean its geometric dimension is literally $r$ . The five milestones follow the source's Bayes operator and the displayed identities in its proof of Theorem 1 Wang, p. ec1.

Significance

The formula determines every posterior component from $r$ real coordinates, the prior, and the observation count. When $r$ is smaller than $N$ , this supplies the representation used by the paper to reformulate a diagnosis problem in a smaller state space. The paper's examples show cases with one or two diagnostic coordinates; Proposition 1 then rewrites its optimality equations using those coordinates Wang, pp. 9–12. This mission formalizes the reconstruction claim itself, including the exact reachable-set statement, while leaving the decision costs and Bellman equations for later work.

A completed development would provide reusable definitions for a finite-class Bayes update and its sequential iterate, an exponential-tilting model over densities, and a rank-factorized reconstruction map. The result is proved in the cited paper. The Lean declarations in this proposal compile as statements, but their sorry bodies are open proof obligations; this mission seeks machine-checked proofs of them.

Difficulty

The main verification burden is connecting several expressions for the same posterior without quietly replacing one definition by another. A sequential posterior is an iterated one-step update; the paper's closed form is a normalized product of likelihoods; and equation (3) is an exponential expression in a projected sum of transformed observations. Each form has its own denominator, so the positivity conditions that make division meaningful must be stated. The rank claim also requires full-rank assumptions on both factors of $\mathbb B$ . For a prior with zero mass on a class, the posterior formula remains meaningful, but the injectivity assertion needs a separate full-support condition.

Formalization scope

Lean represents classes by Fin (N + 1), with class zero as the baseline. Row i : Fin N of the diagnostic matrix is class i.succ. Observations form a List in arrival order; $t$ is its length, and the posterior is the list fold of $\mathcal B$ . The observation space is a measurable type with a reference measure $\mu$ , covering continuous and discrete densities with one notation. This generalizes the paper's $\mathcal Y\subseteq\mathbb R$ ; no order or arithmetic operation on observations is used by Theorem 1. Integrals are real-valued, and $N=0$ and $p=0$ are permitted. The reconstruction identity is stated for $t\ge1$ , matching the paper and avoiding the division by zero in $x_t$ .

The standing assumptions say that every $f_j$ is measurable, $f_0$ is positive at every admitted observation, its integral is one, and each tilted baseline density is integrable. These make the normalizers and the Bayesian denominators meaningful. Positivity, normalization, and integrability are explicit refinements of the paper's use of densities and normalizing constants. The prior lies in the standard simplex; $\theta_0$ need not be positive for reconstruction. The additional full-support condition appears only in the injectivity clause. The paper's conditional independence assumption is represented by multiplying class likelihoods along the list.

The generic Bayesian update and its reachable set are separate from the paper-specific model. In particular, the posterior is an actual fold of the one-step update, and the class densities are given data constrained by exponential tilting. Defining the posterior directly as equation (3), or defining the densities to make the tilting identity true by construction, would erase the result being formalized. A complete proof needs finite-sum identities, exponential and logarithm facts, integrability facts, matrix rank and row identities, and the algebra of probability normalization. The generic Bayes definitions and list-level likelihood identity are reusable beyond this paper; contributions that establish those interfaces or close any source-derived milestone are welcome.

Selected references

J. Wang, Optimal Sequential Multi-class Diagnosis, Operations Research 70(5), 2022; arXiv:1506.08915v4. The mission cites the v4 preprint's pages and indices.

8 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Fluid Limits for Multiclass Many-Server Queues with General Reneging Distributions and Head-of-the-Line Scheduling: Fluid-Scaled States Are Tight and Their Limit Points Are Fluid Model SolutionsResearch Paper

Motivation

Call centers, hospital wards and other service systems with many agents serve several customer classes, and customers who wait too long hang up or leave. The standard model is the multiclass many-server queue with reneging: $N$ identical servers, $J$ classes, class-dependent service-time and patience-time distributions, and a control policy that decides when an idle server takes a customer and from which class. Exact analysis is out of reach once service and patience times are not exponential, so performance is studied through fluid limits: the limit of the system scaled by $1/N$ as $N\to\infty$ .

A. L. Puha and A. R. Ward (MOR 2022, doi:10.1287/moor.2021.1166) prove such a limit theorem for general service and patience distributions, batch arrivals and an arbitrary admissible head-of-the-line policy, including policies that idle or randomize. Earlier results covered one class without reneging (Kaspi and Ramanan, Ann. Appl. Probab. 2011), one class with reneging and unit arrivals (Kang and Ramanan, Ann. Appl. Probab. 2010), and static priority policies (Atar, Kaspi and Shimkin, Math. Oper. Res. 2014).

Setting

Fix $J\ge1$ classes. Class $j$ has a service-time distribution $G^s_j$ on $\mathbb R_+$ with density $g^s_j$ , and a patience-time distribution $G^r_j$ on $[0,\infty]$ with density $g^r_j$ on $\mathbb R_+$ , so a customer may never abandon. For a distribution $G$ with density $g$ , $H=\sup\{x:G(x)<1\}$ is the right edge of its support and $h=g/(1-G)$ on $[0,H)$ is its hazard function.

In the $N$ -th queue, class- $j$ customers arrive by a counting process $E^N_j$ that may jump by more than one. The state is $(\alpha^N,X^N,\nu^N,\eta^N)$ : $X^N_j$ counts class- $j$ customers in system; $\nu^N_j$ is the age-in-service measure, a unit atom at the service age of each class- $j$ customer in service; and $\eta^N_j$ is the potential-queue measure, a unit atom at the time in system of each class- $j$ customer whose patience has not run out. The control enters only through the entry-into-service times. A head-of-the-line (HL) policy serves each class in order of arrival. It is admissible when the entry-into-service process $K^N$ is adapted to the filtration generated by the state history and the policy's own independent uniform random variables.

The fluid model works on the state space $\mathbb X=\mathbb R^J_+\times\prod_j\mathbf M[0,H^s_j)\times\prod_j\mathbf M[0,H^r_j)$ of finite measures with the weak topology. Given an arrival function $E$ (nondecreasing, rcll, $E(0)=0$ ), a path $(X,\nu,\eta)$ defines the auxiliary functions $B_j=\langle1,\nu_j\rangle$ , $Q_j=X_j-B_j$ , $D_j(t)=\int_0^t\langle h^s_j,\nu_j(u)\rangle du$ , $K_j=B_j+D_j-B_j(0)$ , $I=1-\sum_jB_j$ , and the reneging function

R_j(t)=\int_0^t\int_0^{Q_j(u)}h^r_j\big((F_{j,u})^{-1}(y)\big)\,dy\,du,\qquad F_{j,u}(x)=\langle1_{[0,x]},\eta_j(u)\rangle .

A fluid model solution for $E$ satisfies the constraints (35)–(37), the monotonicity of $K$ , the balance law $X_j=X_j(0)+E_j-R_j-D_j$ , and the transport equations (46)–(47) for $\nu_j$ and $\eta_j$ driven by $dK_j$ and $dE_j$ .

Formalization targets

Goal: Theorem 1 (p. 17)

Under Assumptions 4 and 5, for every sequence of admissible HL policies:

\{(\bar X^N,\bar\nu^N,\bar\eta^N)\}_{N}\ \text{is tight in }\mathbf D(\mathbb X),

and every distributional limit point $(X,\nu,\eta)$ is, almost surely, a continuous fluid model solution for $E$ started from $(X^0,\nu^0,\eta^0)$ , with continuous auxiliary functions and each $\eta_j(t)$ charging no points. Assumptions 1–3 ask that the scaled arrivals and initial states converge. Assumption 4 asks that the hazards be bounded or lower semicontinuous near the right edges $H^s_j,H^r_j$ . Assumption 5 adds continuity of $E$ , an atomless $\eta^0$ , and control of $\bar K^N$ by C-tightness or by inequality (55).

Milestones

Lemma 1, (24) and (26): the prelimit dynamic equations for $\langle f,\nu^N_j\rangle$ and $\langle\varsigma,\eta^N_j\rangle$ .
Lemma 6, (61): $\langle1_{[0,x]}h^r_j,\eta^N_j(t)\rangle=\int_0^{F^N_{j,t}(x)}h^r_j((F^N_{j,t})^{-1}(y))\,dy$ .
Lemma 7: the compensator bounds $|\mathcal A^N_{s,j}(\varphi,t)|\le\|\varphi\|_\infty(X^N_j(0)+E^N_j(t))\int_0^mh^s_j$ and the reneging analogue.
Lemma 8: relative compactness in $\mathbf D(\mathbb R_+)$ of the fluid-scaled real processes, and their C-tightness under Assumption 5.
Lemma 2 (i) and (iii): continuity and the absence of atoms propagate along fluid model solutions.

Significance

Theorem 1 characterizes fluid limits for every admissible HL policy at once. To get the fluid limit of a specific policy, one adds the equations that policy imposes and proves uniqueness for the resulting system; the paper does this for weighted random buffer selection (its Theorems 3–5). The reneging equation (40) is the main new feature: abandonment depends on the whole distribution of waiting times in queue, not only on the queue length. Allowing batch arrivals means the reneging count can only be sandwiched between two compensators, which is why Lemma 6 is needed.

The results are proved in the paper, with parts of the tightness argument delegated to Kang–Ramanan and Kaspi–Ramanan. None of them is formalized. The mission defines from scratch a measure-valued queue with abandonment, the Skorokhod space $\mathbf D(\mathbb X)$ with $J_1$ convergence, and the fluid model of §3. These definitions are reusable for the single-class models of Kaspi–Ramanan and Kang–Ramanan, for the WRBS and static-priority policies, and for other measure-valued fluid limits.

Difficulty

Each milestone is a known argument, but the obvious route to the goal breaks at the reneging term. A naive limit passage in the prelimit reneging count $R^N_j$ fails: with batch arrivals, $R^N_j$ is not a functional of $\eta^N_j$ and $Q^N_j$ alone, because customers with equal waiting times may be split between queue and service. Identifying the limit as the nonlinear function (40) requires bounds from above and below by marked point processes. It also requires showing that the compensators of these processes converge to a common limit, which uses that $\eta$ charges no points along the limit. The tightness part needs Kurtz–Jakubowski criteria for measure-valued processes on spaces $[0,H)$ whose right end may carry escaping mass. Lemma 6 is a pathwise identity for finite counting measures, and Lemma 7 is a pathwise bound.

Formalization scope

Classes are Fin J with $J\ge1$ . Time is ℝ≥0. Customers are indexed by integers as in the paper. Event times are extended reals: a patience of $\infty$ keeps a customer in the potential queue forever, and an entry time of $\infty$ means the customer is never served. $\mathbf M[0,H)$ is FiniteMeasure on the subtype $[0,H)$ of ℝ≥0. $J_1$ convergence uses one time change for all coordinates, with the maximum of the sup-norm and Lévy–Prokhorov distances on $\mathbb X$ . Convergence in distribution, distributional limit points, relative compactness and C-tightness are stated in coupling form; on the Polish space $\mathbf D(\mathbb X)$ these are equivalent to the usual notions. Hazards take values in $[0,\infty]$ and are $0$ off $[0,H)$ . The integrals in (37), (40), (41), Lemma 6 and Lemma 7 are integrals of nonnegative functions. The derivative indicators that define the departure, reneging and marked processes are written as explicit counts.

Four readings are disclosed in the items. The goal's initial condition is stated through a coupling carrying $(E,X^0,\nu^0,\eta^0)$ jointly, because the limit point lives on its own probability space. $G^s,G^r$ in (46)–(47) are read as $G^s_j,G^r_j$ . In Lemma 8, the (K.2) branch of Assumption 2 is read as relative compactness of $\bar K^N_j$ , because the printed (K.2) does not imply it. The goal encodes Assumption 2 as printed. The head-of-the-line order is the HL condition stated in words on pp. 8–9 rather than inequality (10) alone, which would let a policy skip a waiting customer for good and serve younger ones.

The statement admits trivializing formalizations, and they are excluded here. The HL predicate contains only the defining constraints of Definitions 1–3: entry no earlier than arrival and before abandonment (9), the head-of-the-line order (the HL condition of pp. 8–9, which contains (10): a customer can enter service only after every earlier customer of its class has entered or abandoned), the state constraints (S.1), (S.2), (15) and (16), and rcll paths. The identities (18)–(26) are not in it. All standing independence and distributional hypotheses and the adaptedness of $K^N$ are explicit. The auxiliary functions $R,D,B,Q,K,I$ are computed from the path, never chosen. The policy is not specialized: idling and randomization are allowed.

Not posed: Lemmas 3–5, 9 and 10, Theorem 2, and Lemma 2 (ii) and (iv). Lemma 4 needs a server-assignment filtration, Lemma 5 needs predictable quadratic variations, and Theorem 2, Lemma 9 and Lemma 10 need measure-valued marked point processes on $[0,H)\times\mathbb R_+$ . Formalizing these, or a sorry-free construction of an admissible system satisfying Assumptions 1–5, is welcome.

Selected references

A. L. Puha, A. R. Ward, Fluid limits for multiclass many-server queues with general reneging distributions and head-of-the-line scheduling, Mathematics of Operations Research, Articles in Advance, 2021 (2022). https://doi.org/10.1287/moor.2021.1166
H. Kaspi, K. Ramanan, Law of large numbers limits for many-server queues, Annals of Applied Probability 21 (2011) 33–114. https://doi.org/10.1214/10-AAP681
W. Kang, K. Ramanan, Fluid limits of many-server queues with reneging, Annals of Applied Probability 20 (2010) 2204–2260. https://doi.org/10.1214/10-AAP683
R. Atar, H. Kaspi, N. Shimkin, Fluid limits for many-server systems with reneging under a priority policy, Mathematics of Operations Research 39 (2014) 672–696. https://doi.org/10.1287/moor.2013.0632
S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

10 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Exploiting Random Lead Times for Significant Inventory Cost Savings: With Exponential Lead Times, the Generalized Base-Stock Policy's Scaled Stationary Inventory Level Converges to N(0, 1/(βγ))Research Paper

Motivation

In continuous-review inventory systems with backlogging, the classical constant base-stock (CBS) policy orders one unit whenever one unit of demand arrives, so that the inventory position (net inventory plus in-transit inventory) stays constant. Under CBS with Poisson demand of rate $r$ and i.i.d. lead times with mean $1/\beta$ , the in-transit inventory has a Poisson law with mean $r/\beta$ , and the steady-state net inventory level $Y^r(\infty)$ fluctuates on the scale $\sqrt r$ : $\mathbb E|Y^r(\infty)|/\sqrt r \to 2(2\pi\beta)^{-1/2}$ . Average holding and backlog costs therefore grow like $\sqrt r$ .

Stolyar and Wang (arXiv:1801.02646, Operations Research 2022) observe that when lead times are random and orders may cross, an inventory manager can exploit the randomness: by ordering more aggressively when the inventory level is low and less when it is high, the variance of the inventory level can be reduced. Their generalized base-stock (GBS) policy implements this with a single gain parameter $\gamma$ . The main theoretical result, Theorem 1, identifies the diffusion-scale steady-state law of the inventory level under GBS when lead times are exponential: it is normal with variance $1/(\beta\gamma)$ , a factor $\gamma$ below the CBS variance. With $\gamma = \gamma(r) \to \infty$ (Corollary 2), the scaled average cost $\mathbb E|Y^r(\infty)|/\sqrt r$ tends to $0$ , so GBS becomes infinitely better than CBS in the limit.

Setting

Demand units (customers) arrive as a Poisson process of rate $r$ . Supply units (items) are ordered by the policy and each arrives after an independent exponential lead time with mean $1/\beta$ . Let $Y$ be the net inventory level (positive or negative, backlog allowed) and $Z \ge 0$ the number of items in transit. Write $a\vee b=\max(a,b)$ , $a\wedge b=\min(a,b)$ , $a^+=a\vee 0$ , $a^-=(-a)^+$ .

The GBS policy has an integer gain $\gamma\ge 1$ , a truncation level $f>0$ and a centering $x_*$ . With $X_* = r/\beta$ it uses the target and the truncated target

X = X_* - \gamma(Y - x_*), \qquad T = [X\wedge(X_*+f)]\vee 0 .

At every arrival: a customer sets $Y := Y-1$ ; an item sets $Y := Y+1$ , $Z := Z-1$ . Then $T$ is recomputed and $A = \lceil T - Z\rceil\vee 0$ items are ordered, $Z := Z + A$ . Under exponential lead times $(Y,Z)$ is a continuous-time Markov chain on $\mathbb Z\times\mathbb Z_+$ with customer rate $r$ and item rate $\beta Z$ .

The systems are indexed by $r\to\infty$ , with $f = f(r)$ satisfying

f(r)/r\to 0, \qquad f(r)/\sqrt r\to\infty,

and $x_* = x_*(r)$ arbitrary. A stationary distribution $p$ of a countable chain with rates $q(s,s')$ and exit rates $q(s)$ is a probability mass function with finite mean exit rate satisfying global balance $\sum_s p(s)q(s,s') = p(s')q(s')$ .

Formalization targets

Goal: Theorem 1

For every $r>0$ some state is reachable from every state, for all large $r$ the chain has a unique stationary distribution, and for every choice of stationary distributions

\frac{Y^r(\infty)-x_*}{\sqrt r}\Rightarrow\mathcal N\big(0,(\beta\gamma)^{-1}\big),\qquad \mathbb E\Big[\frac{Y^r(\infty)-x_*}{\sqrt r}\Big]^{\pm}\to(2\pi\beta\gamma)^{-1/2}.

Milestones

In proof order: the stability part of Theorem 1; the conservation law $\beta\mathbb E Z^r(\infty)=r$ (14); the mean bound for the reflected random walk $Q_n$ that dominates the order gap (p. 16, EC.3); Lemma 4, $\mathbb E D^r(\infty)\le\mathbb E\tilde D^r(\infty)\le C$ ; the conservation law (19) and Lemma 5 for the artificial process, a birth–death chain $\hat Y^r$ that keeps $\hat Z = \lceil\hat T\rceil$ exactly; Corollary 6; the stochastic comparison Lemma 8, $\hat Y^r(\infty)\le_{st}Y^r(\infty)$ and $\hat T^r(\infty)\ge_{st}T^r(\infty)$ ; the target-gap bound (31); the transfer Lemma 9; and the reduction (36), $\mathbb E Y^r(\infty)/\sqrt r - \mathbb E\hat Y^r(\infty)/\sqrt r\to 0$ . For §4 milestones the centering is $x_*\equiv 0$ , as in the paper (p. 12).

Significance

The result. Theorem 1 quantifies the value of random lead times: the GBS policy divides the asymptotic variance of the steady-state inventory level by $\gamma$ , and the half-normal limits of $\mathbb E[\cdot]^\pm$ give the asymptotic holding and backlog costs, which is what makes the cost comparison with CBS (bounds (12)–(13) and Corollary 2) possible. The artificial-process comparison and Lemma 9 form a reusable template for transferring a diffusion limit from a tractable one-dimensional chain to a higher-dimensional controlled chain.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission formalizes the GBS chain itself as explicit transition rates, so the theorem cannot be discharged by a model that only resembles the policy. The stability part is only sketched in the paper ("We omit further details of the stability proof", p. 13), so a complete formal proof also fills that gap. Lemma 5 is a stationary Halfin–Whitt-type limit for a birth–death chain with state-dependent up-rates, including uniform integrability of the scaled tails.

Difficulty

The two-dimensional chain has no product form, and its in-transit inventory does not track the target: after an item arrival $Y$ rises by one while the target $X$ falls by $\gamma$ , but only one item leaves transit, so $Z$ overshoots its target and the gap $D = Z - \lceil T\rceil$ is random. The natural argument, "the chain behaves like the birth–death chain with $Z = \lceil T\rceil$ ", fails on two counts: the steady-state gap must be bounded uniformly in $r$ (Lemma 4), although the rates of the chain grow with $r$ and $Z$ is unbounded on the state space, and the truncations of $T$ at $0$ and at $X_*+f$ produce error terms that must vanish after $1/\sqrt r$ scaling (Corollary 6). Stochastic order alone gives only an inequality between the two laws; closing it needs the mean identity (36), which rests on the exact conservation laws (14) and (19).

Formalization scope

All objects live in the namespace RandomLeadGBS.Diffusion. The state is $(Y,Z)\in\mathbb Z\times\mathbb N$ ; the demand rate $r$ is real and $r\to\infty$ along atTop. The parameters are $\beta>0$ , $\gamma\in\mathbb N$ with $\gamma\ge 1$ , $f:\mathbb R\to\mathbb R$ with $f>0$ and (10), and arbitrary $x_*:\mathbb R\to\mathbb R$ . The policy is encoded literally: target (4), truncated target (5), order step $Z + \mathrm{toNat}\lceil T - Z\rceil$ applied after every arrival; the item rate is $\beta Z$ and the cap is $X_*+f$ (not $X_*+\gamma x_*+f$ ).

Conventions committed to:

a stationary distribution is a probability solution of global balance with finite mean exit rate (the state space is unbounded in $Z$ );
expectations and probabilities are series over states, and every expectation bound also asserts the summability it needs;
weak convergence $\Rightarrow$ is stated by its definition, through every bounded continuous test function, against Mathlib's gaussianReal 0 (1/(βγ));
the paper's "irreducible" is replaced by "some state is reachable from every state", because states with $Z<\lceil T(Y)\rceil$ are never entered;
"uniformly in $r$ " and " $\sup_r$ " (Lemma 4, Corollary 6, (31)) are stated for all $r\ge r_0$ .

The goal concerns the two-dimensional GBS chain; stating it for the artificial chain, or only for an empty family of stationary laws, would trivialize it. The uniqueness clause and the existence clause of Lemma 5 rule out the vacuous reading.

A complete development needs a theory of stationary laws of countable continuous-time chains (existence via drift/Foster criteria, embedded-chain time change), birth–death stationary laws and their local normal asymptotics, and stochastic comparison of chains by coupling. The countable-chain stationarity layer and Lemma 9 are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome. Propositions 3 and 7 (generic comparison results used for Lemma 4 and Lemma 8) are not posed as milestones.

Selected references

A. L. Stolyar and Q. Wang, Exploiting random lead times for significant inventory cost savings, Operations Research, 2022; preprint arXiv:1801.02646v6, 2021. https://arxiv.org/abs/1801.02646
S. M. Disney, A. Maltz, X. Wang and R. D. H. Warburton, Inventory management for stochastic lead times with order crossovers, European Journal of Operational Research 248(2), 473–486, 2016. https://doi.org/10.1016/j.ejor.2015.07.047
S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 567–588, 1981. https://doi.org/10.1287/opre.29.3.567
T. Lindvall, Lectures on the Coupling Method, Dover, 1992.
S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, Springer, 1993. https://doi.org/10.1007/978-1-4471-3267-7

17 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Implications of Price Matching in Supply Chain Negotiation: Under Symmetric Bargaining Power the Seller Prefers Price Matching to Simultaneous Negotiation and Both Buyers Prefer the ReverseResearch Paper

Motivation

A seller that supplies several competing buyers may negotiate a wholesale price with each of them independently and simultaneously (simultaneous negotiation, SN), or may commit to charge all of them the same price (price-matching negotiation, PM). PM is the bargaining counterpart of the most-favoured-customer clause, a contractual guarantee that a customer receives the best price the vendor gives anyone. Retailers such as Walmart and Costco demand such clauses from common suppliers, and buyers command them expecting to obtain the same price as their rivals (Shang and Cai, §1). Shang and Cai (MSOM, 2021; SSRN 3021563) ask who benefits from PM relative to SN when wholesale prices are the outcome of Nash bargaining between the seller and each buyer, and show that with symmetric buyers PM benefits the seller and hurts both buyers.

The model builds on the bilateral-bargaining framework of Horn and Wolinsky (1988), in which a common supplier negotiates simultaneously with competing downstream firms, and on the analysis of negotiated wholesale contracts by O'Brien and Shaffer (2005, RAND Journal of Economics 36, 573–595) and Dukes, Gal-Or and Srinivasan (2006).

Setting

A seller supplies an intermediate good to Buyer 1 and Buyer 2, who each turn one unit of it into one unit of a substitutable end product. With demand base $a > 0$ and substitutability $\gamma \in [0,1)$ , retail prices and quantities satisfy the reverse demand system $p_i = a - x_i - \gamma x_j$ , $j = 3 - i$ .

The game has two stages.

Retail stage. Given wholesale prices $(w_i, w_j)$ , the buyers set retail prices in a differentiated Bertrand game. Buyer $i$ earns $\pi_i = (p_i - w_i)x_i$ and the seller earns $\pi_s = w_i x_i + w_j x_j$ . Writing $\hat p_i(w_i,w_j)$ and $\hat x_i(w_i,w_j)$ for the equilibrium prices and quantities, the second-stage profits are $\pi_i(w_i,w_j)$ and $\pi_s(w_i,w_j)$ .
Negotiation stage. Wholesale prices are set by generalized Nash bargaining: Buyer $i$ has bargaining power $\theta_i \in (0,1)$ against the seller, who has $1-\theta_i$ . A bargain over a price $w \ge 0$ with buyer payoff $U(w)$ , seller payoff $V(w)$ and disagreement point $(0, d)$ selects the individually rational $w$ maximizing $U(w)^{\theta_i}(V(w) - d)^{1-\theta_i}$ .

If a negotiation fails, the seller can sell to the other buyer alone. Then Buyer $j$ faces demand $a - p_j$ , and the seller earns the monopoly profit $\pi^M_s(w_j)$ .

The two mechanisms are:

Simultaneous negotiation (SN). The seller bargains with both buyers at once. A pair $(w^{SN}_1, w^{SN}_2)$ is an equilibrium if each $w^{SN}_i$ solves dyad $i$ 's bargain with payoffs $\pi_i(\cdot, w^{SN}_j)$ , $\pi_s(\cdot, w^{SN}_j)$ and disagreement point $(0, \pi^M_s(w^{SN}_j))$ .
Price matching (PM). The seller bargains with one buyer first; the other buyer accepts the same price. If the first bargain fails, the seller bargains with the other buyer alone, reaching $\hat w_j$ . The PM price $w^{PM}$ solves the bargain with payoffs $\pi_i(w,w)$ , $\pi_s(w,w)$ and disagreement point $(0, \pi^M_s(\hat w_j))$ .

The Lean development uses this notation: pHat, xHat, piB ( $\pi_i$ ), piS ( $\pi_s$ ), piMb, piMs, IsNashBargain, IsSNEq, IsPMPrice.

Formalization targets

Goal: Theorem 1 (p. 10)

With symmetric power $\theta_1 = \theta_2 = \theta \in (0,1)$ , an SN equilibrium and a PM equilibrium price exist, and for every SN equilibrium $(w_1, w_2)$ and every PM price $w$

\pi_s(w_1,w_2) < \pi_s(w,w), \qquad \pi_1(w,w) < \pi_1(w_1,w_2), \qquad \pi_2(w,w) < \pi_2(w_2,w_1).

The goal is stated about the equilibrium predicates, not about the closed-form prices, so that it asserts the comparison of the two mechanisms as the paper defines them.

Milestones

The retail equilibrium $\hat p_i$ , $\hat x_i$ and the profit formulas (1)–(2), §3.1.1.
The single-channel monopoly price and profits, §3.1.2.
The single-channel bargain $\hat w_j = (1-\theta_j)a/2$ , with $\pi^M_s(\hat w_j) = (1-\theta_j^2)a^2/8$ , §3.2.2.
The SN equilibrium is unique and equals $w^{SN} = \dfrac{(1-\theta)(1-\gamma)(2+\gamma)a}{2(1-\gamma)(2+\gamma) + \gamma^2(1+\gamma)(2-\gamma)\theta}$ , §3.2.1.
The PM equilibrium price is unique and equals $w^{PM}_i = \tfrac a4\bigl(3 - \theta_i - \sqrt{1 - \gamma\theta_i + \gamma^2\theta_i + \theta_i^2 + (1+\gamma)(2-\gamma)\theta_i\theta_j^2}\bigr)$ , §3.2.2, for general $\theta_i, \theta_j$ .
$0 < w^{SN} < w^{PM} \le a/2$ under symmetric power, §3.2.2.
At a common price, $\pi_s(w,w)$ increases on $[0, a/2]$ and $\pi_i(w,w)$ decreases on $[0,a]$ (proof of Theorem 1, Online Supplement p. 1).

Significance

Theorem 1 separates the effect of the negotiation mechanism from any asymmetry between buyers: under symmetric power the buyers are interchangeable, SN gives them the same price, and still the mechanism alone moves surplus from the buyers to the seller. The paper's explanation is that price matching lowers a buyer's incentive to negotiate the price down, so the matched wholesale price is higher (p. 10). The paper builds its asymmetric-power, side-payment and spot-market results (§§4–6) on this comparison.

The result is proved in the paper; nothing here is open. Neither the result nor its ingredients have been formalized. The mission produces a machine-checked account of a two-stage bargaining-over-competition model: the Bertrand stage, the Nash-bargaining stage with endogenous disagreement points, and the closed-form equilibria. Two steps the paper only asserts become formal obligations: uniqueness of the SN equilibrium, and the claim that the closed-form PM price is the global maximizer of the Nash product.

Difficulty

The comparison step is short once the closed forms are known: by milestones 6 and 7 the PM price is higher, the seller's diagonal profit increases, and the buyers' decreases. The work is in the equilibrium characterizations.

In SN each dyad's disagreement payoff $\pi^M_s(w_j)$ depends on the other dyad's outcome, so an equilibrium is a fixed point of two coupled Nash-product maximizations. The paper asserts uniqueness. The best-response map is not a contraction for $\gamma$ near $1$ , so a contraction argument does not give uniqueness directly.
The Nash products involve real powers with exponents $\theta$ and $1-\theta$ . Showing that the first-order condition picks out the global maximizer over the individually rational set requires a concavity or single-peakedness argument, not just a derivative computation.
The PM closed form contains a square root. Comparing it with the rational function $w^{SN}$ is an inequality in three parameters $(\gamma, \theta, a)$ .

Formalization scope

All quantities are real numbers. The standing assumptions are $a > 0$ , $\gamma \in [0,1)$ and every bargaining power in $(0,1)$ . The sign $a > 0$ is added; the paper never states it.

Bargaining. A Nash bargaining solution maximizes $U^{\theta}(V-d)^{1-\theta}$ over the individually rational prices $\{w \ge 0 : U(w) \ge 0,\ V(w) \ge d\}$ . Lean's Real.rpow is the real power only on non-negative bases, and the individually rational set guarantees non-negative bases.
Feasible domain. Equilibrium wholesale prices are required to lie in $[0,a]$ , the paper's "entire feasible domain" (p. 9; Online Supplement p. 1); bargaining deviations range over all individually rational $w \ge 0$ .
Second-stage profits. $\pi_i$ and $\pi_s$ are defined from the demand system at $(\hat p_i,\hat p_j)$ , not by the closed forms (1)–(2), so milestone 1 is a genuine identity.
PM outcome. In PM the matched price applies to both buyers, and the seller negotiates first with Buyer 1. With symmetric power the choice of first buyer is immaterial.
Preference. "Prefers" is strict; $\theta \in (0,1)$ excludes the paper's equality cases.

Substituting the closed-form prices $w^{SN}$ , $w^{PM}$ into the profit comparison would turn Theorem 1 into the algebra of milestones 6–7. The goal is therefore stated for every equilibrium of each mechanism, together with existence of both equilibria, so neither the closed forms nor a vacuous equilibrium set can discharge it.

A complete development needs:

concavity of the Nash product along the individually rational interval (reusable for other one-dimensional Nash-bargaining models);
the Bertrand equilibrium of a linear differentiated duopoly;
real-analysis inequalities involving square roots.

Contributions to any milestone, or to reusable lemmas on maximizing $u^{\theta} v^{1-\theta}$ over an interval, are welcome.

Selected references

W. Shang and G. Cai, Implications of Price Matching in Supply Chain Negotiation, Manufacturing & Service Operations Management, 2021 (accepted manuscript, SSRN 3021563). https://ssrn.com/abstract=3021563 — DOI https://doi.org/10.1287/msom.2021.0992
H. Horn and A. Wolinsky, Bilateral Monopolies and Incentives for Merger, RAND Journal of Economics 19(3), 408–419, 1988. https://doi.org/10.2307/2555721
D. P. O'Brien and G. Shaffer, Bargaining, Bundling, and Clout: The Portfolio Effects of Horizontal Mergers, RAND Journal of Economics 36, 573–595, 2005.
A. Dukes, E. Gal-Or and K. Srinivasan, Channel Bargaining with Retailer Asymmetry, Journal of Marketing Research 43, 84–97, 2006. https://doi.org/10.1509/jmkr.43.1.84
E. Kalai, Nonsymmetric Nash Solutions and Replications of 2-Person Bargaining, International Journal of Game Theory 6(3), 129–133, 1977. https://doi.org/10.1007/BF01770215

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Dynamic Fair Resource Division: The Optimal Fairness Ratio of d-Uniform Control Vectors Is 1/((d+1)·ln((d+1)/d)), Attained by the Frugally Fair AlgorithmResearch Paper

Motivation

Shared computing infrastructure — a data-centre cluster, a cloud platform's memory — is divided among users who arrive over time. Two requirements pull against each other. Proportional fairness asks that, when $t$ users are present, each holds at least a $1/t$ fraction of the resource. Limited disruption asks that the system not take resource away from running jobs at every arrival, because preemption and reallocation are costly; production cluster managers such as Google's Borg impose an explicit cap on the number of task disruptions an update may cause (Verma et al., 2015, as quoted in Vardi–Psomas–Friedman 2022, pp. 945–946). If reallocation were free, the resource could be re-split evenly at every arrival; if fairness did not matter, the first user could keep everything. The question is how much fairness survives a hard cap on disruptions.

Earlier work on dynamic fair division (Walsh 2011, online cake cutting; Kash, Procaccia and Shah 2014) did not allow reallocation at all. Friedman, Psomas and Vardi (EC 2017) introduced control vectors and gave non-optimal algorithms. Vardi, Psomas and Friedman (Mathematics of Operations Research, 2022) give an optimal algorithm for every control vector once the target ratio is known, and compute the optimal ratio exactly for uniform disruption budgets. This mission formalizes that exact computation.

Setting

One unit of a homogeneous, divisible resource is shared. Users arrive one at a time and never leave (the paper treats arrivals and departures separately; §§3–5, which this mission covers, are arrivals only). Users are labelled by arrival order, and $X^t_k$ is the share of the $(k+1)$ -th user when $t$ users are present.

A control vector $\psi$ of length $n \in \{1,2,\dots\}\cup\{\infty\}$ fixes, for each arrival $1 \le t \le n$ , a budget $\psi[t]$ : when the $t$ -th user arrives, at most $\psi[t]$ of the $t-1$ users already present may have their share strictly reduced (disrupted). Increasing a share is free. The $d$ -uniform control vector has $\psi[t] = d$ for every $t$ , of any length, finite or infinite.

An allocation sequence $X = (X^1, X^2, \dots)$ for $\psi$ is feasible if at every time $1 \le t \le n$ the shares are nonnegative, sum to at most $1$ , and respect the disruption budget. Its fairness ratio is

\inf_{1 \le t \le n}\; t \cdot \min_{k<t} X^t_k ,

the smallest share relative to the proportional share $1/t$ , in the worst time step. The fairness ratio of the control vector, $\mathrm{FAIRNESS}(\psi)$ , is the supremum of this quantity over all feasible allocation sequences, and

\mathrm{FAIRNESS}(d\text{-uniform}) = \inf_{\psi\ d\text{-uniform}} \mathrm{FAIRNESS}(\psi).

The frugally fair algorithm $\mathrm{FFA}(\psi,\sigma)$ takes a target ratio $\sigma$ : when user $t$ arrives, it gives the newcomer $\sigma/t$ and cuts the $\psi[t]$ largest existing shares to $\sigma/t$ . It may allocate more than one unit; $S^t$ denotes its total allocation at time $t$ .

Formalization targets

Goal: Theorem 4

For every integer $d \ge 1$ ,

\mathrm{FAIRNESS}(d\text{-uniform}) \;=\; \sigma^*_d \;:=\; \frac{1}{(d+1)\ln\!\big(\frac{d+1}{d}\big)} .

The goal states this in three parts: the infinite $d$ -uniform vector admits one feasible allocation sequence with ratio at least $\sigma^*_d$ ; for every $\sigma > \sigma^*_d$ some finite $d$ -uniform vector admits no feasible allocation sequence with ratio $\sigma$ ; and the infimum over all lengths of $\mathrm{FAIRNESS}$ equals $\sigma^*_d$ . For $d = 1$ , $\sigma^*_1 = 1/(2\ln 2) \approx 0.721$ .

Milestones

Feasible runs of FFA yield feasible allocation sequences with the same shares and ratio $\sigma$ (§3, p. 949).
Theorem 1 (p. 950): if any algorithm achieves a nonnegative ratio $\sigma$ on $\psi$ , then $\mathrm{FFA}(\psi,\sigma)$ is feasible at every time.
Lemma 1 (p. 951): $\mathrm{FFA}(\psi,\sigma)$ is $\mathrm{FFA}(\psi,\sigma')$ scaled by $\sigma/\sigma'$ .
Proposition 2 (p. 952): $\mathrm{FAIRNESS}(\psi) \le \mathrm{FAIRNESS}(\psi')$ when $\psi'$ is a prefix of $\psi$ .
Lemma E.1 (p. 959): the explicit allocation of FFA on the infinite $d$ -uniform vector at time $t = \ell(d+1)+i$ .
$S^t$ is nondecreasing in $t$ on the $d$ -uniform vector (p. 959).
Display (E.1) (p. 959): $\lim_{\ell\to\infty} S^{\ell(d+1)} = \sigma(d+1)\ln\frac{d+1}{d}$ .

Significance

The theorem gives a closed-form price of limited disruption: with $d$ reallocations per arrival, a system can guarantee every user $\sigma^*_d/t$ of the resource forever, and no algorithm can guarantee more uniformly over all horizons. Since $\sigma^*_d = 1 - \frac{1}{2d} + O(d^{-2})$ , a modest budget already recovers most of proportional fairness, which is the quantitative content a system designer needs to choose $d$ . Combined with Theorem 1, the value also turns FFA into a concrete optimal algorithm for the infinite $d$ -uniform vector, running online with no knowledge of the horizon.

The result is proved in the paper; to the best of a search of the Prove2Me catalogue, nothing about control vectors, disruption-limited fair division or this constant is formalized there. The mission produces a machine-checked model of disruption-limited dynamic allocation, a formal optimality proof for a greedy online algorithm (Theorem 1) that is reusable for other control vectors (the paper's finite-vector algorithm and $c$ -gap bounds rest on the same theorem), and an explicit harmonic-sum asymptotic.

Difficulty

The impossibility half must rule out every algorithm, including ones that over-allocate early, raise shares opportunistically and choose whom to disrupt adaptively. The first idea, comparing total allocations time by time, fails: an arbitrary algorithm's allocation is not entrywise comparable with any fixed reference allocation, and a single well-chosen disruption can change which users are largest. The attainment half needs one allocation sequence for an unbounded horizon, so it cannot be obtained from finitely many feasibility checks; and the value $\sigma^*_d$ is not the outcome of any finite computation but a limit of harmonic-number differences. The paper's own computation of the one-step change in total allocation contains a slip (a missing factor $\ell$ ; the sign is unaffected), so that step cannot be transcribed as printed.

Formalization scope

Everything is real-valued and lives in DynFairDiv.Uniform. A control vector is ψ : ℕ → ℕ (index $t \ge 1$ ) with a horizon n : ℕ∞, where ⊤ is the infinite vector; uniformCV d is the constant vector. Allocation sequences are X : ℕ → ℕ → ℝ with users labelled by arrival order, which is equivalent to the paper's sorted vectors because feasibility uses only sums, fairness only minima, and a disruption is a strict decrease of a given user's share; the newcomer is never counted as disrupted. Fairness at least $\sigma$ is σ / t ≤ X t k for all $1 \le t \le n$ and $k < t$ . $\mathrm{FAIRNESS}(\psi)$ is a real sSup, genuine for $n \ge 1$ . FFA's state is a list of shares kept in nonincreasing order, so "the $\psi[t]$ largest shares" is the front of the list. Departures (the paper's §6) are not modelled.

Added hypotheses, each disclosed in its item: $d \ge 1$ throughout §5.1 (the paper's own assumption); $\sigma \ge 0$ for milestones 1, 2 and 6 (the paper's fairness ratios lie in $[0,1]$ ); $\sigma' \ne 0$ in Lemma 1; a prefix of length at least $1$ in Proposition 2. Milestone 1 identifies the resulting sequence's shares with FFA's shares at each time.

A trivializing reading is ruled out: the impossibility half quantifies over every feasible allocation sequence, not only FFA-like or sorted ones, and the attainment half asks for a single sequence on the infinite horizon rather than one per finite length.

A complete development needs basic facts about FFA's list (length, order, scaling) and the harmonic asymptotics already in Mathlib (Real.tendsto_harmonic_sub_log). The FFA model and Theorem 1 apply to arbitrary control vectors and are reusable for the paper's finite-vector and $c$ -gap results; contributions of auxiliary lemmas about FFA (length, sortedness, scaling) are welcome.

Selected references

S. Vardi, A. Psomas, E. Friedman, Dynamic Fair Resource Division, Mathematics of Operations Research 47(2):945–968, 2022. https://doi.org/10.1287/moor.2021.1155
E. Friedman, C.-A. Psomas, S. Vardi, Controlled Dynamic Fair Division, Proc. 18th ACM Conference on Economics and Computation (EC), 461–478, 2017.
I. A. Kash, A. D. Procaccia, N. Shah, No Agent Left Behind: Dynamic Fair Division of Multiple Resources, Journal of Artificial Intelligence Research 51:579–603, 2014.
T. Walsh, Online Cake Cutting, Algorithmic Decision Theory (ADT), Springer, 292–305, 2011.
A. Verma, L. Pedrosa, M. Korupolu, D. Oppenheimer, E. Tune, J. Wilkes, Large-Scale Cluster Management at Google with Borg, Proc. 10th European Conference on Computer Systems (EuroSys), 2015.

9 thms2 active usersReviewed

Markov Chain Operations Research Stochastic Systems·Captain: mikedeng1

Smart Policies for Multisource Inventory Systems and General Tandem Queues with Order Tracking and Expediting: State Space and Product-Form Stationary Distribution under Policy-MResearch Paper

Why state-dependent sourcing matters

An inventory system can replenish demand from several stages of a supply process. When an order is placed, the manager chooses where it enters; when work finishes at one stage, the manager may send it past intermediate stages to speed delivery. These choices change the future congestion of every stage. A stationary occupancy distribution is needed to calculate how often stock is available, how often demand waits, and how often expediting is used. Song, Xiao, Zhang, and Zipkin study such policies through a tandem network whose arrival and routing decisions depend on the current occupancies. They identify Policy-M as one family with a product-form stationary distribution, despite this state dependence (Song et al., SSRN 3702068, §§3–4).

The paper's Theorem 1 is the target here. Its formula permits the system's long-run inventory cost to be evaluated by summing over states with known product weights. The same paper develops a distinct Policy-E family, but its theorem has a different routing rule and is outside this mission (Song et al., Theorems 1–2).

The tandem supply system

There are $K\ge1$ service nodes in series, numbered $1,\ldots,K$ . A state $n=(n_1,\ldots,n_K)\in\mathbb N^K$ records the number of units at each node. The segment occupancy $n[a,b]=\sum_{l=a}^{b}n_l$ counts units between nodes $a$ and $b$ , inclusive. Demand arrives at positive rate $\lambda$ . Node $k$ completes service at positive rate $\mu_k$ whenever $n_k>0$ . A completion at node $K$ leaves the supply system.

Policy parameters are thresholds $u_{ij}$ for $0\le i<j\le K$ , with values in $\mathbb N\cup\{\infty\}$ . For fixed origin $i$ , thresholds are nondecreasing as $j$ grows; for fixed destination $j$ , they are nonincreasing as $i$ grows. Every terminal threshold $u_{iK}$ equals $\infty$ . An arriving demand places a new unit at node $1$ when no prefix $n[1,k]$ reaches $u_{0k}$ ; otherwise it places the unit at one node beyond the largest such $k$ . A service completion at node $m<K$ follows the analogous Policy-M rule using downstream segments $n[m+1,k]$ and thresholds $u_{mk}$ . An empty set of reached thresholds sends the unit to $m+1$ (Song et al., (5), (7), §4).

Assumption A imposes two inequalities on these thresholds: a triangle inequality $u_{kj}\le u_{ki}+u_{ij}$ for $k<i<j$ , and supermodularity $u_{ij}+u_{kl}\le u_{kj}+u_{il}$ for $k<i<j<l$ . The indices may include the demand source $0$ . The admissible state set $S_M(u)$ consists of all occupancies whose segments obey $n[k+1,l]\le u_{kl}$ for every $0\le k<l\le K$ (Song et al., Assumption A and (11)).

Formalization targets

The first part of Theorem 1 identifies the states reachable from the empty system through positive-rate Policy-M transitions:

\operatorname{Reach}_{M}(0)=S_M(u) =\{n\in\mathbb N^K:n[k+1,l]\le u_{kl}\text{ for }0\le k<l\le K\}.

For $\lambda<\mu_K$ and finite $u_{0i}$ whenever $1\le i<K$ , define $w(n)=\prod_{k=1}^{K}(\lambda/\mu_k)^{n_k}$ and $G(u)=\sum_{n\in S_M(u)}w(n)$ . The second part gives a normalized product law:

0<G(u)<\infty,\qquad \pi_M(n)=\frac{\mathbf1_{S_M(u)}(n)}{G(u)} \prod_{k=1}^{K}\left(\frac{\lambda}{\mu_k}\right)^{n_k}.

The mission also requires $\pi_M$ to have total mass one and to satisfy global balance for the rates generated by the stated routing rules. Its milestones are the closure claims (A-2) and (A-5), equality of the Appendix proof sets in (A-30), the indicator identity (A-25), and the local balance equations (A-12)–(A-15) (Song et al., Theorem 1 and Appendix A).

What the result gives

The formula describes the joint occupancy of all service nodes from $K$ rates and the policy thresholds. Once its normalizer is known, probabilities of stock levels and congestion events can be summed over $S_M(u)$ , supplying the inputs to the paper's long-run cost calculation (9). The state-space result determines which occupancies contribute to those sums (Song et al., (9), Theorem 1).

Theorem 1 is proved in the paper. This mission asks for machine-checked proofs of its formal statements, not a new queueing result. A complete development would provide reusable finite-segment reasoning, routing-set identities, and countable-state balance calculations. The declarations staged here are open Lean statements, so they do not yet constitute machine-checked proofs.

The obstacle in the balance equations

With fixed routing, a proposed product weight can be compared across neighboring states using only the node rates. Here the route of a newly arriving or completed unit changes with several segment occupancies. An incoming transition to a state may have skipped nodes, and the condition that selected its destination must hold in the predecessor state. Checking only the product ratio therefore leaves out the routing indicators. The source's local equations (A-12)–(A-15) and its proof-set identity (A-25) make those indicators explicit. The paper also gives an example showing that state-dependent routing does not yield product form for every policy (Song et al., Example 1 and Appendix A).

Formalization scope

Lean represents $n$ as a function from Fin K to natural numbers, while the functions occ and seg retain the paper's one-based node numbers. The threshold array takes values in extended natural numbers so $u_{iK}=\infty$ is representable; a strict comparison with a threshold expresses the paper's “at most $u-1$ ” condition. Both routing rules specify the destination when no threshold is reached. A service transition is enabled only when its origin node is occupied. The theorem states $K\ge1$ , which is implicit in the paper's numbered-node model, along with positive arrival and service rates.

The source defines $\pi$ as the limiting law of a continuous-time Markov chain and invokes known ergodicity. This Lean development encodes its stationary claim by a summable, normalized product weight and the global balance equations for explicit Policy-M rates. It does not formalize the CTMC limit or uniqueness of that limit. The normalizer is a countable sum; the goal asserts summability and $G(u)>0$ , so a default value for a divergent sum or division by zero cannot certify the claim. The state space is constructed from $u$ and proved reachable rather than supplied as a hypothesis. Empty-node departures are guarded to avoid natural-number subtraction at zero. The special $K=1$ case remains in the goal; the milestone combining four separate local equations assumes $K\ge2$ because its node-1 and node- $K$ formulas must refer to distinct nodes.

The staged definition supplies segments, thresholds, routing, transition rates, product weights, and the source's Appendix sets. Contributions may prove the listed milestones, build general lemmas about segment sums and reachability, or establish summability and the passage from local to global balance. These supporting tools can be reused for other countable-state queueing models.

Selected references

J.-S. Song, L. Xiao, H. Zhang, and P. Zipkin, Smart Policies for Multisource Inventory Systems and General Tandem Queues with Order Tracking and Expediting, SSRN 3702068, version of September 28, 2020; subsequently published in Operations Research, DOI 10.1287/opre.2021.2124. Source preprint.

8 thms2 active users

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Dynamic Resource Allocation in the Cloud with Near-Optimal Efficiency: The Multiplicative Weight Algorithm Nearly Matches the Offline Dynamic Optimum's Work While Approximately Satisfying Every SLAResearch Paper

Motivation

Cloud platforms divide a shared physical resource, such as a pool of processors, among many users at once. Each user is promised a service level agreement (SLA): a fraction $\beta(i)$ of the resource that it should effectively receive whenever it has work to do. The operator wants two things that pull against each other: to keep the resource busy (total work done should be large) and to honour every SLA. The difficulty is informational. The operator does not see future demand, and in the setting of Perez-Salazar, Menache, Singh and Toriello (arXiv:1809.02688) it does not even see current demand: at each step it only learns which users have a non-empty queue.

The paper answers with a multiplicative weight rule. Multiplicative weight methods go back to online learning (Freund and Schapire, 1997; survey: Arora, Hazan and Kale, 2012) and can be read as entropic mirror descent (Beck and Teboulle, 2003). Their classical guarantees compare an online learner with the best fixed decision in hindsight. This paper compares the algorithm with the best time-varying offline allocation instead, and proves the comparison directly, without the standard regret analysis.

Setting

There are $N \ge 2$ users and discrete time steps $t = 1, 2, \dots$ . Each user $i$ has an SLA $\beta(i) \ge 0$ , with $\sum_i \beta(i) \le 1$ . Loads $L_t(i) \ge 0$ arrive online. User $i$ keeps a queue $Q_t(i)$ of unfinished work. At each step:

the decision maker observes the active users $A_t = \{i : Q_t(i) > 0\}$ ;
it chooses an allocation $h_t$ with $h_t(i) \ge 0$ and $\sum_i h_t(i) \le 1$ ;
the load $L_t$ arrives, user $i$ completes $w_t(i) = \min\{h_t(i),\, L_t(i) + Q_t(i)\}$ , and $Q_{t+1}(i) = \max\{0,\, L_t(i) + Q_t(i) - h_t(i)\}$ .

The total work of an allocation sequence $h$ up to time $t$ is $\mathrm{work}_h(t) = \sum_i \sum_{\tau \le t} w_\tau(i)$ .

Algorithm 1 has parameters $0 < \varepsilon \le 1/10$ and $0 < \eta < 1/3$ , and sets $\lambda = \varepsilon^2/(8N)$ . It keeps $h_t$ in the truncated simplex $\Delta_\varepsilon = \{x : \sum_i x(i) = 1,\ x(i) \ge \varepsilon/N\}$ , starting anywhere in $\Delta_\varepsilon$ . At step $t$ it assigns the gain $g_t(i) = 1 + \lambda$ to active users below their SLA ( $A^1_t$ : $h_t(i) < \beta(i)$ ), $g_t(i) = 1$ to the other active users ( $A^2_t$ ) and $g_t(i) = 0$ to inactive users. It then sets $\widehat h_{t+1}(i) = h_t(i)e^{\eta g_t(i)}$ and takes $h_{t+1} = \pi_{\Delta_\varepsilon}(\widehat h_{t+1})$ , the KL projection: the minimizer over $\Delta_\varepsilon$ of $\sum_i x(i)\ln(x(i)/\widehat h_{t+1}(i))$ .

Formalization targets

Goal: Theorem 1 with the explicit constants of p. 10

Let $\beta(i) \ge 2\varepsilon/N$ for all $i$ and let $h$ be any run of Algorithm 1. For every offline allocation sequence $h^*$ and every time $t$ ,

\mathrm{work}_{\mathrm{alg}}(t) \ge (1 - 4\varepsilon)\,\mathrm{work}_{h^*}(t) - 2000\,\frac{N}{\varepsilon^2\eta}\ln\frac{N}{\varepsilon},

and for every user $i$ , every comparator $h'$ with $0 \le h'_t(i) \le \beta(i)$ and every $t$ ,

\sum_{\tau \le t} w_\tau(i) \ge (1 - 2\varepsilon)\sum_{\tau \le t} w'_\tau(i) - \beta(i)\,\tilde p, \qquad \tilde p = \frac{32N^2}{\varepsilon^3\eta}\ln\frac{N}{\varepsilon}.

Intermediate targets (milestones)

Theorem 3: against every sequence of $(1-4\varepsilon)$ -allocations, $\mathrm{work}_{h^*}(t) - \mathrm{work}_{\mathrm{alg}}(t) \le \frac{8N}{\varepsilon^2\eta}\ln\frac{N}{\varepsilon} + 2$ at every $t$ .
Theorem 4: if $\beta(j) > e^{\eta(1+\lambda)}\varepsilon/N$ for all $j$ , each user's work by time $t + \lceil\tilde p\rceil$ is at least what the constant share $(1-2\varepsilon)\beta(i)$ completes by time $t$ .
Lemma 1 and Lemma 2: per-step growth factors $1 + c$ , $1 - \varepsilon c$ and $1 + c'$ of a busy user's allocation, with $c = \varepsilon\eta/(4N)$ and $c' = \varepsilon\eta\lambda/(2N)$ .
Proposition 1(b): the closed form of the KL projection onto $\Delta_\varepsilon$ .
Proposition 2 (weak-duality half), Claims 3.1 and 3.2 (first conclusion): the amortization behind Theorem 3.
The scaling step of p. 10: scaling an allocation by $\kappa \le 1$ keeps at least a $\kappa$ fraction of its work, and work is monotone in the allocation.
Existence and uniqueness of the KL projection, hence of the run from each start.

Significance

The result. Theorem 1 is a bicriteria guarantee against a dynamic benchmark. The work benchmark may change its allocation arbitrarily over time with full knowledge of all loads, and the algorithm, which sees only which queues are non-empty, loses only an additive amount that does not grow with time, at the price of a $4\varepsilon$ fraction of capacity. At the same time every user receives, up to a fixed delay, at least the work of a dedicated $(1-2\varepsilon)$ fraction of its SLA. The paper also shows (arXiv:1809.02688, Theorem 2) that against the unscaled offline optimum every deterministic online algorithm loses $\Omega(\sqrt T)$ work on some load sequence, so some form of slack is unavoidable.

Formalizing it. The result is proved on paper; no machine-checked proof exists. A formalization would check the constant bookkeeping, where the printed text has slips (an $\varepsilon$ versus $\varepsilon/4$ in Theorem 1, a real block length $\tilde s$ used as an integer, an off-by-one in Claim 3.1). It would also produce a reusable deterministic queueing model and a verified closed form of the KL projection onto a truncated simplex.

Difficulty

The obvious first idea, the regret analysis of mirror descent, does not apply. Regret bounds compare with a fixed decision, but here the benchmark changes over time. The algorithm's gains also depend on its own past decisions through the queues, so they are not an exogenous sequence of losses. The paper notes (p. 10) that its guarantees do not follow from the standard analysis of mirror descent. A second obstacle is the feedback: a busy user is not the same as a user that uses its whole allocation. A user whose queue empties during a step completes less than its allocation, so utilization and work done can differ. Finally, the constants matter, because the goal states them explicitly. The printed derivation mixes $\varepsilon$ and $\varepsilon/4$ , uses the real number $\tilde s$ as a block length, and is off by one step when it identifies the work done with the arrived load.

Formalization scope

Model. Everything is real-valued. Time is 0-based: Lean's step $t$ is the paper's step $t + 1$ , the queue at Lean time $t$ is the paper's $Q_{t+1}$ , and $\sum_{\tau=1}^{t}$ is a sum over the first $t$ steps. Queues start empty, a convention the paper uses but does not state. Loads form an infinite sequence; the horizon $T$ is not a parameter and every bound holds at every $t$ .
Runs. The KL projection is a predicate for positive inputs, the domain where the logarithm is defined; Algorithm 1 always projects a positive vector. A run is any sequence satisfying the recursion. The gains are computed from the queues the run itself produces before step $t$ , so $h_{t+1}$ never uses the load of step $t$ or later. A milestone proves that each start in $\Delta_\varepsilon$ has exactly one run, and a sorry-free sanity check exhibits one. Statements about runs are therefore not vacuous.
Benchmarks. "The optimal offline sequence" is replaced by every allocation sequence with $\sum_i h^*_t(i) \le 1$ (or $\le 1 - 4\varepsilon$ ), which is equivalent and avoids a supremum. The SLA comparator ranges over every sequence with $h'_t(i) \le \beta(i)$ , not only the constant one.
Disclosed readings and corrections. Part 1 of the goal uses the $(1 - 4\varepsilon)$ form of p. 10 for the same $\varepsilon$ , not the headline's $(1-\varepsilon)$ . Theorem 3 carries a $+2$ for integer blocks. Claim 3.1 is stated in its corrected 0-based form. Theorem 4 assumes the SLA bound strictly. $0 < \eta < 1/3$ (Algorithm 1's input) is assumed throughout. $\sum_i \beta(i) \le 1$ replaces the $= 1$ used in the proof of Lemma 2.
Ruled out. The goal is stated for every run of the algorithm, with the active sets read from the run's own queues, against every offline sequence. A formalization that fixes a closed-form allocation, decouples the queues from the allocations, or restricts the benchmark to static allocations does not count.
Needed and reusable. The deterministic single-user queue with its work and monotonicity facts, KKT conditions for an entropic objective over a box-constrained simplex, and elementary exponential and logarithm inequalities. The queue model and the projection closed form are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

S. Perez-Salazar, I. Menache, M. Singh, A. Toriello, Dynamic Resource Allocation in the Cloud with Near-Optimal Efficiency, arXiv:1809.02688v3, 2021 (Operations Research, 2022). https://arxiv.org/abs/1809.02688
Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, Journal of Computer and System Sciences 55(1), 1997. https://doi.org/10.1006/jcss.1997.1504
S. Arora, E. Hazan, S. Kale, The multiplicative weights update method: a meta-algorithm and applications, Theory of Computing 8, 2012. https://doi.org/10.4086/toc.2012.v008a006
A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3), 2003. https://doi.org/10.1016/S0167-6377(02)00231-6

29 thms2 active users

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Large Fork-Join Queues with Nearly Deterministic Arrival and Service Times: Fluid Limit of the Maximum Queue Length with a Non-Zero Initial ConditionResearch Paper

Motivation

A fork-join queue splits every incoming job into tasks, sends one task to each of $N$ parallel servers, and declares the job complete only when all tasks are done. The model describes assembly systems in which a manufacturer orders parts from $N$ suppliers and can only start production when every part has arrived, as well as parallel computing and storage systems in which a request is answered only after all sub-requests return. Because a job waits for its slowest task, the performance of the system is governed by the maximum queue length over the $N$ servers, and the question of interest is how this maximum behaves when $N$ is large and the system is heavily loaded.

Schol, Vlasiou and Zwart (arXiv:1912.11661, Mathematics of Operations Research 47(2), 2022) study this question in a nearly deterministic regime: arrivals and services happen in almost every time slot, and the traffic intensity of each server tends to $1$ at rate $N^{-2}$ . Even in the empty-start case the queue lengths of different servers are dependent, because every server sees the same arrival process; the maximum of $N$ dependent random walks has to be analysed directly.

Timeline. Early work treats two service stations and obtains exact asymptotics (Flatto and Hahn, 1984; Baccelli, 1985; Wright, 1992). For more stations the literature turned to approximations and bounds: Nelson and Tantawi (1988) and Baccelli and Makowski (1989) bound the mean response time, and Ko and Serfozo (2004) approximate the response-time distribution in M/M/s fork-join queues. Heavy-traffic process limits for a fixed number of stations were obtained by Varma (1990) and Nguyen (1993, 1994), with reflected Brownian motion limits, and by Lu and Pang (2015–2017) for many-server stations. Sigman and Whitt (2011) analysed nearly deterministic G/G/1 and G/D/N queues. The paper of this mission gives a process-level (fluid) limit for the largest queue when the number of servers $N$ itself grows, in the nearly deterministic regime and with a non-zero initial condition.

Setting

Fix $\alpha,\beta>0$ . For each $N$ the system runs in discrete time slots $j=1,2,\dots$ . In slot $j$ a task arrives at all $N$ servers with probability $p^{(N)}=1-\alpha/N-\beta/N^2$ (indicator $X^{(N)}(j)$ ), and server $i$ completes a task with probability $q^{(N)}=1-\alpha/N$ (indicator $Y_i^{(N)}(j)$ ), all indicators being independent. The arrival process is $A^{(N)}(n)=\sum_{j=1}^{n}X^{(N)}(j)$ and the service process of server $i$ is $S_i^{(N)}(n)=\sum_{j=1}^{n}Y_i^{(N)}(j)$ .

Server $i$ starts with $Q_i^{(N)}(0)=\lfloor r_NU_i\rfloor$ tasks, where $U_1,U_2,\dots$ are i.i.d. random variables, the initial queue lengths are non-negative, and $r_N\ge0$ is a scaling sequence. By Lindley's recursion the maximum queue length at time $n$ is

Q^{(N)}_{(\alpha,\beta)}(n)=\max_{i\le N}\max\Big(\sup_{0\le k\le n}\big[(A^{(N)}(n)-A^{(N)}(k))-(S_i^{(N)}(n)-S_i^{(N)}(k))\big],\;Q_i^{(N)}(0)+A^{(N)}(n)-S_i^{(N)}(n)\Big).

The first term alone is the maximum queue length of the system started empty. The initial condition is assumed to satisfy $Q^{(N)}_{(\alpha,\beta)}(0)/(N\log N)\to q(0)\ge0$ in probability (Assumption 2.3), and either $U_i$ has a finite right endpoint (Assumption 2.4) or $U_i$ is continuous with $-\log\mathbb P(U_i>vt)/-\log\mathbb P(U_i>t)\to h(v)$ as $t\to\infty$ for all $v\in[0,1]$ (Assumption 2.5, the Gumbel-domain case).

The fluid limit is

q(t)=\max\Big(\big(\sqrt{2\alpha t}-\beta t\big)\mathbb 1\big(t<\tfrac{\alpha}{2\beta^2}\big)+\tfrac{\alpha}{2\beta}\mathbb 1\big(t\ge\tfrac{\alpha}{2\beta^2}\big),\;g(t,q(0))-\beta t\Big),

with $g(t,q(0))=q(0)+\sqrt{2\alpha t}$ under Assumption 2.4 and $g(t,q(0))=\sup\{\sqrt{2\alpha t}\,u+q(0)v : u^2+h(v)\le1,\ 0\le u,v\le1\}$ under Assumption 2.5. In Lean these are fluid, fluidEmpty, gFinite and gGumbel; the queue is maxQueue and the empty-start queue maxQueueEmpty.

Formalization targets

Goal: Theorem 2.1 (fluid limit)

For every $T>0$ and $\epsilon>0$ ,

\mathbb P\left(\sup_{0\le t\le T}\left|\frac{Q^{(N)}_{(\alpha,\beta)}(tN^3\log N)}{N\log N}-q(t)\right|>\epsilon\right)\xrightarrow{N\to\infty}0,

under Assumptions 2.1–2.3 and either Assumption 2.4 or Assumption 2.5 (one conjunct per case).

Milestones

Section 4.2 tools. The pathwise oscillation bound of Lemma 4.1; the non-uniform Berry–Esseen rate of Lemma 4.2 for the standardized service process; the moment bound of Lemma 4.3; the extreme-value Lemma B.1 for sums of independent relatively stable variables and its consequence Lemma 4.4 for the Gaussian surrogate of the initial condition.
Pointwise convergence (Section 4.3). Lemmas 4.6 and 4.8 (bounds for the empty-start system), Lemma 4.5 (its pointwise limit), Lemma 4.9 (the initial-condition part) and Theorem 4.1: $Q^{(N)}_{(\alpha,\beta)}(tN^3\log N)/(N\log N)\to q(t)$ in probability for each $t>0$ .
Tightness (Section 4.4). Lemma 4.10 (maxima preserve uniform convergence), Lemmas 4.11–4.12 (moduli of continuity of the two parts) and Corollary 4.1 (tightness of the scaled process on $[0,T]$ ).

Significance

The result. Theorem 2.1 identifies the scaling under which the maximum queue length of a large, heavily loaded fork-join system follows a deterministic curve: time of order $N^3\log N$ and space of order $N\log N$ . The limit separates the contribution of the empty-start dynamics, which saturate at the steady-state level $\alpha/(2\beta)$ after time $\alpha/(2\beta^2)$ , from the contribution of the initial backlog, which is governed by the extreme-value class of the initial condition. For instance, with $h(v)=v$ and $q(0)=\alpha/(2\beta)$ the system "starts and stays in steady state" on an initial interval (p. 12). The theorem gives the transient behaviour needed to judge how long a backlog at the slowest supplier persists.

Formalizing it. The result is proved in the paper; no part of it has a machine-checked proof. The mission produces a formal statement of the model and of the fluid limit, and the intermediate results of Section 4. The proof combines a non-uniform Berry–Esseen inequality, extreme-value theory for maxima of sums, Doob's maximal inequality and a tightness criterion; formalizing it would give reusable Lean versions of several of these tools.

Difficulty

The obvious argument treats the $N$ queues as independent reflected random walks and applies extreme-value theory to their maximum. It fails because all servers share the arrival process, so the queues are dependent. The paper handles this by splitting each queue into a common arrival term and an individual service term, but the individual terms are maxima of $N$ centred random walks evaluated at a time of order $N^3\log N$ , and their Gaussian approximation must be accurate at the scale of the maximum: a uniform Berry–Esseen bound is too weak, and a non-uniform bound with the right rate in $N$ is needed (Lemma 4.2). Upgrading pointwise convergence to uniform convergence on $[0,T]$ requires a modulus-of-continuity estimate for a maximum of $N$ processes (Lemmas 4.11–4.12), where the number of processes grows with $N$ . The initial-condition term requires an extreme-value result for maxima of sums of two independent coordinates with different tails (Lemma B.1).

Formalization scope

All objects are defined in one module, LargeForkJoin.FluidLimit.Model. Times are natural numbers, and $Q(tN^3\log N)$ is evaluated at $\lfloor tN^3\log N\rfloor$ , which is the paper's own convention $Q(n)=Q(\lfloor n\rfloor)$ . Servers are indexed $0,\dots,N-1$ . All variables live on one probability space; the Bernoulli laws are imposed for $N\ge N_0$ (for small $N$ , $p^{(N)}$ can be negative), and within each $N\ge N_0$ the arrival indicators, service indicators and initial-condition variables $U_i$ used by that system are mutually independent. The independence of $(U_i)$ from arrivals and services is an added assumption: the paper uses it in its proofs but does not state it. Initial queue lengths are non-negative almost surely. Assumption 2.5 adds $\mathbb P(U_i>t)>0$ for all $t$ , without which its ratio is undefined; "continuous" means "no atoms". Convergence in probability to a constant is written with $\epsilon$ -events, and $\sup_{0\le t\le T}|\cdot|>\epsilon$ as "some $t\in[0,T]$ has $|\cdot|>\epsilon$ ", the same event. Lemmas 4.4 and 4.9 speak of Gaussian variables outside the model; they are stated for the law of $N$ independent pairs (standard normal, law of $U_1$ ).

The goal is stated about the maximum queue length built from the Bernoulli indicators through (2.3), uniformly on $[0,T]$ . A statement about a Gaussian or reflected-Brownian surrogate (the heuristics of Sections 2.2–2.3), or a pointwise statement (Theorem 4.1), would not be Theorem 2.1.

Not included: Propositions 2.1–2.3 (other scalings and the steady state), the variant of Theorem 2.1 under Assumption 2.6, Theorem 4.2 (finite-dimensional distributions, a generic fact), and Lemma 4.7, whose statement includes the stationary case $t=\infty$ and needs a stationary-queue object. Contributions of general tools are welcome: a non-uniform Berry–Esseen inequality for Bernoulli sums, extreme-value results for maxima of i.i.d. sequences (relative stability, Gumbel-domain tails), and the tightness criterion of Billingsley's Theorem 7.3.

Selected references

D. Schol, M. Vlasiou, B. Zwart, Large fork-join queues with nearly deterministic arrival and service times, Mathematics of Operations Research 47(2), 2022; arXiv:1912.11661v3. https://arxiv.org/abs/1912.11661v3
L. Flatto, S. Hahn, Two parallel queues created by arrivals with two demands I, SIAM Journal on Applied Mathematics 44(5), 1984. https://doi.org/10.1137/0144072
F. Baccelli, A. M. Makowski, Queueing models for systems with synchronization constraints, Proceedings of the IEEE 77(1), 1989. https://doi.org/10.1109/5.21076
R. Nelson, A. N. Tantawi, Approximate analysis of fork/join synchronization in parallel queues, IEEE Transactions on Computers 37(6), 1988. https://doi.org/10.1109/12.2212
K. Sigman, W. Whitt, Heavy-traffic limits for nearly deterministic queues, Journal of Applied Probability 48(3), 2011. https://doi.org/10.1239/jap/1316796905
S.-S. Ko, R. F. Serfozo, Response times in M/M/s fork-join networks, Advances in Applied Probability 36(3), 2004. https://doi.org/10.1239/aap/1093962240
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

17 thms2 active usersReviewed

Completed

Economics Operations Research Probability·Captain: mikedeng1

Costly Interpretation of Asset Prices: With Costly Price Interpretation There Is a Unique Linear Financial Market Equilibrium, and Its Price Carries Endogenous NoiseResearch Paper

Motivation

A central question of financial economics is how much of the information dispersed among traders ends up in market prices. The workhorse model is the noisy rational expectations equilibrium (REE): investors with private signals trade a risky asset, the price aggregates their information, and each investor learns from the price as well as from her own signal (Grossman and Stiglitz 1980; Hellwig 1980). In that tradition the price is a free public signal: every investor reads off from it exactly what it contains.

Vives and Yang (SSRN 2763813; published with Mondria as Mondria, Vives and Yang 2021) drop that assumption. Extracting information from a price takes effort, so each investor observes the price signal only through her own interpretation error, and can buy sophistication to reduce that error. The interpretation errors share a common component, and the paper's first result is that this common error re-enters the price. Even with no exogenous noise traders, costly interpretation makes the price noisy. This mission formalizes that first result: the existence, uniqueness and closed form of the linear financial-market equilibrium (Proposition 1, with the remark $a_u > 0$ that follows it).

Setting

A risky asset pays $\tilde V = \tilde v + \tilde\xi$ , with independent $\tilde v \sim N(0,\tau_v^{-1})$ (learnable) and $\tilde\xi \sim N(0,\tau_\xi^{-1})$ (unlearnable). A continuum $i\in[0,1]$ of investors have CARA utility with risk aversion $\gamma$ . Investor $i$ observes:

a private signal $\tilde s_i = \tilde v + \tilde\varepsilon_i$ , with $\tilde\varepsilon_i \sim N(0,\tau_\varepsilon^{-1})$ ;
a personalized price signal $\tilde s_{p,i} = \tilde s_p + \tilde u + \tilde e_i$ , where $\tilde s_p$ is the information in the price, $\tilde u \sim N(0,\tau_u^{-1})$ is a common interpretation error and $\tilde e_i \sim N(0,\tau_e^{-1})$ an idiosyncratic one;
an interpretation signal $\tilde z_i = \tilde u + \tilde e_i + \tilde\eta_i$ , with $\tilde\eta_i \sim N(0,\tau_\eta^{-1})$ , where $\tau_\eta$ is the common sophistication level.

All shocks are independent and centred, and all precisions and $\gamma$ are positive. A linear price function is $\tilde p = a_v\tilde v + a_u\tilde u$ ; when $a_v\ne 0$ it is equivalent to the signal $\tilde s_p = \tilde v + \alpha\tilde u$ with $\alpha = a_u/a_v$ . Each investor demands $D_i = (E(\tilde V\mid \tilde s_i,\tilde s_{p,i},\tilde z_i) - \tilde p)/(\gamma\,\mathrm{Var}(\tilde V\mid \tilde s_i,\tilde s_{p,i},\tilde z_i))$ , computed by Bayes' rule from the jointly Gaussian signals. A linear equilibrium is a pair $(a_v,a_u)$ , $a_v\neq0$ , such that aggregate demand $\int_0^1 D_i\,di$ is zero for every realization of $(\tilde v,\tilde u)$ .

The paper's closed forms use the precision of the combined price information,

\tau_p = \frac{\tau_e\tau_u + (\tau_e+\tau_u)\tau_\eta}{\tau_u + \tau_e(\alpha+1)^2 + \alpha^2\tau_\eta},

and the cubic

f(\alpha) = (\tau_e\tau_\varepsilon + \tau_\varepsilon\tau_\eta)\alpha^3 + 2\tau_e\tau_\varepsilon\alpha^2 + (\tau_e\tau_\varepsilon + \tau_e\tau_\eta + \tau_u\tau_\varepsilon)\alpha - \tau_e\tau_u.

Formalization targets

Goal: Proposition 1 and the noise remark

There is exactly one linear equilibrium $(a_v,a_u)$ . In it

a_v = \frac{\tau_\varepsilon+\tau_p}{\tau_v+\tau_\varepsilon+\tau_p},\qquad a_u = \frac{\tau_p}{\tau_v+\tau_\varepsilon+\tau_p}\cdot\frac{\tau_u(\tau_e+\alpha\tau_e+\alpha\tau_\eta)}{\tau_e\tau_u+\tau_e\tau_\eta+\tau_u\tau_\eta},

with $\tau_p$ evaluated at $\alpha = a_u/a_v$ ; $\alpha$ lies in $(0,\bar\alpha)$ , $\bar\alpha = \tau_e\tau_u/(\tau_e\tau_\varepsilon+\tau_e\tau_\eta+\tau_u\tau_\varepsilon)$ , and is the unique positive root of $f$ ; and $a_u > 0$ .

Milestones, in the order of the paper's proof

The Bayes coefficients $(\beta_s,\beta_p,\beta_z)$ of $E(\tilde v\mid\cdot)$ in closed form (proof of Proposition 1, p. 55).
Equation (17): $\mathrm{Var}(\tilde V\mid\cdot) = (\tau_v+\tau_\varepsilon+\tau_p)^{-1} + \tau_\xi^{-1}$ (p. 18).
Market clearing holds iff $a_v = \beta_s+\beta_p$ and $a_u = \beta_p(\alpha+1)+\beta_z$ (p. 56).
These sums equal the closed forms of $a_v$ , $a_u$ (p. 56).
$\alpha\,a_v(\alpha) = a_u(\alpha)$ iff $f(\alpha)=0$ (p. 56).
$f(0) < 0 < f(\bar\alpha)$ , hence a root in $(0,\bar\alpha)$ (p. 56).
The discriminant of $f$ is the printed 25-term expression $\Delta<0$ , hence $f$ has one real root (p. 56).

Significance

Proposition 1 is the foundation of the rest of the paper. Every comparative static on price informativeness, volatility, return predictability, disagreement and trading volume (Propositions 2–3), and the analysis of the sophistication-acquisition game (Propositions 4–6), is computed from the closed forms of $a_v$ , $a_u$ and the root $\alpha$ . The remark $a_u>0$ is the paper's mechanism: the common interpretation error is a source of price noise generated by the traders themselves, which vanishes only in the limit of full sophistication (Corollary 1).

The result is proved in the paper; nothing here is open. To our knowledge no part of it, nor any noisy-REE equilibrium with Bayesian price learning, has been machine-checked. The mission produces a formal account of the equilibrium construction of the noisy REE literature, from Gaussian conditioning to market clearing to a polynomial fixed point. The same pattern (conjecture a linear price, condition, match coefficients, solve for the fixed point) recurs throughout that literature.

Difficulty

Each step is elementary, but each is a large symbolic computation. Inverting the $3\times3$ covariance matrix and simplifying $\Sigma^{-1}c$ to the printed fractions involves rational functions in seven variables. The discriminant of $f$ is a polynomial of degree ten with 25 terms, and its sign has to be established for all positive parameters.

The conceptual pitfall is uniqueness. Showing that $f$ has one positive root is not enough: a linear equilibrium may a priori have $\alpha = a_u/a_v \le 0$ , so uniqueness among all linear equilibria needs $f$ to have one real root, which is what the discriminant gives. The fixed-point condition $\alpha = a_u(\alpha)/a_v(\alpha)$ also needs $a_v(\alpha)\neq0$ at every candidate, which has to be proved rather than assumed.

Formalization scope

All quantities are real. A parameter structure carries $\tau_v,\tau_\xi,\tau_\varepsilon,\tau_e,\tau_u,\tau_\eta,\gamma$ ; the standing assumption is that all seven are positive, and nothing else is assumed. The model is encoded in reduced form:

Conditioning. The conditional mean coefficients are the linear projection $\Sigma(\alpha)^{-1}c$ , with $\Sigma(\alpha)$ the covariance matrix of $(\tilde s_i,\tilde s_{p,i},\tilde z_i)$ and $c$ their covariance with $\tilde v$ . The conditional variance is $\tau_v^{-1} - c^\top\Sigma^{-1}c + \tau_\xi^{-1}$ . No probability space is built.
Market clearing. It is stated for every $(\tilde v,\tilde u)\in\mathbb R^2$ rather than almost surely, which is equivalent for linear functions of a nondegenerate Gaussian pair. Aggregate demand is the demand at the cross-sectional mean $(\tilde v,\ \tilde v+(\alpha+1)\tilde u,\ \tilde u)$ of the signals, the usual continuum convention.
The equilibrium predicate. It requires $a_v\neq0$ , as on p. 17 of the paper.
Equation (4). As printed, it attaches the law $N(0,\tau_\eta^{-1})$ to $\tilde z_i$ ; (5) and (15) show it belongs to $\tilde\eta_i$ , which is the reading used.

The equilibrium predicate is defined from Bayesian demands and market clearing only. Defining it by the closed forms of $a_v$ , $a_u$ , or as " $\alpha$ is a root of (18)", would make Proposition 1 a statement about a cubic and is ruled out. Likewise the Bayes coefficients are $\Sigma^{-1}c$ , never the printed fractions.

A complete development needs $3\times3$ matrix inversion over $\mathbb R$ (Mathlib's Matrix.inv), rational-function simplification, Mathlib's Cubic and its discriminant, and the intermediate value theorem. A reusable lemma "a real cubic with negative discriminant has exactly one real root" would serve beyond this mission. Proofs of any milestone, and alternative proofs of uniqueness, are welcome.

Selected references

X. Vives and L. Yang, Costly Interpretation of Asset Prices, SSRN working paper 2763813, September 2018 version (the version cited throughout). https://ssrn.com/abstract=2763813
J. Mondria, X. Vives and L. Yang, Costly Interpretation of Asset Prices, Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3871
S. J. Grossman and J. E. Stiglitz, On the Impossibility of Informationally Efficient Markets, American Economic Review 70(3), 1980. https://www.jstor.org/stable/1805228
M. F. Hellwig, On the Aggregation of Information in Competitive Markets, Journal of Economic Theory 22(3), 1980. https://doi.org/10.1016/0022-0531(80)90065-5

9 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Stochastic Knapsack Revisited: The Service Level Perspective: Anticipative Policies Need at Most 2Δ More Capacity Than Adaptive Policies to Meet Type-I Service LevelsResearch Paper

Motivation

A central planner holds a single pool of $Q$ units of a product and must supply $N$ customers whose demands $\tilde d_1, \dots, \tilde d_N$ are random. Each customer $i$ asks to be fully served, i.e. to receive her entire demand, with probability at least a target $\alpha_i$ . This Type-I service level (the persistency value of the stochastic knapsack) is the standard requirement in supply-chain allocation and in humanitarian logistics. The planner's question is how much capacity the targets require.

The answer depends on when the planner learns the demands. Lyu, Chou, Teo, Zheng and Zhong (SSRN 3674463, 2021) compare three information regimes:

a responsive policy sees every demand before allocating;
an adaptive policy learns a customer's demand only once it has decided to serve her, and may choose the next customer in light of what it has seen (Dean, Goemans and Vondrák, 2008);
an anticipative policy fixes a priority order before any demand is realized (Alptekinoğlu, Banerjee, Paul and Jain, M&SOM 15(1), 2013).

Anticipative rules are the ones used in practice, because they are simple to announce and to audit. The paper's main result quantifies what they cost in capacity compared with adaptive rules.

Timeline. Alptekinoğlu et al. (2013) introduced capacity pooling with differentiated service probabilities under anticipative priority rules. Dean, Goemans and Vondrák (2008) bounded the adaptivity gap of the stochastic knapsack for revenue maximization by a constant factor. Zhong, Zheng, Chou and Teo (Management Science 64(4), 2018) treated the Type-II (fill-rate) version, in which partial service counts in proportion. They showed that its achievable region is a polymatroid $\Gamma(Q)$ and that anticipative policies are optimal there. Lyu et al. (2021) use this Type-II system to compare the Type-I classes.

Setting

Customers are $i \in \{1, \dots, N\}$ . The demands are random variables on a probability space $(\Omega, \mathcal F, \mathbf P)$ . An allocation run with capacity $Q \ge 0$ serves customers one at a time. A chosen customer is fully served if her demand does not exceed the remaining capacity, and her demand is then deducted. Otherwise she is not fully served, and the run stops.

A deterministic adaptive policy chooses the next customer as a function of the customers chosen so far and their realized demands.
A deterministic anticipative policy is a priority order $\sigma$ , fixed in advance.
A randomized policy in either class is a finite mixture $\sum_k w_k A_k$ of deterministic ones, drawn independently of the demands.

The optimal Type-I capacities are

Q^{\mathrm{Adap}}_I = \inf\{Q \ge 0 : \text{some randomized adaptive policy has } \mathbf P(i \text{ fully served}) \ge \alpha_i\ \forall i\},

and $Q^{\mathrm{Anti}}_I$ is defined in the same way with anticipative policies. These are the optimal values of problem (CPP-A) of the paper.

On the Type-II side, $\Gamma(Q)$ is the set of $\alpha$ with $\sum_{i \in U} \alpha_i \mathbf E[\tilde d_i] \le \mathbf E[\min(Q, \sum_{i\in U} \tilde d_i)]$ for every $U \subseteq \{1,\dots,N\}$ . $Q_{II}$ is the least $Q \ge 0$ with $\alpha \in \Gamma(Q)$ . For a priority order $\sigma$ , the greedy fill $x^*_i(\sigma, \tilde d, Q) = \min\{\tilde d_i, \max(0, Q - \sum_{j \text{ ahead of } i} \tilde d_j)\}$ solves the fractional knapsack (CPP-F).

Standing assumptions (§3.3): the demands are independent and positive, and almost surely $\max_i \tilde d_i \le \Delta$ for a constant $\Delta > 0$ . The targets satisfy $0 \le \alpha_i \le 1$ .

Formalization targets

Goal: Theorem 5

Q^{\mathrm{Anti}}_I - Q^{\mathrm{Adap}}_I \le 2\Delta.

The bound is uniform in $N$ and in the joint law of the demands, subject only to the standing assumptions.

The two halves: Theorems 3 and 4

Q^{\mathrm{Anti}}_I \le Q_{II} + \Delta, \qquad Q^{\mathrm{Adap}}_I \ge Q_{II} - \Delta.

Milestones inside the proofs

Achievability of $\Gamma(Q)$ in fill rate by randomized priority orders (p. 21, from Zhong et al. 2018).
Structure of the greedy fill: it is fractional for at most one customer, and positive exactly when the demand ahead is below $Q$ (p. 17).
$\mathbf E[x^*_i]/\mathbf E[\tilde d_i] \le \mathbf P(x^*_i > 0)$ (p. 17).
Theorem 3.
The rounded adaptive policy $A'$ , which also serves the one customer the run turns away, satisfies $\mathbf E[\sum_{k\in U}\tilde d_k y^{A'}_k] \ge \sum_{k \in U} \mathbf E[\tilde d_k]\alpha_k$ (p. 37).
Adaptive feasibility of $Q$ implies $\alpha \in \Gamma(Q + \Delta)$ (p. 37). The page writes $Q^{\mathrm{Adpt}}_I$ , a misprint for $Q^{\mathrm{Adap}}_I$ .
Theorem 4.

Significance

The result. Theorem 5 says that the information an adaptive planner gains costs at most two maximal demands of capacity, independently of the number of customers. Anticipative priority rules are therefore near-optimal for Type-I service whenever individual demands are small relative to the pool. This contrasts with the responsive regime: Example 1 of the paper shows that $Q^{\mathrm{Adap}}_I$ can exceed $Q^{\mathrm{Resp}}_I$ by an unbounded factor. In Theorems 3–4 the Type-II capacity $Q_{II}$ serves as a common yardstick, so each policy class is compared with an explicitly computable polymatroid quantity.

Formalizing it. The theorem is proved on paper. To our knowledge none of it is machine-checked. A formal development has to make precise what the paper leaves informal: what a randomized adaptive policy is, why the event "customer $i$ is reached" is independent of $\tilde d_i$ , and why the infima defining the optimal capacities are over non-empty sets. The milestones on the greedy fill and the polymatroid $\Gamma(Q)$ can be reused for other fill-rate and persistency problems.

Difficulty

The obvious comparison fails because the two classes face different constraints. A Type-I requirement is an all-or-nothing event, so a deterministic priority order cannot hedge. With three identical unit-demand customers and targets $1/3$ , any fixed order needs $Q = 3$ , while $Q_{II} = 1$ . Randomization over orders is therefore essential on the anticipative side, and the link between a Type-I requirement and the Type-II region $\Gamma(Q)$ is not a statement about any single order. On the adaptive side, the decisions depend on revealed demands. Whether customer $k$ is fully served is correlated with $\tilde d_k$ , so a Type-I service probability does not translate directly into a bound on the expected demand served, which is what $\Gamma(Q)$ constrains. Conditioning arguments that ignore this correlation give false inequalities.

Formalization scope

Demands are a vector d : Fin N → Ω → ℝ on a probability space. Probabilities are μ.real, expectations are Bochner integrals. The standing assumptions are bundled in Standing μ d Δ α: measurable, iIndepFun, almost surely positive, almost surely ≤ Δ, 0 < Δ, and α i ∈ [0, 1].
A run has at most $N$ steps. A demand equal to the remaining capacity is served. Every run, anticipative ones included, stops at the first customer not fully served.
Adaptive policies are functions of the chosen list and the demand vector that depend only on the chosen customers' demands, with measurable decision events. Anticipative policies are permutations, embedded as adaptive policies that ignore the demands.
Randomized policies are finite mixtures. Service levels are probabilities, not the long-run scenario frequencies of p. 11.
$Q^{\mathrm{Adap}}_I$ , $Q^{\mathrm{Anti}}_I$ and $Q_{II}$ are real infima. Under the standing assumptions every feasible set is non-empty ( $Q = N\Delta$ works) and bounded below by $0$ , so no value is a junk default. $Q_{II}$ uses the subset form $\Gamma(Q)$ , which p. 17 shows equals the Type-II problem (CPP-B).
The greedy fill is stated for a priority order $\sigma$ rather than for weights $\theta'$ . It equals $x^*(\theta', \tilde d, Q)$ for every $\theta'$ whose decreasing order, ties broken by index, is $\sigma$ .
Two encodings would trivialize the goal, and both are excluded. Restricting to deterministic priority orders makes Theorem 3 false. Letting adaptive runs skip an oversized customer and continue enlarges the adaptive class beyond the paper's.

The infrastructure the proofs need: measurability of runs, independence of functions of disjoint coordinates, continuity of $Q \mapsto \mathbf E[\min(Q, S)]$ (so that $Q_{II}$ is attained), and the greedy description of a polymatroid's base polytope. Proofs of any milestone are welcome. So are alternative proofs of milestone 1 that avoid the general polymatroid theorem.

Selected references

G. Lyu, M. C. Chou, C.-P. Teo, Z. Zheng, Y. Zhong, Stochastic Knapsack Revisited: The Service Level Perspective, SSRN working paper 3674463, 2021. https://ssrn.com/abstract=3674463
Y. Zhong, Z. Zheng, M. C. Chou, C.-P. Teo, Resource Pooling and Allocation Policies to Deliver Differentiated Service, Management Science 64(4), 1555–1573, 2018.
A. Alptekinoğlu, A. Banerjee, A. Paul, N. Jain, Inventory Pooling to Deliver Differentiated Service, Manufacturing & Service Operations Management 15(1), 33–44, 2013.
B. C. Dean, M. X. Goemans, J. Vondrák, Approximating the Stochastic Knapsack Problem: The Benefit of Adaptivity, Mathematics of Operations Research 33(4), 945–964, 2008. https://doi.org/10.1287/moor.1080.0330

9 thms2 active usersReviewed

All missions

On properties of the space of quantum states and their application to construction of entanglement monotonesResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Attainability and lower semi-continuity of the relative entropy of entanglement, and variations on the themeResearch Paper

Motivation

What is formalized

Deferred results

Selected references

The Zero Set of a Real Analytic FunctionResearch Paper

Motivation

What is formalized

Selected references

The optimal unitary dilation for bosonic Gaussian channelsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Comparison of Quantum Channels by SuperchannelsResearch Paper

Motivation

What is formalized

Selected references

A Primal-Dual Smoothing Framework for Max-Structured Non-Convex Optimization: The Framework Returns an ε-Near-Stationary Point Within an Explicit Number of IterationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Brand Spillover as a Marketing Strategy: The Weak-Brand Firm Should Commit to Forgo Brand Spillover if and only if the Supplier Would Otherwise Drop It or the Insourcing Cost Is LowResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Decoding Quantum Tanner Codes: The Parallel Decoder Corrects Every Error of Weight Linear in the Code Length in Logarithmically Many RoundsResearch Paper

Why decoding good quantum LDPC codes matters

The code and the decoder

Formalization targets

Goal: Theorem 20 (= Theorem 3)

Milestones

Significance

Difficulty

Formalization scope

Selected references

High-Dimensional Learning Under Approximate Sparsity with Applications to Nonsmooth Estimation and Regularized Neural Networks: Excess-Risk Bounds at S3ONC Solutions of MCP-Regularized M-EstimationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 18)

Milestones (the paper's proof chain)

Significance

Difficulty

Formalization scope

Selected references

On Co-opetitive Supply Partnerships with End-Product Rivals: Information Asymmetry, Dual Sourcing and Supply Market Efficiency: The Equilibrium Wholesale Price and When the VI Buys InformationResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Quality Regulation on Two-Sided Platforms: Exclusion, Subsidization, and First-Party Applications: Exclusion Is a Special Case of Subsidization and Is Dominated by ItResearch Paper

Why platform quality rules matter

Market and decisions

Formalization targets

What the comparison establishes

Why the target is difficult