Missions · Prove2Me

Operations Research Probability Reinforcement Learning+1·Captain: mikedeng1

Asynchronous Stochastic Approximation and Q-Learning 2: Asynchronous Stochastic Approximation with Outdated Information Converges with Probability 1 Under a Weighted Maximum Norm ContractionResearch Paper

Motivation

Many iterative algorithms update only part of a vector at a time. In a parallel implementation, one processor may read a value written several rounds earlier by another processor. Random observations also perturb each update. John N. Tsitsiklis's 1994 paper gives conditions under which such an asynchronous stochastic iteration still converges. The paper develops the result to analyze Q-learning, where state-action values are revised from sampled costs and successor states. Its general theorem also applies to iterative fixed-point calculations beyond that application.

The central issue is that a processor can choose which component to update after seeing the past, and its input can be stale. A convergence theorem that presumes a fixed update schedule or current data would miss both features. The paper's Assumptions 1–3 describe when delays, sampling noise, and random step sizes remain compatible with almost-sure convergence. Assumption 5 gives a weighted maximum norm contraction for the iteration map. Theorem 3 combines these conditions into the target of this mission.

Setting

Fix a positive integer $n$ and write $x(t)\in\mathbb R^n$ for the vector after round $t\ge0$ . Let $F:\mathbb R^n\to\mathbb R^n$ be the map whose fixed point the iteration seeks. For component $i$ , the step size $\alpha_i(t)$ lies in $[0,1]$ , the noise is $w_i(t)$ , and $\tau^i_j(t)\le t$ is the time from which component $j$ was read. Thus $x^i(t)$ has coordinates $x_j(\tau^i_j(t))$ . With $\alpha_i(t)=0$ when component $i$ is idle, all rounds obey the single update equation

x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr).

All quantities live on a probability space with law $\mathsf P$ . The increasing filtration $\mathcal F(t)$ represents information available when the step sizes and delays are selected, before the round's noise is observed. Assumption 1 says every timestamp $\tau^i_j(t)$ tends to infinity almost surely: no fixed old value remains in use forever. Assumption 2 makes the initial state, chosen step sizes, delays, and noise measurable at the specified times; the noise has conditional mean zero, and its conditional second moment is bounded by a deterministic affine function of the largest squared iterate seen so far. Assumption 3 requires, for each component, divergent total step size and a square-summable step-size sequence, with a deterministic bound on all squared partial sums.

For a vector $v$ with strictly positive coordinates, the weighted maximum norm is $\|z\|_v=\max_i |z_i|/v_i$ . Assumption 5 provides $x^*\in\mathbb R^n$ and $\beta\in[0,1)$ such that $\|F(x)-x^*\|_v\le\beta\|x-x^*\|_v$ for every $x$ . Assumption 6, used in the boundedness milestone, requires the related growth bound $\|F(x)\|_v\le\beta\|x\|_v+D$ for some real $D$ . The weighted norm permits different component scales.

Formalization targets

Boundedness under a weighted growth bound

Theorem 1 is the main intermediate target. Under Assumptions 1, 2, 3, and 6, it asserts

\mathsf P\!\left(\exists M\in\mathbb R\;\forall t,i,\ |x_i(t)|\le M\right)=1.

The bound $M$ may depend on the sample path. Lemmas 1–3 of the paper are milestones in its analysis: a scalar noisy recursion converges, its tails become uniformly small, and the pathwise bounds in the contradiction step hold.

Almost-sure convergence under a weighted contraction

The goal is Theorem 3, under Assumptions 1, 2, 3, and 5:

\mathsf P\!\left(\lim_{t\to\infty}x(t)=x^*\right)=1.

This theorem does not assume bounded iterates or Assumption 6 separately. Its proof uses Theorem 1 after deriving the needed growth bound from the contraction condition. Lemma 8 is the remaining milestone, comparing the coordinate iterates to an auxiliary deterministic recursion and a noise tail.

Significance

The result gives a fixed-point convergence guarantee when coordinates update at different times, delays can vary, and update choices can depend on past observations. In the paper's Q-learning application, these features describe exploratory sampling and possible parallel computation with old state-action values. For discounted problems, the associated Q-learning map contracts in the maximum norm, so Theorem 3 supplies the convergence step once the stochastic assumptions are checked (Tsitsiklis 1994, §7).

The mathematical results were proved in 1994; this mission asks for machine-checked proofs of their formal statements. Its reusable output would include a model of asynchronous noisy iteration, a scalar martingale-noise convergence lemma with random conditional variance bounds, and a precise interface between weighted contractions and pathwise convergence. The goal and milestone theorem files are currently statements with proof holes, while the definition file compiles without one.

Difficulty

A coordinate's next value depends on a vector assembled from observations at several earlier times. A direct estimate against the current error therefore does not close: the stale coordinates can reflect larger past errors. The noise condition is also tied to the largest iterate seen so far, so a deterministic global variance bound is unavailable before boundedness has been established. These two dependencies make the ordinary synchronous contraction argument insufficient. The scalar noise result and the pathwise comparison lemmas isolate the conditions needed for the boundedness and convergence statements.

Formalization scope

Vectors are functions Fin n → ℝ, with $n>0$ ; the source labels coordinates $1,\ldots,n$ , while Fin n starts at zero. Function order is componentwise. The model sets $\alpha_i(t)=0$ on idle rounds and uses the paper's unified update equation. It does not store the sets of update times separately. The delay values on idle rounds are left arbitrary because they do not affect the update; the source chooses the current time there. All step sizes lie in $[0,1]$ , and all delays are at most the current time, on every sample path.

The probability law is a probability measure. The filtration consists of increasing sub-σ-algebras. The iterate sequence is explicitly assumed adapted in the main theorems, matching the paper's use of $x(t)$ and its running maximum as $\mathcal F(t)$ -measurable random variables. Conditional moment assumptions use integral inequalities over measurable sets, allowing generalized conditional expectations when the noise need not have a finite unconditional second moment. The conditional upper bound is required nonnegative almost surely, as the original inequality entails. Divergence and square summability use partial sums, so a non-summable series cannot receive a default value.

The maximum norm is the finite supremum of coordinate absolute values, and the weighted norm divides by the strictly positive coordinates of $v$ . Almost-sure boundedness means a path-dependent finite bound on every coordinate and time. Pathwise Lemmas 3 and 8 are stated on a retained sample path, with the auxiliary quantities and hypotheses established at their locations in the paper; Lemma 8 uses the proof's translated and rescaled coordinates. These conventions rule out an empty coordinate type, junk integrals, and a vacuous boundedness claim. Contributions to the stated lemmas, their probabilistic infrastructure, and the final convergence proof are within scope.

Selected references

John N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. DOI: 10.1023/A:1022689125041.

7 thms2 active usersReviewed

Operations Research Probability Reinforcement Learning+1·Captain: mikedeng1

Asynchronous Stochastic Approximation and Q-Learning 1: Bounded Asynchronous Stochastic Approximation Iterates Converge with Probability 1 to the Unique Fixed Point of a Monotone Continuous MapResearch Paper

Motivation

Q-learning (Watkins, 1989) learns the optimal action values of a Markov decision problem from sampled transitions, without a model of the transition probabilities. At each step only one state–action pair is updated, with a noisy estimate of the Bellman operator evaluated at possibly outdated values of the other pairs. Watkins and Dayan (1992) gave a first convergence proof for discounted problems. Tsitsiklis (1994) and, independently, Jaakkola, Jordan and Singh (1994) placed Q-learning inside the theory of stochastic approximation: the Robbins–Monro scheme of iterating $x \leftarrow x + \alpha\,(F(x) - x + w)$ with decreasing stepsizes and zero-mean noise, here in an asynchronous form where different components are updated at different times using delayed information, as in the distributed iterations of Bertsekas and Tsitsiklis (1989).

Tsitsiklis's paper proves convergence with probability 1 under two structural hypotheses on the iteration mapping $F$ : a weighted maximum-norm contraction (Theorem 3), which covers discounted Q-learning, and monotonicity (Theorem 2), which covers undiscounted (stochastic shortest path) problems, whose Bellman operator is monotone but in general not a contraction. This mission formalizes the monotone case.

Setting

A mapping $F:\mathbb R^n\to\mathbb R^n$ with components $F_1,\dots,F_n$ is given, and the goal is to solve $F(x)=x$ . Time is discrete, $t=0,1,2,\dots$ . The iterate $x(t)\in\mathbb R^n$ evolves by

x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr),\qquad x^i(t)=\bigl(x_1(\tau^i_1(t)),\dots,x_n(\tau^i_n(t))\bigr),

where $\alpha_i(t)\in[0,1]$ is a stepsize ( $\alpha_i(t)=0$ when component $i$ is not updated), $w_i(t)$ is noise, and $0\le\tau^i_j(t)\le t$ are delays: the update of component $i$ may read component $j$ as it was at an earlier time. All quantities are random variables on a probability space $(\Omega,\mathcal F,P)$ with an increasing sequence of σ-fields $\{\mathcal F(t)\}$ , the history up to the choice of the stepsizes at time $t$ .

Vector inequalities are componentwise and $e$ is the vector of ones. The paper's assumptions are:

Assumption 1: every delay index $\tau^i_j(t)$ tends to infinity, with probability 1.
Assumption 2: $x(0)$ , $\alpha_i(t)$ , $\tau^i_j(t)$ are $\mathcal F(t)$ -measurable and $w_i(t)$ is $\mathcal F(t+1)$ -measurable; $E[w_i(t)\mid\mathcal F(t)]=0$ ; and $E[w_i^2(t)\mid\mathcal F(t)]\le A+B\max_j\max_{\tau\le t}|x_j(\tau)|^2$ for deterministic constants $A,B$ .
Assumption 3: $\sum_t\alpha_i(t)=\infty$ and $\sum_t\alpha_i^2(t)\le C$ with probability 1, for a deterministic $C$ .
Assumption 4: $F$ is monotone ( $x\le y\Rightarrow F(x)\le F(y)$ ), continuous, has a unique fixed point $x^*$ , and $F(x)-re\le F(x-re)\le F(x+re)\le F(x)+re$ for all $x$ and all $r>0$ .

In Lean the algorithm is the structure AsyncSA.Monotone.Algorithm with fields F, x, α, w, τ, and the assumptions are Assumption1–Assumption4.

Formalization targets

Goal: Theorem 2 (p. 189)

Under Assumptions 1–4, if $x(t)$ is bounded with probability 1, then

\lim_{t\to\infty}x(t)=x^*\qquad\text{with probability 1.}

Boundedness is a hypothesis, not a conclusion: for monotone $F$ it must be established separately (the paper does so for Q-learning in §7). The bound may differ between sample paths.

Milestones

Lemma 1 (p. 190): for a scalar recursion $W(t+1)=(1-\alpha(t))W(t)+\alpha(t)w(t)$ with martingale-difference noise whose conditional variance is bounded by an a.s. bounded $B(t)$ , and stepsizes with $\sum\alpha=\infty$ , $\sum\alpha^2\le C$ , $W(t)\to0$ with probability 1.
Lemma 4 (p. 193): the sequences $U^{k+1}=(U^k+F(U^k))/2$ , $U^0=x^*+re$ , and $L^{k+1}=(L^k+F(L^k))/2$ , $L^0=x^*-re$ , satisfy $F(U^k)\le U^{k+1}\le U^k$ and $F(L^k)\ge L^{k+1}\ge L^k$ .
Lemma 5 (p. 193): $U^k\to x^*$ and $L^k\to x^*$ .
Lemma 6 (p. 194): on a sample path where $L^k\le x(t)\le U^k$ from time $t_k$ on and all delays exceed $t_k$ from time $t'_k$ on, $x_i(t)\le X_i(t)+W_i(t;t'_k)$ , where $X_i$ relaxes from $U^k_i$ towards $F_i(U^k)$ and $W_i(t;t'_k)$ accumulates the noise from $t'_k$ .
Lemma 7 (p. 195): under the choices of $\delta_k$ and $t''_k$ made on pp. 194–195, $x_i(t)\le U^{k+1}_i$ for all $t\ge t''_k$ .

Significance

Theorem 2 is the convergence result for asynchronous stochastic approximation driven by a monotone mapping whose fixed point is unique. Its main application is Q-learning for stochastic shortest path problems with improper policies excluded, and more generally any learning scheme whose expected update is a monotone, sup-norm nonexpansive operator in the sense of (7) (dynamic programming operators are the standard examples). The same pattern, an a.s. bounded iterate plus a monotone mean map, recurs in later analyses of asynchronous and distributed learning algorithms.

The result has a published proof but, as far as the platform's catalog shows, no machine-checked one: there is no formalized asynchronous stochastic approximation theorem, and no formal Lemma 1 for random stepsizes and random conditional-variance bounds. A complete development provides the scalar almost-sure convergence lemma, the deterministic envelope argument for monotone maps, and the pathwise comparison steps, each of which is reusable.

Difficulty

The noise has a conditional variance that grows with the iterate, so it is neither bounded nor integrable a priori, and the stepsizes are random and chosen adaptively. The classical deterministic-bound argument for Lemma 1 does not apply directly. The iteration is not a contraction in any norm, so there is no Lyapunov function giving a geometric decrease, and the delays mean that the mapping is evaluated at a vector no single time index describes. Convergence has to be propagated from the deterministic envelopes $U^k,L^k$ to the random iterate through a sequence of random times, one envelope at a time, and each step requires the noise accumulated after a random time to be small uniformly in the remaining horizon.

Formalization scope

Components are Fin n (0-based); vectors are Fin n → ℝ with the componentwise order, so Monotone F is Assumption 4(a) exactly. $re$ is r • 1.
The update is stated in the paper's unified form for every $t$ , with $\alpha_i(t)=0$ off the update times; the update sets $T^i$ are not represented. The paper sets $\tau^i_j(t)=t$ off $T^i$ ; the formalization leaves $\tau^i_j(t)$ free there, which is more general. $\alpha_i(t)\in[0,1]$ and $\tau^i_j(t)\le t$ hold on every sample path.
Conditional expectations are generalized, written with set integrals (CondMeanZero, CondSqLe): $\int_S w\,dP=0$ for every $\mathcal F(t)$ -set $S$ on which $w$ is integrable, and $\int_S w^2\,dP\le\int_S g^+\,dP$ in $[0,\infty]$ . Mathlib's condExp is not used: it is $0$ for non-integrable functions and would make the noise assumptions vacuous.
Series conditions use partial sums (divergence to $+\infty$ ; every partial sum at most $C$ ), never tsum, which is $0$ for non-summable sequences. The constants $A,B,C$ are chosen before the almost-sure quantifier; the bound on $x(t)$ is chosen after it.
The paper treats $x(t)$ as determined by $\mathcal F(t)$ and uses this implicitly; Theorem 2 assumes it explicitly (Adapted).
Lemma 1 leaves $W(0)$ unconstrained, as on the page. Lemmas 4 and 5 hold for every $r>0$ . Lemmas 6 and 7 are pathwise: they fix one sample path and take the induction's objects ( $k$ , $t_k$ , $t'_k$ , $t''_k$ , $X$ , $\delta_k$ ) as given with exactly the properties the paper has established for them; they are not existential statements about these times.
A trivializing formalization (junk conditional expectations, tsum for the series, a deterministic bound on $x(t)$ , or a second unrelated $x^*$ ) is ruled out by the choices above.

Contributions welcome: a general almost-sure convergence theorem for Robbins–Monro recursions with generalized conditional moments (Lemma 1 and its tail version $W(t;t_0)$ ), and lemmas on monotone maps satisfying (7).

Selected references

J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994) 185–202. https://doi.org/10.1023/A:1022689125041
C. J. C. H. Watkins and P. Dayan, Q-learning, Machine Learning 8 (1992) 279–292. https://doi.org/10.1007/BF00992698
T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994) 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://hdl.handle.net/1721.1/3719
B. T. Poljak and Ya. Z. Tsypkin, Pseudogradient adaptation and training algorithms, Automation and Remote Control 34 (1973) 377–397.
H. Robbins and S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

7 thms2 active usersReviewed

Completed

Analysis Operations Research Optimization·Captain: mikedeng1

Vertical Integration and Antitrust Policy: Integrating Successive Monopolies Lowers the Final Price and Raises Output, Joint Profit and Consumer SurplusResearch Paper

Motivation

In 1950 the United States Supreme Court appeared to be moving toward treating corporate integration, horizontal or vertical, as illegal per se under the antitrust laws. Joseph J. Spengler's note in the Journal of Political Economy argued that this conflates two different things: horizontal integration can suppress competition, but vertical integration, the joining of successive stages of production under one owner, can lower prices when the stages are already imperfectly competitive. The note is the standard origin of what industrial organization now calls double marginalization: when a monopolist upstream sells to a monopolist downstream, each adds its own markup, and the final price is higher than a single integrated monopolist would charge.

The argument underlies the modern economics of vertical mergers and vertical restraints (resale price maintenance, two-part tariffs, franchise fees) and the supply-chain coordination literature in operations research, where a wholesale-price contract between a supplier and a retailer reproduces the same distortion.

A short timeline: Cournot (1838, Chapter IX) analysed complementary monopolists selling inputs to a common product; Spengler (1950) gave the successive-monopoly version and drew the antitrust conclusion; Tirole's textbook (1988, §4.2) made it the canonical example of vertical externalities; Cachon and Lariviere (2005) and the coordination literature studied the same inefficiency in newsvendor supply chains.

Setting

A product passes through three successive stages $A\to B\to C$ before reaching consumers. Production uses fixed proportions: one unit of stage A's product goes into one unit of B's, and one unit of B's into one unit of C's, so all stages handle the same quantity. Each stage has a constant unit variable cost $V_a,V_b,V_c$ (marginal cost equal to average variable cost at every relevant output).

Final demand is a function $D:\mathbb R\to\mathbb R$ : $D(p)$ units of $C$ are bought at price $p$ . A firm with constant unit cost $c$ that sells at price $p$ earns the profit (return above variable outlay)

\pi_c(p)=(p-c)\,D(p),

and $p$ is a profit-maximizing price at cost $c$ when $\pi_c(x)\le\pi_c(p)$ for every $x$ .

Unintegrated chain. Stage A sells to B at a transfer price $P_a$ , B sells to C at $P_b$ . Their per-unit profits are $R_a=P_a-V_a$ and $R_b=P_b-(V_b+P_a)$ ; horizontal integration within each stage lets these be positive "monopolistic surcharges". Stage C's unit cost is $C_c=V_c+P_b$ ; it charges a profit-maximizing price $P_c$ at that cost and sells $Q=D(P_c)$ . The chain's aggregate profit is $R_aQ+R_bQ+R_cQ$ with $R_c=P_c-(V_c+P_b)$ .

Integrated firm. One firm owns all three stages. Its unit cost is $C'_c=V_a+V_b+V_c$ ; it charges a profit-maximizing price $P'_c$ at that cost and sells $Q'=D(P'_c)$ , earning $(P'_c-C'_c)\,Q'$ .

The price elasticity of demand at $p$ is $e(p)=-p\,D'(p)/D(p)$ (positive for a downward-sloping curve) and the marginal revenue is $r(p)=p+D(p)/D'(p)$ . The consumers' surplus gained when the price falls from $P_c$ to $P'_c$ is $\int_{P'_c}^{P_c}D(x)\,dx$ .

Formalization targets

Goal: vertical integration benefits producer and consumer

For every non-increasing demand curve $D$ , all unit costs $V_a,V_b,V_c$ , and all transfer prices with $R_a>0$ , $R_b>0$ , if $P_c$ is profit-maximizing at cost $V_c+P_b$ , $P'_c$ is profit-maximizing at cost $V_a+V_b+V_c$ , $D$ is differentiable at $P_c$ and $Q=D(P_c)>0$ , then

P'_c<P_c,\qquad D(P_c)<D(P'_c),\qquad R_aQ+R_bQ+R_cQ<(P'_c-C'_c)\,Q',

0<\int_{P'_c}^{P_c}D(x)\,dx,\qquad Q\,(P_c-P'_c)\le\int_{P'_c}^{P_c}D(x)\,dx.

The goal fixes no functional form and no numbers; it is the general statement behind the paper's "under all cases conceivable … within the framework here employed".

Milestones

Footnote 6, equilibrium identities. At a profit-maximizing price, $r=c$ , $e=p/(p-r)=p/(p-c)$ , and $p=c\,e/(e-1)$ when $c\ne0$ .
Section III, unitary elasticity. At zero cost, $e=1$ ; at positive cost, $p>c$ and $e>1$ .
Section III, cost raises price. For $c_1<c_2$ , profit-maximizing prices satisfy $D(p_2)\le D(p_1)$ , and $p_1<p_2$ under the goal's regularity hypotheses.
Footnote 6, straight-line demand. For $D(p)=b(a-p)$ : $p^*(c)=(a+c)/2$ , $\Delta r=2\Delta p$ , $e(p^*(c))=(a+c)/(a-c)$ , the elasticity rises relatively more than the price, and the relative rise grows with $c$ .
Figure 1. With $D_c(p)=\tfrac85(140-p)$ and $V_a=V_b=V_c=20$ : $P_c=115$ , $Q=40$ , aggregate profit $2{,}200$ ; $P'_c=100$ , $Q'=64$ , profit $2{,}560$ ; consumers' surplus rises by $780$ .

Significance

The result. The theorem shows that removing an upstream markup can only lower the final price and raise output, so that producers and consumers gain together. This is the economic content of the rule that vertical integration is not anticompetitive as such, and it is the reason modern merger guidelines credit the "elimination of double marginalization" as an efficiency of vertical mergers. Milestone 3, monotonicity of the monopoly price in cost, is the general comparative-statics fact used in tax incidence and cost pass-through.

Formalizing it. The result is classical and proved in every industrial-organization textbook, usually for linear demand. The mission states it for an arbitrary non-increasing demand curve, without concavity, continuity or uniqueness of the profit maximizer, which makes explicit which hypotheses the strict conclusions actually need. Related items on the platform formalize double marginalization in a different model, the newsvendor wholesale-price contract of Cachon and Lariviere, where the supplier-induced order quantity falls short of the integrated one; this mission covers the price-setting, deterministic-demand version.

Difficulty

The weak inequalities ( $P'_c\le P_c$ , $Q\le Q'$ , profit $\le$ ) follow from comparing the two maximization problems (the price comparison also uses $Q>0$ : if $D\equiv 0$ , every price is profit-maximizing). The strict inequalities do not: a demand curve with a kink can have the same profit-maximizing price at two different costs, so integration need not change the price at all. The strict claims therefore need a first-order condition at $P_c$ , and the argument has to combine global optimality (all prices) with local information (a derivative at one point) without assuming the profit function is concave or the maximizer unique. The consumers'-surplus clause requires a lower bound on an integral of a monotone, possibly discontinuous function.

Formalization scope

Prices, costs and quantities are real numbers; maximization is over all prices $p\in\mathbb R$ . Demand is a function $D:\mathbb R\to\mathbb R$ ; the goal assumes only that it is non-increasing (Antitone D).
Profit-maximizing prices are hypotheses (IsProfitMax D c p), never closed forms; the closed form $(a+c)/2$ appears only for straight-line demand.
The transfer prices $P_a,P_b$ are arbitrary data with positive markups; they need not be profit-maximizing for $D_a,D_b$ , which the paper draws only in its figure.
Explicit readings of the paper's prose. "Benefits both producer and consumer" and "will lower the price" become the four strict inequalities of the goal. "Aggregate profit" is the sum over the three stages, $Q[P_c-(V_a+V_b+V_c)]$ , not stage C's profit alone. Consumers' surplus "in the Marshallian sense" is the interval integral of $D$ between the two prices; footnote 5's trapezoid formula is used only for the straight line of Figure 1. Elasticity is a positive number $-pD'(p)/D(p)$ . "Relatively greater increment in the elasticity" is made exact for straight-line demand as $e(p^*(c'))/e(p^*(c))>p^*(c')/p^*(c)$ ; the literal $\Delta e/e>\Delta c/c$ is false for small $c$ . Footnote 6's $e'=(p+\Delta p)/(p-2\Delta p)$ and "approximating $3\Delta p/p$ " are a printed slip; the exact $e(p^*(c))=(a+c)/(a-c)$ is stated instead, and no approximation is formalized. Figure 1's demand line $D_c(p)=\tfrac85(140-p)$ is the line through the three points the text gives.
Added hypotheses. Differentiability of $D$ at $P_c$ and $D(P_c)>0$ , which the paper's marginal-revenue reasoning presupposes. Every statement involving elasticity or marginal revenue carries differentiability and positive demand, because Lean's deriv and division return $0$ on bad input.
Ruled out. Formalizations that hard-code linear demand in the goal, compare the integrated profit with stage C's profit alone, or prove only the weak ( $\le$ ) inequalities do not capture the result.
Sections IV and the policy remarks of Section III (rent evasion, taxes, co-operatives) are not formalized.
Only Mathlib is needed: Fermat's rule (IsLocalMax.hasDerivAt_eq_zero), interval integrals of monotone functions, and real arithmetic. Proofs of the general milestones are reusable for any monopoly-pricing comparative statics.

Selected references

J. J. Spengler, Vertical integration and antitrust policy, Journal of Political Economy 58(4), 1950, 347–352. https://doi.org/10.1086/256964
A. A. Cournot, Recherches sur les principes mathématiques de la théorie des richesses, Hachette, 1838, Chapter IX.
J. Tirole, The Theory of Industrial Organization, MIT Press, 1988, §4.2.
G. P. Cachon and M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

7 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Theoretical Computer Science·Captain: mikedeng1

A Theorem on Boolean Matrices: Warshall's Construction M* Equals the Boolean Sum M ∨ M² ∨ ⋯ ∨ Mᵈ of the Boolean Powers of MResearch Paper

Motivation

A finite directed graph on $d$ vertices is recorded by its adjacency matrix, a $d \times d$ array of zeros and ones. Many questions about the graph are questions about reachability: can vertex $j$ be reached from vertex $i$ by following one or more edges? In the late 1950s this question arose in the analysis of programs. Prosser (Applications of Boolean matrices to the analysis of flow diagrams, 1959) represented the flow diagram of a program by a boolean matrix and read off properties such as which blocks can follow which; Marimont (A new method of checking the consistency of precedence matrices, J. ACM 1959) used the same matrices to check precedence relations for consistency.

In both works the reachability matrix is described as a boolean sum of boolean powers of the adjacency matrix. Computed that way, it costs $d$ boolean matrix products, that is on the order of $d^3$ operations per product. Stephen Warshall's two-page note (A theorem on Boolean matrices, J. ACM 9 (1962) 11–12) proves that a much shorter procedure, $d$ passes of row updates performed in place, gives the same matrix. The same procedure was published in the same year by Floyd as Algorithm 96: Ancestor (Comm. ACM 5 (1962) 344), and its weighted version is Floyd's Algorithm 97: Shortest Path. The procedure is now taught as the Floyd–Warshall or Roy–Warshall algorithm.

Timeline. 1959: Prosser and Marimont describe reachability as a sum of boolean powers. 1959: Roy publishes the same closure construction in French (C. R. Acad. Sci. Paris 249). 1962: Warshall's note proves the in-place construction correct; Floyd's Algorithm 96 publishes it as code, and Algorithm 97 extends it to shortest paths.

Setting

Fix a natural number $d$ and let $M = (m_{ij})$ be a $d \times d$ matrix each of whose entries is $0$ or $1$ .

The boolean product of two such matrices $A$ and $B$ is the matrix $A \wedge B$ with $(A \wedge B)_{ij} = \bigvee_k (a_{ik} \wedge b_{kj})$ : the entry is $1$ when some index $k$ has $a_{ik} = b_{kj} = 1$ .
The boolean sum $A \vee B$ is the entrywise disjunction, $(A \vee B)_{ij} = a_{ij} \vee b_{ij}$ .
The boolean powers are $M^1 = M$ and $M^{p+1} = M^p \wedge M$ .
The introduction's matrix is the power sum

M' \;=\; \bigvee_{p=1}^{d} M^p .

The THEOREM defines $M'$ instead by chains: $m'_{ij} = 1$ if and only if either $m_{ij} = 1$ or there are indices $k_1, \dots, k_n$ with $m_{ik_1} = m_{k_1k_2} = \cdots = m_{k_nj} = 1$ . Footnote 2 states that the two definitions agree.
Warshall's construction $M^*$ : set $M^* = M$ ; for $i = 1, \dots, d$ in turn, for every row $j$ with $m^*_{ji} = 1$ and every column $k$ , set $m^*_{jk} = m^*_{jk} \vee m^*_{ik}$ . Entries are overwritten during a pass and later steps of the same pass read the new values.
Footnote 3 gives a recursive version: $(m_{ij})_0 = m_{ij}$ and $(m_{ij})_{n+1} = (m_{ij})_n \vee \bigl((m_{i,n+1})_n \wedge (m_{n+1,j})_n\bigr)$ , and asserts $m^*_{ij} = (m_{ij})_d$ .

In Lean the matrix is M : Fin d → Fin d → Bool. The power sum is powerSum M, the chain relation ChainRel M i j, the recursion warshallRec M n, all in the namespace WarshallBool.Closure. The construction $M^*$ is the published FloydAlgorithms.ShortestPath.algorithm96 M.

Formalization targets

Goal: the construction computes the power sum

M^* \;=\; \bigvee_{p=1}^{d} M^p \qquad \text{for every } d \text{ and every } d \times d \text{ 0-1 matrix } M .

This is the transformation the introduction asks for, combined with the THEOREM's assertion $M^* = M'$ and footnote 2. The goal has no hypothesis beyond the shape of $M$ .

Milestone 1 (Proved, referenced): the THEOREM

m^*_{ij} = 1 \iff m_{ij} = 1 \text{ or } m_{ik_1} = \cdots = m_{k_nj} = 1 \text{ for some } k_1, \dots, k_n .

It is already on the platform as FloydAlgorithms.ShortestPath.algorithm96_eq_transGen, stated with Mathlib's transitive closure Relation.TransGen, and it is not posed again.

Milestone 2: footnote 2

m_{ij} = 1 \text{ or a chain } i \to k_1 \to \cdots \to k_n \to j \text{ of 1 entries} \iff \Bigl(\bigvee_{p=1}^{d} M^p\Bigr)_{ij} = 1 .

Companion: footnote 3

M^* \;=\; \bigl((m_{ij})_d\bigr)_{i,j} .

This is not a milestone of the goal; it identifies the in-place construction with its stage-by-stage recursion.

Significance

The result. The theorem says that reachability in a directed graph on $d$ vertices, defined through matrix powers, can be computed by $d$ passes of in-place row operations, on the order of $d^2$ row updates instead of $d$ full boolean matrix products. The same scheme, with $(\min, +)$ in place of $(\vee, \wedge)$ , is the Floyd–Warshall shortest-path algorithm; with other semirings it computes regular expressions of finite automata (Kleene, McNaughton–Yamada) and path problems in general. Footnote 3's recursion is the form in which the algorithm is usually proved correct today, and its equivalence with the in-place version is what justifies running it without a second copy of the matrix.

Formalizing it. The chain form of the THEOREM is already machine-checked on Prove2Me (algorithm96_eq_transGen). What this mission adds is the statement in the paper's own terms: the introduction's power sum $\bigvee_{p=1}^d M^p$ , footnote 2's equivalence between powers and chains, which requires that chains can be shortened to length at most $d$ , and footnote 3's in-place versus recursive equivalence. None of these three is on the platform. The paper itself proves only the THEOREM; footnotes 2 and 3 are stated without proof.

Difficulty

Footnote 2 calls the equivalence "trivial", but one direction needs a pigeonhole argument: a chain $i \to k_1 \to \cdots \to k_n \to j$ of arbitrary length witnesses some power $M^{n+1}$ , and the power sum stops at $M^d$ . A chain with repeated indices has to be shortened, and the shortening must keep at least one step, since there is no reflexive part ( $m'_{ii} = 1$ only through a cycle). For a $d$ -cycle the diagonal entries appear only in $M^d$ , so the range $1..d$ is exact.

Footnote 3 compares two computations that read different data. The construction overwrites entries during a pass, and later steps of the same pass read the overwritten values; the recursion reads only the previous stage. The two agree only because of what a pass does and does not overwrite, and the published algorithm96 is three nested left folds over List.finRange, so the comparison has to be made against that concrete loop structure rather than an idealized simultaneous update.

Formalization scope

Matrices are Fin d → Fin d → Bool, with $1$ as true. Indices are $0, \dots, d-1$ instead of the page's $1, \dots, d$ ; the pivot of pass $i$ (1-based) is the 0-based index $i-1$ .
$d = 0$ is allowed; all statements are then trivially true, as on the page.
The boolean product boolProd A B i j is decide (∃ k, A i k = true ∧ B k j = true). Mathlib's matrix product on Matrix (Fin d) (Fin d) Bool is not the boolean product: Bool is a boolean ring there, its addition is exclusive or, and that product counts walks modulo 2. A formalization through * or ^ on Matrix _ _ Bool states a different, false theorem and is ruled out.
boolPow M p is the page's $M^p$ for $p \ge 1$ ; the base boolPow M 0 is the identity matrix, which is not on the page and does not enter the sum. powerSum M i j holds iff boolPow M p i j for some $p \in \{1, \dots, d\}$ . No reflexive closure is included anywhere.
ChainRel M i j is the existence of a list $[k_1, \dots, k_n]$ (possibly empty) making $i, k_1, \dots, k_n, j$ a List.IsChain of true entries.
warshallRec M n uses the 0-based pivot $n$ at stage $n+1$ and is constant after stage $d$ , which footnote 3 never uses.
$M^*$ is the published algorithm96, which fixes the inner loops over rows and columns in ascending order; Warshall leaves that order open, and it does not affect the result.
The goal must not be stated through TransGen, ChainRel or warshallRec, and powerSum is defined from boolPow, not from the closure or the algorithm.

Reusable beyond this mission: the boolean matrix product and powers, the power-sum characterization of the transitive closure of a relation on Fin d (footnote 2), and the in-place/recursive equivalence (footnote 3), which carries over to Floyd's Algorithm 97. Proofs of milestone 2 and of the companion are welcome independently of the goal.

Selected references

S. Warshall, A theorem on Boolean matrices, J. ACM 9(1) (1962) 11–12. https://doi.org/10.1145/321105.321107
R. W. Floyd, Algorithm 96: Ancestor, Comm. ACM 5(6) (1962) 344–345. https://doi.org/10.1145/367766.368166
R. W. Floyd, Algorithm 97: Shortest path, Comm. ACM 5(6) (1962) 345. https://doi.org/10.1145/367766.368168
R. T. Prosser, Applications of Boolean matrices to the analysis of flow diagrams, Proc. Eastern Joint Computer Conference (1959) 133–138. https://doi.org/10.1145/1460299.1460314
R. B. Marimont, A new method of checking the consistency of precedence matrices, J. ACM 6(2) (1959) 164–171. https://doi.org/10.1145/320964.320975
B. Roy, Transitivité et connexité, C. R. Acad. Sci. Paris 249 (1959) 216–218.

5 thms2 active usersReviewed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

On Cores and Indivisibility 1: The Housing Market's Game Without Side Payments Is BalancedResearch Paper

Motivation

A market in which each trader owns one indivisible good has a basic coordination question: can all goods be reassigned so that no group of traders can withdraw its own goods and improve every member's outcome? Houses are the paper's running example. Monetary transfers and fractional houses are absent, so ordinary convex allocation arguments do not describe the setting. Shapley and Scarf use games without side payments to express what each coalition of owners can achieve, and identify a balance property of this game in their Section 4 theorem (Shapley and Scarf, 1974).

The paper states that a general balanced-game theorem gives a nonempty core once balance has been established. Its Section 4 contribution is the classification of this particular housing market game. The separate top-trading-cycles construction in Section 6 gives another route to a core allocation and is the subject of the second mission in this series (Shapley and Scarf, 1974).

Setting

Let $N$ be a nonempty finite set of traders. Trader $j$ brings one indivisible item $j$ . Trader $i$ 's ranking of item $j$ is represented by a real number $a_{ij}$ . Only comparisons within one trader's row matter: $a_{ij}>a_{ik}$ means that $i$ prefers $j$ to $k$ , while equality represents indifference. No strict-preference or positivity assumption is imposed on the preference matrix $A=(a_{ij})$ .

A coalition $S\subseteq N$ can redistribute the items brought by its members. Its allocation matrix $P$ has $P_{ij}=1$ when trader $i$ receives item $j$ , and zero otherwise. An $S$ -allocation puts exactly one 1 in each column indexed by $S$ and has zeros in rows and columns outside $S$ . An $S$ -permutation is an $S$ -allocation with row sums at most one, so every member of $S$ receives exactly one of the coalition's items. Rows index traders and columns index items.

For a proposed payoff vector $x\in\mathbb R^N$ , define the acceptability matrix

b_{S|ij}(x)= \begin{cases} 1,& i\in S\text{ and }x_i\le a_{ij},\\ 0,&\text{otherwise}. \end{cases}

The coalition payoff set is

V(S)=\{x\in\mathbb R^N:\text{some }S\text{-permutation }P \text{ satisfies }P_{ij}\le b_{S|ij}(x)\text{ for all }i,j\}.

Thus a coalition can reach a payoff threshold if it can give each member an item that member values at least as highly. The comparison is weak, so ties count as acceptable. This is the characteristic function used in the paper's Section 4 (Shapley and Scarf, 1974, pp. 109–110 of the source printing).

A balanced family $T$ is a family of nonempty coalitions with nonnegative real weights $\delta_S$ , zero outside $T$ , such that every trader has total covering weight one:

\sum_{\substack{S\in T\\j\in S}}\delta_S=1 \quad(j\in N).

The weights may be zero even for a coalition listed in $T$ . A balanced game is a game without side payments whose feasible payoff sets obey

\bigcap_{S\in T}V(S)\subseteq V(N)

for every balanced family $T$ . This includes overlapping families, not merely partitions (Shapley and Scarf, 1974, pp. 108–109).

Formalization targets

The goal is the paper's Section 4 theorem:

\text{For every finite nonempty }N\text{ and every }A:N\times N\to\mathbb R,\quad V_A\text{ is a balanced game}.

It contains four requirements. For each nonempty $S$ , $V_A(S)$ is closed; it is downward closed in the coordinates of $S$ ; and its payoff slice after removing the interiors of singleton payoff sets is bounded and nonempty. The fourth requirement is the balanced-family inclusion displayed above.

The milestones name the paper's intervening claims in their order: the three game conditions, the identity $B_N(x)=\sum_{S\in T}\delta_SB_S(x)$ , the doubly stochastic character of a balanced mixture $D=\sum_{S\in T}\delta_SP_S$ , and the existence of a grand-coalition permutation $P_N\le B_N(x)$ when $D\le B_N(x)$ . The final milestone states the matrix existence claim made at the end of Section 4, without committing the theorem statement to a particular construction.

Significance

The result establishes that the finite housing market falls under the paper's general balance framework. In the paper, the cited theorem that balanced games have nonempty cores then yields a core existence conclusion for this market. That general existence theorem is external to the Section 4 proof and is not asserted by this mission's goal (Shapley and Scarf, 1974, pp. 109–110).

The formal development supplies reusable definitions of games without side payments and balanced families alongside the market-specific allocation and acceptability matrices. It also gives precise targets for the matrix claims used in the paper. The source result is proved in print; these Lean statements are proposed formalization targets and their proof bodies remain open. Nearby platform items about transferable-utility games, including the Bondareva–Shapley goal, use a real value for each coalition and do not define this paper's payoff-set game. They are not substituted for these objects.

Difficulty

The challenge is the passage from coalition-wise feasibility to feasibility for all traders together. A balancing family can overlap: choosing one feasible permutation for each coalition does not immediately give a single permutation of $N$ . Their weighted mixture has fractional matrix entries. The condition $B_N(x)\ge D$ also has to survive the move from such a mixture to an actual zero-one permutation matrix. Without that last assertion, the balancing equations alone do not prove the inclusion $V(S)$ requires. Separately, the bounded nonempty payoff-slice condition must be checked for every nonempty coalition; merely proving closedness and downward closure would define a weaker class of games.

Formalization scope

Traders are an arbitrary finite nonempty Lean type, and payoffs live in $N\to\mathbb R$ . The paper's $E^S$ is encoded as the coordinate subspace of vectors zero outside $S$ ; interiors are taken in the product topology on $N\to\mathbb R$ . The boundedness and nonemptiness test applies to the intersection of that subspace with $V(S)$ after removing the singleton interiors. All conditions defining a game quantify over nonempty coalitions. The market formula is also defined at $S=\varnothing$ , where it yields all of $\mathbb R^N$ .

Allocation matrices are real zero-one matrices. An $S$ -permutation retains the paper's column, support, and row conditions; it is not replaced by an unconstrained permutation of all traders. The inequality between matrices is entrywise. The acceptability matrix has a 1 exactly when $i\in S$ and $x_i\le a_{ij}$ ; its columns are not independently restricted to $S$ . Balancing weights are nonnegative, may vanish inside the family, and cover every trader in $N$ . These choices exclude the trivializations $V(N)=\mathbb R^N$ , balance tested only on partitions, and coalitions using outsiders' items.

The definitions need finite-sum and matrix support from Mathlib, while the eventual proof can use Mathlib's doubly stochastic matrix and permutation-matrix library. Contributions that establish the stated game conditions or any of the four sourced matrix milestones are within scope. The paper's Section 8 counterexample and the optional superadditivity observation are outside this mission's attack path.

Selected references

Lloyd S. Shapley and Herbert Scarf, On cores and indivisibility, Journal of Mathematical Economics 1 (1974), 23–37. DOI: 10.1016/0304-4068(74)90033-0. The supplied scan has printed folios 104–123; Section 4 is on folios 109–111.

11 thms2 active users

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

METRIC: A Multi-Echelon Technique for Recoverable Item Control 2: Under Poisson Demand Expected Backorders Are Strictly Convex in the Mean, So a Point Estimate Understates ThemResearch Paper

Motivation

Spare-parts provisioning for repairable ("recoverable") items is a classical inventory problem: aircraft components fail, are sent to repair, and a stock of spares covers the units in the repair pipeline. Sherbrooke's METRIC model (Sherbrooke 1968), developed at RAND for the U.S. Air Force, measures the performance of a stock level by the expected number of backorders, the average number of unfilled demands outstanding at a random time. Every allocation computed by METRIC is driven by this quantity, and in particular by how it depends on the mean demand of each item.

For a new item that mean is not known. Air Force practice at the time produced a single engineering estimate of mean demand and computed backorders from it as if it were exact. In the section Demand Prediction (pp. 138–139) Sherbrooke argues that this practice is biased in one direction: under Poisson demand and any positive spare stock, the point estimate always understates expected backorders whenever the true mean is genuinely uncertain. This is his reason why a Bayesian treatment of demand is "of fundamental importance for all items, not merely low-demand items". The mission formalizes that claim and the computation behind it.

Setting

Fix one item. Its spare stock $s \in \{0, 1, 2, \dots\}$ is stock on hand plus on order plus in repair, minus backorders; under one-for-one replenishment it is constant. Let the number of units in resupply at a random time be Poisson distributed with mean $\lambda > 0$ :

p(x \mid \lambda) = e^{-\lambda}\frac{\lambda^x}{x!}, \qquad x = 0, 1, 2, \dots

The expected backorders at spare stock $s$ are, by the paper's eq. (2),

B(s \mid \lambda) = \sum_{x=s+1}^{\infty} (x - s)\, p(x \mid \lambda).

In eq. (2) the mean is $\lambda T$ (customer rate times mean resupply time); on p. 138 it is the mean demand over a unit time interval. Only the mean enters, so it is written as one parameter $\lambda$ . In Lean this is SherbrookeMetric.PointEstimate.backorders s lam, built on the published Poisson probabilities ServiceParts.StockLevels.poissonPmf.

Uncertain mean demand. The true mean takes the values $\lambda_k > 0$ , $k \in K$ ( $K$ finite), with probabilities $w_k \ge 0$ , $\sum_k w_k = 1$ . The point estimate is the mean of this distribution, $\bar\lambda = \sum_k w_k \lambda_k$ , and the expected backorders accounting for the uncertainty are $\sum_k w_k B(s \mid \lambda_k)$ . The paper's example (p. 138) takes $\lambda \in \{0.5, 1.5\}$ with probability $0.5$ each, so $\bar\lambda = 1$ ; its procedure (p. 139) discretizes a gamma prior to five to ten values.

Formalization targets

Goal: the point estimate understates backorders (pp. 138–139)

If two distinct values $\lambda_k \ne \lambda_{k'}$ both carry positive probability, then for every spare stock $s \ge 1$

B(s \mid \bar\lambda) < \sum_k w_k\, B(s \mid \lambda_k),

and for $s = 0$ the two sides are equal for every prior. The goal fixes no constants and no particular prior.

Milestones

Eq. (10), p. 139: for $\lambda > 0$ , $B(s \mid \cdot)$ is twice differentiable at $\lambda$ with

\frac{\partial^2 B(s \mid \lambda)}{\partial\lambda^2} = \frac{e^{-\lambda}\lambda^{s-1}}{(s-1)!} > 0 \quad (s \ge 1),

and second derivative $0$ for $s = 0$ . 2. Strict convexity, p. 139: for $s \ge 1$ , $\lambda \mapsto B(s \mid \lambda)$ is strictly convex on $(0, \infty)$ . 3. The worked example, p. 138 (off the goal's path): $B(2 \mid 1) = 3e^{-1} - 1 \approx 0.1036$ and $0.5\,B(2 \mid 0.5) + 0.5\,B(2 \mid 1.5) \approx 0.1486$ .

Significance

The result. Expected backorders are the objective METRIC minimizes, item by item, subject to a budget. If the objective is evaluated at a point estimate, every item with uncertain demand looks better stocked than it is, and since the size of the error varies by item, the marginal comparisons that drive the allocation are distorted. The inequality is the quantitative statement behind the paper's recommendation to compute backorders as a posterior mixture over possible mean demands. It also says that an underestimate of demand costs more than an overestimate of the same size when backorders are the objective. For $s = 0$ the bias vanishes because $B(0 \mid \lambda) = \lambda$ is linear.

Formalizing it. The paper proves the statement in one line ("it is easy to show") by differentiating twice. No machine-checked version exists. A formal proof needs termwise differentiation of the Poisson backorder series, a closed form for its second derivative, and the passage from a positive second derivative to strict convexity and then to a strict finite Jensen inequality under a nondegenerate prior. The resulting facts about $\lambda \mapsto B(s \mid \lambda)$ are reusable in any Poisson inventory model (base-stock, $(s-1, s)$ policies, METRIC and VARI-METRIC). Convexity of $B$ in the stock level $s$ , the paper's eq. (3), is a different statement; it is already posed on the platform as ServiceParts.StockLevels.backorder_differences (compound Poisson demand) and is not repeated here. The definition of the Poisson probabilities is the published ServiceParts.StockLevels.Basic (Muckstadt 2005).

Difficulty

Each step is classical, but none is a one-liner in Lean. The series $B(s \mid \lambda)$ is an infinite sum whose terms depend on $\lambda$ both through $e^{-\lambda}$ and through $\lambda^x$ , so differentiating it twice under the summation sign requires a uniform summability bound for the derivative series on a neighbourhood of $\lambda$ . The tempting shortcut of reasoning with deriv alone fails: deriv returns $0$ at points of non-differentiability, so a formula for deriv (deriv B) says nothing about smoothness, and the milestone is stated with HasDerivAt for this reason. The strict inequality further needs strict convexity, not just convexity, and a hypothesis that the prior is not concentrated on one value: with a one-point prior both sides coincide.

Formalization scope

$B(s \mid \lambda)$ is a real-valued tsum over $x \in \mathbb N$ of $(x - s)\,p(x \mid \lambda)$ for $x > s$ and $0$ otherwise. The family is summable for every real $\lambda$ ; no statement relies on the tsum junk value.
Spare stock is a natural number; mean demand is real. Convexity and the second-derivative formula are stated for $\lambda > 0$ , the paper's "for any positive $\lambda$ ".
Explicit readings of the paper's phrases: "backorders computed from a point estimate" is $B(s \mid \bar\lambda)$ with $\bar\lambda$ the prior mean (the paper assumes "the initial estimate is the mean of the true mean demand distribution"); "the correct value" is the prior expectation $\sum_k w_k B(s \mid \lambda_k)$ ; "mean demand can assume more than one value" means two distinct values each of positive probability; "positive spare stock" means $s \ge 1$ ; "understate" is strict.
The prior is a finite distribution with positive support points. This covers the paper's two-point example and its five-to-ten-point discretization of a gamma prior; a general prior on $(0, \infty)$ would need integrability hypotheses and is not part of the mission.
The printed value $B^*(2) = 0.1485$ is a rounding slip; the exact value is $0.14864\ldots$ , and the worked example states $0.1486$ .
A formalization that fixes $s$ , uses $\le$ in place of $<$ , drops the nondegeneracy hypothesis (making the strict statement false), or states the second derivative with deriv alone (vacuous at non-differentiable points) does not meet the target.
Not formalized: the remark that the understatement "is also true for probability distributions like the negative binomial, though difficult to prove analytically" (unproved on the page), the gamma prior and Bayes updating (a procedure), and the comment that the resulting allocation "will produce inferior results" (not a mathematical statement).
Contributions welcome: termwise differentiation lemmas for Poisson-weighted series, the closed form $B(s \mid \lambda) = \lambda - s + \sum_{x<s}(s - x)p(x \mid \lambda)$ , and a strict finite Jensen inequality in the form used here.

Selected references

C. C. Sherbrooke, METRIC: A Multi-Echelon Technique for Recoverable Item Control, Operations Research 16(1) (1968), 122–141. https://doi.org/10.1287/opre.16.1.122
G. J. Feeney and C. C. Sherbrooke, The (s−1, s) Inventory Policy under Compound Poisson Demand, Management Science 12(5) (1966), 391–411. https://doi.org/10.1287/mnsc.12.5.391
J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005. https://doi.org/10.1007/0-387-27288-8

6 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Discrete Dynamic Programming with Sensitive Discount Optimality Criteria 1: If Every Stationary Policy Is Transient, Some Stationary Policy Maximizes the Expected Total Reward over All PoliciesResearch Paper

Motivation

A finite dynamic program with total reward is the basic model of sequential decision making without discounting: a system moves among finitely many states, a decision maker picks an action in each state, collects a reward, and the system moves on or stops. The quantity of interest is the expected total reward of a policy, summed over the whole (possibly infinite) horizon, and the question is whether a simple policy — one that uses the same decision rule at every step — is as good as any other.

For discounted or strictly substochastic models the answer has long been known. Shapley (1953) showed by successive approximations that, when every transition matrix has row sums strictly below one, some stationary policy maximizes the total reward among stationary policies; Howard (1960) gave the policy-improvement method for finding one; Blackwell (1962) showed that the maximum over all policies is attained among stationary ones. All of these rest on a contraction hypothesis $\|P(f)\|<1$ .

Veinott's 1969 paper (DOI 10.1214/aoms/1177697379), best known for its sensitive discount optimality criteria, opens in §2 by proving these classical results under the much weaker hypothesis that each stationary policy is transient, and without requiring the transition weights to be substochastic at all. Partial results in this direction were due to Eaton and Zadeh, Derman, and Denardo. The total-reward model without a contraction assumption covers stopping problems, shortest-path type problems and models in which "transition weights" are not probabilities (growth factors, populations), which is why the generalized model is of independent interest.

Setting

There are $S\ge 1$ states $1,\dots,S$ . In state $s$ a finite nonempty set $A_s$ of actions is available; taking action $a$ earns the real reward $r(s,a)$ and assigns the transition weight $p(t\mid s,a)\ge 0$ to each state $t$ . No bound on $\sum_t p(t\mid s,a)$ is assumed. The set of decision rules is $F=\times_{s=1}^S A_s$ ; for $f\in F$ , $r(f)$ is the vector $(r(s,f(s)))_s$ and $P(f)$ the matrix $(p(t\mid s,f(s)))_{s,t}$ .

A policy is a sequence $\pi=(f_1,f_2,\dots)$ of decision rules. The policy $f^\infty=(f,f,\dots)$ is stationary; $(g,\pi)=(g,f_1,f_2,\dots)$ uses $g$ first and then follows $\pi$ ; ${}^N\pi$ repeats the first $N$ rules of $\pi$ forever and is called periodic. Let $P^0(\pi)=I$ and $P^N(\pi)=P(f_1)\cdots P(f_N)$ . The policy $\pi$ is transient if $\sum_{N\ge0}P^N(\pi)$ converges, and then its vector of total returns is

V(\pi)=\sum_{N=0}^\infty P^N(\pi)\,r(f_{N+1}).

The one-step comparison $v(g,\pi^*)=V(g,\pi^*)-V(\pi^*)$ measures the gain from deviating to $g$ for one step. Vectors are compared coordinatewise, and $x>y$ means $x\ge y$ , $x\ne y$ . For a matrix $B$ , $\|B\|=\max_i\sum_j|b_{ij}|$ and $|\sigma(B)|$ is its spectral radius. Finally $V^*=\max_f V(f^\infty)$ and $\Re V=\max_g[r(g)+P(g)V]$ , both coordinatewise.

Formalization targets

Goal: Corollary 6

If every stationary policy is transient, there is $f\in F$ with

V(\pi)\le V(f^\infty)\qquad\text{for every policy }\pi.

The hypothesis concerns only the finitely many stationary policies; the conclusion compares against every policy, stationary or not.

Milestones

Lemma 1. For transient $\pi=(g_i)$ and $\pi^*$ : $V(\pi)-V(\pi^*)=\sum_N P^N(\pi)\,v(g_{N+1},\pi^*)$ , and $V(g^\infty)-V(\pi^*)=[I-P(g)]^{-1}v(g,\pi^*)$ .
Lemma 2. If every stationary policy is transient and $f\in F$ : either $v(g,f^\infty)>0$ for some $g$ , and then $V(g^\infty)>V(f^\infty)$ , or $v(g,f^\infty)\le0$ for all $g$ , which holds iff $f^\infty$ is best among stationary policies.
Corollary 1. If every stationary policy is transient, some stationary policy maximizes $V$ over the stationary policies.
Corollary 2. Under the same hypothesis, $V^*$ is the unique fixed point of $\Re$ .
Lemma 3 (Hoffman). For every $\varepsilon>0$ and every program there is a positively similar program with $\max_g\|\tilde P(g)\|<\max_g|\sigma(P(g))|+\varepsilon$ .
Corollary 4, read with "every" and with "some": stationary, periodic and arbitrary policies are transient together, and this is equivalent to $\|P^N(\pi)\|<1$ for some $N\ge1$ ; with $\|P(g)\|\le1$ also to $\|P^S(\pi)\|<1$ .
Theorem 1. If every stationary policy is transient and $\pi^*$ is any policy: $v(g,\pi^*)>0$ implies $V(g^\infty)>V(\pi^*)$ , and $v(\cdot,\pi^*)\le0$ iff $V(\pi)\le V(\pi^*)$ for all $\pi$ .

Significance

Corollary 6 is the existence half of the theory of total-reward Markov decision processes: it says that the search for an optimal policy can be restricted to the finite set of stationary policies, and, together with Corollary 2 and Theorem 1, that such a policy is characterized by the optimality equation $\Re V=V$ and by the absence of one-step improvements. Corollary 4, which the paper's introduction singles out as the section's main new result, shows that transience of the finitely many stationary policies already forces transience of every policy, uniformly; this is what makes $V(\pi)$ well defined for all policies. Hoffman's Lemma 3 converts transience into a contraction in a rescaled norm, the device behind geometric convergence of value iteration (Corollary 3 of the paper).

On the formal side, Mathlib has matrices, summability and spectral radii but no total-reward decision model. These results are proved in the 1969 paper and are standard in the textbook literature on Markov decision processes; none of them has a machine-checked proof that we know of. Related platform items concern other models: the stochastic shortest path results of Bertsekas and Tsitsiklis (a cost model with a termination state, stochastic rows and an infinite-cost assumption on improper policies) and Blackwell's discounted model; neither covers nonnegative, non-substochastic weights.

Difficulty

Without a contraction, the standard argument — $\Re$ is a contraction, so it has a unique fixed point attained by a stationary policy — has nothing to start from: $\|P(g)\|$ may exceed one for every $g$ , and the transition weights need not be probabilities, so no probabilistic coupling or stopping-time argument applies directly. Transience of each stationary policy is a statement about finitely many matrix powers $P(g)^N$ , whereas the goal concerns infinite products of different matrices $P(f_1)P(f_2)\cdots$ , whose behaviour is not controlled by the spectral radii of the factors in general. Passing from the stationary policies to all policies is the step where the obvious argument fails.

Formalization scope

The Lean development fixes these conventions.

States are a nonempty finite type St; actions are a family of nonempty finite types A : St → Type, so $F$ is the dependent function type (s : St) → A s, not a common action set.
A program is a structure Program St A with real rewards and nonnegative weights; no row-sum bound is part of the structure. Only 5° of Corollary 4 assumes $\|P(g)\|\le1$ .
Policies are deterministic Markov sequences ℕ → F, indexed from $0$ : π 0 is $f_1$ . "All policies" means all such sequences.
Transience is Summable of $N\mapsto P^N(\pi)$ in the entrywise topology. $V$ is a tsum; it is the genuine series exactly for transient policies.
$>$ on vectors is written out as $\ge$ and $\ne$ ; $\|\cdot\|$ is the maximum absolute row sum, defined explicitly; $|\sigma(\cdot)|$ is Mathlib's spectralRadius ℂ of the complexified matrix, valued in $[0,\infty]$ .
$V^*$ and $\Re$ are coordinatewise Finset.sup' over the finite set $F$ .

A trivializing formalization is ruled out: the goal and Theorem 1 do not assume the competing policies transient (that would hide Corollary 4 inside the hypothesis), and since a non-summable tsum is $0$ , no statement compares $V$ of a policy whose transience is not either assumed or implied by the hypotheses. The hypothesis "every stationary policy is transient" is satisfiable (for instance when all weights are zero) and is not implied by any row-sum bound.

A complete development needs Neumann series for nonnegative matrices, the Perron–Frobenius-type fact that a nonnegative matrix with spectral radius below one has a nonnegative $(I-B)^{-1}=\sum B^N$ , and finite-dimensional spectral theory relating $|\sigma(B)|<1$ to $B^N\to0$ . These are reusable well beyond this mission; contributions of such lemmas, and of proofs of the milestones in any order, are welcome.

Selected references

A. F. Veinott, Jr., Discrete dynamic programming with sensitive discount optimality criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
D. Blackwell, Discrete dynamic programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
L. S. Shapley, Stochastic games, Proc. Nat. Acad. Sci. 39(10):1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2):165–177, 1967. https://doi.org/10.1137/1009030
C. Derman, On sequential decisions and Markov chains, Management Sci. 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16

12 thms2 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research I: Time-Mean Speed Equals Space-Mean Speed plus σₛ²/v̄ₛ, so v̄ₜ ≥ v̄ₛ with Equality Only Without Speed VariationResearch Paper

Why two traffic speed averages differ

A speed recorded as a vehicle passes a fixed point and a speed recorded among vehicles occupying a road segment answer different questions. Fast vehicles pass a detector more often per unit time; slow vehicles remain visible along the segment for longer. Traffic studies therefore need to identify which distribution a measurement samples before comparing average speeds. J. G. Wardrop made this distinction explicit in his 1952 treatment of road traffic, then quantified it through the variance of the spatial speed distribution (Wardrop 1952, pp. 327–331 and Appendix II).

The result belongs to the paper's mathematical account of traffic flow. It is useful even when the subsidiary streams do not describe a random vehicle process: the identities concern finite positive flows and speeds. The paper also applies the same distributions to speed samples from radar and aerial photographs and to an idealized count of overtaking events (Wardrop 1952, pp. 330, 333–334).

Traffic streams and their two distributions

A road's traffic stream is divided into $C$ subsidiary streams, indexed by $i=1,\ldots,C$ . Stream $i$ has flow $q_i$ , the number of vehicles passing a point per unit time, and speed $v_i$ . Its concentration is $k_i=q_i/v_i$ , the number of vehicles occupying a unit road length. Total flow and concentration are $Q=\sum_i q_i$ and $K=\sum_i k_i$ . The time frequency $f_i=q_i/Q$ weights each stream by how often its vehicles pass a point. The space frequency $f'_i=k_i/K$ weights it by the fraction of vehicles present along the road.

The time-mean speed is $\bar v_t=\sum_i q_i v_i/Q=\sum_i f_i v_i$ . The space-mean speed is $\bar v_s=\sum_i k_i v_i/K=\sum_i f'_i v_i$ . Both are averages of the same speeds; the weights differ. Wardrop defines the space-distribution variance independently as $\sigma_s^2=\sum_i k_i(v_i-\bar v_s)^2/K$ , and the corresponding coefficient of variation as $c_s=\sigma_s/\bar v_s$ (equations (1)–(3), (7), pp. 328–331).

These are finite sums, not limits of a stochastic process. The model requires at least one subsidiary stream and positive flow and speed for each stream. Positive flows ensure that every speed in the equality criterion belongs to a present stream; positive speeds make concentration meaningful. The count $C$ is allowed to be one. In that case both means coincide and the variance is zero, as the formulas require.

Formalization targets

The main target is Wardrop's equation (6), together with its stated comparison and equality case (p. 330; Appendix II, p. 356):

\bar v_t=\bar v_s+\frac{\sigma_s^2}{\bar v_s},\qquad \bar v_s\le\bar v_t,\qquad \bar v_t=\bar v_s\iff v_i=v_j\text{ for every }i,j.

The subsidiary targets follow the paper's order. Equation (4) says $k_i v_i=q_i$ for each stream, giving equation (5), $Q=K\bar v_s$ . Appendix II then uses the centered identity $\sum_i f'_i(v_i-\bar v_s)=0$ and rewrites the time mean as $\bar v_t=(\sum_i f'_i v_i^2)/\bar v_s$ . These three claims are the mission milestones. Equation (8) is included as a companion formulation:

\bar v_t=\bar v_s(1+c_s^2).

The mission also records the paper's formulas for equally weighted time and space speed samples and the equivalent space- and time-frequency formulas for the idealized overtaking count. These companions use the same definitions without changing the main target (pp. 330–334).

What the result supplies

The identity gives an exact size and direction for the difference between the two averages. Since the variance is nonnegative and $\bar v_s$ is positive, the time mean cannot fall below the space mean. If all constituent speeds are equal, the difference vanishes; if any two present streams have different speeds, the difference is positive. The formula therefore lets a reader decide whether two reported speed averages can be compared directly, and it identifies the spatial variance as the quantity needed to convert between them.

The sample formulas sharpen that interpretation. Equal weights among vehicles passing a point make the time mean the arithmetic mean of the sampled speeds and the space mean their harmonic mean. Equal concentrations reverse which mean is arithmetic; the time mean becomes $\sum_i v_i^2/\sum_i v_i$ . The overtaking formulas express a single pairwise count using either frequency system, provided the speeds are ordered and the paper's assumption of no interference with overtaking is used (Wardrop 1952, pp. 330, 333–334).

Wardrop proved these formulas in print. The remaining work in this mission is a machine-checked proof of the finite-sum identities and their strict equality case. The proposal supplies typed statements and definitions, but the theorem proofs are open. The resulting concentration and frequency definitions are reusable in other traffic-flow formalizations; the statements also provide small algebraic interfaces for testing more elaborate traffic models.

Where the formal proof needs care

The relation looks like a routine identity for weighted means, but the two weight systems are coupled through $k_i=q_i/v_i$ . One cannot treat the time and space frequencies as independent arbitrary probability vectors and still obtain equation (6). The strict case needs more than nonnegativity of the variance: it needs the fact that every space weight is positive, so zero variance forces every constituent speed to equal the mean. The single-stream case and every denominator need the same attention.

The overtaking statement has a separate modelling boundary. Its algebraic equalities use a rate defined by pairwise speed differences. Wardrop's physical interpretation of that rate assumes that overtaking does not interfere with other overtaking. The mission records the identities for that idealized rate, without claiming that a measured road necessarily meets the physical assumption.

Formalization scope

Lean uses Fin C for the streams and real numbers for $q_i$ , $v_i$ , $k_i$ , both means, the variance, and the overtaking rate. Finite sums are taken over all streams. The theorem hypotheses require $0<C$ , $0<q_i$ , and $0<v_i$ for every $i$ . These requirements make $Q$ , $K$ , and $\bar v_s$ positive; Lean's total division would otherwise assign a zero value at a zero denominator that has no meaning in the paper's model. For the overtaking identity, StrictMono v retains Wardrop's ordering $v_1<\cdots<v_C$ .

The variance is defined from equation (7), $\sum_i k_i(v_i-\bar v_s)^2/K$ . Defining it by rearranging equation (6) would make the target true by definition and would erase the mathematical claim. The standard deviation uses the real square root of that variance. An observation in the sample companion is represented as one subsidiary stream of equal time or space weight; this is the formal reading of the paper's sampling paragraphs. No probability-measure library is needed, since $f_i$ and $f'_i$ are explicit finite weights.

A complete proof needs finite-sum rearrangements, elementary real division under positive denominators, nonnegative weighted squares, and the equality case of a positive weighted sum of squares. The definitions and the mean identities are welcome as separate reusable contributions. The mission does not include the paper's normal approximation for overtaking density in equation (11), which Wardrop presents as an approximation rather than an exact finite-sum theorem.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II 1 (1952), 325–362. DOI: 10.1680/ipeds.1952.11259.

5 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting 1: If G(f) ∪ H(f) Is Empty, f Maximizes the Gain and Then the Bias, and Each Improvement Step Raises (x, y, z)Research Paper

Motivation

A controller observes a finite system period after period, chooses an action in each state, earns an income and moves the system at random. When future income is not discounted, the natural criterion is the average return per unit time (the gain), but many policies share the maximal gain while differing in their transient income. Blackwell (1962) showed that the policies that are optimal as the discount factor tends to one, the 1-optimal policies, are exactly the stationary policies that first maximize the gain and then, among those, the bias. He gave no finite procedure for the second maximization. Veinott (1966) supplied one: an extension of Howard's policy improvement method in which a second improvement test, on the bias, is run after the gain test is exhausted, with a third vector $z(f)$ guaranteeing termination. The method and its sensitivity hierarchy became the starting point of the $n$ -discount optimality theory developed by Veinott (1969) and treated in Puterman's Markov Decision Processes (1994), Chapter 10.

Timeline:

1960: Howard, Dynamic Programming and Markov Processes: policy improvement for the discounted and the average-return problems.
1962: Blackwell, Discrete Dynamic Programming: existence of stationary policies optimal for all discount factors near one; the expansion $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+o(1)$ ; nearly optimal (1-optimal) policies characterized by lexicographic maximization of $(x,y)$ .
1966: Veinott, this paper: the extended policy improvement method that finds a 1-optimal stationary policy in finitely many steps (Theorem 6), and a finite-horizon characterization of the same policies (Theorem 7).
1969: Veinott, Discount optimality and sensitive optimality: the full hierarchy of $n$ -discount optimal policies and the corresponding nested improvement method.

Setting

There are finitely many states $s$ and a finite set of actions. Choosing action $a$ in state $s$ earns the income $i(s,a)$ and moves the system to state $s'$ with probability $q(s'\mid s,a)$ . A decision rule $f\in F$ picks an action $f(s)$ in each state; $r(f)$ is the vector with entries $i(s,f(s))$ and $Q(f)$ the stochastic matrix with entries $q(s'\mid s,f(s))$ . A policy is a sequence $(f_1,f_2,\dots)$ of decision rules, $f^\infty=(f,f,\dots)$ is a stationary policy, and for $0\le\beta<1$

V_\beta(\pi)=\sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\,r(f_{n+1})

is the vector of expected discounted returns. For vectors, $u\ge v$ is coordinatewise and $u>v$ means $u\ge v$ and $u\ne v$ .

Let $Q^*(f)$ be the Cesàro limit of the powers of $Q(f)$ . The gain $x(f)$ and the bias $y(f)$ are the unique solutions of

[I-Q(f)]x=0,\quad Q^*(f)x=Q^*(f)r(f);\qquad [I-Q(f)]y=r(f)-x(f),\quad Q^*(f)y=0,

and $z(f)$ is the unique solution of $[I-Q(f)]z=-y(f)$ , $Q^*(f)z=0$ . Write $F'$ for the decision rules of maximal gain and $F''\subset F'$ for those of maximal bias within $F'$ .

The two improvement sets compare $f$ with a decision rule $g$ through the state-by-state tests

\text{(i) } [Q(g)x(f)]_s\ge[x(f)]_s,\qquad \text{(ii) } [r(g)+Q(g)y(f)]_s\ge[x(f)+y(f)]_s .

$G(f)$ consists of the $g$ for which (i) holds everywhere, (ii) holds wherever (i) is an equality, some inequality is strict, and $g(s)=f(s)$ wherever both are equalities. $E(f)$ consists of the $g$ for which (i) and (ii) are equalities at every state. For $g\in E(f)$ ,

\text{(iii) } [-y(f)+Q(g)z(f)]_s\ge[z(f)]_s,

and $H(f)$ consists of the $g\in E(f)$ for which (iii) holds everywhere, strictly somewhere, with $g(s)=f(s)$ wherever it is an equality.

Formalization targets

Goal: Theorem 6 (p. 1290)

For every $f\in F$ :

$G(f)=\varnothing\ \Rightarrow\ f\in F'$ ;
$G(f)\cup H(f)=\varnothing\ \Rightarrow\ f\in F''$ ;
$g\in G(f)\ \Rightarrow\ x(g)>x(f)$ , or $x(g)=x(f)$ and $y(g)>y(f)$ ;
$g\in H(f)\ \Rightarrow\ x(g)=x(f)$ , and $y(g)>y(f)$ , or $y(g)=y(f)$ and $z(g)>z(f)$ .

Part 2 is the stopping certificate and parts 3 and 4 are the progress guarantee; together they say that the extended method raises $(x,y,z)$ lexicographically and stops at a decision rule in $F''$ .

Milestones

Theorem 3 (Blackwell): $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+\epsilon(\beta,f)$ with $\epsilon(\beta,f)\to0$ as $\beta\to1^-$ , and the unique-solution characterizations of $x(f)$ , $y(f)$ (already posed on the platform, referenced).
Lemma 1 (Blackwell): $g\in E(f)\Rightarrow x(g)=x(f)$ , and $y(g)=y(f)$ if moreover $Q^*(g)Q^*(f)=Q^*(g)$ (referenced).
Theorem 1: for fixed $0\le\beta<1$ , exactly one of " $f^\infty$ has no one-step improvement and is $\beta$ -optimal" and "some $g$ gives $V_\beta(g,f^\infty)>V_\beta(f^\infty)$ and $V_\beta(g^\infty)>V_\beta(f^\infty)$ ".
Theorem 4: $F''$ is the nonempty set of $f$ with $f^\infty$ 1-optimal.
Theorem 5 and Corollary 1: $G(f)=\varnothing\Rightarrow f\in F'$ ; $g\in G(f)\Rightarrow V_\beta(g^\infty)>V_\beta(f^\infty)$ for $\beta$ near one, hence the lexicographic increase of $(x,y)$ .
Lemma 4: for $g\in E(f)$ , $y(g)=y(f)+w(g)$ , where $w(g)$ is the unique solution of $[I-Q(g)]w=0$ , $Q^*(g)w=Q^*(g)(-y(f))$ .
(12): $z(f)$ is the unique solution of its system.
Lemma 5: $G(f)=\varnothing$ and $y(f)\ge y(g)$ for all $g\in E(f)$ imply $f\in F''$ .
Two steps of the proof of Theorem 6: $H(f)=\varnothing\Rightarrow y(g)\le y(f)$ on $E(f)$ ; and $g\in H(f)\Rightarrow w(g)>w(f)=0$ , or $w(g)=w(f)=0$ and $z(g)>z(f)$ .

Significance

Theorem 6 turns Blackwell's existence result into an algorithm. Blackwell's characterization requires maximizing the bias over $F'$ , a set with no explicit description; Lemma 5 shows that maximizing over the explicitly available set $E(f)$ suffices, and Lemma 4 shows that this maximization has the same form as the original gain maximization, so the familiar policy improvement machinery applies a second time. The same mechanism, iterated, gives the $n$ -discount optimal policies of the later sensitivity theory and the lexicographic policy improvement algorithms in standard texts.

The results are proved in the paper (with a correction to the proof of Lemma 5 credited to Bruce Miller). They are not formalized in any proof assistant known to the mission. A complete development yields machine-checked policy improvement for average and bias optimality on top of the published Blackwell model, including the convergence-free closed forms of gain, bias and $z$ and the facts about the limit matrix $Q^*$ and the deviation matrix they rest on.

Difficulty

Parts 1 and 3 are Blackwell's policy improvement for the gain, transported to Veinott's set $G(f)$ . The new content is in parts 2 and 4, and in both the obvious argument fails at the same place: the bias of $g\in E(f)$ cannot be compared with the bias of $f$ by a state-by-state test in the original problem, because $E(f)$ is a product of action sets $E(s,f)$ different from the original ones, and Blackwell's comparison works only after a reduction to a problem in which the reward is $-y(f)$ and the role of the gain is played by $w(g)$ . A second difficulty is Lemma 5: $E(f)$ may be a proper subset of $F'$ (Example 3 of the paper), so maximizing the bias over $E(f)$ does not obviously maximize it over $F'$ . The certificate does not follow from the gain and bias tests at $f$ alone, and the paper's original proof of it contained an error (corrected, as the paper records, by Bruce Miller).

Formalization scope

Everything is built on the published Blackwell definitions (BlackwellDiscreteDP.NearOne.Model, LimitMatrix, GainBias): one finite action type available in every state (Veinott's $A_s$ are all equal to it), decision rules St → Act, policies indexed from $0$ (π 0 is $f_1$ ), real vectors St → ℝ with the pointwise order, and VecGt for the paper's $>$ (not coordinatewise strict). $Q^*(f)$ is the published Cesàro limit $\lim (N+1)^{-1}\sum_{i=0}^N Q(f)^i$ , the same limit as Veinott's $N^{-1}\sum_{i=0}^{N-1}$ . The gain and bias are the published closed forms $x(f)=Q^*(f)r(f)$ and $y(f)=H(f)r(f)$ with the deviation matrix $H(f)$ ; the new vectors are closed forms too: $w(g)=Q^*(g)(-y(f))$ and $z(f)=H(f)(-y(f))$ , and their characterizations by (10) and (12) are milestones. 1-optimality is the published IsNearlyOptimal, which compares against every policy. Veinott's set $H(f)$ is HSet, to keep it apart from the deviation matrix Hf.

$G(f)$ and $H(f)$ are defined literally from the paper's inequalities, including the clauses "at least one strict" and " $g(s)=f(s)$ where the tests are equalities". Dropping either clause makes parts 3 and 4 false (a $g$ that only reshuffles ties would count as an improvement); replacing $F''$ or $G(f)$ by a set defined through the conclusion of the theorem would make the goal trivial. Neither is acceptable.

The reduction "replace $A_s$ by $E(s,f)$ and $r(g)$ by $-y(f)$ " is not instantiated, since the published model has a single action set; its two uses in the proof of Theorem 6 are milestones stated in the original model. A development of the general model with state-dependent action sets, and of the limit-matrix identities $Q^*Q=QQ^*=Q^*Q^*=Q^*$ , $(I-Q)H=I-Q^*$ , $Q^*H=0$ , would be reusable well beyond this mission. Proofs of any milestone are welcome, as is a proof of the published Theorem 3 and Lemma 1, on which most of the mission rests.

Selected references

D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
A. F. Veinott, Jr., On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting, Ann. Math. Statist. 37(5):1284–1294, 1966. https://doi.org/10.1214/aoms/1177699272
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
A. F. Veinott, Jr., Discount Optimality and Sensitive Optimality, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

16 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design·Captain: mikedeng1

Strategy-Proofness and Arrow's Conditions 2: Strategy-Proof Voting Procedures Correspond One-to-One to Social Welfare Functions Satisfying CS, NNR and IIAResearch Paper

Motivation

Two impossibility theorems frame the theory of collective choice. Arrow's theorem (1951) says that a rule aggregating individual preference orderings into a social ordering, subject to a short list of reasonable conditions, must be dictatorial. The Gibbard–Satterthwaite theorem (Gibbard 1973, Satterthwaite 1975) says that a voting procedure selecting a single alternative, which no voter can manipulate by misreporting, must be dictatorial once at least three outcomes are possible. Both conclusions are the same, and the two conditions—Arrow's axioms and strategy-proofness—look unrelated: one is about the coherence of a social ranking, the other about voters' incentives.

Satterthwaite's paper (Northwestern Discussion Paper No. 122, 1974; J. Econ. Theory 10, 1975) shows that the two conditions are in fact the same condition. Section 4 constructs a one-to-one correspondence between strict strategy-proof voting procedures with full range and strict social welfare functions satisfying Arrow's conditions, under which each social welfare function's top choice is the voting procedure's outcome. This mission formalizes that correspondence.

Timeline. Arrow (1951, 2nd ed. 1963) proved the general possibility theorem with conditions of non-negative response (NNR), citizens' sovereignty (CS), independence of irrelevant alternatives (IIA) and non-dictatorship. Gibbard (1973) proved that strategy-proof game forms with at least three outcomes are dictatorial, by first showing that a strategy-proof procedure induces an Arrovian social welfare function and then applying Arrow's theorem. Satterthwaite (1974/75) gave an independent direct proof of the voting-procedure theorem and proved the correspondence theorem (Theorem 2), which turns Gibbard's construction into an exact equivalence.

Setting

A committee $I_n$ of $n$ individuals chooses from a finite set $S_m$ of $m$ alternatives. A strong order on $S_m$ is a complete, transitive relation $R$ with no indifference between distinct alternatives; $x\,\bar R\,y$ denotes strict preference. Let $\rho_m$ be the set of strong orders and $\rho_m^n$ the set of strict ballot sets $B=(B_1,\dots,B_n)$ .

A strict voting procedure is a map $v:\rho_m^n\to S_m$ ; its range is $T_p=\{v(B):B\in\rho_m^n\}$ . It is strategy-proof if no individual $i$ , at any $B$ , has a ballot $B_i'$ with $v(B_1,\dots,B_i',\dots,B_n)\,\bar B_i\,v(B)$ .
A strict social welfare function is a map $u:\rho_m^n\to\rho_m$ ; $A_B=u(B)$ is the social ordering.
For $W\subseteq S_m$ , $\Psi_W(R)$ is the set of $R$ -best elements of $W$ , and $\theta_W(R)$ is the restriction of $R$ to $W$ .
$u$ underlies $v$ , and $v$ is derived from $u$ , if $\Psi_{S_m}[u(B)]=\{v(B)\}$ for every $B$ .

Arrow's conditions on $u$ : CS—for all $x\ne y$ some $B$ gives $x\,\bar A_B\,y$ ; IIA—if $\theta_W(C_i)=\theta_W(D_i)$ for all $i$ then $\Psi_W(A_C)=\Psi_W(A_D)$ ; NNR—raising an alternative $x$ in individual ballots, with the order of the other alternatives unchanged, never lowers $x$ against any other alternative in the social ordering. PO (Pareto optimality): unanimous strict preference for $x$ over $y$ yields $x\,\bar A\,y$ .

Formalization targets

Goal: Theorem 2 (p. 35)

For $n\ge2$ and $m\ge3$ there is a bijection

\lambda:\{v \text{ strict, strategy-proof},\ T_p=S_m\}\ \longrightarrow\ \{u \text{ strict},\ \text{CS},\ \text{NNR},\ \text{IIA}\}

with $\Psi_{S_m}[\lambda(v)(B)]=\{v(B)\}$ for every $v$ and every $B\in\rho_m^n$ .

Milestones

CS, NNR and IIA imply PO (p. 31, after Arrow), and PO implies CS (p. 31).
Lemma 7 (p. 30): the voting procedure derived from a strict $u$ with CS, NNR, IIA exists, is strategy-proof and has range $S_m$ .
Gibbard's claim (p. 33): for a strict strategy-proof $v$ with range $S_m$ and a fixed strong order $Q$ , the relation $P(B)$ defined by $x\,\bar P\,y\iff x=v[\Delta_{xy}(B_1),\dots,\Delta_{xy}(B_n)]$ is a strong order, and $\mu:B\mapsto P(B)$ underlies $v$ and satisfies PO and IIA.
Uniqueness (p. 34): at most one strict $u$ with PO and IIA underlies a strict strategy-proof $v$ .
NNR (p. 34): such an underlying $u$ satisfies NNR.
Lemma 8 (p. 35): a strict strategy-proof $v$ with range $S_m$ has exactly one underlying strict $u$ with CS, NNR, IIA.

Significance

The correspondence explains why the two impossibility theorems have the same conclusion: for strict preferences, a strategy-proof procedure with full range and an Arrovian social welfare function are two descriptions of one object. In particular either impossibility theorem, together with Theorem 2, yields the other. The paper draws a second consequence: a social welfare function violating rationality or IIA has a derived voting procedure that is manipulable, so Arrow's much-debated conditions are forced by the practical requirement of strategy-proofness.

On the formal side, the platform already has machine-checked proofs of the strict Arrow theorem (AGT.arrow_theorem, unanimity and pairwise IIA) and of the strict full-range Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite). Together these determine both sides of Theorem 2 as sets of dictatorships, but neither states the correspondence, the derived/underlying relation, Gibbard's construction or NNR, and nothing on the platform states Lemmas 7 or 8. The milestones here formalize the paper's direct argument, which does not pass through the impossibility theorems.

Difficulty

The obvious argument fails in two places. First, a strategy-proof voting procedure determines only the top of a social ordering, and the whole ordering must be recovered; Gibbard's relation $P$ does this, but proving that $P$ is transitive is the core of Gibbard's proof of the Gibbard–Satterthwaite theorem, which the paper cites rather than proves. Second, NNR as stated allows many individuals to move $x$ at once, while the manipulation argument works with one ballot at a time; one must pass from a single-voter change to an arbitrary one without losing IIA or PO along the way.

A newcomer's first idea is to prove both sides are dictatorships and match dictators. That proves the bijection but needs both impossibility theorems as inputs, and the correspondence must still carry the underlying relation for every procedure.

Formalization scope

Alternatives and individuals are finite types A, ι with decidable equality; $n=|\iota|\ge2$ , $m=|A|\ge3$ throughout.
Weak orders are a structure (relation, completeness, transitivity); strong orders are the subtype with no indifference between distinct elements. Strict ballot sets are functions ι → StrongOrder A, and voting procedures and social welfare functions are defined only on them. Two social welfare functions are therefore equal exactly when they agree on every strict ballot set; this is what makes uniqueness in Lemma 8 and the bijection in Theorem 2 meaningful.
The range $T_p$ is the image of strict ballot sets; " $T_p\equiv S_m$ " is Set.range v = Set.univ.
$\theta_W(C_i)=\theta_W(D_i)$ is agreement of the two relations on $W\times W$ .
CS is stated for $x\ne y$ : as printed ("for every $x,y$ ") it is unsatisfiable at $x=y$ for a strict social ordering, and every statement would become vacuous. NNR's "for some $x$ " is read as "for every $x$ ".
"Derived from" and "underlies" are the same relation $\Psi_{S_m}[u(B)]=\{v(B)\}$ ; Lemma 7 asserts existence of the derived procedure and its properties for every derived procedure.
Gibbard's $\Delta_{xy}$ and $P$ are definitions; $P$ is the reflexive closure of the paper's $\bar P$ .
The PO claim, PO ⇒ CS, uniqueness and the NNR claim are unconditional in the paper; they are stated under §4's standing $n\ge2$ , $m\ge3$ , since with no individuals PO fails.
Theorem 2 is stated as an Equiv together with " $\lambda(v)$ underlies $v$ " for every $v$ . A bare existence of a bijection between the two sets is a cardinality fact and is not the theorem.

Reusable beyond this mission: the strict-preference vocabulary (strong orders, $\Psi_W$ , Arrow's conditions in the paper's form) and Gibbard's $\Delta_{xy}$ construction. Contributions welcome: proofs of each milestone, and bridges to AGT.arrow_theorem and AGT.gibbard_satterthwaite.

Selected references

M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
K. J. Arrow, Social Choice and Individual Values, 2nd ed., Wiley, 1963.

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design·Captain: mikedeng1

Strategy-Proofness and Arrow's Conditions 4: With Indifference Allowed, a Social Welfare Function Satisfying CS, NNR and IIA Is DictatorialResearch Paper

Motivation

A social welfare function turns the rankings of the members of a committee into one ranking for the committee. Arrow's general possibility theorem (Arrow, 1951/1963) shows that, once there are at least three alternatives, no such rule satisfies a short list of conditions that each look harmless unless it follows a single member's ranking. The theorem is the starting point of social choice theory and underlies the study of voting rules, preference aggregation in economics, and rank aggregation in computer science.

Arrow's own setting allows indifference: ballots and the social ordering are weak orders, and the conditions he imposed are citizens' sovereignty, non-negative response, and independence of irrelevant alternatives. Many textbook proofs, and the existing machine-checked versions, instead take strict ballots and replace the first two conditions by the Pareto condition.

Satterthwaite's discussion paper (Satterthwaite, Northwestern DP No. 122, 1974, journal version J. Econ. Theory 10 (1975)) gives a new proof of Arrow's theorem. Strict Arrovian social welfare functions correspond one-to-one to strategy-proof voting procedures with full range, and the Gibbard–Satterthwaite theorem then forces a dictator. His §6 extends the argument to weak orders by decomposing a social welfare function into a tie-breaking step followed by a strict one. This mission formalizes that weak-order extension and the strict theorem it rests on.

Timeline.

1951: Arrow proves the general possibility theorem for weak orders under CS, NNR, IIA and non-dictatorship. The second edition (1963) corrects the first edition's statement.
1973: Gibbard proves that every strategy-proof game form with at least three outcomes is dictatorial (Econometrica 41).
1975: Satterthwaite proves the same independently for voting procedures, and shows that strategy-proof procedures and Arrovian social welfare functions correspond. This gives a proof of Arrow's theorem by way of strategy-proofness.

Setting

A committee $I_n$ of $n$ individuals ranks a finite set $S_m$ of $m$ alternatives. A weak order $R$ on $S_m$ is a complete, transitive relation, and $x\,R\,y$ reads " $x$ is preferred or indifferent to $y$ ". Its strict part is $x\,\bar R\,y$ : $x\,R\,y$ and not $y\,R\,x$ . The weak orders form $\pi_m$ . A strong order is a weak order with no indifference between distinct alternatives, and the strong orders form $\rho_m$ . A ballot set is $B=(B_1,\dots,B_n)\in\pi_m^n$ .

A social welfare function $u$ assigns to every ballot set a social ordering $A=u(B)\in\pi_m$ . A strict social welfare function $\mu$ is defined only on strong ballot sets $\rho_m^n$ and takes values in $\rho_m$ . For $W\subseteq S_m$ , $\Psi_W(R)$ is the set of $R$ -best elements of $W$ , and $\theta_W(R)$ is the restriction of $R$ to $W$ .

CS (citizens' sovereignty): for all distinct $x,y$ some ballot set yields $x\,\bar A\,y$ .
IIA (independence of irrelevant alternatives): if $\theta_W(C_i)=\theta_W(D_i)$ for every $i$ , then $\Psi_W(A_C)=\Psi_W(A_D)$ .
NNR (non-negative response): if $D$ differs from $C$ only by raising an alternative $x$ on some ballots, then $x\,\bar A_C\,z$ implies $x\,\bar A_D\,z$ for all $z\neq x$ .
Dictatorial: some $i$ exists such that $x\,\bar B_i\,y$ implies $x\,\bar A\,y$ for every ballot set and all $x,y$ .

A tie-breaking function $\alpha$ maps every weak ballot set to a strong one while keeping every strict preference. It is regular if each individual's ties are broken by a fixed strong order $Q_i$ .

Formalization targets

Goal: Theorem 3' (p. 49)

For $n\ge 2$ , $m\ge 3$ and any social welfare function $u$ on weak ballot sets,

u \text{ satisfies CS, NNR, IIA} \;\Longrightarrow\; \exists\, i\;\forall B\;\forall x,y:\; x\,\bar B_i\,y \Rightarrow x\,\overline{u(B)}\,y .

The converse is false with indifference, so the goal is one-directional.

Milestones

Theorem 3 (p. 36): for strict $\mu$ , CS, NNR and IIA hold if and only if $\mu$ is dictatorial.
Lemma 10, first sentence (p. 44): if $u$ has range in $\rho_m$ and $u=\mu\circ\gamma$ with $\gamma$ regular and $\mu$ strict Arrovian, then $u$ satisfies IIA, CS and NNR.
Lemma 10, second sentence (p. 44): if $u$ has range in $\rho_m$ and satisfies IIA, CS and NNR, then $u=\mu\circ\alpha$ for a tie-breaking function $\alpha$ and a strict $\mu$ satisfying IIA, CS and NNR.
Lemma 11 (p. 48): breaking the ties of each social ordering $u(B)$ by a strong order $Q$ preserves CS, NNR and IIA and gives range in $\rho_m$ .

Significance

Theorem 3' is Arrow's theorem in the setting Arrow stated it: weak-order ballots, a weak social ordering, and the conditions CS and NNR instead of the Pareto condition. Lemma 10 and Lemma 11 together say that Arrovian social welfare functions with indifference are determined by strict ones up to tie-breaking. This is the structural fact the paper also uses for its weak-order correspondence (Theorem 2').

All results here are proved in the paper. None is formalized as stated. The platform holds a proved strict Arrow theorem, AGT.arrow_theorem, for social welfare functions on strict total orders under unanimity and pairwise IIA. Theorem 3's only-if half follows from it once CS, NNR and IIA are shown to imply the Pareto condition and the two encodings are bridged. The weak-order statement, the tie-breaking lemmas, and the "if" half of Theorem 3 are new to the platform.

Difficulty

Passing from strict to weak orders is the hard step. Restricting a weak ordering to a pair of alternatives does not determine its choice sets on larger sets once ties are present. A social welfare function that satisfies IIA on weak orders need not induce one on strong orders through an arbitrary tie-breaker. Breaking ties ballot by ballot with a non-regular rule can destroy IIA, and breaking ties in the social ordering can destroy NNR unless the same fixed order is used throughout. The obvious reduction is "break all ties and apply the strict theorem", and it fails: the dictator of the tie-broken function could depend on the tie-breaking order. The fact that it does not is part of what must be shown.

Formalization scope

Alternatives and individuals are finite types A and ι with decidable equality. $n$ = Fintype.card ι, $m$ = Fintype.card A, and $n\ge 2$ , $m\ge 3$ are hypotheses as printed. All statements live in StrategyProofArrow.WeakArrow.
A weak order is a structure (a relation with completeness and transitivity). A strong order is the subtype with no indifference between distinct elements. Strong ballot sets are functions into that subtype, so a strict social welfare function is defined on admissible profiles only.
$\theta_W(C)=\theta_W(D)$ is agreement of the two relations on $W\times W$ . $\Psi_W$ is a set, compared as a set, since weak orders can have several best elements.
CS is stated for distinct $x\neq y$ . As printed ("for every $x,y$ ") it is unsatisfiable at $x=y$ , and every theorem would become vacuous. No other trivializing reading is possible: the dictator conclusion is the paper's one-directional negation of ND, not $u(B)=B_i$ , which would be false for weak orders.
Lemma 11's tie-breaker acts on a single ordering. It is encoded as breaking the ties of $u(B)$ by a strong order $Q$ , the "tie-breaking order for $\gamma$ " of the proof of Theorem 3'.
Lemma 10's printed $u^{nm}(B)=u^{nm}[\gamma(B)]$ is read $u(B)=\mu(\gamma(B))$ , following the proof.

The definitions duplicate objects drafted in the sibling missions of this series (weak and strong orders, CS, NNR, IIA). Proofs of the strict theorem from the Gibbard–Satterthwaite theorem, bridges to AGT.arrow_theorem, and reusable lemmas about tie-breaking of weak orders are all welcome.

Selected references

M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, 1974 (rev. Dec. 12, 1974); J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
K. J. Arrow, Social Choice and Individual Values, 2nd ed., Yale University Press, 1963. https://doi.org/10.12987/9780300186987
A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083

6 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

A Dual Approach to Solving Nonlinear Programming Problems by Unconstrained Optimization 3: Under Second-Order Conditions, Tolerances αₖ ≤ q[sup g_r − g_r(yᵏ)] Give |xᵏ − x̄| ≤ s|yᵏ − ȳ|Research Paper

Motivation

The method of multipliers (augmented Lagrangian method), proposed independently by Hestenes and Powell in 1969, solves a constrained optimization problem by a sequence of unconstrained minimizations of a penalized Lagrangian, updating a multiplier estimate between them. It became one of the standard algorithms of nonlinear programming and is the ancestor of ADMM and of the proximal-point view of dual methods. Rockafellar's 1973 paper (Math. Programming 5, 354–373) extended the method to inequality constraints with the penalty Lagrangian $L_r$ and reinterpreted it as unconstrained maximization of a smooth concave dual function $g_r$ . Its §4 shows that primal points recovered from any maximizing dual sequence are asymptotically minimizing; its §5, the subject of this mission, asks how fast they converge.

Timeline. 1969: Hestenes and Powell introduce multiplier methods for equality constraints. 1973: Rockafellar treats inequality constraints in the convex case through $L_r$ and its dual (this paper), and in the same year applies the multiplier method of Hestenes and Powell to convex programming (J. Optim. Theory Appl. 12). 1976: Rockafellar's "Augmented Lagrangians and applications of the proximal point algorithm in convex programming" (Math. Oper. Res. 1) gives the general convergence theory.

Setting

Let $X \subset \mathbb R^n$ be convex and $f_0, f_1, \dots, f_m : X \to \mathbb R$ convex. The problem is

\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \text{ subject to } f_i(x) \le 0,\ i = 1, \dots, m.

With $\theta(t) = \max\{0, t\}$ and a parameter $r > 0$ , the penalty Lagrangian is

L_r(x, y) = f_0(x) + \frac{1}{4r}\sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big], \qquad x \in X,\ y \in \mathbb R^m,

and the dual problem $(D_r)$ maximizes $g_r(y) = \inf_{x \in X} L_r(x, y)$ over all $y \in \mathbb R^m$ ; $\sup g_r$ is its supremum. A maximizing sequence is a sequence $\{y^k\}$ with $g_r(y^k) \to \sup g_r$ . The dual method of Theorem 4.1 takes a bounded maximizing sequence $\{y^k\}$ and, for each $k$ , a point $x^k \in X$ that minimizes $L_r(\cdot, y^k)$ to within a tolerance $\alpha_k$ :

L_r(x^k, y^k) - g_r(y^k) \le \alpha_k, \qquad \alpha_k \to 0. \qquad (4.7)

The standing assumptions of §5 concern a point $\bar x \in \operatorname{int} X$ that is an optimal solution of (P), near which $f_0, \dots, f_m$ are twice continuously differentiable, and a multiplier vector $\bar y$ satisfying with $\bar x$ the Kuhn–Tucker conditions ( $\bar y_i \ge 0$ , $f_i(\bar x) \le 0$ , $\bar y_i f_i(\bar x) = 0$ , and $\bar x$ minimizes $f_0 + \sum_i \bar y_i f_i$ over $X$ ). With $I = \{i : f_i(\bar x) = 0\}$ the active set and $H(x, y) = \nabla^2 f_0(x) + \sum_{i \in I} y_i \nabla^2 f_i(x)$ , they are: (i) $\bar y_i \ne 0$ for $i \in I$ ; (ii) the $\nabla f_i(\bar x)$ , $i \in I$ , are linearly independent; (iii) $z \cdot H(\bar x, \bar y) z > 0$ for every nonzero $z$ with $z \cdot \nabla f_i(\bar x) = 0$ for all $i \in I$ .

Formalization targets

Goal: Corollary 5.3

Under the standing assumptions, with $\{y^k\}, \{x^k\}, \{\alpha_k\}$ as in (4.7), if for some $q > 0$

\alpha_k \le q\,[\sup g_r - g_r(y^k)] \quad \text{for all sufficiently large } k, \qquad (5.18)

then there is a constant $s > 0$ with

|x^k - \bar x| \le s\,|y^k - \bar y| \quad \text{for all sufficiently large } k. \qquad (5.19)

No rate for $\{y^k\}$ is fixed: the statement compares the primal error with the dual error, whatever method produces the dual sequence.

Milestones

$\bar x$ is the unique optimal solution to (P) and $\bar y$ the unique optimal solution to the ordinary dual $(D_0)$ and every $(D_r)$ for $r > 0$ (§5, after (5.1)).
Theorem 5.1 (i)–(iii): for every $r, \beta > 0$ there are $\varepsilon, \alpha > 0$ such that $\sup g_r - g_r(y) \le \varepsilon$ and $L_r(x, y) - g_r(y) \le \alpha$ force $(x, y)$ into a $\beta$ -neighborhood of $(\bar x, \bar y)$ with $x \in \operatorname{int} X$ , where $L_r$ is $C^2$ , given locally by (5.4), and $\nabla_x^2 L_r(x, y)$ is positive definite.
Theorem 5.1 (iv): the unique minimizer $\xi(y)$ of $L_r(\cdot, y)$ over $X$ is $C^1$ in $y$ with derivative (5.5).
Theorem 5.1 (v): $g_r$ is $C^2$ with negative definite Hessian (5.6)–(5.7).
Corollary 5.2 (5.14): $x^k \to \bar x$ and $y^k \to \bar y$ .
Corollary 5.2 (5.15)–(5.17): $a|x^k - \xi(y^k)|^2 \le \alpha_k$ , $b_1|y^k - \bar y|_I \le |\xi(y^k) - \bar x| \le b_2|y^k - \bar y|_I$ , and $c_1|y^k - \bar y|^2 \le g_r(\bar y) - g_r(y^k) \le c_2|y^k - \bar y|^2$ .

Significance

Corollary 5.3 is the paper's answer to the practical question of how accurately each inner minimization must be done. A tolerance proportional to the current dual gap costs nothing in the order of convergence: the primal iterates then converge at least as fast as the dual ones. Since $g_r$ is $C^2$ with a negative definite Hessian near $\bar y$ (Theorem 5.1 (v)), any locally linearly or superlinearly convergent unconstrained method applied to $g_r$ yields a primal sequence with the same rate. The estimates (5.15)–(5.17) are the quantitative bridge between inner accuracy, dual error and primal error, and reappear in later analyses of inexact augmented Lagrangian methods.

The results are proved in the paper (1973) and in textbook treatments; none of them has a machine-checked proof on this platform or in Mathlib. The mission produces a formal statement of the second-order theory of the penalty Lagrangian: the local smooth structure of $L_r$ and $g_r$ , the implicit minimizer map $\xi$ , and the rate comparison. Complete formal proofs of each milestone are the remaining work.

Difficulty

The obvious argument linearizes everything at $(\bar x, \bar y)$ , but $L_r$ is only $C^1$ globally: $\theta^2$ has a kink in its second derivative, so smoothness of $L_r$ must first be established on a neighborhood of $(\bar x, \bar y)$ , using complementary slackness and strict complementarity (i) to fix which branch of (2.4) each constraint follows. The sequence $\{(x^k, y^k)\}$ is not assumed to converge; localizing it into that neighborhood requires the uniform statement of Theorem 5.1 (i) (with $\varepsilon, \alpha$ chosen after $r, \beta$ ) and the uniqueness of $\bar x$ and $\bar y$ . The minimizer map $\xi$ then comes from the implicit function theorem applied to $\nabla_x L_r(x, y) = 0$ , and the formula for $\nabla^2 g_r$ needs the derivative of the envelope $g_r(y) = L_r(\xi(y), y)$ .

Formalization scope

Spaces. Primal points lie in EuclideanSpace ℝ (Fin n), multipliers in EuclideanSpace ℝ (Fin m); constraint indices are Fin m (0-based), and $f_0$ is a separate argument.
Functions. The $f_i$ are total functions on $\mathbb R^n$ ; convexity is assumed on $X$ only (ConvexOn ℝ X, an explicit hypothesis of every theorem, the paper's standing assumption of p. 358), and twice continuous differentiability only on a neighborhood of $\bar x$ . Smoothness of $L_r$ and $g_r$ is always a conclusion, never a hypothesis.
Extended values. $g_0$ , $g_r$ , $\sup g_r$ and the infimum in (P) are computed in EReal, so (4.7), (5.2), (5.3) and (5.18) are differences in $[-\infty, +\infty]$ ; $r > 0$ is explicit for the penalty Lagrangian, while $L_0$ is defined separately.
Derivatives. Hessians are quadratic forms $z \cdot D(\nabla\varphi)(x) z$ ; every inverse matrix appears together with positive definiteness of the same matrix, so Lean's convention that a non-invertible map has inverse $0$ never applies. Local identities such as (5.4) are stated as equality on a neighborhood, not globally.
Choices. The assumption of Theorem 4.1 that the asymptotic optimal value is finite is omitted because it holds under the §5 assumptions. "Generated as in Theorem 4.1" is spelled out as its hypotheses. In (5.15)–(5.17), $\xi$ is any function that picks a minimizer of $L_r(\cdot, y)$ over $X$ whenever one exists; along $y^k$ it eventually coincides with the paper's unique minimizer. In (iv) and (v), the conclusions are stated for every $y$ with $\sup g_r - g_r(y) \le \varepsilon$ , since they do not depend on $x$ .
Ruled out. The goal does not assume that $x^k$ or $y^k$ converge, nor that $y^k \ne \bar y$ , and $s > 0$ is one constant valid for all large $k$ ; a formalization assuming convergence, or one with an unsatisfiable second-order hypothesis, would be trivial. The standing assumptions and all sequence hypotheses are satisfiable (checked on $f_0(x) = |x|^2$ , $f_1(x) = 1 - e\cdot x$ in $\mathbb R^1$ ).
Infrastructure. The proofs need the implicit function theorem (Mathlib's Analysis/Calculus/Implicit), second derivatives of compositions, envelope differentiation, and the quadratic-growth estimates of a $C^2$ function with definite Hessian. Results on Hessian forms and on strict complementarity are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
R. T. Rockafellar, The multiplier method of Hestenes and Powell applied to convex programming, Journal of Optimization Theory and Applications 12 (1973) 555–562. https://doi.org/10.1007/BF00934777
R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1 (1976) 97–116. https://doi.org/10.1287/moor.1.2.97

8 thms2 active usersReviewed

Completed

Analysis Probability Statistics·Captain: mikedeng1

Estimating Variance From High, Low and Closing Prices II: Under the Overshoot Law (9), E(Z ∨ Z′) = aσ√h and E(Z ∨ Z′)² = bσ²hResearch Paper

Motivation

Volatility estimates from daily high, low and closing prices have been used since Parkinson (1980) and Garman and Klass (1980): the range of a day's log-price carries much more information about the volatility $\sigma$ than the close alone. Rogers and Satchell (1991) propose an estimator, $S_1(S_1-X_1)+I_1(I_1-X_1)$ , that is unbiased for $\sigma^2$ whatever the drift of the log-price. The companion mission (Part I) formalizes that unbiasedness.

Every such estimator meets the same practical problem. The true high and low of the continuous path are never observed; one sees the maximum and minimum of the path sampled at $N$ times. The sampled maximum $S$ falls short of the true maximum $S_1$ by an amount $\Delta = S_1 - S \ge 0$ , and the resulting downward bias is large in practice (Garman and Klass, and Beckers (1983), identified it). Section 3 of Rogers and Satchell proposes a correction: model $\Delta$ by a random variable with an explicit law, compute its first two moments exactly, and subtract their effect. The constants that appear,

a=\sqrt{2\pi}\Big[\tfrac14-\tfrac{\sqrt2-1}{6}\Big],\qquad b=\frac{1+3\pi/4}{12},

enter the corrected estimator directly. Their simulations (Tables 1–3 of the paper) show that the correction removes most of the bias.

Setting

Fix a volatility $\sigma>0$ and a sampling mesh $h>0$ (in the paper $h=1/N$ ). For a level $\alpha\ge0$ define

G_{\sigma,h}(\alpha)=\int_0^h e^{-2\alpha^2/(u\sigma^2)}\,\frac{du}{(4uh)^{1/2}} .

The factor $e^{-2\alpha^2/(u\sigma^2)}$ is the probability that a Brownian bridge of duration $u$ and volatility $\sigma$ climbs above level $\alpha$ . The factor $(4uh)^{-1/2}$ is a probability density on $(0,h]$ . Since $G_{\sigma,h}(0)=1$ and $G_{\sigma,h}$ decreases continuously to $0$ , it is the survival function of a law on $(0,\infty)$ . This law is the paper's display (9).

A real random variable $Z$ has distribution (9) if it is measurable and $P(Z>\alpha)=G_{\sigma,h}(\alpha)$ for every $\alpha\ge0$ . In the paper, $Z$ is the overshoot of the continuous maximum over the sampled maximum $x$ in the sampling interval to the left of the time $t$ at which $x$ is attained, and $Z'$ is the overshoot in the interval to the right. The paper then assumes (p. 508) that $Z$ and $Z'$ are independent, each with distribution (9), and approximates $\Delta$ by $Z\vee Z'=\max(Z,Z')$ . Write $Z\wedge Z'=\min(Z,Z')$ .

In Lean, overshootSurvival σ h α is $G_{\sigma,h}(\alpha)$ , HasOvershootLaw P σ h Z is " $Z$ has distribution (9) under $P$ ", and constA, constB are $a$ and $b$ .

Formalization targets

Goal: the two moments of $Z\vee Z'$ (Eq. (11), p. 508, and the display on p. 509)

For $\sigma,h>0$ and $Z,Z'$ independent with distribution (9), the variables $Z\vee Z'$ and $(Z\vee Z')^2$ are integrable, and

E(Z\vee Z')=a\,\sigma\sqrt h,\qquad E\big[(Z\vee Z')^2\big]=b\,\sigma^2h .

Milestones, in the order the paper uses them

(9), p. 507. The two integral forms of the survival function agree:

\int_0^h e^{-2\alpha^2/(u\sigma^2)}\frac{du}{(4uh)^{1/2}}=\int_{h^{-1}}^\infty e^{-2\alpha^2s/\sigma^2}\frac{ds}{(4hs^3)^{1/2}} .

(10), p. 508. $EZ=\sigma(2\pi h)^{1/2}/8$ .
Display before (11), p. 508. $E(Z\wedge Z')=\sqrt{2\pi h}\,(\sqrt2-1)\,\sigma/6$ .
(12), p. 508. $EZ^2=\sigma^2h/6$ .
(13), p. 509. $E[(Z\wedge Z')^2]=\frac{\sigma^2h}{4}\big(1-\frac\pi4\big)$ .

The goal combines milestones 2–5 through $Z\vee Z'=Z+Z'-Z\wedge Z'$ , which the paper uses in (11).

Significance

The result. The two identities are the coefficients of the corrected estimator (5): replacing $\Delta$ and $\Delta^2$ by $a\sigma\sqrt h$ and $b\sigma^2h$ turns the high–low estimator into an equation whose positive root $\hat\sigma_h$ largely removes the discretization bias. The same constants correct the Garman–Klass estimator (p. 509). Without exact values for $a$ and $b$ the correction has no concrete form.

Formalizing it. The paper does each of the four double integrals in a line and says "after some calculation" twice. A machine-checked derivation confirms the printed constants, which are reused in the high–low volatility literature. It also states precisely what is exact (moments of the model law (9) under independence) and what is approximation (that the model describes $\Delta$ ). To our knowledge none of these identities has been formalized before.

Difficulty

The statements are elementary but none of them is a one-line identity. Each moment is a double or triple improper integral with singular weights $(4hs^3)^{-1/2}$ on an unbounded domain. The minimum of $Z$ and $Z'$ couples two such integrals, and the resulting kernels $(s+u)^{-1/2}$ and $\sqrt{st}/(s+t)$ have to be integrated in closed form over the unit square. Matching $\sqrt2-1$ and $1-\pi/4$ exactly leaves no room for slack. In Lean, every exchange of integration order, change of variables and passage from survival functions to moments has to be justified for non-negative but unbounded functions, and the expectations must be shown finite: the Bochner integral of a non-integrable function is $0$ .

Formalization scope

Model. Random variables live on an arbitrary probability space (Ω, P) with [IsProbabilityMeasure P]. "Distribution (9)" is Measurable Z ∧ ∀ α ≥ 0, P.real {α < Z} = G σ h α, imposed only at levels $\alpha\ge0$ : the formula is even in $\alpha$ , and imposing it at negative levels would make the hypothesis unsatisfiable. Independence is IndepFun Z Z' P. $Z\vee Z'$ and $Z\wedge Z'$ are max and min.
Parameters. $\sigma>0$ and $h>0$ only. The paper's $h=1/N\le1$ is not needed and not imposed.
Explicit readings. "E" is the Bochner integral, and every expectation identity carries its integrability (Integrable, or MemLp … 2 for second moments). The conditioning " $\mid t-h<H_x<t,\ X_t=x$ " in (9) and (10) is the modelling context in which the paper derives the law, not a hypothesis. The paper's " $E(Z\wedge Z')^2$ " in (13) is read as $E[(Z\wedge Z')^2]$ , as its first line shows. The integrals in (9) run over $(0,h]$ and $[h^{-1},\infty)$ .
Not formalized. The approximate statements $E\Delta\doteq a\sigma\sqrt h$ and $E\Delta^2\doteq b\sigma^2h$ , the densities (6) and (7), and the independence remark of p. 508 are modelling approximations about the random walk, not theorems. The estimators (5) and $\hat\sigma^2_{GK,h}$ are definitions with no claim attached. The Brownian-bridge maximum (8) is not stated (its print also has a slip: $1-2/u$ for $1-s/u$ ). Section 4 (simulations) is out of scope.
Non-triviality. The hypotheses are satisfiable for every $\sigma,h>0$ : a probability measure on $\mathbb R$ with survival function $G_{\sigma,h}$ exists, and the two coordinates under its product measure are independent copies. A formalization that stated the survival condition for all $\alpha\in\mathbb R$ would be vacuous and is ruled out. So is one without the integrability conjuncts, which could hold with both sides $0$ .
Related items. The platform's generic identity survival_mean_ibp (mean as an integral of the survival function, under derivative hypotheses) is related but does not fit this setting. Mathlib's layer-cake formula is the general tool for passing between survival functions and moments.
Welcome contributions. Closed forms for $\int_0^1\!\int_0^1(s+t)^{-1/2}\,ds\,dt$ and $\int_0^1\!\int_0^1\sqrt{st}/(s+t)\,ds\,dt$ , which are reusable lemmas, and a general "moments of $\max$ and $\min$ of independent variables from their survival functions" lemma.

Selected references

L. C. G. Rogers and S. E. Satchell, Estimating variance from high, low and closing prices, The Annals of Applied Probability 1(4) (1991), 504–512. https://doi.org/10.1214/aoap/1177005835
M. B. Garman and M. J. Klass, On the estimation of security price volatilities from historical data, Journal of Business 53(1) (1980), 67–78. https://doi.org/10.1086/296072
M. Parkinson, The extreme value method for estimating the variance of the rate of return, Journal of Business 53(1) (1980), 61–65. https://doi.org/10.1086/296071
S. Beckers, Variances of security price returns based on high, low and closing prices, Journal of Business 56(1) (1983), 97–112.

8 thms2 active usersReviewed

Mathematical Physics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XIII: The Sherrington–Kirkpatrick Model at High Temperature — Deviations of log Z_N from β²N/4Textbook

Motivation

The Sherrington–Kirkpatrick model assigns random interactions to every pair of spins in a system. Its partition function aggregates the weights of all spin configurations, and the logarithm of that partition function is the free energy. For a finite system, the free energy is a random quantity because the interactions are random. A useful question is therefore how far it can move from a deterministic high-temperature scale. Aizenman, Lebowitz and Ruelle (1987), and Comets and Neveu (1995) for Gaussian couplings, proved that for $\beta<1$ the variable $\log Z_N-\beta^2N/4$ converges in law to a normal random variable ALR 1987; Talagrand asks instead for tail estimates valid for every $N$ . Talagrand's Chapter 12 gives a finite-size tail bound and a bound on the expected free energy per site under explicit moment conditions on the interaction law Talagrand 1995.

The chapter belongs to a larger study of concentration inequalities on product spaces. Its relevance to the spin model is concrete: each pair interaction is an independent coordinate, while every spin configuration uses all those coordinates. The number of coordinates grows quadratically with the number of spins. A uniform estimate must respect both this growing dimension and the normalization in the energy Talagrand 1995, pp. 191–195.

Setting

Fix an integer $N\ge1$ . A spin configuration is a vector $\varepsilon=(\varepsilon_i)_{1\le i\le N}$ with each $\varepsilon_i\in\{-1,1\}$ . Each unordered pair of sites $i<j$ has a real coupling $h_{ij}$ . For an inverse temperature $\beta>0$ , the normalized partition function is

Z_N(h)=2^{-N}\sum_{\varepsilon\in\{-1,1\}^N} \exp\left(\frac{\beta}{\sqrt N}\sum_{1\le i<j\le N} h_{ij}\varepsilon_i\varepsilon_j\right).

Write $F_N(h)=\log Z_N(h)$ . The factor $2^{-N}$ averages over configurations. Since every summand is positive, $Z_N(h)>0$ for every array $h$ , so this logarithm is defined without excluding any coupling array.

The couplings are independent with a common probability law $\nu$ on $\mathbb R$ ; their joint law is $P_N=\nu^{\otimes\binom N2}$ . Under $\nu$ , a single coupling $H$ satisfies $\mathbb EH=\mathbb EH^3=0$ and $\mathbb EH^2=1$ . The chapter also assumes $\mathbb E e^{\alpha|H|}<\infty$ for some $\alpha>0$ . Its main theorem adds $\mathbb Ee^H<2$ and $\mathbb Ee^{-H}<2$ . These inequalities describe a class of interaction laws rather than one chosen distribution. A median $M_N$ of $F_N$ means that both $P_N(F_N\le M_N)$ and $P_N(F_N\ge M_N)$ are at least $1/2$ Talagrand 1995, pp. 191–193.

Formalization targets

The goal is Theorem 12.1. There is one absolute constant $K>0$ such that, for $0<\beta<1$ and $0<t<N/K$ ,

P_N\left(\left|F_N-\frac{\beta^2N}{4}\right|\ge K\left(t+\sqrt{\log\frac K{1-\beta^2}}\right)\sqrt N\right) \le 2e^{-t^2},

and the same constant satisfies

-\frac K{\sqrt N}\sqrt{\log\frac2{1-\beta^2}} \le \frac1N\mathbb EF_N-\frac{\beta^2}{4} \le \frac KN.

The first formula controls deviations at finite $N$ ; the second locates the expected free energy per site. The theorem leaves the absolute value of $K$ unspecified, as the source does Talagrand 1995, Theorem 12.1.

Four numbered displays form the supporting targets. Equation (12.6) bounds the change in $F_N$ when all couplings are changed. Equation (12.5) bounds deviations about any median. Equations (12.7) and (12.8) give first- and second-moment estimates for $Z_N$ . Together these specify the deterministic regularity and probabilistic estimates used by the chapter Talagrand 1995, pp. 192–195.

Significance

The theorem gives a nonasymptotic probability estimate, valid for each finite size and each law meeting the stated conditions. It also bounds the difference between the mean free energy per site and $\beta^2/4$ as $N$ grows, for fixed $\beta<1$ . The moment estimates separately describe the scale of the partition function and limit its relative second moment. These conclusions keep the coupling law general within the stated moment class Talagrand 1995, Theorem 12.1 and Eqs. (12.7)–(12.8).

The result is proved in the cited paper; the open work here is its Lean formalization. A completed development would connect product-measure concentration, finite spin sums, exponential-moment bounds, and real-valued expectations in one reusable interface. The coupling product space and median conventions can also serve other finite random-interaction models. No machine-checked proof of this chapter's target is claimed by this proposal.

Difficulty

A direct bounded-differences estimate cannot be applied to this model as stated: the couplings are real and may be unbounded. An estimate that handles each coordinate must account for the law's exponential moments while still retaining the $N$ and $\beta$ factors in the chapter's explicit bounds. The normalization by $\sqrt N$ makes a single coupling's influence small, but there are $\binom N2$ couplings, so treating the total sensitivity as dimension-free would lose the scale of the theorem. The first moment alone also does not control the lower tail of $Z_N$ ; this is why the second-moment target is present Talagrand 1995, pp. 192–195.

Formalization scope

Lean indexes sites by Fin N and interactions by pairs with $i<j$ . A spin is a Boolean choice interpreted as $-1$ or $1$ , and the configuration sum is normalized by $2^N$ . The coupling array is a function on the pair type, carrying the finite product measure of the common law $\nu$ . The theorem uses $N\ge1$ , $0<\beta<1$ , and exactly the common-law moment assumptions above; the median deviation milestone uses $N\ge2$ because its denominator contains $N-1$ . The main theorem places its single universal $K$ before every size, temperature, law, and deviation level.

Expectations are Bochner integrals, so integrability is explicit in the law predicates or in each conclusion that needs it. Probability expressions are real values of measurable events under the product measure. This avoids relying on Lean's default value for a nonintegrable integral. The model retains the entire real coupling law and does not replace it with a finite alphabet or a Gaussian special case. The partition function is built from the couplings and spins, rather than supplied as an unconstrained variable.

The source's displayed (12.5) omits $\beta$ , whereas the derivation following (12.6) gives, for each tail separately, the range $0<t\le4\beta\sqrt N(N-1)$ and the exponent $-t^2/(32\beta^2(N-1))$ with the factor $2$ . The formal milestone states exactly these two one-sided bounds, while its milestone text preserves the printed display verbatim. The first- and second-moment displays are kept with an absolute constant; the second-moment target uses the proof's $N\ge8$ range, since for smaller sizes the chapter's interaction-law assumptions do not ensure that $Z_N^2$ is integrable. Integrability of $F_N$ is a conclusion of the main theorem, never a hypothesis, and the median is quantified universally, so neither the expectation in (12.4) nor the deviation bound can hold by a default value of an undefined integral or by an unsatisfiable hypothesis; the Rademacher law $\nu=\frac12(\delta_{-1}+\delta_1)$ satisfies every assumption. Reusable contributions include integrability and measurability of $Z_N$ and $F_N$ , product-law estimates, and the source's numbered inequalities.

Selected references

Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.
Michael Aizenman, Joel L. Lebowitz, David Ruelle, Some rigorous results on the Sherrington–Kirkpatrick spin glass model, Communications in Mathematical Physics 112 (1987), 3–20. DOI: 10.1007/BF01217677.
Francis Comets, Jacques Neveu, The Sherrington–Kirkpatrick model of spin glasses and stochastic calculus: the high temperature case, Communications in Mathematical Physics 166 (1995), 549–564. DOI: 10.1007/BF02099887.

6 thms2 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VI: The Symmetric Group — ∫ exp(f(A,σ)/16) dP_N ≤ 1/P_N(A) for the Convex Distance on S_NTextbook

Motivation

Concentration of measure on the symmetric group concerns random permutations. A uniformly random permutation of $N$ objects appears in random assignment problems, in sampling without replacement, in the longest increasing subsequence and in the analysis of randomized algorithms. A tail bound for a function of a random permutation is useful when it does not require computing the function's distribution. The symmetric group is not a product space, so the inequalities proved for product spaces do not apply to it directly.

Timeline. B. Maurey [Maurey 1979] gave the first concentration inequality on $S_N$ , for distances that count the coordinates in which two permutations differ. Every permutation can be written uniquely as $\sigma=t_{N,i(N)}\circ\cdots\circ t_{2,i(2)}$ with $i(j)\le j$ , where $t_{i,j}$ is the transposition of $i$ and $j$ . Through this decomposition the Hamming bound (2.1.3) for product spaces carries over to $S_N$ . Milman and Schechtman present the result in their monograph [Milman–Schechtman 1986]. In Chapter 5 of his 1995 memoir Talagrand 1995, M. Talagrand proves the analogue on $S_N$ of his convex hull inequality (Theorem 4.1.1 of the memoir). In the author's words, it improves Maurey's result in the way that Theorem 4.1.1 improves Proposition 2.1.1.

Setting

$S_N$ is the group of permutations of $\{1,\dots,N\}$ and $P_N$ is the uniform probability on it. Fix $A\subseteq S_N$ and $\sigma\in S_N$ . A 0–1 vector $s$ is admissible if some $\tau\in A$ agrees with $\sigma$ at every coordinate where $s$ is zero:

U_A(\sigma)=\bigl\{s\in\{0,1\}^N:\ \exists\tau\in A,\ \forall\ell\le N,\ s_\ell=0\Rightarrow\tau(\ell)=\sigma(\ell)\bigr\}.

$V_A(\sigma)\subseteq[0,1]^N$ is the convex hull of $U_A(\sigma)$ , and

f(A,\sigma)=\inf\Bigl\{\sum_{\ell\le N}s_\ell^2:\ s\in V_A(\sigma)\Bigr\}

is the squared convex distance from $\sigma$ to $A$ . Unlike $f_c$ of Chapter 4, $f$ here is already squared. If $\sigma\in A$ , then $0\in U_A(\sigma)$ and $f(A,\sigma)=0$ . A permutation that agrees with some element of $A$ outside $k$ coordinates has $f(A,\sigma)\le k$ .

The proof uses three variants. $f(A,\sigma,p)$ counts coordinate $p$ twice, $s_p^2+\sum_\ell s_\ell^2$ . $f(A,\sigma,p,m)$ , for $p\ne m$ , restricts that infimum to the face $s_m=0$ (Eq. (5.5)). $g(A,\sigma,i,j)$ drops coordinates $i$ and $j$ (Eq. (5.6)). In $S_{N+1}$ , $G_i=\{\sigma:\sigma(i)=N+1\}$ and $G'_i=\{\sigma:\sigma(N+1)=i\}$ , with uniform probabilities $Q_i$ and $Q'_i$ . $t_i$ is the transposition of $N+1$ and $i$ . The maps $R(\rho)=\rho\circ t_i$ and $R'(\rho)=t_i\circ\rho$ send $G_i$ and $G'_i$ , respectively, onto the permutations fixing $N+1$ , that is, onto $S_N$ .

Formalization targets

Goal: Theorem 5.1

For every $N$ and every $A\subseteq S_N$ ,

\int_{S_N}\exp\frac1{16}f(A,\sigma)\,dP_N(\sigma)\le\frac1{P_N(A)}.\tag{5.2}

The constant $1/16$ is the paper's.

Stronger: Proposition 5.2

For every $A\subseteq S_N$ and every $p\le N$ ,

\int\exp\tfrac1{16}f(A,\sigma,p)\,dP_N\le\tfrac1{P_N(A)}\quad(5.3)_N,\qquad\int\exp\tfrac1{16}f(A,\sigma,\sigma^{-1}(p))\,dP_N\le\tfrac1{P_N(A)}\quad(5.4)_N.

Since $f(A,\sigma)\le f(A,\sigma,p)$ , this pair implies Theorem 5.1.

Milestones

The milestones are the numbered results of the induction step from $N$ to $N+1$ , in the order of the paper:

the deterministic inequalities Lemma 5.3 (5.7) and Lemma 5.7 (5.14);
the transfer lemmas Lemma 5.4 (5.8) and Lemma 5.8 (5.15);
the integral bounds Corollary 5.5 (5.10), Lemma 5.6 (5.11), Corollary 5.9 (5.16) and Lemma 5.10 (5.17).

Significance

The result. Theorem 5.1 has the same form as Theorem 4.1.1. By Markov's inequality, $P_N(A)\,P_N\{f(A,\cdot)\ge t\}\le e^{-t/16}$ . Any function on $S_N$ that is controlled by the convex distance therefore concentrates around its median with Gaussian tails whose scale does not depend on $N$ . Because the convex distance weighs coordinates by an arbitrary unit vector, this includes functions that are Lipschitz only in a weighted, configuration-dependent sense, which a Hamming-distance bound does not reach. This is the setting of random permutation problems such as the longest increasing subsequence and the assignment problem.

Formalizing it. The result has been proved since 1995. To the best of current knowledge none of Chapter 5 has a machine-checked proof, and the platform has no concentration statement on $S_N$ . This mission formalizes the statements and the induction of the chapter. Its reusable output is the convex distance on $S_N$ and the embedding of $S_N$ into $S_{N+1}$ through the blocks $G_i$ , $G'_i$ .

Difficulty

$S_N$ sits inside $\{1,\dots,N\}^N$ through $\sigma\mapsto(\sigma(i))_{i\le N}$ . If $S_N$ were the whole product, (5.2) would follow from Theorem 4.1.1. But $S_N$ is a very small subset of that product, and the uniform measure on $S_N$ is not a product measure. The decomposition into transpositions does give a product structure, but it is highly non-commutative. Coordinate distances in the decomposition do not match coordinate distances of the permutations, so it transfers only the weaker Hamming-type bound. The paper notes that a direct induction on $N$ for (5.2) itself apparently fails. The strengthened pair $(5.3)_N$ , $(5.4)_N$ is needed, and its two halves cross: $(5.4)_{N+1}$ is proved from $(5.3)_N$ , and $(5.3)_{N+1}$ from $(5.4)_N$ .

Formalization scope

$S_N$ is Equiv.Perm (Fin N), with indices from $0$ . In $S_{N+1}$ the point $N+1$ is Fin.last N, and composition is the group product, so $\rho\circ t_i$ is ρ * t N i.
$U_A(\sigma)\subseteq\mathbb R^N$ , and $V_A(\sigma)$ is convexHull ℝ. The functionals $f$ , $f(\cdot,\cdot,p)$ , $f(\cdot,\cdot,p,m)$ and $g$ are infima of explicit sums of squares, so the sup norm on Fin N → ℝ plays no role. They take values in $[0,+\infty]$ , so an empty infimum is $+\infty$ and $f(\emptyset,\sigma)=+\infty$ . The integrand $\exp(z/16)$ is computed in EReal, so $\exp(+\infty)=+\infty$ .
The uniform probabilities $P_N$ , $Q_i$ and $Q'_i$ are explicit finite averages over $S_N$ , $G_i$ and $G'_i$ . $Q_i(A)$ means $|A\cap G_i|/|G_i|$ . $1/P_N(A)$ is computed in ℝ≥0∞, so $A=\emptyset$ gives $+\infty$ on both sides.
$R(\sigma)$ and $R'(\sigma)$ enter through the relation Restricts ρ τ ( $\rho(\ell)=\tau(\ell)$ for $\ell\le N$ ). $R(A_i)$ and $R'(A'_i)$ are the corresponding image sets.
The integral bounds 5.5, 5.6, 5.9 and 5.10 are stated in the paper inside the induction step. Each carries the induction hypothesis it uses as an explicit binder: $(5.3)_N$ , $(5.4)_N$ , or "either" as a disjunction.
A trivializing formalization is ruled out. The distance is the convex-hull distance with sums of squares, not a sup norm or Hamming count. The constant $1/16$ is kept, and the infimum over the empty set is $+\infty$ , not a junk $0$ .
Lemma 4.1.3, the numerical inequality used in the Hölder step, belongs to mission V of this series and is not posed again here.

Contributions are welcome at every level: proofs of the deterministic lemmas, the bijections $G_i\to S_N$ and their measure-transport facts, and the final Hölder–Lemma 4.1.3 step.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205, Chapter 5, pp. 144–150. https://doi.org/10.1007/BF02699376
B. Maurey, Construction de suites symétriques, C. R. Acad. Sci. Paris Sér. A 288 (1979), 679–681 (reference [M1] of the memoir; no DOI).
V. D. Milman, G. Schechtman, Asymptotic theory of finite dimensional normed spaces, Lecture Notes in Math. 1200, Springer, 1986. https://doi.org/10.1007/978-3-540-38822-7

11 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

A Dual Approach to Solving Nonlinear Programming Problems by Unconstrained Optimization 1: Approximate Minimizers of L_r(·, yᵏ) along a Bounded Maximizing Dual Sequence Are Asymptotically MinimizingResearch Paper

Motivation

Constrained convex programs are routinely solved by turning them into a sequence of unconstrained problems. The classical route is the ordinary Lagrangian $L_0(x, y) = f_0(x) + \sum_i y_i f_i(x)$ , whose dual function $g_0$ is in general nonsmooth and equal to $-\infty$ off the orthant $y \ge 0$ , so maximizing it requires a constrained, nonsmooth method. In 1969 Hestenes (JOTA 4, 1969) and Powell (in Optimization, ed. Fletcher, Academic Press, 1969) proposed the method of multipliers for equality constraints, which adds a quadratic penalty to the Lagrangian. Rockafellar's paper (Math. Programming 5, 1973) gives the inequality-constrained version, the penalty Lagrangian $L_r$ , and shows that for convex programs its dual is a smooth, unconstrained, concave maximization problem with the same solutions and value as the ordinary dual. The method of multipliers built on this Lagrangian, now called the augmented Lagrangian method, underlies ADMM and many large-scale solvers.

Timeline. Hestenes and Powell (1969): multiplier method for equality constraints. Rockafellar (1973, this paper; and JOTA 12, 1973): the inequality-constrained penalty Lagrangian, its duality theory, and convergence of the multiplier method for convex programs. Rockafellar (Math. Oper. Res. 1, 1976): the method of multipliers identified as the proximal point algorithm applied to the dual. Bertsekas (Constrained Optimization and Lagrange Multiplier Methods, 1982): the general nonconvex theory.

This mission covers the first half of the paper: the duality theory of $L_r$ (§3) and the theorem that maximizing the penalty dual yields asymptotically optimal primal sequences (§4, Theorem 4.1).

Setting

Let $X$ be a nonempty convex subset of a real vector space $E$ and $f_0, f_1, \dots, f_m$ convex real functions on $X$ . The problem is

\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \text{ subject to } f_i(x) \le 0,\ i = 1, \dots, m.

Multipliers $y$ range over $\mathbb R^m$ , with Euclidean norm $|\cdot|$ and inner product $u \cdot y$ . With $\theta(t) = \max\{0, t\}$ and a parameter $r > 0$ , the penalty Lagrangian is

L_r(x, y) = f_0(x) + \frac{1}{4r} \sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big],

defined for all $y \in \mathbb R^m$ with no sign restriction. The dual function is $g_r(y) = \inf_{x \in X} L_r(x, y)$ , and the dual problem $(D_r)$ maximizes $g_r$ over $\mathbb R^m$ ; $g_0$ and $(D_0)$ are the same with $L_0$ , and $\sup g_0$ is the dual optimal value. In Lean these objects are Lr, L0, gr, g0, dualValue, and Fr is the perturbed objective $F_r(x, u) = f_0(x) + r|u|^2$ if $u \ge f(x)$ , $+\infty$ otherwise.

A sequence $\{x^k\}$ in $X$ is asymptotically feasible if $\limsup_k f_i(x^k) \le 0$ for every $i$ . The asymptotic optimal value (asympValue) is the infimum of $\limsup_k f_0(x^k)$ over asymptotically feasible sequences, and a sequence attaining it is asymptotically minimizing (IsAsympMinimizing). A maximizing sequence for $(D_r)$ is a sequence $\{y^k\}$ with $g_r(y^k) \to \sup g_r$ .

Formalization targets

Goal: Theorem 4.1

Suppose the asymptotic optimal value in (P) is finite, $r > 0$ , $\{y^k\}$ is a bounded maximizing sequence for $(D_r)$ , and $x^k \in X$ satisfies

L_r(x^k, y^k) - g_r(y^k) \le \alpha_k, \qquad \alpha_k \to 0.

Then $\{x^k\}$ is asymptotically minimizing for (P).

Milestones

Theorem 3.1: $L_r(x, y) = \min_u \{F_r(x, u) + u \cdot y\}$ ; $L_r$ is convex in $x$ and concave in $y$ .
Theorem 3.2: $g_r(y) = \max_z \{g_0(z) - \frac{1}{4r}|z - y|^2\}$ ; $(D_r)$ and $(D_0)$ have the same supremum and optimal solutions; if $g_0 \not\equiv -\infty$ , $g_r$ is finite and $C^1$ with $\partial g_r/\partial y_i = \max\{-y_i/2r, f_i(x)\}$ at any $x$ attaining $g_r(y)$ .
Corollary 3.3: $g_r(y) + (y' - y)\cdot\nabla g_r(y) \ge g_r(y') \ge g_r(y) + (y'-y)\cdot\nabla g_r(y) - \frac{1}{4r}|y'-y|^2$ .
§4 (p. 364): the asymptotic optimal value equals the dual optimal value when the latter is not $-\infty$ or asymptotically feasible sequences exist.
Lemmas 4.2 and 4.3: $r|\nabla g_r(y)|^2 \le \sup g_r - g_r(y)$ , and $r|\nabla_y L_r(x, y) - \nabla g_r(y)|^2 \le \alpha$ under (4.7).
(4.9)–(4.11): $u \mapsto F_0(x, u) + u \cdot y + r|u|^2$ has the unique minimizer $\nabla_y L_r(x, y)$ .

Significance

Theorem 4.1 says that any procedure that drives the smooth, unconstrained dual $g_r$ to its supremum, while computing $L_r(\cdot, y^k)$ -minimizers only approximately, produces an asymptotically optimal primal sequence. It needs no constraint qualification, no existence of a dual or primal optimal solution, and not even feasibility of (P): only that the asymptotic optimal value is finite. Together with Theorem 3.2 it justifies the multiplier method as a dual ascent on a $C^1$ concave function with Lipschitz gradient, and it is the starting point of the convergence theory of augmented Lagrangian methods.

None of these statements is formalized on Prove2Me or in Mathlib, which has Lagrangian duality only in special forms and no theory of the penalty Lagrangian or of asymptotic optimal values. The Qi–Sun augmented Lagrangian items on the platform (NonsmoothNewton.AugLagrangian.*) use the $(r/2)$ -scaled function on $\mathbb R^n$ and concern smoothness in $(x, y)$ , not the dual function. The results of this paper are classical and proved; this mission formalizes them.

Difficulty

The obvious argument compares the primal iterates with a saddle point: if $\bar y$ is a dual optimal solution and (P) is normal, approximate minimizers of $L_r(\cdot, \bar y)$ are approximately optimal. Theorem 4.1 assumes neither. The function $g_r$ need not attain its supremum, (P) need not be normal or even feasible, and there may be no Kuhn–Tucker vector, so there is no saddle point to compare with; the only data are the dual values $g_r(y^k)$ , the boundedness of $\{y^k\}$ and the tolerances $\alpha_k$ . The difficulty is to obtain primal feasibility and optimality information from dual convergence alone, measured against the asymptotic optimal value rather than the infimum in (P). Every ingredient is extended-real-valued: $g_0$ is $-\infty$ off the orthant, $g_r$ may be identically $-\infty$ , and the asymptotic optimal value may be $\pm\infty$ . Mathlib does not package this part of convex analysis (partial conjugates, envelopes of extended-real concave functions, the asymptotic duality theorem).

Formalization scope

$E$ is a bare real vector space (AddCommGroup E, Module ℝ E) with no topology, as in the paper. The functions $f_i$ are total functions $E \to \mathbb R$ assumed convex on $X$ ; only their values on $X$ enter. Constraint indices are Fin m (0-based) and $f_0$ is a separate argument. Multipliers live in EuclideanSpace ℝ (Fin m). The standing assumption of §3 ( $X$ nonempty convex, all $f_i$ convex) is a hypothesis of every theorem.

Explicit choices:

$g_r$ , $g_0$ , the dual value, the asymptotic optimal value and every $\limsup$ are computed in EReal, so $\pm\infty$ are represented and no infimum is replaced by a junk real value.
$r > 0$ is an explicit hypothesis wherever $L_r$ is used; $L_0$ is a separate definition.
(4.7) is written $L_r(x^k, y^k) \le g_r(y^k) + \alpha_k$ in EReal, equivalent to the printed difference; only $\alpha_k \to 0$ is assumed.
Concavity or convexity of extended-real functions is stated through convex hypographs and epigraphs; "max" in (3.5) is attainment of the greatest value.
Gradients are taken of the real coercion of $g_r$ , and only under hypotheses that make $g_r$ finite.
Dual optimal solutions do not exist when $g_r \equiv -\infty$ (the paper's convention, p. 361).
Lemmas 4.2, 4.3 and (4.9)–(4.11) are stated for one point rather than along a sequence; the paper's statements are their instances.
Misprints: "concave in $y \in Y$ " (Theorem 3.1) reads $\mathbb R^m$ ; the lost minus sign in Lemma 4.2 is restored.

The goal must not be replaced by " $f_0(x^k) \to \inf\text{(P)}$ and $\limsup f_i(x^k) \le 0$ ": that is the special case of normal problems with feasible solutions. Nor may it assume a Slater point, a Kuhn–Tucker vector, or feasibility of (P), each of which makes it a special case.

A complete development needs extended-real convex analysis on $\mathbb R^m$ (partial conjugates, Moreau envelopes of concave functions, the asymptotic duality theorem), which is reusable beyond this mission. Contributions proving any milestone, or general lemmas on Moreau envelopes of extended-real concave functions, are welcome.

Selected references

R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
R. T. Rockafellar, The multiplier method of Hestenes and Powell applied to convex programming, Journal of Optimization Theory and Applications 12 (1973) 555–562. https://doi.org/10.1007/BF00934777
R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1 (1976) 97–116. https://doi.org/10.1287/moor.1.2.97
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982.

11 thms2 active usersReviewed

Completed

Analysis Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces I: Control by One Point — ∫ e^{t f(A,x)} dP ≤ P(A)^{−α} exp(Nt²(1+1/α)/8) for the Hamming Distance to ATextbook

Motivation

Concentration of measure is the observation that, on a high-dimensional product probability space, any set that is not too small already contains most of the space within a small neighbourhood. For functions of many independent random variables this yields Gaussian-type tail bounds without any explicit computation of the distribution, and these bounds are the working tool behind the analysis of random combinatorial optimisation problems (bin packing, the travelling salesman problem, the longest increasing subsequence, the assignment problem), random graphs, and empirical processes.

M. Talagrand's 1995 memoir Talagrand 1995 develops a family of such inequalities that hold on an arbitrary product of probability spaces and are proved by induction on the number of coordinates. Chapter 2 opens with the simplest instance, control by one point: the distance from $x$ to a set $A$ is measured by the number of coordinates in which $x$ differs from the best single point $y \in A$ . The method of this chapter is the template for every later chapter of the memoir.

Timeline. Bounds of the form (2.2.7) for the Hamming distance were first obtained with martingale (bounded differences) methods, collected in McDiarmid's survey McDiarmid 1989. Talagrand's 1995 memoir gives the induction proof reproduced here, with exponent $-\tfrac2N(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}})^2$ , which the paper notes is exactly the best bound obtained by martingales. Earlier, the isoperimetric inequality on the discrete cube (Harper, 1966) settles the case of the uniform measure on $\{0,1\}^N$ .

Setting

Let $(\Omega,\Sigma,\mu)$ be a probability space and $N \ge 0$ an integer. Points of the product $\Omega^N$ are written $x=(x_1,\dots,x_N)$ , and $P=\mu^N$ denotes the product probability. For a set $A \subseteq \Omega^N$ and a point $x$ , the Hamming distance to $A$ is

f(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i\ne y_i\}\ :\ y\in A\big\},

the least number of coordinates that must be changed to move $x$ into $A$ ; it is $+\infty$ when $A$ is empty. Given positive weights $(a_i)_{i\le N}$ , the weighted Hamming distance replaces the count by $\sum\{a_i: x_i\neq y_i\}$ .

Two families of constants appear. The first is

a(t)=\frac12+\frac{e^t+e^{-t}}4 ,

and the second, for $\alpha>0$ and $t>0$ ,

a(\alpha,t)=\frac{\alpha^{\alpha}}{(\alpha+1)^{\alpha+1}}\,\frac{(e^t-e^{-t/\alpha})^{1+\alpha}}{(1-e^{-t/\alpha})(e^t-1)^{\alpha}},

extended by its limit $a(\alpha,0)=1$ ; one checks $a(1,t)=a(t)$ .

Formalization targets

Goal: Corollary 2.2.3

For every measurable $A\subseteq\Omega^N$ , every $\alpha>0$ and every $t\ge0$ ,

\int e^{t f(A,x)}\,dP(x)\ \le\ \frac{1}{P(A)^{\alpha}}\exp\Big(N\frac{t^2}{8}\Big(1+\frac1\alpha\Big)\Big), \tag{2.2.6}

and, when $P(A)>0$ , for every $k\ge\sqrt{\tfrac N2\log\tfrac1{P(A)}}$ ,

P\big(\{f(A,\cdot)\ge k\}\big)\ \le\ \exp\Big(-\frac2N\Big(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}}\Big)^2\Big). \tag{2.2.7}

Milestones, in attack order

Lemma 2.1.2 — for measurable $0\le g\le1$ on $\Omega$ : $\int\min(e^t,1/g)\,d\mu\int g\,d\mu\le a(t)$ .
Proposition 2.1.1 — $\int e^{tf(A,x)}dP\le a(t)^N/P(A)\le e^{t^2N/4}/P(A)$ for $t>0$ , and $P(f(A,\cdot)\ge k)\le e^{-k^2/N}/P(A)$ .
Remark 2.1.3 — the same with the weighted Hamming distance and $\sum a_i^2$ in place of $N$ .
Eq. (2.2.3) — $a(\alpha,t)=\sup_{0\le u\le1}(1+u(e^t-1))(1-u(1-e^{-t/\alpha}))^{\alpha}$ .
Proposition 2.2.1 — $\int e^{tf(A,x)}dP\le a(\alpha,t)^N/P(A)^{\alpha}$ for $t\ge0$ .
Lemma 2.2.2 — $a(\alpha,t)\le\exp\frac{t^2}8(1+\frac1\alpha)$ .

The goal is the weakest statement of the section that is stated with fully explicit, closed-form constants; the milestones are the steps the paper's proof passes through.

Significance

The result. Inequality (2.2.7) shows that if $P(A)$ is bounded below, the set of points at Hamming distance at least $\sqrt{N/2\cdot\log(1/P(A))}+s$ from $A$ has probability at most $e^{-2s^2/N}$ , with no assumption on $\Omega$ or $\mu$ . Applied to $A=\{F\le M\}$ for a function $F$ that changes by at most one when a coordinate changes, it gives concentration of $F$ around its median at scale $\sqrt N$ . The exponential moment bound (2.2.6) is the form that composes with other estimates, and the free parameter $\alpha$ is what makes the constant $2/N$ in (2.2.7) attainable rather than $1/N$ as in (2.1.3).

Formalizing it. The results are classical and fully proved in the paper; they are not available in Mathlib, and no machine-checked proof of them is known. A formalization supplies the one-coordinate inequalities (Lemma 2.1.2 and its $\alpha$ -version) and the induction over $\Omega^{N+1}=\Omega^N\times\Omega$ as reusable components: every later chapter of the memoir (two-point space, penalties, $q$ points, convex hull distance) follows the same induction with a different one-coordinate lemma.

Difficulty

The bound does not follow from a union bound or from independence of coordinates, because $f(A,\cdot)$ depends on all coordinates jointly through an arbitrary set $A$ : changing one coordinate of $x$ changes $f(A,x)$ by at most one, but which point of $A$ is nearest can change completely. A naive coordinate-by-coordinate estimate loses either the dependence on $P(A)$ or a constant factor in the exponent, and the constant $2/N$ in (2.2.7) is the sharp one, so no slack is available. The one-dimensional inequalities (Lemma 2.1.2 and its $\alpha$ -version) are extremal problems over all measurable functions $0\le g\le1$ rather than over numbers, and Lemma 2.2.2 is a two-parameter inequality in which the closed form (2.2.2) is not convenient. On the measure-theoretic side, all integrands take values in $[0,\infty]$ and $f(A,\cdot)$ need not be measurable in general.

Formalization scope

Space. $(\Omega,\Sigma,\mu)$ is an arbitrary measurable space with a probability measure; $\Omega^N$ is Fin N → Ω (0-based coordinates) and $P$ is Measure.pi (fun _ => μ). $\Omega$ is never restricted to a finite or countable set.
Measurability. The paper ignores measurability and states Proposition 2.1.1 with an upper integral and outer probability. Here $A$ carries MeasurableSet A and the map $x\mapsto f(A,x)$ carries an explicit Measurable hypothesis; probabilities of arbitrary sets are Mathlib's outer measure.
Values. Distances are in $[0,\infty]$ (ℝ≥0∞), so $f(\emptyset,x)=+\infty$ ; integrals are lower Lebesgue integrals ∫⁻ in $[0,\infty]$ ; $e^{tz}$ is EReal.exp; $P(A)^{-1}$ and $P(A)^{-\alpha}$ are computed in $[0,\infty]$ , so $P(A)=0$ makes the right-hand sides $+\infty$ .
Constants. $a(\alpha,t)$ is formula (2.2.2) for $t\ne0$ and $1$ at $t=0$ . Every constant ( $1/4$ , $1/8$ , $2/N$ ) is the paper's.
Ruled out. Defining $f$ through a real infimum (whose junk value on $\emptyset$ is $0$ ), or letting $a(\alpha,0)=0/0=0$ , would make several statements false or trivial; neither is done.

Needed infrastructure: Fubini/Tonelli for Measure.pi split as $\Omega^N\times\Omega$ , Chebyshev–Markov for ∫⁻, and one-variable calculus for (2.2.3)–(2.2.5). The one-coordinate lemmas and the induction scheme are reusable in the later missions of this series. Proofs of individual milestones and alternative proofs (for example via martingales for (2.2.7)) are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/bf02699376
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Ser. 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
L. H. Harper, Optimal numberings and isoperimetric problems on graphs, J. Combin. Theory 1 (1966), 385–393. https://doi.org/10.1016/S0021-9800(66)80059-5

8 thms2 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces IV: Control by q Points — ∫ q^{f(A_1,…,A_q,x)} dP ≤ 1/∏ P(A_i)Textbook

Motivation

A recurring phenomenon in probability is concentration of measure: on a product of many probability spaces, a set of non-negligible measure has a neighbourhood that carries almost all of the mass. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces developed a systematic method — induction over the number of coordinates — that yields such statements for several different ways of measuring "how far" a point is from a set. These inequalities underlie sharp tail bounds for combinatorial optimization problems (bin packing, travelling salesman, longest increasing subsequence), for empirical processes, and for spin glasses, and Part II of the memoir develops several of these applications.

This mission formalizes Section 3 of the memoir, Control by q points. In Section 2 the distance from a point $x$ to a set $A$ counts the coordinates of $x$ that a single point of $A$ fails to reproduce (the Hamming distance). Section 3 lets several points cooperate: a coordinate of $x$ is captured if any one of $q$ chosen points agrees with $x$ there. The memoir's introduction (p. 79) presents Theorem 3.1.1 as a much simpler substitute for the isoperimetric inequality of Talagrand's earlier work on sums of independent Banach-space valued random variables (Talagrand, Ann. Probab. 17 (1989), 1546–1570), whose phenomenon "had a major impact in Probability in Banach spaces"; Chapter 13 of the memoir applies it to tails of such sums.

Setting

Let $(\Omega,\mu)$ be a probability space, $N\ge0$ an integer, and $P=\mu^{\otimes N}$ the product probability on $\Omega^N$ . Fix an integer $q\ge2$ ; this is a standing assumption throughout the section. For $x\in\Omega^N$ and points $y^1,\dots,y^q\in\Omega^N$ , coordinate $i$ of $x$ is captured if $x_i\in\{y^1_i,\dots,y^q_i\}$ . For subsets $A_1,\dots,A_q\subseteq\Omega^N$ the $q$ -point control is

f(A_1,\dots,A_q,x)=\inf\big\{\#\{i\le N: x_i\notin\{y^1_i,\dots,y^q_i\}\};\ y^1\in A_1,\dots,y^q\in A_q\big\}\qquad(3.1.1),

the least number of coordinates of $x$ that remain uncaptured when one point is chosen in each $A_j$ . It is a whole number between $0$ and $N$ , or $+\infty$ when some $A_j$ is empty.

For the sharpening of Section 3.2, given $\alpha>1$ , the number $a(q,\alpha)$ is the unique $x>1$ with

x+q\alpha\,x^{-1/\alpha}=1+q\alpha\qquad(3.2.2).

Formalization targets

Goal: Theorem 3.1.1

For all subsets $A_1,\dots,A_q$ of $\Omega^N$ ,

\int q^{f(A_1,\dots,A_q,x)}\,dP(x)\le\frac{1}{\prod_{i\le q}P(A_i)}\qquad(3.1.2),

and in particular, for $A\subseteq\Omega^N$ and $k\ge0$ ,

P(\{f(A,\dots,A,x)\ge k\})\le\frac{1}{q^k\,P(A)^q}\qquad(3.1.3).

The constant is exact: the base of the exponential moment is $q$ itself, and the dimension $N$ does not appear.

Milestones on the way

Lemma 3.1.2: for $1/q\le g\le1$ , $\int g^{-1}\,d\mu\,(\int g\,d\mu)^q\le1$ .
Corollary 3.1.3: for $0\le g_i\le1$ , $\int\min_{i\le q}(q,1/g_i)\,d\mu\prod_{i\le q}\int g_i\,d\mu\le1$ .
Eq. (3.1.6): the two pointwise comparisons between $f$ on $\Omega^{N+1}$ and $f$ on $\Omega^N$ for sections and projections of the sets.

Sharpening (Section 3.2)

Eq. (3.2.2): $a(q,\alpha)$ is well defined.
Eq. (3.2.1): $\int a(q,\alpha)^{f(A_1,\dots,A_q,x)}\,dP(x)\le1/\prod_{i\le q}P(A_i)^\alpha$ for $\alpha>1$ .
Proposition 3.2.1: there is a universal $q_0$ such that for $q\ge q_0$

P(\{f(A,\dots,A,x)\ge k\})\le\Big(\frac{e}{(e-1)\,q\log q}\Big)^k\Big(\frac1{P(A)}\Big)^{q\log q}.

Significance

Theorem 3.1.1 gives an exponential tail for $f(A,\dots,A,x)$ whose rate $q^{-k}$ is independent of the dimension $N$ and of the space $\Omega$ . Applied with a set $A$ of probability at least $1/2$ , it says that outside an event of probability $2^q q^{-k}$ a random point agrees, on all but $k$ coordinates, with one of $q$ points of $A$ . This is the form in which the memoir (Chapter 13) bounds the tail of $\|\sum_{i\le N}X_i\|$ for independent Banach-space valued $X_i$ : taking $A=\{\|\sum_i x_i\|\le a\}$ , on most of the space the sum is controlled by $q$ points of $A$ up to the $k$ largest terms. Proposition 3.2.1 shows the base can be improved from $q$ to order $q\log q$ for large $q$ , and the memoir's example on $\Omega=\{0,1\}$ shows that this is sharp up to a universal constant in the base.

None of these results has a machine-checked proof. A formalization produces reusable Lean infrastructure for the induction method on product measures (sections and projections of subsets of $\Omega^{N+1}$ , Fubini on Measure.pi, one-coordinate functional inequalities) that the other chapters of the memoir — the Hamming distance of Section 2, penalties of Section 3.3, the convex hull distance of Section 4 — share.

Difficulty

The inequality cannot be obtained by a union bound over choices of $q$ points or by a coordinate-wise martingale argument with bounded differences: both lose a factor depending on $N$ , while (3.1.2) has none. The induction on $N$ needs a functional inequality on one coordinate that holds uniformly over $q$ functions at once, with the exact constant $q$ , and the induction step has to pass through the projections $B_i$ of the sets — which, for measurable $A_i$ , need not be measurable. The exact constant $e/((e-1)q\log q)$ in Proposition 3.2.1 additionally requires quantitative control of the root of (3.2.2) as $q\to\infty$ .

Formalization scope

$\Omega^N$ is Fin N → Ω (coordinates $0,\dots,N-1$ ), $P$ is Measure.pi (fun _ => μ) with [IsProbabilityMeasure μ], and $(x,\omega)\in\Omega^{N+1}$ is Fin.snoc x ω.
$f$ is computed as an infimum in ℕ∞, so an empty $A_j$ gives $+\infty$ , not $0$ ; $q^{+\infty}=+\infty$ ; integrals are ∫⁻ and probabilities are in ℝ≥0∞, where $1/0=+\infty$ . Hence the degenerate case $P(A_i)=0$ makes the right sides infinite and cannot trivialize any statement.
The memoir ignores measurability and prints (3.2.1) with an upper integral. The formal statements take the sets measurable and assume $x\mapsto f(A_1,\dots,A_q,x)$ measurable, which is the memoir's stated convention (Section 2.1).
$q\ge2$ is a hypothesis of every statement; in Proposition 3.2.1 the constant $q_0$ is quantified before every other object, so it is universal.
$a(q,\alpha)$ is defined as $\sup\{x>1: x+q\alpha x^{-1/\alpha}\le1+q\alpha\}$ ; that this is the unique root is a milestone, not an assumption.

A complete development needs the induction step over Measure.pi on Fin (N+1) (splitting off the last coordinate), measurability of sections, and the one-coordinate inequalities. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
M. Talagrand, A new look at independence, Annals of Probability 24 (1996), 1–34. https://doi.org/10.1214/aop/1042644705
M. Talagrand, Isoperimetry and integrability of the sum of independent Banach-space valued random variables, Annals of Probability 17 (1989), 1546–1570 (reference [T2] of the memoir).
M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089

9 thms2 active usersReviewed

Completed

Analysis Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces III: Penalties — Exponential Moments of the Penalized Distance f_h(A, x)Textbook

Motivation

Concentration of measure in a product space $\Omega^N$ asks how much of the space lies close to a set $A$ of non-negligible probability. In the simplest setting closeness is the Hamming distance: the number of coordinates of $x$ that cannot be matched by a point of $A$ . Talagrand's 1995 memoir in Publications Mathématiques de l'IHÉS develops a family of such inequalities with one method, induction over the number of coordinates, and applies them to combinatorial optimization, random graphs, spin glasses and sums of Banach-space-valued random vectors.

Counting a missed coordinate as $1$ ignores how far apart the two coordinate values are. Sections 2.4 and 2.5 of the memoir replace the unit cost by a penalty $h(x_i, y_i)$ that depends on the values being matched. The resulting bounds have the shape of Bernstein's inequality: a Gaussian tail for moderate deviations, governed by the $L^2$ size of the penalty, and an exponential tail for large ones, governed by its sup norm. Theorem 2.4.1 is used again in Chapter 11 of the memoir, Corollary 2.4.4 in the study of the Sherrington–Kirkpatrick model in Chapter 12, and Theorem 2.5.1 in Section 11.5.

Setting

Let $(\Omega, \mu)$ be a probability space, $N \ge 0$ an integer, and $P = \mu^{\otimes N}$ the product probability on $\Omega^N$ . A penalty is a measurable function $h : \Omega \times \Omega \to [0, \infty)$ with $h(\omega, \omega) = 0$ for every $\omega$ (the paper's standing assumption (2.4.2)). For $A \subseteq \Omega^N$ and $x \in \Omega^N$ the penalized distance is

f_h(A, x) = \inf\Big\{ \sum_{i \le N} h(x_i, y_i)\,\mathbf 1_{\{x_i \ne y_i\}} \;;\; y \in A \Big\},

with $f_h(\emptyset, x) = +\infty$ . For $h = 1$ off the diagonal this is the Hamming distance. Theorem 2.4.1 also uses the symmetrized penalty $v(\omega, \omega') = \max(h(\omega, \omega'), h(\omega', \omega))$ .

Section 2.5 measures the penalty against sets: for $B \subseteq \Omega$ ,

h(\omega, B) = \inf\{ h(\omega, \omega') \;;\; \omega' \in B \},

the infimum being over the second variable, as in $f_h$ . The one-coordinate steps of the two inductions use the transforms $\hat g(x) = \inf_{y}(g(y) + t\,h(x,y))$ (2.4.5) and $\hat g(x) = \inf_{s>0} s + t\,h(x, B_s)$ with $B_s = \{g \le s\}$ (2.5.7), for a function $g \ge 0$ on $\Omega$ .

Formalization targets

Goal: Theorem 2.4.1

For each measurable $A \subseteq \Omega^N$ and each $t > 0$ with $\iint \exp t h(x,y)\, d\mu(x)\, d\mu(y) < \infty$ ,

\int_{\Omega^N} e^{t f_h(A,x)}\, dP(x) \le \frac{1}{P(A)} \Big( \frac12 \int_{\Omega^2} \big(e^{t v(\omega,\omega')} + e^{-t v(\omega,\omega')}\big)\, d\mu(\omega)\, d\mu(\omega') \Big)^N.

It is the most general exponential-moment bound of the section; every tail bound of Section 2.4 is derived from it.

Milestones

Proposition 2.4.2, the one-coordinate inequality $\int e^{\hat g}\, d\mu \int e^{-g}\, d\mu \le \frac12 \iint (e^{tv} + e^{-tv})\, d\mu\, d\mu$ for $g \ge 0$ .
Theorem 2.4.3: if $\iint e^{h} < \infty$ , then for $0 \le t \le 1$

\int e^{t f_h(A,x)}\, dP(x) \le \frac{1}{P(A)} \exp\Big( N t^2 \iint (e^{h} + e^{-h} - 2)\, d\mu\, d\mu \Big).

Corollary 2.4.4: if $\iint e^{h} \le 2$ , then $P(f_h(A,\cdot) \ge u) \le P(A)^{-1} e^{-u^2/4N}$ for $0 \le u \le 2N$ .
Corollary 2.4.5: if $\|h\|_\infty = \sup h < \infty$ , then

P(f_h(A,\cdot) \ge u) \le \frac{1}{P(A)} \exp\Big( -\min\Big( \frac{u^2}{8N\|h\|_2^2},\ \frac{u}{2\|h\|_\infty} \Big) \Big).

Proposition 2.5.2, the one-coordinate inequality $\int e^{\hat g}\, d\mu \int e^{-g}\, d\mu \le e^{3t^2}$ for the transform (2.5.7), under condition (2.5.2) below.
Theorem 2.5.1: if $\int_\Omega \exp 2h(x, B)\, d\mu(x) \le e/\mu(B)$ for each $B \subseteq \Omega$ (condition (2.5.2)), then for $0 \le t \le 1$

\int e^{t f_h(A,x)}\, dP(x) \le \frac{e^{3t^2 N}}{P(A)}.

Significance

The results. Theorem 2.4.1 turns a single integrability condition on the penalty into a bound on the exponential moment of the distance to any set, uniform over all sets of a given probability and factorized over coordinates. Chebyshev's inequality then gives the Bernstein-type tails of Corollaries 2.4.4 and 2.4.5, which hold for every set $A$ , not only for half-spaces or for sums of independent variables. Theorem 2.5.1 replaces exponential integrability of $h$ by condition (2.5.2) on the set functional $h(x, B)$ , which is much weaker: when $\Omega$ is itself a product of $m$ spaces, $m^{-1/2}$ times the Hamming distance on $\Omega$ satisfies (2.5.2) but not (2.4.12). Applied to blocks of coordinates, it shows that the coordinates a typical point misses in $A$ are concentrated in few blocks.

Formalizing them. All six results are proved in the memoir with short arguments. None of them has a machine-checked proof. A complete development would give a general-alphabet version of Talagrand's induction on product measures, written once for a cost function, that later chapters (the $q$ -point control, the convex-hull distance) also rely on.

Difficulty

The induction over $N$ requires a one-coordinate inequality whose right-hand side does not depend on the set. The difficulty is that the natural one-coordinate quantity, a section measure $P(A(\omega))$ , can vanish on part of $\Omega$ , so the function $g = -\log P(A(\omega))$ takes the value $+\infty$ , and a statement proved for finite $g$ must be extended by truncation. The other subtle point is measure theoretic: $f_h(A, \cdot)$ need not be measurable even when $A$ is, and the paper's convention of ignoring measurability has to be matched by explicit hypotheses. In Section 2.5 the integrand $x \mapsto h(x, B)$ in condition (2.5.2) may be non-measurable for the sets the proof uses, and Fubini's theorem is applied to the function $(x, y) \mapsto h(x, B_{g(y)})$ .

Formalization scope

Points of $\Omega^N$ are functions Fin N → Ω (coordinates indexed from $0$ ), $P$ is Measure.pi (fun _ => μ) for a probability measure μ, and double integrals are over μ.prod μ. The penalty is a real function h : Ω → Ω → ℝ with explicit hypotheses $h \ge 0$ , $h(\omega,\omega) = 0$ and joint measurability, in every statement. The distance $f_h$ is defined by (2.4.1) with the indicator and takes values in $[0,\infty]$ , so $f_h(\emptyset, x) = +\infty$ ; likewise $h(\omega, B)$ and the transform (2.5.7). All integrals are Lebesgue integrals of $[0,\infty]$ -valued functions, $e^{+\infty} = +\infty$ , and $1/P(A) = +\infty$ when $P(A) = 0$ .

Measurability follows the paper's convention (pp. 81–82) as explicit hypotheses: $A$ is measurable and $x \mapsto f_h(A, x)$ is measurable; in the propositions, $g$ and $\hat g$ are measurable. Condition (2.5.2) is stated for every subset $B$ with the upper integral $\int^*$ , which the paper prescribes when measurability fails. In Corollary 2.4.5, the quotients are computed in $[0,\infty]$ , so a quotient by $\|h\|_2 = 0$ , $\|h\|_\infty = 0$ or $N = 0$ is $+\infty$ when its numerator is positive. The bound is $+\infty$ when $P(A)=0$ , as the printed factor $1/P(A)$ intends. No statement is restricted to a finite or countable $\Omega$ : restricting it would turn the general theorems into their finite-alphabet special cases. Dropping $h(x,x) = 0$ or defining the distance by a real infimum (whose value on the empty set is $0$ ) would change the theorems and is ruled out.

A complete development needs product measures on Fin (N+1) → Ω split as $\Omega^N \times \Omega$ , sections of measurable sets, Tonelli's theorem, and the elementary convexity inequalities used in the proofs; the induction scaffold is reusable for the other distance functionals of the memoir. Proofs of any milestone are welcome, as are proofs of the extension of Proposition 2.4.2 to $g$ with values in $[0,\infty]$ , which the paper states without number on p. 92.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
M. Talagrand, A new look at independence, Annals of Probability 24 (1996), 1–34. https://doi.org/10.1214/aop/1042644705
M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089

8 thms2 active usersReviewed

Completed

Formal Verification Theoretical Computer Science·Captain: mikedeng1

Reaching Agreement in the Presence of Faults 3: With Authenticated Messages, the S_pq Procedure Assures Interactive Consistency for m Faults for Every n ≥ mResearch Paper

Motivation

Processors in a distributed system may hold separate readings of a sensor, clock, or diagnostic result while some processors give misleading reports. The aim of interactive consistency is for every functioning processor to compute the same vector of reported values and to put each functioning processor's actual private value in its corresponding position. A shared vector can then be used for a common decision. Pease, Shostak, and Lamport formulated this problem for isolated processors communicating by two-party messages; their paper discusses clock synchronization, input stabilization, and diagnostic tests as concrete applications Pease–Shostak–Lamport 1980.

In the paper's oral-message model, faulty processors can invent reports about values they received from others. The other two missions in this series formalize the recursive majority procedure for $n\ge 3m+1$ and the matching impossibility result below that bound. Section 5 changes the communication assumption: a faulty processor may refuse to pass on a received value but cannot pass on an altered value as if it came from its original sender. Under that assumption, the authors give a procedure for every $n\ge m$ , including configurations outside the oral-message threshold Pease–Shostak–Lamport 1980, §§3–5.

Setting

Let $P$ be a finite set of $n$ processors and $V$ a type of private values. Each processor $q\in P$ has a value $\sigma(q)\in V$ . A scenario $\sigma$ records the values reported along chains of processors. A string $p_1p_2\cdots p_r$ is read from receiver to originator: $p_1$ receives a report ultimately attributed to $p_r$ . A recorded value may be NIL, meaning that no authenticated value is available. The view available to receiver $p$ is its $p$ -scenario, the restriction $w\mapsto\sigma(pw)$ ; it contains no report that begins with a different receiver.

Choose a set $N\subseteq P$ of nonfaulty processors. At most $m$ processors may be faulty, expressed as $|P|\le |N|+m$ . An authenticated scenario consistent with $N$ obeys two conditions whenever the displayed strings are in the $(m+1)$ -level scenario. If $p\in N$ and $q\in P$ , the report made by nonfaulty relay $p$ is truthful: $\sigma(qpw)=\sigma(pw)$ . For any prefix $w'$ , a chain passing through nonfaulty $p$ carries either the value at $p$ or NIL: $\sigma(w'pw)\in\{\sigma(pw),\mathrm{NIL}\}$ . The second condition allows omission by later relays while excluding a changed value falsely attributed to $p$ Pease–Shostak–Lamport 1980, p. 233.

For each receiver $p$ and originator $q$ , the procedure forms $S_{pq}$ , the set of all non-NIL values in $p$ 's view on strings $pwq$ . The intermediate string $w$ has at most $m$ distinct letters, all in $P\setminus\{p,q\}$ . Receiver $p$ records the sole value in $S_{pq}$ when this set is a singleton; otherwise it records NIL. The resulting entries, one for each $q\in P$ , form $p$ 's proposed consistency vector Pease–Shostak–Lamport 1980, p. 233.

Formalization targets

The first milestone covers a nonfaulty originator $q$ : every nonfaulty receiver $p$ sees exactly its true value. The second covers a faulty originator: the set of non-NIL values seen by one nonfaulty receiver is contained in the set seen by another. The same statement with the receivers exchanged gives equality of their sets.

The goal is the procedure's full interactive-consistency guarantee, for every choice of $N$ and every authenticated scenario satisfying the conditions above:

\begin{aligned} R_p(q)&=\sigma(q) &&(p,q\in N),\\ R_p(r)&=R_{p'}(r) &&(p,p'\in N,\ r\in P). \end{aligned}

Here $R_p(r)$ is the optional value recorded by processor $p$ for processor $r$ . Both clauses matter: agreement alone could be achieved by always recording NIL, while correct nonfaulty entries alone would leave faulty entries inconsistent.

Significance

The result identifies an exact communication assumption under which the paper's $3m+1$ oral-message bound no longer governs the procedure. Even if a faulty originator gives conflicting values, nonfaulty receivers finish with identical entries for that originator; if an originator is nonfaulty, they retain its actual value. The paper describes authenticators as a practical approximation to the assumption, but the guarantee here is a mathematical statement about scenarios satisfying its two conditions, not a probability claim about a cryptographic implementation Pease–Shostak–Lamport 1980, §5.

Formalizing this result supplies precise interfaces for authenticated scenario consistency, local views, the set $S_{pq}$ , and the recording rule. The paper proves the result on pp. 233–234; this mission asks for a machine-checked proof of those statements in Lean. The scenario and local-view definitions can support later formalizations of message-passing protocols with truthful or omissible relays. Contributions that establish the two source milestones and the final guarantee, or develop reusable list and finite-set facts needed by them, are within scope.

Difficulty

The case of a faulty originator is the central difficulty. Its private value has no required relationship to what different nonfaulty receivers hear, so simply asserting that every receiver obtains the same direct report is unjustified. A faulty relay may also omit a report, which makes equality of raw scenario entries too strong. The target must compare sets of non-NIL values obtained along admissible relay chains. At the longest allowed chain, the length bound prevents adding another relay, and the number of faulty processors is needed to establish that an admissible nonfaulty relay occurs in the chain Pease–Shostak–Lamport 1980, p. 234.

Formalization scope

Lean represents processors by a finite set P : Finset α, values by a type V, strings by List α, and NIL by none : Option V. A scenario is a total function from strings to optional values. Only strings over $P$ of length at most $m+2$ are constrained by authenticated consistency, matching the $(m+1)$ -level scenario that the procedure reads. A single-letter string has a non-NIL private value for every processor in $P$ . Conditions (i) and (ii) constrain nonfaulty relays only; condition (ii) allows either the original value or NIL for every prefix over $P$ , including an empty prefix.

The procedure is applied only to $p$ 's view $w\mapsto\sigma(pw)$ , so it has no access to the full scenario or to $N$ . Its intermediate strings are repetition-free, exclude both $p$ and $q$ , and have length at most $m$ . The set $S_{pq}$ contains values in $V$ , not NIL; an empty set and a set with multiple values both cause a NIL record. The formal theorem retains the printed $n\ge m$ condition, although it is not needed in the proof of the stated set relationships. It also covers $p=q$ , $m=0$ , and empty or singleton processor sets when their quantified conditions apply. These conventions rule out an always-NIL decision rule and the trivial rule that reads $\sigma(q)$ from outside the receiver's view.

The cryptographic maps $A_p$ , their message encodings, and the paper's assertion that practical authenticators can meet the assumption with arbitrarily high probability are outside scope. The formal result assumes the two exact authenticated-scenario conditions. A complete development needs finite-set cardinality and list facts, especially about distinct relay strings and bounded concatenation; these facts can be reused for other authenticated relay models.

Selected references

M. Pease, R. Shostak, and L. Lamport, Reaching Agreement in the Presence of Faults, Journal of the ACM 27(2), 1980, 228–234. DOI: 10.1145/322186.322188.

5 thms2 active usersReviewed

Completed

Formal Verification Theoretical Computer Science·Captain: mikedeng1

Reaching Agreement in the Presence of Faults 2: If |V| ≥ 2 and 3 ≤ n ≤ 3m, No Family {F_p} Assures Interactive Consistency for m Faults, However Many Rounds Are UsedResearch Paper

Motivation

A fault-tolerant system built from several processors must let its working processors act on the same data, even though some processors may have failed in ways nobody can predict: a failed processor may stop relaying information, relay something it invented, or tell different processors different things. Pease, Shostak and Lamport (J. ACM 27 (1980) 228–234) isolated the core question in the setting of the SIFT aircraft-control computer: each of $n$ processors holds a private value, at most $m$ processors are faulty, and processors communicate only by two-party messages. Can the nonfaulty processors each compute a vector of values, one entry per processor, such that all nonfaulty processors compute the same vector and the entry of each nonfaulty processor is its true private value? This requirement is called interactive consistency.

The paper answers with a sharp threshold. Interactive consistency can be achieved when $n\ge 3m+1$ (Section 3), and it cannot be achieved when $n\le 3m$ , however many rounds of message exchange are allowed (Section 4). With unforgeable signatures it can be achieved for every $n\ge m$ (Section 5). The impossibility half is the origin of the " $3m+1$ " bound that appears throughout Byzantine fault tolerance, popularised two years later as the Byzantine Generals Problem (Lamport, Shostak, Pease, ACM TOPLAS 4 (1982)). This mission is the impossibility theorem.

Timeline:

1980: Pease, Shostak and Lamport prove the threshold $n\ge 3m+1$ for interactive consistency with oral messages, including the impossibility for $n\le 3m$ stated in terms of scenarios.
1982: Lamport, Shostak and Pease restate the problem as the Byzantine Generals Problem, with the same bound.
1985–1986: Fischer, Lynch and Merritt give a short "hexagon" proof of the same bound for several agreement problems (Distributed Computing 1 (1986)).

Setting

Let $P$ be a finite set of $n$ processors and $V$ a set of values. Write $P^*$ for the set of strings over $P$ (the empty string included) and $P^+$ for the nonempty strings. A string $p_1p_2\cdots p_r$ is read as a chain of reports: $p_1$ was told by $p_2$ that $\dots$ $p_{r-1}$ was told by $p_r$ that $p_r$ 's private value is the recorded value.

A scenario is a map $\sigma: P^+\to V$ . The value $\sigma(p)$ is processor $p$ 's private value, and $\sigma(p_1\cdots p_r)$ is the value $p_1$ received for the chain $p_2\cdots p_r$ . For $p\in P$ , the $p$ -scenario $\sigma_p$ is the restriction of $\sigma$ to the strings beginning with $p$ : everything $p$ ever learns.

For a set $N\subseteq P$ of nonfaulty processors, $\sigma$ is consistent with $N$ if

\sigma(pqw)=\sigma(qw)\qquad\text{for all }q\in N,\ p\in P,\ w\in P^*,

that is, every nonfaulty processor reports truthfully what it knows or hears. Faulty processors are unconstrained.

A decision family assigns to each $p\in P$ a map $F_p$ that takes a $p$ -scenario and a processor $q$ and returns a value $F_p(\sigma_p,q)\in V$ : the entry $p$ computes for $q$ . The family assures interactive consistency for $m$ faults if for every $N\subseteq P$ with $|N|\ge n-m$ and every scenario $\sigma$ consistent with $N$ ,

$F_p(\sigma_p,q)=\sigma(q)$ for all $p,q\in N$ ;
$F_p(\sigma_p,r)=F_q(\sigma_q,r)$ for all $p,q\in N$ , $r\in P$ .

In the Lean development these are InteractiveConsistency.Impossibility.ConsistentWith P N σ and AssuresIC P m F, with restrict σ p the $p$ -scenario.

Formalization targets

Goal: the THEOREM of Section 4

If $|V|\ge 2$ and

3\le n\le 3m,

then no family $\{F_p\mid p\in P\}$ assures interactive consistency for $m$ faults. Since scenarios are defined on strings of every length, no bound on the number of rounds is assumed.

Milestones, in the order the proof of the paper uses them

If $3\le n\le 3m$ , then $P$ is the disjoint union of three nonempty sets $A$ , $B$ , $C$ , each with at most $m$ members (p. 232).
For such a partition and values $v,v'$ , the scenarios $\alpha,\beta,\sigma$ that the page defines by recursion on the length of strings are consistent with $A\cup C$ , $B\cup C$ and $A\cup B$ respectively (p. 233).
For the same scenarios, $\alpha(aw)=\sigma(aw)$ and $\beta(bw)=\sigma(bw)$ for all $a\in A$ , $b\in B$ , $w\in P^*$ (p. 233).

Significance

The theorem shows that the algorithm of Section 3 is optimal in its fault tolerance: with oral messages, $n\ge 3m+1$ processors are not only sufficient but necessary. Every later lower bound for Byzantine agreement, Byzantine broadcast and approximate agreement with unauthenticated messages rests on this bound or a variant of its argument, and it is the reason replicated state machines tolerating $m$ Byzantine faults use $3m+1$ replicas. It also explains why Section 5 needs authentication: the argument depends on faulty processors being able to relay fabricated values.

The result has been proved since 1980; what is open here is its formalization. Nothing on Prove2Me models message-passing agreement, and this mission states the theorem in the paper's own model: scenarios on unbounded strings and decision functions of a single $p$ -scenario. The mission produces a reusable vocabulary (scenarios, consistency, interactive consistency) and the explicit three-scenario construction.

Difficulty

The obvious attempt is to argue round by round about what a processor can know after $k$ rounds; with unboundedly many rounds this never terminates in a contradiction. The paper's argument instead needs three entire scenarios, each a legitimate behaviour for a different set of faulty processors, that two processors cannot tell apart from their own views. Writing these scenarios down so that consistency holds on every string while the indistinguishability survives on every string is the delicate part: the faulty set of each scenario must relay exactly the values that keep the other scenario's view intact, and one of the defining equations ( $\beta(paw)=\alpha(aw)$ ) looks like a misprint but is what the argument requires. The counting step is elementary but carries the hypothesis $n\ge 3$ that the printed theorem leaves implicit.

Formalization scope

Processors are a Finset P in a type with decidable equality; strings are lists read left to right ( $p_1$ is the head of the list); a scenario is a total function List α → V whose values on the empty list and on lists with a letter outside $P$ carry no meaning: every condition quantifies only over strings whose letters lie in $P$ . Decision functions have type α → (List α → V) → α → V and are applied only to the $p$ -scenario fun w => σ (p :: w), never to $\sigma$ ; giving $F_p$ the whole scenario would make the problem trivial (output $\sigma(q)$ ). Consistency with $N$ constrains only relays by members of $N$ , and includes the empty $w$ . The quorum $|N|\ge n-m$ is written $|P|\le |N|+m$ , which avoids truncated subtraction on $\mathbb N$ . $|V|\ge 2$ is the existence of two distinct values.

Explicit readings of the page:

The printed hypothesis " $n\ge 3m$ " is a misprint for $n\le 3m$ (the proof opens "Since $n\le 3m$ ", and the section title is "Proof of Impossibility for $n<3m+1$ "); with $n\ge 3m$ the statement is false.
The hypothesis $n\ge 3$ is implicit in the proof's "three nonempty sets". It is necessary: for $n\le 2$ the family $F_p(\sigma_p,q)=\sigma(pq)$ assures interactive consistency.
In the construction, each letter $a$ , $b$ , $c$ ranges independently over $A$ , $B$ , $C$ (so " $\alpha(cc)$ " covers $\alpha(c'c)$ ); the value $\sigma(c'cw)$ , which the page leaves unspecified, is fixed to $\sigma(cw)$ .
The construction is stated as a definition, and the two "easy" claims about it (consistency, indistinguishability) are separate milestones.

A complete development needs only finite sets and lists from Mathlib. The vocabulary of p. 232 is shared with the other two missions of this series, Reaching Agreement in the Presence of Faults 1 (the algorithm for $n\ge 3m+1$ ) and 3 (authenticated messages, $n\ge m$ ), each of which defines it in its own namespace. Proofs of the milestones and of the goal are welcome, as is a proof of the goal by a different route.

Selected references

M. Pease, R. Shostak, L. Lamport, Reaching agreement in the presence of faults, Journal of the ACM 27(2) (1980) 228–234. https://doi.org/10.1145/322186.322188
L. Lamport, R. Shostak, M. Pease, The Byzantine Generals Problem, ACM Transactions on Programming Languages and Systems 4(3) (1982) 382–401. https://doi.org/10.1145/357172.357176
M. J. Fischer, N. A. Lynch, M. Merritt, Easy impossibility proofs for distributed consensus problems, Distributed Computing 1 (1986) 26–39. https://doi.org/10.1007/BF01843568

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

An Iterative Method of Solving a Game: For Every Vector System, min U(t)/t and max V(t)/t Converge to the Value of the GameResearch Paper

Motivation

A finite two-person zero-sum game is given by a real pay-off matrix, and its value can be computed by linear programming. In 1949 George W. Brown proposed a much simpler procedure, now called fictitious play: each player in turn plays a best pure reply to the accumulated play of the opponent so far, and the running averages are read off as estimates of the value (Brown, RAND P-78, 1949). Brown conjectured that both estimates converge to the value. Julia Robinson proved the conjecture in An Iterative Method of Solving a Game, Annals of Mathematics 54 (1951).

The result is the starting point of the theory of learning in games. Fictitious play is the basic model of boundedly rational players who best-respond to empirical frequencies, and the question "for which classes of games does it converge?" has driven a long line of work.

Timeline.

1949–1951: Brown proposes the method and conjectures convergence for zero-sum games.
1951: Robinson proves it for every vector system of every zero-sum matrix game; the statement contains no rate.
1958: Shapiro extracts from Robinson's argument a rate: the gap $(\max V(t) - \min U(t))/t$ is $O(t^{-1/(m+n-2)})$ (doi:10.1002/cpa.3160110408).
1964: Shapley gives a 3 × 3 bimatrix (non-zero-sum) game in which fictitious play does not converge (doi:10.1515/9781400882014-002).
1996: Monderer and Shapley prove convergence for games with identical interests (doi:10.1006/jeth.1996.0014).
2014: Daskalakis and Pan show that with adversarial tie-breaking the convergence can be much slower than the rate $t^{-1/2}$ conjectured by Karlin (arXiv:1412.4840).

Setting

Let $A = (a_{ij})$ be a real $m \times n$ matrix, $m, n \ge 1$ . The first player chooses a row $i$ , the second a column $j$ , and the second pays the first $a_{ij}$ . A mixed strategy is a probability vector $x = (x_1, \dots, x_m)$ for the first player, or $y = (y_1, \dots, y_n)$ for the second. For all mixed strategies,

\min_j \sum_i a_{ij} x_i \le \max_i \sum_j a_{ij} y_j. \tag{1}

A pair $(X, Y)$ for which equality holds is a solution, and the common number $v$ is the value of the game. The minimax theorem says that a solution exists.

Write $A_{i\cdot}$ for the $i$ -th row, $A_{\cdot j}$ for the $j$ -th column, and $\max W$ , $\min W$ for the largest and smallest component of a vector $W$ . A vector system for $A$ is a pair of sequences $U(0), U(1), \dots$ of $n$ -vectors and $V(0), V(1), \dots$ of $m$ -vectors with $\min U(0) = \max V(0)$ and

U(t+1) = U(t) + A_{i\cdot}, \qquad V(t+1) = V(t) + A_{\cdot j},

where $v_i(t) = \max V(t)$ and $u_j(t) = \min U(t)$ . In the alternate vector system the column satisfies $u_j(t+1) = \min U(t+1)$ instead. A row $i$ is eligible in the interval $(t, t')$ if $v_i(t_1) = \max V(t_1)$ for some $t \le t_1 \le t'$ , and similarly a column $j$ if $u_j(t_2) = \min U(t_2)$ for some $t \le t_2 \le t'$ .

With $U(0) = V(0) = 0$ , $U(t)/t$ is the payoff vector of the first player's empirical mixed strategy against each column, and $V(t)/t$ that of the second player's against each row. In the Lean development these objects are vmax, vmin, IsVectorSystem, IsAltVectorSystem, RowEligible, ColEligible and IsSolution, in the namespace RobinsonFP.Convergence.

Formalization targets

Goal: the Theorem (p. 297)

For every vector system $(U, V)$ for $A$ , and $v$ the value of the game,

\lim_{t\to\infty} \frac{\min U(t)}{t} = \lim_{t\to\infty} \frac{\max V(t)}{t} = v.

The statement holds for arbitrary initial vectors with $\min U(0) = \max V(0)$ and for every way of breaking ties.

Milestones, in the order of the proof

Inequality (1).
Lemma 1: $\liminf_{t\to\infty} (\max V(t) - \min U(t))/t \ge 0$ .
Lemma 2: if every row and column is eligible in $(s, s+t)$ , then $\max U(s+t) - \min U(s+t) \le 2at$ and $\max V(s+t) - \min V(s+t) \le 2at$ , where $a = \max_{i,j}|a_{ij}|$ .
Lemma 3: under the same hypothesis, $\max V(s+t) - \min U(s+t) \le 4at$ .
Display (3) of the proof of Lemma 4: if some row or column is not eligible in $(s, s+t^*)$ , the gap $\max V - \min U$ grows by less than $\tfrac12 \varepsilon t^*$ over that window, given the bound $\tfrac12\varepsilon t$ for the vector systems of the submatrices.
Lemma 4: for every $\varepsilon > 0$ there is $t_0$ , uniform over all vector systems for $A$ , with $\max V(t) - \min U(t) < \varepsilon t$ for $t \ge t_0$ .
$(\max V(t) - \min U(t))/t \to 0$ .
$\limsup \min U(t)/t \le v$ and $\liminf \max V(t)/t \ge v$ .

Two further items are not milestones: the Theorem for the alternate vector system, which the paper says follows by the same proofs, and the bracketing $\min U(t)/t \le v \le \max V(t')/t'$ when $U(0) = V(0) = 0$ (p. 297).

Significance

The Theorem shows that a payoff-based procedure with no linear algebra finds the value of every zero-sum matrix game. It was one of the first iterative methods for linear programs with a convergence proof, and it is the base case for every later convergence result about fictitious play: potential games, games with identical interests, $2\times n$ games, and continuous-time best-response dynamics.

The result is proved, and its proof is short. To our knowledge it has no machine-checked proof. The mission produces a Lean proof of the Theorem and its four lemmas, together with reusable definitions of vector systems and eligibility. A statement with an explicit rate, such as Shapiro's, or a proof for the alternate system, is a natural extension.

Difficulty

Lemmas 1–3 are elementary estimates. The difficulty is Lemma 4. The obvious approach follows a single run of the iteration and tries to show that the gap $\max V(t) - \min U(t)$ grows sublinearly. This fails because a run can spend arbitrarily long windows in which some row or column is never a best reply, and nothing about one fixed run controls the gap over such a window. What is needed is a bound that is uniform over all vector systems, whatever their initial vectors and tie-breaking, which is why $t_0$ in Lemma 4 comes before the vector system, and why display (3) quantifies over every vector system of the smaller matrices. In Lean, this uniformity has to range over matrices of every smaller size, so the statements must be general in the index types.

Formalization scope

Rows and columns are indexed by finite nonempty types ι, κ (the paper's $m, n \ge 1$ ); Fin m, Fin n is a special case. The matrix is Matrix ι κ ℝ.
$\max W$ , $\min W$ are Finset.sup' and Finset.inf' over all indices, hence attained.
A vector system allows any maximizing row and minimizing column at each step (an existential per step). No tie-breaking rule is fixed, and the initial vectors are arbitrary subject to $\min U(0) = \max V(0)$ . The case $U(0) = V(0) = 0$ is not imposed.
Time is a natural number. Limits are Tendsto … atTop (𝓝 ·); lim inf and lim sup of real sequences are stated in $\varepsilon$ -form (for every $\varepsilon > 0$ , eventually), with no boundedness side conditions.
The value $v$ is given by a solution: every statement about $v$ assumes IsSolution A x y v, i.e. probability vectors $x$ , $y$ with $\min_j \sum_i a_{ij} x_i = v = \max_i \sum_j a_{ij} y_j$ . Such a solution exists by the minimax theorem, which is proved on the platform as MatousekLP.ZeroSum.minimax_equality in a different encoding. A statement with $v$ free, or with "there exists $v$ ", would be false or would lose the identification with the value; neither is used.
In Lemmas 2 and 3, $a$ is any upper bound on the $|a_{ij}|$ . This is equivalent to the paper's $a = \max_{i,j}|a_{ij}|$ .
In display (3), the bound for submatrices is assumed only for the submatrices that delete one row or one column, which makes the statement at least as strong as the paper's.
The paper's closing display on p. 301 prints $\lim \min V(t)/t$ for $\lim \min U(t)/t$ . The goal follows the statement of the Theorem on p. 297.

A general "restriction of a vector system to a submatrix" lemma would be reusable for later work on fictitious play. Proofs of any milestone are welcome, as are proofs of the two extra items.

Selected references

J. Robinson, An Iterative Method of Solving a Game, Annals of Mathematics 54(2), 296–301, 1951. https://doi.org/10.2307/1969530
G. W. Brown, Some notes on computation of games solutions, RAND Report P-78, 1949. https://www.rand.org/pubs/papers/P78.html
H. N. Shapiro, Note on a computation method in the theory of games, Communications on Pure and Applied Mathematics 11(4), 587–593, 1958. https://doi.org/10.1002/cpa.3160110408
L. S. Shapley, Some topics in two-person games, Advances in Game Theory, Annals of Mathematics Studies 52, 1964. https://doi.org/10.1515/9781400882014-002
D. Monderer, L. S. Shapley, Fictitious play property for games with identical interests, Journal of Economic Theory 68, 258–265, 1996. https://doi.org/10.1006/jeth.1996.0014
C. Daskalakis, Q. Pan, A counter-example to Karlin's strong conjecture for fictitious play, FOCS 2014. https://arxiv.org/abs/1412.4840

10 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Some Aspects of the Sequential Design of Experiments III: Optional Stopping — P(Sₙ > αn^½ for Some n₁ ≤ n ≤ n₂) < (1 − Φ(α))/(1 − Φ(α(λ^½ − 1)/(λ − 1)^½))Research Paper

Optional stopping and the size of a test

Section 4 of Herbert Robbins's 1952 address Some aspects of the sequential design of experiments (Bull. Amer. Math. Soc. 58, 527–535, doi:10.1090/S0002-9904-1952-09620-8) isolates a problem that every user of significance tests meets: if the sample size is not fixed in advance, an experimenter can keep sampling until the test rejects. Robbins shows that a fixed-sample test then loses all control of its error probability, and he proposes the compromise of allowing the sample size to range over a window $n_1\le n\le n_2$ , with an explicit bound on the resulting error.

The question is still current. "Optional stopping" and "peeking" at accumulating data are a standard concern in clinical trials and online A/B testing, and the modern theory of always-valid inference and confidence sequences (for example Howard, Ramdas, McAuliffe and Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), arXiv:1810.08240) answers exactly the question Robbins raises: how large is the probability that a running statistic crosses a boundary at some time in a range. The earlier treatment Robbins cites is Feller's 1940 discussion of the statistics of ESP experiments.

Setting

Let $x_1,x_2,\dots$ be independent real random variables on a probability space $(\Omega,\mathcal F,P)$ , each normal with mean $0$ and variance $1$ . This is the null hypothesis $H_0:\theta=0$ for observations that are normal with unknown mean $\theta$ and unit variance; the alternative is $H_1:\theta>0$ . Write

S_n=x_1+\cdots+x_n,\qquad S_0=0 .

The fixed-sample test of size $n$ rejects $H_0$ if and only if

S_n>\alpha n^{1/2}\qquad(21)

for a real constant $\alpha$ . (In this mission $\alpha$ always denotes this test constant; in Section 2 of the paper the same letter is the mean of a coin.) The standard normal distribution function is

\Phi(x)=\frac{1}{(2\pi)^{1/2}}\int_{-\infty}^{x}e^{-t^2/2}\,dt .\qquad(23)

For integers $n_1\le n_2$ the window probability is

g(n_1,n_2,\alpha)=P\bigl[S_n>\alpha n^{1/2}\ \text{for some}\ n_1\le n\le n_2\bigr],\qquad(24)

and $\lambda=n_2/n_1$ . In Lean these are Phi, S X n ω = ∑ i ∈ Finset.range n, X i ω and g P X n₁ n₂ α, in the namespace RobbinsSeqDesign.OptionalStopping.

Formalization targets

Goal: the window bound (25)

For integers $1\le n_1<n_2$ and every real $\alpha$ , with $\lambda=n_2/n_1$ ,

g(n_1,n_2,\alpha)<\frac{1-\Phi(\alpha)}{1-\Phi\!\Bigl(\alpha\cdot\dfrac{\lambda^{1/2}-1}{(\lambda-1)^{1/2}}\Bigr)} .

The inequality is strict, as printed, and holds for every real $\alpha$ , not only the large values of practical interest.

Milestone: the fixed-sample error (22)

For every $n\ge1$ and real $\alpha$ ,

\varepsilon(\alpha)=P\bigl[S_n>\alpha n^{1/2}\bigr]=1-\Phi(\alpha).

Milestone: rejection infinitely often

For every real $\alpha$ , with probability $1$ the inequality $S_n>\alpha n^{1/2}$ holds for infinitely many $n$ .

Significance

The results. (22) says that the fixed-sample test has error probability $1-\Phi(\alpha)$ whatever $n$ is. The infinitely-often statement says that this guarantee is void under unrestricted optional stopping: sampling until (21) holds rejects a true $H_0$ with probability one, however large $\alpha$ is. The goal (25) quantifies the compromise: if the stopping time is confined to $[n_1,n_2]$ , the error probability is at most the fixed-sample error divided by $1-\Phi(\alpha c_\lambda)$ , where $c_\lambda=(\lambda^{1/2}-1)/(\lambda-1)^{1/2}<1$ depends only on the window's ratio. For large $\alpha$ and moderate $\lambda$ this keeps the error of the same order as the fixed-sample error; Robbins notes that it is useful when $\lambda$ is not too large and that sharper inequalities can be devised.

Formalizing it. The three statements are classical and their proofs are short on paper, but none is machine-checked for Gaussian partial sums. The goal needs stopping-time machinery for discrete-time Gaussian random walks; the infinitely-often statement is a consequence of the lower half of the law of the iterated logarithm, which Mathlib does not contain. On the platform, DurrettProbability.brownian_limsup_sqrt (proved) gives $\limsup_t B_t/\sqrt t=\infty$ for Brownian motion, a different process, and AzumaWeightedSums.IteratedLog.theorem2_limsup_le_one gives an upper iterated-logarithm bound for weighted sums, the opposite direction; neither states any of the targets here, but both are related infrastructure.

Difficulty

The goal is a maximal inequality over a window of times. The obvious argument, a union bound over $n_1\le n\le n_2$ , gives $(n_2-n_1+1)(1-\Phi(\alpha))$ , which grows with the window length instead of depending on $\lambda$ alone, and exceeds $1$ for long windows. The events $\{S_n>\alpha n^{1/2}\}$ for different $n$ are strongly dependent, and the boundary $\alpha n^{1/2}$ is curved, so the bound has to account for when, inside the window, the boundary is first crossed; this requires stopping-time arguments for a discrete-time walk that are not yet available for Gaussian random walks in Mathlib. The strictness of the inequality also has to be tracked through the argument. The infinitely-often statement cannot be obtained from the central limit theorem alone, which gives only $P(S_n>\alpha n^{1/2}\ \text{i.o.})\ge 1-\Phi(\alpha)>0$ ; upgrading this to probability one needs a zero–one law or the law of the iterated logarithm.

Formalization scope

The observations are X : ℕ → Ω → ℝ on a probability space (Ω, P) with [IsProbabilityMeasure P], iIndepFun X P and ∀ i, HasLaw (X i) (gaussianReal 0 1) P; the paper's $x_i$ is X (i - 1). The explicit readings committed to are:

$\Phi$ is the integral printed in (23) (a local check shows it equals Mathlib's cdf (gaussianReal 0 1)).
"The probability of rejecting $H_0$ " is P.real of the event; (22) is stated for $n\ge1$ .
"With probability 1 … for infinitely many values of $n$ " is ∀ᵐ ω ∂P, ∃ᶠ n in atTop, α * √n < S X n ω, for every real $\alpha$ .
The window of (24) is $n_1\le n\le n_2$ with both endpoints; the stray comma printed in " $n_1, \le n$ " is a typesetting slip.
In (25), $\lambda$ is the real quotient $n_2/n_1$ , and the hypotheses $1\le n_1<n_2$ make $\lambda>1$ well defined; the inequality is strict and there is no sign restriction on $\alpha$ .
The numeric example " $\alpha=3.09$ then $\varepsilon(\alpha)\cong .001$ " and the phrase "useful when $\lambda$ is not too large" are not formalized.

A trivializing formalization is ruled out: $g$ is the probability of the union over the whole window (not the event at $n=n_2$ alone), $\Phi$ is the fixed standard normal distribution function (not an arbitrary monotone function), and the parameter range excludes $\lambda=1$ , where Lean's convention $x/0=0$ would replace the right side by $2(1-\Phi(\alpha))$ .

A complete development needs the law of a sum of independent Gaussians, the strong Markov property of a Gaussian random walk at a stopping time (or an equivalent first-passage decomposition), and, for the infinitely-often milestone, either the lower law of the iterated logarithm for Gaussian walks or the Hewitt–Savage/Kolmogorov zero–one law combined with the central limit theorem. These pieces are reusable well beyond this mission; contributions of any of them, as separate lemmas, are welcome.

Selected references

H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58 (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
W. Feller, Statistical aspects of ESP, J. Parapsychology 4 (1940), 271–298 (reference [11] of the paper).
S. R. Howard, A. Ramdas, J. McAuliffe, J. Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), 1055–1080. https://arxiv.org/abs/1810.08240

4 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming: The Set-Inclusive LP Has the Same Feasible Set as the LP of Support FunctionalsResearch Paper

Motivation

A linear program $\max c\cdot x$ subject to $Ax\le b$ , $x\ge 0$ assumes that the constraint matrix $A$ is known exactly. In practice the columns of $A$ — the activity vectors, describing how much of each resource one unit of activity $j$ consumes — are estimates. A. L. Soyster's 1973 technical note in Operations Research (doi:10.1287/opre.21.5.1154) asked what a decision $x$ should satisfy if every activity vector is known only to lie in a given convex set, and the decision has to be feasible for every possible realisation. He called this inexact linear programming, a term he attributes to K. O. Kortanek.

The note is the earliest formulation of what is now called robust linear optimization. Its answer — replace each uncertain column by its coordinatewise worst case — is the "Soyster model" that later work on robust optimization takes as its point of departure: Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Math. Program. 2000) and Bertsimas and Sim (Oper. Res. 2004) both introduce their less conservative uncertainty sets as alternatives to it.

Setting

Fix integers $m,n\ge0$ . Vectors in $\mathbb R^m$ are compared componentwise. For a set $S\subseteq\mathbb R^m$ and a scalar $t$ , $tS=\{ta: a\in S\}$ , and the sum of sets is Minkowski addition, $S+T=\{s+t: s\in S,\ t\in T\}$ .

Let $K_1,\dots,K_n\subseteq\mathbb R^m$ be nonempty convex activity sets and $K\subseteq\mathbb R^m$ a nonempty convex resource set. Problem (I) is

\sup\ c\cdot x\quad\text{subject to}\quad x_1K_1+x_2K_2+\cdots+x_nK_n\subseteq K,\quad x_j\ge0,

and $X\subseteq\mathbb R^n$ denotes its set of feasible $x$ . Problem (Ib) is the special case $K=K(b)=\{y\in\mathbb R^m: y\le b\}$ for a right-hand side $b\in\mathbb R^m$ .

The support functional of a set $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y\cdot a$ , a value in $[-\infty,+\infty]$ . With $e_i$ the $i$ -th unit vector, the auxiliary matrix $\bar A$ is the $m\times n$ matrix with entries

\bar a_{ij}=\delta^*(e_i\mid K_j)=\sup_{a_j\in K_j}a_{ij},

defined when all of these are finite, and LP $(\bar A)$ is the linear program $\max c\cdot x$ subject to $\bar Ax\le b$ , $x\ge0$ . Finally $M$ is the set of $m\times n$ matrices $(a_1,\dots,a_n)$ whose $j$ -th column lies in $K_j$ .

In the application, the activity sets are Euclidean balls $K_j=\{a\in\mathbb R^m:\|a-a_j\|_2\le\rho_j\}$ around nominal columns $a_j$ of a matrix $A_0$ , with radii $\rho_j\ge0$ .

Formalization targets

Goal: the THEOREM (p. 1156)

Assume every $K_j$ is nonempty and convex and $\delta^*(e_i\mid K_j)<\infty$ for all $i,j$ . Then

\{x : x\ \text{feasible for (Ib)}\}=\{x : \bar Ax\le b,\ x\ge 0\},

and for every objective $c$ , the optimal solutions of (Ib) and of LP $(\bar A)$ coincide.

Milestones

Feasibility for (I) is equivalent to $x\ge0$ and $\sum_j x_ja_j\in K$ for every choice $a_j\in K_j$ (p. 1154).
LEMMA (p. 1155): $X$ is convex.
If $\delta^*(e_i\mid K_j)=\infty$ for some $i$ , every feasible $x$ of (Ib) has $x_j=0$ (p. 1155).
Compact activity sets have $\delta^*(e_i\mid K_j)<\infty$ (p. 1156).
$x$ is feasible for (Ib) iff $Ax\le b$ for every $A\in M$ and $x\ge0$ (p. 1156).
Every $A\in M$ satisfies $A\le\bar A$ entrywise (proof of THEOREM).
Feasible for LP $(\bar A)$ implies feasible for (Ib) (proof of THEOREM).
Feasible for (Ib) implies $\sum_j x_j\sup_{a_j\in K_j}a_{ij}\le b_i$ for every $i$ , i.e. feasible for LP $(\bar A)$ (proof of THEOREM).
For Euclidean balls, $\delta^*(e_i\mid K_j)=a_{ij}+\rho_j$ , so $\bar a_j=a_j+\rho_je$ with $e$ the all-ones vector (p. 1157).
Inexact LP over balls: (Ib) has the same feasible and optimal solutions as $\max c\cdot x$ subject to $\sum_j x_j(a_j+\rho_je)\le b$ , $x\ge0$ (p. 1157).

Significance

The THEOREM turns a semi-infinite constraint — one linear inequality for every matrix in $M$ , of which there are typically uncountably many — into a single linear program of the original size, whose data are the support functionals of the activity sets. Any LP solver then solves the uncertain problem. The hypersphere corollary shows the cost of this guarantee concretely: every entry of column $j$ is inflated by the full radius $\rho_j$ , which is why the model is called conservative and why later robust-optimization work introduced ellipsoidal and budgeted uncertainty sets as less conservative alternatives. The LEMMA classifies (I) as a convex program in general, for resource sets that are not half-space intersections.

The results are proved in the paper and are standard. To our knowledge they have no machine-checked proof in Lean or Mathlib. The mission produces a formal statement of the set-inclusive constraint as an actual Minkowski-sum inclusion, the support-functional reduction with its finiteness hypotheses made explicit, and the Euclidean-ball computation — a base that robust-counterpart results for other uncertainty sets can be compared against.

Difficulty

The individual arguments are short; the work is in the bookkeeping that the paper leaves implicit. The step from "for every $A\in M$ " to $\bar A$ uses that the supremum of a sum of independent terms is the sum of suprema, which needs every $K_j$ nonempty and the scalars $x_j$ nonnegative; with an empty activity set the Minkowski sum is empty and every $x\ge0$ becomes feasible. The support functional is valued in the extended reals, and its conversion to a real matrix entry is exact only under the finiteness assumption, which the paper secures by deleting columns. The ball computation needs the Euclidean norm and its dual characterisation of the maximum of a coordinate over a ball.

Formalization scope

Vectors are Fin m → ℝ and Fin n → ℝ, with indices $0,\dots,m-1$ in place of $1,\dots,m$ ; the order on vectors is componentwise.
Feasibility of (I) is the Minkowski-sum inclusion (∑ j, x j • K j) ⊆ R (pointwise set operations) together with $x\ge0$ . It is not defined as "for every choice $a_j\in K_j$ ", which would make milestones 1 and 5 trivial, and $\bar A$ is constructed from the $K_j$ , not an arbitrary matrix dominating $M$ , which would make the goal trivial.
$\delta^*$ is valued in EReal. The entries of $\bar A$ are its real conversions, so every statement mentioning $\bar A$ assumes $K_j\neq\emptyset$ and $\delta^*(e_i\mid K_j)<\infty$ , the paper's standing assumptions (pp. 1154–1156). Convexity of the $K_j$ is also kept as a hypothesis wherever the paper has it, although only the LEMMA uses convexity (of $K$ ).
An optimal solution is a feasible point attaining the maximum of $c\cdot x$ ; the paper writes $\sup$ and does not discuss attainment. Because the goal identifies the feasible sets, the two problems also have equal suprema.
Hyperspheres use the Euclidean norm (EuclideanSpace ℝ (Fin m)), not the sup norm of Fin m → ℝ, with radii $\rho_j\ge0$ .
The support functional restates the published FenchelRobust.Counterpart.supportFun with the same body.
Not formalized: Magnanti's extension to $\ge$ and $=$ rows (p. 1156), and the remarks on (GLP) and stochastic programming. Contributions of proofs of any milestone, and of an EReal statement equating the optimal values, are welcome.

Selected references

A. L. Soyster, Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming, Operations Research 21(5), 1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Mathematics of Operations Research 23(4), 769–805, 1998. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal and A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Mathematical Programming 88, 411–424, 2000. https://doi.org/10.1007/PL00011380
D. Bertsimas and M. Sim, The Price of Robustness, Operations Research 52(1), 35–53, 2004. https://doi.org/10.1287/opre.1030.0065

12 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Inventory Control in a Fluctuating Demand Environment I: With Linear Order Costs, a World-Dependent Basestock Policy Is Optimal over the Infinite HorizonResearch Paper

Motivation

An inventory controller must decide how much to order while demand changes with an observed external condition. A single demand rate misses that dependence: the same inventory position can justify different orders when the condition changes. Song and Zipkin's 1993 study asks whether a simple policy remains optimal when the condition follows a continuous-time Markov chain and orders arrive after a random lead time. The answer for linear ordering costs is a world-dependent basestock policy: each world state has one target inventory position, and an order raises the current position to that target when it lies below it.

The policy claim concerns an infinite horizon. It is stronger than showing that a particular collection of target levels performs well or that such a policy minimizes a one-step cost. Theorem 2 of Song and Zipkin identifies the targets through a limiting value function and establishes optimality for the full discounted problem. This mission formalizes that theorem and the finite-stage results the authors use to state its limit precisely.

Setting

The world state $i$ belongs to a nonempty countable set $I$ . The world evolves according to a conservative continuous-time Markov generator $Q=(q_{ij})$ , with exit rate $q_i=-q_{ii}$ . When the world is in state $i$ , customers demand individual units at rate $\lambda_i\ge0$ . The exit rates and demand rates are bounded above. Inventory is fully backlogged: a negative inventory level records unmet demand. The controller observes the world state and the inventory position $x\in\mathbb Z$ , which includes outstanding orders, and chooses an order-up-to position $y\ge x$ .

An order has actual unit cost $\bar c\ge0$ and may have fixed cost $\bar K\ge0$ . This mission takes the linear-cost case, so the discounted fixed cost is $K=0$ . The lead time $L$ is a finite nonnegative random time, independent of the world and demand process. Its Laplace transform discounts the ordering costs to $c=\bar c\,E[e^{-\alpha L}]$ , where $\alpha>0$ is the discount rate. Holding one unit costs $h>0$ per unit time; backlogging one unit costs $p>0$ .

Write $D_L^i$ for the number of demands during the lead time conditional on initial world state $i$ . The cost rate of an inventory level $z$ is $\widehat C(z)=-pz$ for $z<0$ and $hz$ otherwise. The lead-time cost and myopic cost are

C(i,y)=E[e^{-\alpha L}\widehat C(y-D_L^i)],\qquad G^+(i,y)=(1-\gamma)cy+\beta C(i,y),

where $\mu>0$ is a uniformization rate at least $\sup_iq_i+\sup_i\lambda_i$ , $\beta=(\mu+\alpha)^{-1}$ , and $\gamma=\beta\mu$ . The paper's Assumption 1, $\alpha\bar c<p$ , applies to the later results. It ensures the myopic cost has finite nonnegative minimizers. The smallest such minimizer in world state $i$ is $y^+(i)$ , and $y^+_{\min}=\min_i y^+(i)$ .

With zero fixed cost and zero terminal cost, the $n$ -stage transformed cost $W_n(i,x)$ minimizes the auxiliary cost $G_n(i,y)$ over $y\ge x$ . Each $G_n$ combines the myopic cost with the expected discounted continuation after a demand, a world-state jump, or a self-loop. Let $W_\infty$ and $G_\infty$ denote their pointwise limits. A basestock policy $\pi(y)$ orders to $\max\{x,y(i)\}$ in state $(i,x)$ ; it never cancels an outstanding order.

Formalization targets

The main target is the finite, smallest global minimizer $y^*(i)$ of $G_\infty(i,\cdot)$ for each world state, with the inequalities of Theorem 2(c):

0\le y^+_{\min}\le y^*(i)\le y^*_\infty(i)\le y^+(i), \qquad G_\infty(i,y^*_\infty(i))=\min_{z\in\mathbb Z}G_\infty(i,z).

Here $y^*_\infty(i)$ is the limit of the smallest finite-stage minimizers $y^*_n(i)$ . Theorem 2(e) then asserts that $\pi(y^*)$ has minimum infinite-horizon expected discounted cost from every state among all feasible policies. The milestone list states Lemmas 1, 2 and 4, Corollaries 1 and 2, all parts of Theorem 1 as identified by the paper's internal references, and the limit and optimality-equation clauses of Theorem 2. Together they fix the finite-stage and limiting objects used by the goal.

Significance

The theorem reduces a decision at every integer inventory position to one integer target for each observed world state. It gives an exact policy structure for a model with a changing demand rate and random lead time, rather than an approximation derived from a constant-demand model. The limiting inequalities also locate an optimal target relative to the myopic target and the finite-stage targets, giving a mathematically specified range for policy computation. These claims are the linear-cost part of Song and Zipkin's analysis; the paper proves the result but supplies no Lean proof.

Formalization will leave reusable definitions for countable-state uniformization with a demand counter, integer convexity of inventory cost functions, and discounted costs of history-dependent policies. The mission's theorem statements compile as open goals. The remaining work is to verify the analytic properties of the lead-time demand law, the finite-stage inequalities, convergence, and the infinite-horizon policy comparison. The fixed-order-cost and monotone-world-state results of the paper are separate missions.

Difficulty

The world can have countably many states, so a continuation value includes a series over possible world jumps. The stage cost grows with inventory position, so a bounded-cost finite-state dynamic-programming theorem does not directly cover the model. The minimization is over an unbounded set of integers, and the minimizers themselves change with the stage number. Convexity of a one-stage cost alone does not establish that the limiting policy beats policies that use the entire observation history. These are the specific gaps the paper's bound, ordered-difference, and limit results address.

Formalization scope

World states are a nonempty countable Lean type, inventory positions and order-up-to levels are integers, and costs are real until policy evaluation. The lead-time law is a probability measure on finite nonnegative real times, independent of world and demand. The demand-count law is defined by exact Poisson uniformization at rate $\mu$ , with demand, world-jump, and self-loop branches. The infinite-horizon policy cost uses extended nonnegative reals and a supremum of finite-horizon costs, so it can express an infinite expected cost without a default real value. Policies may depend on all past observed states; the goal compares its basestock policy against every feasible deterministic policy in this class. Randomized policies are omitted because they cannot improve expected nonnegative costs on this countable state space.

Assumption 1 is attached only to the results that use it. The linear-cost recursion has $K=0$ and $W_0=0$ . Integer convexity means nondecreasing forward differences. Smallest minimizers and the minimum across world states are asserted to exist; neither is encoded by an integer infimum that returns a default on an empty or unbounded set. The goal requires an actual optimal policy cost comparison from every state, so solving the limiting optimality equation only within basestock policies cannot close it. Contributions to the lead-time mixture, integer convexity, boundedness of the real series and infima, and unrestricted policy comparison all fit this scope.

Selected references

Jing-Sheng Song and Paul Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. DOI 10.1287/opre.41.2.351.

12 thms2 active usersReviewed

All missions

Asynchronous Stochastic Approximation and Q-Learning 2: Asynchronous Stochastic Approximation with Outdated Information Converges with Probability 1 Under a Weighted Maximum Norm ContractionResearch Paper

Motivation

Setting

Formalization targets

Boundedness under a weighted growth bound

Almost-sure convergence under a weighted contraction

Significance

Difficulty

Formalization scope

Selected references

Asynchronous Stochastic Approximation and Q-Learning 1: Bounded Asynchronous Stochastic Approximation Iterates Converge with Probability 1 to the Unique Fixed Point of a Monotone Continuous MapResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 189)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Vertical Integration and Antitrust Policy: Integrating Successive Monopolies Lowers the Final Price and Raises Output, Joint Profit and Consumer SurplusResearch Paper

Motivation

Setting

Formalization targets

Goal: vertical integration benefits producer and consumer

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Theorem on Boolean Matrices: Warshall's Construction M* Equals the Boolean Sum M ∨ M² ∨ ⋯ ∨ Mᵈ of the Boolean Powers of MResearch Paper

Motivation

Setting

Formalization targets

Goal: the construction computes the power sum

Milestone 1 (Proved, referenced): the THEOREM

Milestone 2: footnote 2

Companion: footnote 3

Significance

Difficulty

Formalization scope

Selected references

On Cores and Indivisibility 1: The Housing Market's Game Without Side Payments Is BalancedResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

METRIC: A Multi-Echelon Technique for Recoverable Item Control 2: Under Poisson Demand Expected Backorders Are Strictly Convex in the Mean, So a Point Estimate Understates ThemResearch Paper

Motivation

Setting

Formalization targets

Goal: the point estimate understates backorders (pp. 138–139)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Discrete Dynamic Programming with Sensitive Discount Optimality Criteria 1: If Every Stationary Policy Is Transient, Some Stationary Policy Maximizes the Expected Total Reward over All PoliciesResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Some Theoretical Aspects of Road Traffic Research I: Time-Mean Speed Equals Space-Mean Speed plus σₛ²/v̄ₛ, so v̄ₜ ≥ v̄ₛ with Equality Only Without Speed VariationResearch Paper

Why two traffic speed averages differ

Traffic streams and their two distributions

Formalization targets

What the result supplies

Where the formal proof needs care

Formalization scope

Selected references

On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting 1: If G(f) ∪ H(f) Is Empty, f Maximizes the Gain and Then the Bias, and Each Improvement Step Raises (x, y, z)Research Paper

Goal: the two moments of $Z\vee Z'$ (Eq. (11), p. 508, and the display on p. 509)