Prove2Me

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

Markov Chain

189 missions · 85 completed

Missions

Mathematical PhysicsProbability·Captain: wurtle

A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phaseResearch Paper

Motivation

The Sherrington–Kirkpatrick (SK) model (1975) is the basic mean-field spin glass: nn Ising spins interact through independent Gaussian couplings of variance β2/n\beta^2/n, so each spin is weakly coupled to every other one with random signs. The model is the testing ground for questions about disordered systems, about sampling from Gibbs measures, and about the performance of Markov chain Monte Carlo. A central question is whether Glauber (heat-bath) dynamics, which resamples one spin at a time from its conditional law, relaxes at a rate independent of the system size. Equivalently: does the Gibbs measure satisfy a dimension-free Poincaré inequality with respect to the heat-bath Dirichlet form?

The equilibrium high-temperature phase is β<1\beta<1, where the free energy equals its annealed value (Aizenman, Lebowitz and Ruelle 1987). Dynamical results had reached only part of this range.

Timeline

The source of this mission is an OpenAI preprint dated September 24, 2026, which treats every fixed β<1\beta<1.

Setting

Fix 0<β<10<\beta<1. Let JJ be a symmetric n×nn\times n matrix with zero diagonal and independent entries Jik∼N(0,β2/n)J_{ik}\sim N(0,\beta^2/n) for i<ki<k. The zero-field Gibbs law on {−1,1}n\{-1,1\}^n is

μ0(x)=1Zexp⁡{12xTJx}.\mu_0(x)=\frac1{Z}\exp\Bigl\{\tfrac12x^{\mathsf T}Jx\Bigr\}.

Let PiP_i be the conditional expectation under μ0\mu_0 given all spins except xix_i; it averages ff over xx and its ii-th flip with Gibbs weights. The unscaled Dirichlet form is

D(f)=∑i=1nEμ0(f−Pif)2.\mathcal D(f)=\sum_{i=1}^n\mathbb E_{\mu_0}\bigl(f-P_if\bigr)^2 .

The discrete heat-bath chain picks a uniform site and resamples it, with transition operator n−1∑iPin^{-1}\sum_iP_i; its spectral gap is inf⁡fD(f)/(nVar⁡μ0f)\inf_f \mathcal D(f)/(n\operatorname{Var}_{\mu_0}f) over nonconstant ff.

Formalization targets

Goal: Theorem 1.1

There is a finite constant CβC_\beta such that

PJ{Var⁡μ0(f)≤Cβ D(f) for every f:{−1,1}n→R} ⟶ 1,\mathbb P_J\Bigl\{\operatorname{Var}_{\mu_0}(f)\le C_\beta\,\mathcal D(f)\ \text{for every }f:\{-1,1\}^n\to\mathbb R\Bigr\}\ \longrightarrow\ 1,

and consequently the discrete heat-bath chain has spectral gap at least 1/(Cβn)1/(C_\beta n) with probability tending to one. Lean: OAI.SKGap.sk_main, open on the platform.

Significance

The theorem gives a size-independent relaxation time for continuous-time heat-bath dynamics (rate-one clocks) throughout the high-temperature phase, for every observable simultaneously on one disorder event. It extends the dynamical picture from β<1/2+ε0\beta<1/2+\varepsilon_0 to the full equilibrium range β<1\beta<1, where only linear-observable (covariance) control was previously known. A Poincaré inequality is the input for L2L^2 mixing bounds and for companion results on cutoff and critical slowing down.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Dobrushin-type influence bounds fail because the sum of absolute couplings at a site grows like n\sqrt n; any argument must exploit cancellations from the random signs. Covariance bounds control only linear observables, while the Poincaré inequality must hold for all 22n2^{2^n}-dimensional families of test functions at once. The natural route through stochastic localization runs into rare observation events: an event of exponentially small probability can still carry most of the variance of a particular test function, and invertibility of the field equation must hold at every sufficiently accurate solution along the observation path.

Formalization scope

  • Spins are Fin n → Bool, with spinValue mapping to ±1\pm1; couplings are indexed by pairs i<ki<k (Edge n) and symmetrized with zero diagonal by coupling.
  • hamiltonian g 0 x = ½ ∑_{i,k} x_i J_{ik} x_k; mass, expectation, variance are exact finite sums over {−1,1}n\{-1,1\}^n.
  • conditionalExpectation g h i f x is the two-point Gibbs average over xx and its ii-th flip; dirichlet is the unscaled form ∑iE(f−Pif)2\sum_i\mathbb E(f-P_if)^2.
  • disorderLaw β n = Measure.pi (fun _ => gaussianReal 0 (β^2/n)) over the edges (variance β2/n\beta^2/n).
  • discreteGap g is the infimum of D(f)/(nVar⁡f)\mathcal D(f)/(n\operatorname{Var}f) over ff with positive variance.
  • MainStatement β asserts a single C>0C>0 for which both the Poincaré event and the gap event have probability tending to 11.

Formalization needs Gaussian product measures, finite Gibbs measures and heat-bath operators, and the analysis behind the proof: matrix concentration, TAP/AMP-type field recursions and stochastic localization. Formal versions of the paper's intermediate results (for example Proposition 8.3, the terminal observation gap) are welcome.

Selected references

2 thms1 active userReviewed
CombinatoricsTheoretical Computer Science·Captain: wurtle

An FPRAS for Cell-Bounded Contingency TablesResearch Paper

Motivation

A cell-bounded contingency table is a nonnegative integer matrix with prescribed row sums, column sums and an upper bound on each entry. Bounds of zero forbid entries (structural zeros), and bounds of one give bipartite graphs with prescribed degrees, so the model contains degree-constrained subgraph counting and perfect matchings (the permanent). Counting such tables is central to exact conditional inference in statistics and is equivalent to counting integer flows in bipartite networks. Exact counting is #P-complete even for two-row ordinary tables (Dyer, Kannan and Mount, 1997), so the target is a fully polynomial randomized approximation scheme (FPRAS): a randomized algorithm that, for any ε,δ∈(0,1)\varepsilon,\delta\in(0,1), returns a (1±ε)(1\pm\varepsilon)-approximation with probability at least 1−δ1-\delta in time polynomial in the input length, 1/ε1/\varepsilon and log⁡(1/δ)\log(1/\delta).

Timeline

  • 1986. Jerrum, Valiant and Vazirani relate approximate counting and sampling through self-reducibility.
  • 1995. Diaconis and Gangolli survey fixed-margin arrays (doi:10.1007/978-1-4612-0801-3_3).
  • 1997. Dyer, Kannan and Mount prove #P-completeness for two-row tables and give geometric methods for large margins; Morris improves the margin requirements in 2002 (doi:10.1002/rsa.10049).
  • 2000–2003. Dyer and Greenhill (two rows), Cryan and Dyer (fixed number of rows), Dyer (dynamic programming) give approximate counting for a bounded number of rows.
  • 2004. Jerrum, Sinclair and Vigoda's permanent algorithm yields an FPRAS for all 0/1 caps (doi:10.1145/1008731.1008738).
  • 2009–2010. Barvinok bounds weighted table counts within NO(m+n)N^{O(m+n)} (doi:10.1093/imrn/rnn133); Barvinok, Luria, Samorodnitsky and Yong give quasipolynomial randomized approximations for smooth margins (doi:10.1002/rsa.20301).
  • 2010. Cryan, Dyer and Randall give an FPRAS for integral flows with large tight capacities and for cell-bounded tables with a fixed number of rows, and list unrestricted approximation as open (doi:10.1137/060650544).
  • 2023. Brändén, Leake and Pak give capacity lower bounds via Lorentzian polynomials (doi:10.1007/s11856-022-2364-9); Guo and Jerrum count vertices of certain 0/1 polytopes (doi:10.1007/s00454-022-00406-8).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims an FPRAS with no restriction on dimensions, margins or caps.

Setting

For positive integers m,nm,n, margins r∈Z≥0mr\in\mathbb Z_{\ge0}^m, c∈Z≥0nc\in\mathbb Z_{\ge0}^n with equal totals, and bounds b∈Z≥0m×nb\in\mathbb Z_{\ge0}^{m\times n},

Ω(r,c,b)={X∈Z≥0m×n: ∑jXij=ri, ∑iXij=cj, Xij≤bij},Z(r,c,b)=∣Ω(r,c,b)∣.\Omega(r,c,b)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j,\ X_{ij}\le b_{ij}\Bigr\},\qquad Z(r,c,b)=|\Omega(r,c,b)|.

All numbers are written in binary, so a capacity can be exponentially larger than its description. LL denotes the total binary input length including the rational accuracy parameters ε,δ\varepsilon,\delta. The algorithm uses independent unbiased random bits and is charged for every bit operation.

Formalization targets

Goal: Theorem 1.1 (FPRAS)

One randomized algorithm, given (r,c,b)(r,c,b) and rational ε,δ∈(0,1)\varepsilon,\delta\in(0,1), outputs a nonnegative rational Z^\widehat Z with

Pr⁡[(1−ε)Z(r,c,b)≤Z^≤(1+ε)Z(r,c,b)]≥1−δ,\Pr\bigl[(1-\varepsilon)Z(r,c,b)\le\widehat Z\le(1+\varepsilon)Z(r,c,b)\bigr]\ge1-\delta,

outputs exactly 00 on every execution when Ω(r,c,b)=∅\Omega(r,c,b)=\emptyset, and performs at most poly(L,ε−1,log⁡δ−1)\mathrm{poly}(L,\varepsilon^{-1},\log\delta^{-1}) bit operations on every execution. Lean: OAI.ContingencyTables.counting, open on the platform.

Significance

The theorem would answer the question left open by Cryan, Dyer and Randall in 2010: approximate counting of cell-bounded tables (equivalently, integral flows in bipartite networks with arbitrary capacities) without any fixed-dimension, large-capacity, density or balance assumption, with polynomial cost on every execution and no oracle. It contains the 0/1 case handled by Jerrum–Sinclair–Vigoda and the fixed-row results as special cases, and via self-reduction it gives approximate samplers for integer flows. A companion preprint of the same family treats exact uniform sampling of uncapped tables. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Two regimes clash. Large capacities cannot be expanded into that many binary choices without exponential blow-up, so geometric (polytope volume) methods are needed for them; but those methods require every cell to be large. Small capacities need combinatorial Markov chains, which in turn must preserve exactly one unit of mass per table despite the multiplicities created by encoding a bounded integer by binary choices. Arbitrary mixtures of tiny and huge caps, zero caps and variable dimensions defeat each approach used alone.

Formalization scope

  • Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table on an 8-symbol alphabet, one random bit per tick; time is counted in ticks (polynomially equivalent to bit operations).
  • Inputs are delimited binary encodings of m,n,r,c,bm,n,r,c,b and of ε,δ\varepsilon,\delta as reduced fractions (encodeCountingInput); outputs are encoded rationals.
  • count r c b is Fintype.card of bounded tables.
  • CountingStatement: one machine and constants C>0C>0, dd; with t=C(∣input∣+⌈1/ε⌉+⌈log⁡2⌈1/δ⌉⌉+1)dt=C(|\text{input}|+\lceil1/\varepsilon\rceil+\lceil\log_2\lceil1/\delta\rceil\rceil+1)^d, every tape of length tt halts with a rational q≥0q\ge0; if count = 0 every tape outputs 00; and the fraction of tapes with (1−ε)Z≤q≤(1+ε)Z(1-\varepsilon)Z\le q\le(1+\varepsilon)Z is at least 1−δ1-\delta.
  • m,n≥1m,n\ge1 and equal margin totals are hypotheses, as in the paper.

Needed infrastructure: randomized Turing machines, Markov chain mixing and Poincaré inequalities, log-concavity (Prékopa–Leindler), and network-flow feasibility. The machine model and encodings are shared with the exact-sampling mission of this family. Contributions formalizing Proposition 2.2 (contamination bound), Lemma 3.3 (log-concave tree marginals), Proposition 6.1 (weight evaluation) or Proposition 7.2 are welcome.

Selected references

2 thms1 active userReviewed
CombinatoricsTheoretical Computer Science·Captain: wurtle

Exact Uniform Sampling of Contingency Tables with Arbitrary MarginsResearch Paper

Motivation

A contingency table with margins r=(r1,…,rm)r=(r_1,\dots,r_m) and c=(c1,…,cn)c=(c_1,\dots,c_n) is a nonnegative integer matrix whose row sums are rr and column sums are cc. Such tables are the basic objects of categorical data analysis: conditional tests of independence (Fisher's exact test and its generalizations) compare an observed table with the uniform distribution on all tables with the same margins, and in practice this requires sampling uniformly from that set. The set is finite but can be exponentially large in the input size when margins are written in binary. Whether one can sample it (approximately or exactly) in time polynomial in both dimensions and in the bit length of the margins has been open since the 1990s.

Timeline

  • 1995. Diaconis and Gangolli survey enumeration and random generation of rectangular arrays with fixed margins (doi:10.1007/978-1-4612-0801-3_3).
  • 1997–2002. Dyer, Kannan and Mount sample dense tables via the transportation polytope; Morris improves the dense bounds (doi:10.1002/rsa.10049).
  • 2000. Dyer and Greenhill give polynomial-time approximate counting and sampling for two-rowed tables.
  • 2003. Kijima and Matsui give exact sampling for two rows by coupling from the past; Cryan and Dyer approximately count for a fixed number of rows (doi:10.1016/S0022-0000(03)00014-X); Dyer gives an exact dynamic-programming sampler for fixed row count.
  • 2006. Cryan, Dyer, Goldberg, Jerrum and Martin prove rapid mixing of the heat-bath chain for every fixed number of rows (doi:10.1137/S0097539703434243).
  • 2016. DeSalvo and Zhao give an exact divide-and-conquer sampler whose polynomial runtime is conditional on a conjecture (arXiv:1507.00070).
  • 2021. Arman, Gao and Wormald give linear-time exact generation for sparse margins with 5Δ4<N5\Delta^4<N, and report that no polynomial-time approximately uniform sampler for arbitrary margins was known (arXiv:2104.09413).
  • 2024. Göbel, Liu, Manurangsi and Pappik turn sufficiently accurate samplers into perfect samplers (arXiv:2410.00882).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims both an almost-uniform and an exactly uniform sampler for arbitrary margins.

Setting

For nonnegative integer vectors r∈Z≥0mr\in\mathbb Z_{\ge0}^m, c∈Z≥0nc\in\mathbb Z_{\ge0}^n with common total N=∑iri=∑jcjN=\sum_ir_i=\sum_jc_j, let

Ω(r,c)={X∈Z≥0m×n: ∑jXij=ri, ∑iXij=cj}.\Omega(r,c)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j\Bigr\}.

The input is (m,n,r,c)(m,n,r,c) with margins in binary, so its length is polynomial in mm, nn and log⁡(N+1)\log(N+1). An algorithm uses unbiased random bits. For laws on a finite set, TV(μ,ν)=12∑x∣μ(x)−ν(x)∣\mathrm{TV}(\mu,\nu)=\tfrac12\sum_x|\mu(x)-\nu(x)|.

Formalization targets

Milestone: Theorem 1.1(i) (almost-uniform, bounded time)

For each k≥1k\ge1, an algorithm halts on every execution in time poly(m,n,log⁡(N+1),k)\mathrm{poly}(m,n,\log(N+1),k) and outputs X∈Ω(r,c)X\in\Omega(r,c) with

TV(law(X), Unif Ω(r,c))≤2−k.\mathrm{TV}\bigl(\mathrm{law}(X),\ \mathrm{Unif}\,\Omega(r,c)\bigr)\le2^{-k}.

Goal: Theorem 1.1(ii) (exact uniform sampling)

An algorithm outputs X∈Ω(r,c)X\in\Omega(r,c) with

Pr⁡[X=Y]=1∣Ω(r,c)∣(Y∈Ω(r,c)),\Pr[X=Y]=\frac1{|\Omega(r,c)|}\quad(Y\in\Omega(r,c)),

terminates almost surely, and has expected running time poly(m,n,log⁡(N+1))\mathrm{poly}(m,n,\log(N+1)), with polynomials uniform over all margins. Lean: OAI.ContingencyTables.exactSampling, open on the platform.

Significance

The theorem would give the first unconditional polynomial-time exact uniform sampler for contingency tables with arbitrary dimensions and binary margins, with no positivity, sparsity, balance or fixed-dimension restriction, and with all random bits and integer arithmetic counted. It removes the fixed-row restriction of the Dyer–Greenhill and Cryan–Dyer line and the sparsity condition of Arman–Gao–Wormald. The exponents are deliberately large; the contribution is the existence of a polynomial algorithm. Exact time is polynomial in expectation, not on every run. A companion preprint of the same family gives an FPRAS for counting tables with cell bounds. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Markov-chain approaches mix rapidly for a fixed number of rows, but the bounds degrade with the row count. Geometric (polytope) methods need all margins to be large, and fail when some margins are tiny while others are huge, which is exactly the mixed regime that arbitrary binary margins allow. Making the sampler exact rather than approximate adds a separate difficulty: the residual-mixture correction requires that the actual output law of the approximate sampler can be computed, with cost polynomial in the accuracy bits.

Formalization scope

  • Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table over an 8-symbol tape alphabet; each tick reads one random bit and either moves, writes or halts. Time is counted in ticks, polynomially equivalent to bit operations.
  • Inputs are binary encodings with delimiters (encodeNat, encodeMargins); outputs are row-major matrix encodings left on the tape (OutputsTable).
  • tableMass A input t X and haltMass A input t are the fractions of the 2t2^t random tapes of length tt that halt with output XX, respectively halt at all, within tt ticks.
  • ExactSamplingStatement: one machine and constants C>0C>0, dd such that for all m,n,r,cm,n,r,c with equal totals: every halted output is in Ω(r,c)\Omega(r,c); tableMass → 1/|Ω| for each table; haltMass → 1; and ∑t(1−haltMasst)\sum_t(1-\text{haltMass}_t), the expected running time, is at most C(m+n+⌈log⁡2(N+1)⌉+1)dC(m+n+\lceil\log_2(N+1)\rceil+1)^d.
  • BoundedSamplingStatement: every tape of length t=C(m+n+⌈log⁡2(N+1)⌉+k+1)dt=C(m+n+\lceil\log_2(N+1)\rceil+k+1)^d halts with a feasible table, and the TV distance to uniform is at most 2−k2^{-k}.
  • Dimensions m,nm,n vary freely (zero allowed); the machine is uniform, not one per size.

Needed infrastructure: randomized Turing machines and their output laws, Markov chain mixing (conductance, Poincaré inequalities), and log-concave sampling. Contributions formalizing Theorem 4.3 (graph Poincaré inequality), Theorem 5.1 (dense completion draw), Proposition 6.3 (law tabulation) or the Göbel–Liu–Manurangsi–Pappik correction are welcome.

Selected references

3 thms1 active userReviewed
CombinatoricsTheoretical Computer Science·Captain: wurtle

Approximate counting of common bases of two matroidsResearch Paper

Motivation: counting common bases of two matroids

A matroid abstracts linear independence: a finite ground set with a family of "independent" subsets that is closed under subsets and satisfies the augmentation axiom. Its maximal independent sets, the bases, all have the same size, the rank. Matroid intersection, finding a common basis of two matroids, is one of the central polynomially solvable problems of combinatorial optimization (Edmonds, 1979). Counting common bases is much harder. It contains counting bases of a single matroid (take both matroids equal) and counting perfect matchings of a bipartite graph (take two partition matroids), and exact counting is #P-hard. The natural goal is therefore a fully polynomial randomized approximation scheme (FPRAS): an algorithm whose output is within relative error ϵ\epsilon with probability at least 1−δ1-\delta, in time polynomial in the input size, ϵ−1\epsilon^{-1} and log⁡δ−1\log\delta^{-1}. The matroids should be accessible only through independence oracles.

Background and timeline

  • 1979 — Edmonds gives a polynomial-time algorithm for matroid intersection (Ann. Discrete Math. 4).
  • 1992 — Feder and Mihail give sampling and approximate counting for balanced matroids (STOC 1992).
  • 2004 — Jerrum, Sinclair and Vigoda give an FPRAS for the permanent of nonnegative matrices, covering bipartite perfect matchings (J. ACM 51).
  • 2007 — Barvinok and Samorodnitsky obtain coarse logarithmic estimates via random weighting (Israel J. Math. 158).
  • 2016–2017 — Anari, Oveis Gharan and Rezaei prove rapid mixing for strongly Rayleigh distributions (COLT 2016); Anari and Oveis Gharan obtain exponential-factor approximations from real-stable polynomials (arXiv:1702.02937).
  • 2020 — Brändén and Huh develop Lorentzian polynomials (Ann. of Math. 192).
  • 2021 — Anari, Oveis Gharan and Vinzant give a deterministic 2O(r)2^{O(r)}-factor approximation for common bases of rank-rr matroids (Duke Math. J. 170); Cryan, Guo and Mousa ask for a rapidly mixing chain for common bases (Ann. Probab. 49).
  • 2023–2024 — Liu's dissertation records the FPRAS question for two arbitrary oracle matroids (Section 13.2, Problem 1, thesis); Anari, Liu, Oveis Gharan and Vinzant give an FPRAS for bases of a single matroid (Ann. of Math. 199).
  • 2026 — An OpenAI preprint, Approximate counting of common bases of two matroids (OpenAI Math Release, September 23, 2026), claims an independence-oracle FPRAS for common bases of two arbitrary matroids of equal rank. It has not been peer reviewed, and its proof is not formally verified.

Setting

Let M1,M2M_1,M_2 be matroids of the same rank rr on the ground set [n][n], supplied by exact independence oracles: a query is an nn-bit indicator of a subset, and the answer says whether it is independent. The quantity to estimate is

Z(M1,M2)=∣B(M1)∩B(M2)∣,Z(M_1,M_2)=\bigl|\mathcal B(M_1)\cap\mathcal B(M_2)\bigr|,

the number of common bases. The input also contains rationals ϵ,δ∈(0,1)\epsilon,\delta\in(0,1); ℓ\ell denotes the binary encoding length of n,r,ϵ,δn,r,\epsilon,\delta. Oracle calls are counted separately from the bit operations used to build queries and process answers.

Formalization targets

Goal: an FPRAS for common bases in the independence-oracle model (Theorem 1.1)

There is a single randomized oracle algorithm and a fixed polynomial pp such that, for all rank-rr matroids M1,M2M_1,M_2 on [n][n] and rational ϵ,δ∈(0,1)\epsilon,\delta\in(0,1), it outputs a nonnegative rational Z^\widehat Z with

Pr⁡[(1−ϵ)Z≤Z^≤(1+ϵ)Z] ≥ 1−δ,\Pr\bigl[(1-\epsilon)Z\le\widehat Z\le(1+\epsilon)Z\bigr]\ \ge\ 1-\delta,

the output is always 00 when Z=0Z=0, and on every execution the numbers of oracle calls and bit operations are at most p(n,ℓ,ϵ−1,log⁡δ−1)p(n,\ell,\epsilon^{-1},\log\delta^{-1}). The algorithm uses only independent fair random bits. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.1 answers the question recorded by Liu (2023) and extends both the single-matroid FPRAS of Anari–Liu–Oveis Gharan–Vinzant and, in the bipartite-matching case, the permanent FPRAS of Jerrum–Sinclair–Vigoda. It needs no representation of either matroid and holds for unrestricted rank, whereas the previous oracle-model scheme was fully polynomial only for r=O(log⁡n)r=O(\log n). The source derives FPRASs and almost-uniform samplers for common independent sets of prescribed, unrestricted or maximum size, even for matroids of different ranks (Corollary 9.1).

Formalizing it. The Lean goal fixes a concrete machine model, so it states a complete complexity-theoretic claim with no informal "polynomial-time" left. A proof would combine Lorentzian-polynomial inequalities (Brändén–Huh), a transport inequality, a Markov-chain Poincaré bound, and simulated annealing with explicit bit accounting. Each layer is reusable: Mathlib has matroids, but no Lorentzian polynomials, no mixing-time theory of this kind and no randomized-algorithm framework.

Difficulty

For one matroid, the bases-exchange walk mixes rapidly because the basis generating polynomial is log-concave. The intersection of two matroids has no such structure: its common bases need not be connected by short exchanges, and the natural chain on transversals of the paired construction passes through states of exponentially small weight, so positivity and connectivity alone give no polynomial bound. Earlier approaches either lost exponential factors or needed real-stable polynomials that an independence oracle does not provide. The proof must balance defect classes, as in Jerrum–Sinclair–Vigoda, and establish a Poincaré inequality for observables from matroid-theoretic inequalities alone.

Formalization scope

  • Matroids are Mathlib Matroid (Fin n) with ground set univ and eRank = r for both. Oracles are functions Bool → (Fin n → Bool) → Bool, required to answer independence queries exactly.
  • The algorithm is one fixed Program k s for a register machine with k+8k+8 binary stacks: push/pop, fair coin, oracle query on an nn-bit register, and halt with output (register 6)/(register 7) as a rational. Inputs n,r,ϵ,δn,r,\epsilon,\delta are loaded in binary.
  • The resource bound is B=C(1+n+ℓ+⌈ϵ−1⌉+⌈log⁡2⌈δ−1⌉⌉)dB=C(1+n+\ell+\lceil\epsilon^{-1}\rceil+\lceil\log_2\lceil\delta^{-1}\rceil\rceil)^d with constants C>0,dC>0,d fixed before the instance. For every infinite bit stream, the run halts within BB steps with at most BB oracle calls and BB bit operations, outputs a nonnegative rational, and outputs 00 when Z=0Z=0.
  • The success probability is expressed by counting: at least (1−δ)2B(1-\delta)2^B of the 2B2^B bit strings of length BB lead to an output within relative error ϵ\epsilon of ZZ.
  • A trivializing reading is excluded: the program and constants come first and must work for every n,rn,r, matroid pair, oracle and ϵ,δ\epsilon,\delta.
  • Needed infrastructure: Lorentzian polynomials and the homogeneous Tutte inequalities, Markov chains on finite state spaces with Poincaré/variance bounds, annealing estimators, and correctness proofs for the register machine. Contributions on any layer are welcome.

Selected references

2 thms1 active userReviewed
CombinatoricsTheoretical Computer Science·Captain: wurtle

A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General GraphsResearch Paper

Motivation: approximately counting perfect matchings

A perfect matching of a graph is a set of edges covering every vertex exactly once. Finding one is easy — Edmonds (1965) gave a polynomial-time algorithm for general graphs — but counting them is hard: Valiant (1979) proved exact counting #P-complete already for bipartite graphs, where the count is the permanent of a 0–1 matrix. Exact counting is tractable only in special classes, such as planar graphs via Pfaffians (Kasteleyn 1963). The natural relaxation is a fully polynomial randomized approximation scheme (FPRAS): an algorithm that, with probability at least 1−δ1-\delta, returns the count within relative error ε\varepsilon, in time polynomial in the input size, 1/ε1/\varepsilon and log⁡(1/δ)\log(1/\delta). Whether perfect matchings in general (nonbipartite) graphs admit an FPRAS was explicitly raised by Jerrum and Sinclair in 1989 and has been a benchmark question in approximate counting since. Perfect-matching counts are partition functions of the monomer–dimer model, so the question also connects to statistical physics.

Timeline

  • 1963 — Kasteleyn: exact counting of perfect matchings in planar graphs (J. Math. Phys. 1963).
  • 1965 — Edmonds: polynomial-time maximum matching in general graphs (Canad. J. Math. 1965).
  • 1979 — Valiant: computing the permanent is #P-complete (TCS 1979).
  • 1986 — Jerrum, Valiant and Vazirani: equivalence of approximate counting and almost-uniform sampling for self-reducible problems (TCS 1986).
  • 1989 — Jerrum and Sinclair: FPRAS for the number of all matchings in any graph, and for perfect matchings when the near-perfect/perfect ratio is polynomially bounded; they raise the general question (SIAM J. Comput. 1989, Section 7(i)).
  • 2004 — Jerrum, Sinclair and Vigoda: FPRAS for the permanent of every nonnegative matrix, i.e. bipartite perfect matchings (J. ACM 2004); accelerated by Bezáková, Štefankovič, Vazirani and Vigoda (SIAM J. Comput. 2008).
  • 2018 — Štefankovič, Vigoda and Wilmes: graphs on which every chain of Jerrum–Sinclair–Vigoda type either gives perfect matchings exponentially small mass or mixes exponentially slowly (LATIN 2018).
  • 2020–2025 — Cai and Liu relate the problem to the eight-vertex model (ICALP 2020); Fei, Goldberg and Lu locate it among two-state spin systems (Inf. Comput. 2025).
  • 2026 — Further permanent speedups by Chen, Vigoda and Yang (arXiv:2608.26599) and Chen, Guo, Vigoda and Yang (arXiv:2609.20717); deterministic hafnian approximation for dense graphs by Yi (arXiv:2609.04079). An OpenAI preprint, A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs (OpenAI Math Release, September 23, 2026), claims an FPRAS for every finite simple graph. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

A finite simple undirected graph GG on vertices {0,…,n−1}\{0,\dots,n-1\} is given by a set of edges, each written once as a pair (u,v)(u,v) with u<vu<v. A set M⊆EM\subseteq E is a perfect matching if every vertex lies in exactly one edge of MM, and

Z(G)=#{M⊆E:M is a perfect matching of G}.Z(G)=\#\{M\subseteq E: M\text{ is a perfect matching of }G\}.

(The graph with no vertices has Z=1Z=1; any graph with an odd number of vertices has Z=0Z=0.)

A randomized algorithm is modelled as a single fixed machine with a finite transition table over a finite tape alphabet, which at each step reads the current tape symbol and one fresh fair random bit, then writes, moves, or halts. The input is the graph in binary (number of vertices, number of edges, the sorted edge list) followed by the rationals ε\varepsilon and δ\delta in reduced form; the output is a rational number written on the tape when the machine halts.

Formalization targets

Goal: Theorem 1.1 (FPRAS for perfect matchings)

There are a machine AA and constants C>0C>0, dd such that for every graph GG and rationals 0<ε<10<\varepsilon<1, 0<δ<1/20<\delta<1/2, with t=C (∣input∣+⌈ε−1⌉+⌈log⁡2⌈δ−1⌉⌉+1)dt=C\,(|\mathrm{input}|+\lceil\varepsilon^{-1}\rceil+\lceil\log_2\lceil\delta^{-1}\rceil\rceil+1)^d:

  • on every random string of length tt, AA halts within tt steps with a nonnegative rational output Z^\widehat Z;
  • if Z(G)=0Z(G)=0, the output is 00 on every random string;
Pr⁡bits[(1−ε)Z(G)≤Z^≤(1+ε)Z(G)]  ≥  1−δ.\Pr_{\text{bits}}\big[(1-\varepsilon)Z(G)\le\widehat Z\le(1+\varepsilon)Z(G)\big]\;\ge\;1-\delta.

The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem answers the Jerrum–Sinclair question affirmatively: perfect matchings in arbitrary graphs can be approximately counted as efficiently, up to polynomial factors, as in the bipartite case. The worst-case time bound holds for every execution, not just in expectation. Via standard reductions, the source also derives counting schemes for edge subsets with prescribed vertex degrees and for matchings of a fixed size (Corollary 10.1). The accompanying samplers for those families always return a feasible object and approximate the uniform law in total variation.

Formalizing it. The statement fixes a concrete machine model, input encoding and time bound, so a formal proof would certify both correctness of the estimator and the polynomial running time of an explicit algorithm — a level of rigor rarely reached for Markov-chain Monte Carlo results, whose analyses involve many interacting constants.

Difficulty

The natural approach extends the Jerrum–Sinclair–Vigoda Markov chain on perfect and near-perfect matchings, with weights learned while edge activities are gradually lowered. In general graphs this approach provably fails: Štefankovič, Vigoda and Wilmes constructed graphs on which every chain of that type, for any hole-dependent weights, has either exponentially small stationary mass on perfect matchings or exponentially slow mixing. Odd cycles (blossoms) are the reason the bipartite canonical-path arguments do not carry over. A solution needs a different state space and a different mixing analysis.

Formalization scope

  • GraphInput is a vertex count n and a Finset (Fin n × Fin n) of edges with strictly increasing endpoints, so loops and duplicate edges are excluded. Perfect G M requires M ⊆ edges and that each vertex is incident to exactly one edge of M; Z G is the number of such M.
  • The machine model is RandomMachine: a finite transition table on Fin 8 symbols, whose step consumes one random bit and performs a Turing.TM0 write or move, or halts. run folds tick over a list of t bits; halted configurations are absorbing.
  • encodeInput writes the vertex count, edge count and lexicographically sorted edges in binary, then encodeRat ε and encodeRat δ (reduced numerator with sign, denominator). Outputs requires that the machine has halted and the tape to the right of the head is exactly the encoding of the output rational.
  • The time bound is a fixed polynomial with natural ceilings; the success probability is the fraction of good tapes among all 2t2^t tapes.
  • The scheme must be uniform: one machine for all inputs, quantified before the graph. A trivializing reading is excluded because every tape must halt within the bound with a nonnegative output, and zero must be returned exactly when Z(G)=0Z(G)=0.
  • Infrastructure needed: a compiler-style layer turning structured randomized algorithms into RandomMachine transitions, Markov-chain spectral-gap bounds, and sampling-to-counting reductions. The machine model and encodings are reusable for other approximate-counting missions.

Selected references

2 thms1 active userReviewed
ProbabilityReinforcement LearningStochastic Systems·Captain: mikedeng1

On Actor-Critic Algorithms: Convergence of Actor-Critic Algorithms with TD(1) and TD(λ) Critics on Finite MDPsResearch Paper

Motivation

Reinforcement-learning methods for Markov decision processes split into critic-only methods, which learn an approximate value function and act greedily with respect to it, and actor-only methods, which adjust a parameterized policy along a simulated estimate of the gradient of its performance. Critic-only methods with function approximation can fail to converge; actor-only gradient estimates have high variance. Actor–critic methods combine the two: a critic learns, by temporal-difference (TD) learning, just enough about the value function to give the actor a low-variance gradient direction.

Konda and Tsitsiklis (SIAM J. Control Optim. 42 (2003)) gave the first convergence proof for actor–critic algorithms whose critic uses linear function approximation. Their key observation, found independently by Sutton, McAllester, Singh and Mansour (NIPS 1999), is that the critic need not approximate the value function: it suffices to compute its projection onto a low-dimensional subspace spanned by features determined by the policy parameterization. Earlier convergence results (Konda and Borkar, 1999) covered lookup-table representations only. Actor–critic algorithms, in many later variants, are now a standard tool of reinforcement learning, and this paper is the reference for their asymptotic analysis in the average-cost setting.

Setting

A finite cost MDP consists of finite sets X\mathbb X (states) and U\mathbb U (actions), transition probabilities p(y∣x,u)p(y\mid x,u) and a one-stage cost c(x,u)∈Rc(x,u)\in\mathbb R. A randomized stationary policy with parameter θ∈Rn\theta\in\mathbb R^n chooses action uu in state xx with probability μθ(u∣x)\mu_\theta(u\mid x). Under the policy θ\theta, the states {Xk}\{X_k\} form a Markov chain with transition matrix P(θ)xy=∑uμθ(u∣x)p(y∣x,u)P(\theta)_{xy}=\sum_u\mu_\theta(u\mid x)p(y\mid x,u), and the pairs {Xk,Uk}\{X_k,U_k\} a chain with matrix PθP_\theta. When these chains are irreducible and aperiodic, πθ\pi_\theta denotes the stationary law of {Xk}\{X_k\}, ηθ(x,u)=πθ(x)μθ(u∣x)\eta_\theta(x,u)=\pi_\theta(x)\mu_\theta(u\mid x), and the average cost is

αˉ(θ)=∑x,uc(x,u) ηθ(x,u).\bar\alpha(\theta)=\sum_{x,u}c(x,u)\,\eta_\theta(x,u).

The score is ψθ(x,u)=∇ln⁡μθ(u∣x)∈Rn\psi_\theta(x,u)=\nabla\ln\mu_\theta(u\mid x)\in\mathbb R^n, and ⟨f,g⟩θ=∑x,uηθ(x,u)f(x,u)g(x,u)\langle f,g\rangle_\theta=\sum_{x,u}\eta_\theta(x,u)f(x,u)g(x,u).

The critic approximates Q-values by r′ϕθ(x,u)r'\phi_\theta(x,u) with features ϕθ(x,u)∈Rm\phi_\theta(x,u)\in\mathbb R^m whose span contains the components of ψθ\psi_\theta. Along one simulated trajectory (X^k,U^k)(\hat X_k,\hat U_k), where U^k+1\hat U_{k+1} is drawn from μθk(⋅∣X^k+1)\mu_{\theta_k}(\cdot\mid\hat X_{k+1}), the algorithm updates an average-cost estimate αk\alpha_k, the critic parameter rkr_k and an eligibility trace Z^k\hat Z_k at step size γk\gamma_k (equation (3.1)), and the actor parameter by

θk+1=θk−βkΓ(rk) rk′ϕθk(X^k+1,U^k+1) ψθk(X^k+1,U^k+1)(3.2)\theta_{k+1}=\theta_k-\beta_k\Gamma(r_k)\,r_k'\phi_{\theta_k}(\hat X_{k+1},\hat U_{k+1})\,\psi_{\theta_k}(\hat X_{k+1},\hat U_{k+1})\qquad(3.2)

at a slower step size βk\beta_k. The TD(1) critic resets its trace when the state x∗x^* is entered; the TD(λ\lambda) critic discounts it by λ∈(0,1)\lambda\in(0,1).

Formalization targets

Goal: Theorem 3.4

Under Assumptions 2.1 (positive, smooth policies; irreducible aperiodic chains; uniform reachability of x∗x^*), 3.1–3.2 (bounded smooth features spanning the scores, uniformly nondegenerate) and 3.3 (two-time-scale step sizes and the scaling Γ\Gamma),

(a) TD(1):  lim inf⁡k∣∇αˉ(θk)∣=0  w.p.1;(b) ∀ϵ>0 ∃λˉ<1 ∀λ∈[λˉ,1): lim inf⁡k∣∇αˉ(θk)∣<ϵ  w.p.1.\text{(a) TD(1): }\ \liminf_k|\nabla\bar\alpha(\theta_k)|=0\ \text{ w.p.1};\qquad \text{(b) }\forall\epsilon>0\ \exists\bar\lambda<1\ \forall\lambda\in[\bar\lambda,1):\ \liminf_k|\nabla\bar\alpha(\theta_k)|<\epsilon\ \text{ w.p.1}.

The statement leaves the initial parameters and the initial state–action law arbitrary.

Milestones

In attack order: the gradient formula ∇αˉ(θ)=⟨ψθ,Qθ⟩θ\nabla\bar\alpha(\theta)=\langle\psi_\theta,Q_\theta\rangle_\theta for every Poisson solution, with bounded Hessian (Theorem 4.6); boundedness of the regenerative quantities (Lemma 5.1) and of the trace moments (Lemma 5.2); uniform positive definiteness of the critic's mean matrix Gˉ(θ)\bar G(\theta) for TD(1) and TD(λ\lambda) (Lemmas 5.3, 5.6); critic tracking, ∣Gˉ(θk)Rk−hˉ(θk)∣→0|\bar G(\theta_k)R_k-\bar h(\theta_k)|\to0 (Theorem 5.7); the bias of the actor direction, sup⁡θ∣f(θ)−∇αˉ(θ)∣≤C(1−λ)\sup_\theta|f(\theta)-\nabla\bar\alpha(\theta)|\le C(1-\lambda) (Lemma 6.1); the descent inequality (6.1); and the convergence of the noise terms (Lemma 6.2).

Significance

The theorem says that a policy-gradient method whose gradient is estimated by a linearly parameterized TD critic, rather than by Monte Carlo returns, still converges to a stationary point of the average cost (exactly for TD(1), approximately for TD(λ\lambda)). It justifies the compatible features principle (the critic's features must span the score functions), the two-time-scale step-size design, and the trade-off in λ\lambda between variance and bias of the actor direction. The intermediate results are of independent use: Theorem 4.6 is the average-cost policy-gradient theorem for arbitrary Poisson solutions, and Theorem 5.7 is a tracking result for linear stochastic approximation driven by a Markov chain whose kernel changes slowly.

The result is proved in the paper, but the proofs of Theorem 4.6, of parts of the verification of the stochastic-approximation hypotheses and of Theorem 6.3 are given as outlines, with details deferred to a separate appendix and to Theorem A.7, recalled from another paper. No machine-checked proof of the theorem, or of the convergence of any actor–critic method, is known. The mission asks for a formal proof of the finite-case theorem and its milestones, which fills in the outlined steps. The finite-case gradient formula of §2 (Theorem 2.2, recalled from Marbach and Tsitsiklis) is posed, unproved, elsewhere on the platform in a reward-MDP form; it is a special case of milestone Theorem 4.6.

Difficulty

The obvious argument treats the actor as a stochastic gradient method with a noisy gradient estimate. It fails at the first step: the critic's estimate rk′ϕθkr_k'\phi_{\theta_k} is biased at every finite time, and the bias does not vanish unless the critic converges, while the critic's target rˉ(θk)\bar r(\theta_k) moves with the actor. The noise is Markovian, generated by a chain whose transition kernel depends on the current parameter, not a martingale difference sequence. Making the two time scales interact correctly requires a Poisson-equation decomposition of the Markov noise that is uniform in θ\theta, together with moment bounds for the eligibility trace, which for TD(1) is an unbounded sum over a regeneration cycle. Uniformity in θ\theta is essential, because the actor iterates θk\theta_k are not assumed to stay in a bounded set.

Formalization scope

State and action sets are finite types; parameters live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), so ∣⋅∣|\cdot| is the Euclidean norm and Mathlib's gradient is ∇\nabla. The transition probability p(y∣x,u)p(y\mid x,u) is stored as p x u y. πθ\pi_\theta is a stationary probability vector of P(θ)P(\theta), unique under Assumption 2.1(c). The law of the simulated path is built on (X×U)N(\mathbb X\times\mathbb U)^{\mathbb N} by the Ionescu-Tulcea construction (Kernel.trajMeasure), with the next action drawn under the actor parameter that the recursion computes from the history; nothing about the critic or the actor's behaviour is assumed.

Readings and corrections, each also recorded in the affected items:

  • Assumption 3.3(b) is corrected. The printed ∣r∣Γ(r)∈[C1,C2]|r|\Gamma(r)\in[C_1,C_2] for all rr is unsatisfiable at r=0r=0 and would make the theorem vacuous; it is formalized as (1+∣r∣)Γ(r)∈[C1,C2](1+|r|)\Gamma(r)\in[C_1,C_2], which Γ(r)=1/(1+∣r∣)\Gamma(r)=1/(1+|r|) satisfies. The second inequality of (3.3) is quantified over Rm\mathbb R^m, the domain of Γ\Gamma, not the printed Rn\mathbb R^n.
  • Assumption 4.9 (the features have zero mean under μθ(⋅∣x∗)\mu_\theta(\cdot\mid x^*)) is added to part (a), and to the TD(1) cases of Theorem 5.7 and Lemma 6.2: the TD(1) analysis uses it and Theorem 6.3 assumes it, though Theorem 3.4 does not list it.
  • "λ\lambda sufficiently close to 1" means: some λˉ<1\bar\lambda<1 such that all λ∈[λˉ,1)\lambda\in[\bar\lambda,1) work.
  • The α\alpha-update of (3.1) uses c(X^k+1,U^k+1)c(\hat X_{k+1},\hat U_{k+1}) as printed.
  • In (6.1), Γ(rˉ(θ))\Gamma(\bar r(\theta)) is read as Γ(rˉ(θk))\Gamma(\bar r(\theta_k)).
  • The matrix ⟨Pθk+1ϕθ,ϕθ′⟩θ\langle P_\theta^{k+1}\phi_\theta,\phi_\theta'\rangle_\theta in the TD(λ\lambda) Gˉ1\bar G_1 is oriented so that Gˉ1\bar G_1 is the steady-state mean of the critic's update matrix.
  • Results stated in the paper for Polish spaces (Theorems 4.6, 5.7) are stated under the finite assumptions that the paper says imply them; "w.p.1" in Theorem 5.7 is made explicit.

The lim inf⁡\liminf is taken in [0,∞][0,\infty], so a sequence with ∣∇αˉ(θk)∣→∞|\nabla\bar\alpha(\theta_k)|\to\infty cannot satisfy the conclusion through a junk value, and differentiability of αˉ\bar\alpha is part of the conclusion, so the statement cannot hold because Lean's gradient returns 00 at non-differentiable points. Series (tsum) and matrix inverses in the milestone objects converge, respectively are invertible, under the assumptions. The hypotheses are satisfiable: Γ(r)=1/(1+∣r∣)\Gamma(r)=1/(1+|r|), βk=(k+1)−1\beta_k=(k+1)^{-1}, γk=(k+1)−2/3\gamma_k=(k+1)^{-2/3} and the features ϕθ=ψθ\phi_\theta=\psi_\theta (which satisfy Assumption 4.9 at every state) meet the parts that could be in doubt.

A complete development needs finite Markov-chain theory uniform in a parameter (existence, uniqueness and smooth dependence of stationary laws; geometric ergodicity; Poisson equations; regeneration), differentiation of θ↦πθ\theta\mapsto\pi_\theta, almost-sure convergence of linear stochastic approximation with Markov noise, and martingale convergence. The Markov-chain and stochastic-approximation parts are reusable well beyond this mission. Contributions of proofs of any milestone, of auxiliary lemmas on parameterized finite Markov chains, and of the general two-time-scale tracking theorem (the paper's Theorem A.7) are welcome.

Selected references

14 thms1 active userReviewed
Algorithmic Game TheoryProbability·Captain: mikedeng1

The Evolution of Conventions III: In 2 × 2 Games with Two Strict Equilibria, the Generically Stable Equilibria of Adaptive Play Are the Weakly Risk Dominant OnesResearch Paper

Motivation

Many games have several strict Nash equilibria, and equilibrium analysis alone does not say which one a population will settle on. Harsanyi and Selten (1988) proposed risk dominance as a selection criterion for 2×22\times2 games: of two strict equilibria, select the one whose basin is "larger" in a precise payoff sense. That criterion is axiomatic. H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) derives a selection from a dynamic model instead: boundedly rational players with finite memory, incomplete information about the past and occasional mistakes. Its Theorem 3 says that, in 2×22\times2 games, the dynamic selection and risk dominance coincide.

Timeline.

  • 1984. Freidlin and Wentzell develop the theory of small random perturbations of dynamical systems, including the tree characterization of limiting stationary measures.
  • 1990. Foster and Young introduce stochastic stability for evolutionary processes with vanishing noise.
  • 1993. Kandori, Mailath and Rob prove that in symmetric 2×22\times2 games with a single population, the long-run equilibrium of a mutation process is the risk dominant one. Young (1993) proves the same selection for adaptive play, a two-population model with sampling from a finite memory, for every 2×22\times2 game with two strict equilibria, not only symmetric ones. Its Example 3 shows that in 3×33\times3 games the selected equilibrium can differ from both the risk dominant and the Pareto optimal one.

Setting

A finite game Γ\Gamma has players ii with finite strategy sets SiS_i and payoffs ui(s)u_i(s). Fix a memory mm and a sample size kk with 1≤k≤m1\le k\le m. A state is the sequence hh of the last mm plays (strategy-tuples), oldest first; a successor of hh drops the oldest play and appends a new one. In each period each player draws a sample of kk of the mm recorded plays and chooses a best reply to it (maximizing total payoff against the sampled plays). The choice probabilities pi(s∣h)p_i(s\mid h) form a best-reply distribution: pi(s∣h)>0p_i(s\mid h)>0 exactly when ss is a best reply to some sample of size kk. This gives adaptive play P0P^0, display (1).

With mistakes, each player ii independently experiments with probability ελi\varepsilon\lambda_i and then plays ss with probability qi(s∣h)>0q_i(s\mid h)>0. This gives the perturbed chain PεP^\varepsilon of display (2). It has a unique stationary distribution με\mu^\varepsilon. A state hh is stochastically stable if lim⁡ε→0μhε>0\lim_{\varepsilon\to0}\mu^\varepsilon_h>0. A convention is mm repetitions of a strict pure Nash equilibrium. With LΓL_\Gamma the longest shortest best-reply path to a strict equilibrium, a strict equilibrium is generically stable if its convention is stochastically stable for all sufficiently large kk and all mm with k≤m/(LΓ+2)k\le m/(L_\Gamma+2).

For a 2×22\times2 game in normal form, with Row's payoffs arca_{rc} and Column's brcb_{rc} satisfying a11>a21a_{11}>a_{21}, b11>b12b_{11}>b_{12}, a22>a12a_{22}>a_{12}, b22>b21b_{22}>b_{21}, set

R1=min⁡{a11−a21a11−a12−a21+a22,b11−b12b11−b12−b21+b22},R2=min⁡{a22−a12a11−a12−a21+a22,b22−b21b11−b12−b21+b22}.R_1=\min\Big\{\tfrac{a_{11}-a_{21}}{a_{11}-a_{12}-a_{21}+a_{22}},\tfrac{b_{11}-b_{12}}{b_{11}-b_{12}-b_{21}+b_{22}}\Big\},\qquad R_2=\min\Big\{\tfrac{a_{22}-a_{12}}{a_{11}-a_{12}-a_{21}+a_{22}},\tfrac{b_{22}-b_{21}}{b_{11}-b_{12}-b_{21}+b_{22}}\Big\}.

(1,1)(1,1) weakly risk dominates (2,2)(2,2) if R1≥R2R_1\ge R_2.

Formalization targets

Goal: Theorem 3 (p. 72)

(1,1) generically stable  ⟺  R1≥R2,(2,2) generically stable  ⟺  R2≥R1.(1,1)\text{ generically stable}\iff R_1\ge R_2,\qquad (2,2)\text{ generically stable}\iff R_2\ge R_1.

This holds for every 2×22\times2 game in normal form, for every best-reply distribution and every admissible experimentation.

Milestones, in the order the proof uses them

  1. PεP^\varepsilon is irreducible and aperiodic and has a unique stationary distribution (§6, pp. 67–68).
  2. (2) is a regular perturbation of (1): Pε→P0P^\varepsilon\to P^0, and Phh′εP^\varepsilon_{hh'} is of exact order εr(h,h′)\varepsilon^{r(h,h')}, with r(h,h′)r(h,h') the number of mistakes (Appendix, p. 77).
  3. Theorem 2 (p. 69): the stochastically stable states are those in the recurrent classes of P0P^0 of minimum stochastic potential, independently of λ\lambda and qq.
  4. Corollary (p. 70): for weakly acyclic games with k≤m/(LΓ+2)k\le m/(L_\Gamma+2), the stable states are the conventions of minimum stochastic potential.
  5. The 2×22\times2 case is acyclic with LΓ=1L_\Gamma=1, and for k≤m/3k\le m/3 the recurrent classes of P0P^0 are {h1}\{h_1\} and {h2}\{h_2\} (p. 70).
  6. r12=⌈R1k⌉r_{12}=\lceil R_1k\rceil and 7. r21=⌈R2k⌉r_{21}=\lceil R_2k\rceil (pp. 71–72).
  7. If R1>R2R_1>R_2, then h1h_1 is the unique stable convention, and if R1=R2R_1=R_2, both are, for all large kk and m≥3km\ge3k (p. 72).

Significance

Theorem 3 gives a dynamic foundation for risk dominance: an equilibrium selection criterion defined from payoffs alone is the long-run outcome of a decentralized learning process with sampling and rare mistakes. It requires no symmetry between the two player roles. Theorem 2 makes stochastic stability computable: a limit of stationary distributions is reduced to a minimum-weight arborescence over recurrent classes. That reduction is what the 2×22\times2 computation, and later applications of the method to bargaining and contracting, rely on. The equivalence of the RR-form with the product form (a11−a21)(b11−b12)≥(a22−a12)(b22−b21)(a_{11}-a_{21})(b_{11}-b_{12})\ge(a_{22}-a_{12})(b_{22}-b_{21}) of Harsanyi and Selten is elementary algebra and is not a target here.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The mission produces formal statements of the model (adaptive play, its perturbation, stochastic stability, resistance and stochastic potential) that are reusable for other stochastic-stability results. Closing the goal also requires formalizing Young's finite version of the Freidlin–Wentzell theorem, the subject of the companion mission The Evolution of Conventions II.

Difficulty

The paper's argument has two hard parts. The first is Theorem 2: identifying the limit of με\mu^\varepsilon requires the Markov chain tree theorem (the stationary distribution of an irreducible chain as a ratio of sums over spanning in-trees) together with an order-of-magnitude analysis in ε\varepsilon. The second is the exact resistance ⌈R1k⌉\lceil R_1k\rceil. The page constructs a path with that many mistakes (Table 1), but the matching lower bound, that no combination of mistakes by both players does better, is only asserted. It needs an argument about the first period in which some player's best reply switches. A naive count of single-player mistake runs gives only the upper bound. The tie case of (5) also matters: equality makes strategy 2 a best reply, which is why the ceiling and not the floor appears.

Formalization scope

Players are a finite type and strategies finite types. A state is Fin m → (∀ i, S i) with position 0 the oldest play. A sample is a set of kk positions, and a best reply maximizes the summed payoff against the sampled plays. Transition matrices are Matrix H H ℝ. Stochastic stability is a one-sided limit ε→0+\varepsilon\to0^+ of the stationary distributions of PεP^\varepsilon, over the admissible range 0<ε0<\varepsilon, ελi≤1\varepsilon\lambda_i\le1. Resistances are natural numbers on successor pairs. Recurrent classes are the essential classes of P0P^0, and ii-trees are parent maps on the set of classes that reach the root. "k≤m/(LΓ+2)k\le m/(L_\Gamma+2)" is the natural-number inequality k(LΓ+2)≤mk(L_\Gamma+2)\le m. In the 2×22\times2 game, players and strategies are Fin 2, with the paper's 1,21,2 written as 0, 1.

Two corrected slips are recorded in the statements. On p. 68 the recurrent classes are "of PεP^\varepsilon" for P0P^0, and on p. 77 "the process PεP^\varepsilon defined in (1)" is P0P^0.

Trivializing formalizations are ruled out. Stochastic stability is defined from stationary distributions, not from resistances, and generic stability is defined from stochastic stability, not from ⌈R1k⌉\lceil R_1k\rceil versus ⌈R2k⌉\lceil R_2k\rceil. Both definitions quantify over every best-reply distribution and every admissible (λ,q)(\lambda,q) rather than a fixed sampling law. "Sufficiently large kk" is an eventual statement with a threshold, not "for some kk".

A complete development needs Markov chain stationary distributions on finite spaces, the Markov chain tree theorem, limits of rational functions of ε\varepsilon, and the combinatorics of sampling in 2×22\times2 games. The perturbation theory (milestones 1–3) is reusable for any finite stochastic-stability model. Contributions to the tree theorem and to the two resistance computations are particularly welcome.

Related platform work: stochastic fictitious play (StochFictPlay.*, Hofbauer–Sandholm) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra) study other learning dynamics in games. The sibling missions The Evolution of Conventions I (Theorem 1, convergence of adaptive play) and II (Theorem 4, regular perturbations of Markov chains) formalize the results this mission's milestones invoke.

Selected references

45 thms1 active userReviewed
Dynamic ProgrammingOperations Research·Captain: mikedeng1

Discrete Dynamic Programming with Sensitive Discount Optimality Criteria 2: No Improvement of Order n+1 Implies n-Discount Optimality, Which Rules Out Improvement of Order nResearch Paper

Motivation

A finite Markov decision process is usually solved under one of two criteria: the expected total discounted reward, for a fixed interest rate, or the long-run average reward. Neither is satisfactory when the interest rate is small and not known precisely. Blackwell (Blackwell 1962) showed that some stationary policy is optimal for every discount factor close enough to one, and that the average-reward criterion cannot tell apart policies with the same gain but very different transient rewards. Veinott's 1969 paper interpolates between these two: it introduces a hierarchy of nn-discount optimality criteria, indexed by n=−1,0,1,…n=-1,0,1,\dots, each more selective than the previous, and characterizes the stationary policies that meet each level through the Laurent expansion of the discounted return in the interest rate.

Timeline. Blackwell (1962) introduced the expansion of the discounted return near β=1\beta=1 to first order and the criteria now called −1+-1^+ and ∞+\infty^+ discount optimality. Veinott (1966) gave a policy improvement method for the bias (0+0^+) criterion. Miller and Veinott (1969) gave the full Laurent expansion and a policy improvement algorithm for Blackwell optimality in the stochastic case. The present paper (1969) extends this to substochastic transition matrices and to negative interest rates in the transient case, defines the n±n^\pm criteria, and proves Theorem 4, the subject of this mission.

Setting

There are finitely many states ss (the paper's 1,…,S1,\dots,S); in each state a finite nonempty action set AsA_s. Action aa in state ss earns r(s,a)∈Rr(s,a)\in\mathbb R and leads to state tt with weight p(t∣s,a)≥0p(t\mid s,a)\ge0, where ∑tp(t∣s,a)≤1\sum_t p(t\mid s,a)\le1 (the remaining mass is the probability of stopping). A decision rule f∈F=×sAsf\in F=\times_s A_s picks one action per state; r(f)r(f) and P(f)P(f) are its reward vector and substochastic transition matrix, Q(f)=P(f)−IQ(f)=P(f)-I. A policy is a sequence π=(f1,f2,… )\pi=(f_1,f_2,\dots) of decision rules, f∞=(f,f,… )f^\infty=(f,f,\dots) is a stationary policy, and PN(π)=P(f1)⋯P(fN)P^N(\pi)=P(f_1)\cdots P(f_N).

For an interest rate ρ>−1\rho>-1 and β=(1+ρ)−1\beta=(1+\rho)^{-1}, the discounted return is

Vρ(π)=∑N=1∞βNPN−1(π) r(fN).V_\rho(\pi)=\sum_{N=1}^{\infty}\beta^N P^{N-1}(\pi)\,r(f_N).

For a substochastic PP, P∗P^* is the Cesàro limit of its powers and H=(I−P+P∗)−1−P∗H=(I-P+P^*)^{-1}-P^* its deviation matrix.

A policy π∗\pi^* is n±n^\pm discount optimal if, componentwise,

lim inf⁡ρ→0±∣ρ∣−n [Vρ(π∗)−Vρ(π)]≥0for all policies π.\liminf_{\rho\to0\pm}|\rho|^{-n}\,[V_\rho(\pi^*)-V_\rho(\pi)]\ge0\quad\text{for all policies }\pi .

Dn±D_n^\pm is the set of ff with f∞f^\infty n±n^\pm discount optimal, and D−2=FD_{-2}=F. The sign −- (interest rate approaching zero from below) is considered only in the transient case, where ∑NP(f)N\sum_N P(f)^N converges for every ff.

The Laurent coefficients of Vρ(f∞)V_\rho(f^\infty) are y−1±(f)=±P∗(f)r(f)y_{-1}^\pm(f)=\pm P^*(f)r(f) and yn±(f)=(∓1)nH(f)n+1r(f)y_n^\pm(f)=(\mp1)^nH(f)^{n+1}r(f), n≥0n\ge0; with y−2±=0y_{-2}^\pm=0 and r0=rr_0=r, rn=0r_n=0 otherwise, the test quantities are

ψn±(g,f)=rn(g)+Q(g) yn±(f)∓yn−1±(f),n≥−1.\psi_n^\pm(g,f)=r_n(g)+Q(g)\,y_n^\pm(f)\mp y_{n-1}^\pm(f),\qquad n\ge-1 .

Ψn±(g,f)\Psi_n^\pm(g,f) is the matrix with columns ψ−1±,…,ψn±\psi_{-1}^\pm,\dots,\psi_n^\pm, and Gn±(f)={g∈F:Ψn±(g,f)≻0}G_n^\pm(f)=\{g\in F:\Psi_n^\pm(g,f)\succ0\}, where C≻0C\succ0 means that the first nonzero entry of every row of CC is positive and C≠0C\ne0.

Formalization targets

Goal: Theorem 4

For f∈Ff\in F and n=−2,−1,…,S−1n=-2,-1,\dots,S-1:

Gn+1±(f)=∅ ⟹ f∈Dn±,f∈Dn± ⟹ Gn±(f)=∅.G_{n+1}^\pm(f)=\varnothing\ \Longrightarrow\ f\in D_n^\pm,\qquad f\in D_n^\pm\ \Longrightarrow\ G_n^\pm(f)=\varnothing .

The two halves bracket Dn±D_n^\pm between two finitely checkable conditions.

Milestones

In the order the proof uses them: the Cesàro limit and (15); Lemma 5 (the reduced resolvent); Theorem 2 (the Laurent expansion Rρ(Q)=ρ−1P∗+∑n≥0(−ρ)nHn+1R_\rho(Q)=\rho^{-1}P^*+\sum_{n\ge0}(-\rho)^nH^{n+1}); Lemma 7 (P∗+ρHP^*+\rho H nonnegative, positive diagonal, nonsingular for small ρ>0\rho>0); Theorem 3 (the expansion of Vρ(f∞)V_\rho(f^\infty)); (30)–(31) (the comparison identity); Lemma 8 (the expansion of the test quantity); Lemma 9 (the coefficient identity); the nonemptiness of D∞±D_\infty^\pm; the characterization Dn±={f:Yn±(f)⪰Yn±(g) ∀g}D_n^\pm=\{f: Y_n^\pm(f)\succeq Y_n^\pm(g)\ \forall g\}; Theorem 5 (lexicographic improvement).

Significance

Theorem 4 turns a criterion stated through limits over all, possibly non-stationary, policies into a finite test on one-step switches. It is what lets the policy improvement method of Miller and Veinott stop early when only an n±n^\pm discount optimal policy is sought, rather than an S±S^\pm (Blackwell) optimal one, and it recovers Blackwell's algorithm for −1+-1^+ and Veinott's 1966 algorithm for 0+0^+ as the cases n=−1,0n=-1,0. The nn-discount hierarchy is the standard framework for sensitive optimality in Markov decision processes and underlies the average-overtaking and bias criteria used in later work.

The results are proved in the paper (Theorem 3 and Lemma 8 by reference to Miller–Veinott). None of them is formalized: the platform has the Cesàro limit matrix and the deviation matrix as definitions (from Blackwell 1962), and an open statement of their basic properties for stochastic matrices only. This mission adds the substochastic matrix theory of §3, the Laurent expansion of discounted returns with Veinott's normalization, and the lexicographic characterization of n±n^\pm discount optimality.

Difficulty

The definition of Dn±D_n^\pm compares f∞f^\infty with every policy, and the comparison is a liminf of a scaled difference of infinite series. The obvious route, comparing Laurent coefficients, applies only to stationary policies, whose returns have Laurent expansions; reducing the comparison with arbitrary policies to stationary ones requires the existence of an ∞±\infty^\pm discount optimal stationary policy, which is a separate existence theorem. The second difficulty is that P∗P^* may be singular or zero and the chain may have several recurrent classes: Lemma 7 is what replaces an analysis of the chain structure in the inductive step of the proof.

Formalization scope

Lean 4 with Mathlib, namespace VeinottSensitiveDP.Sensitive. States form a nonempty Fintype; each state has its own finite nonempty action type A s; policies are sequences ℕ → F with π 0 the paper's f1f_1. All quantities are real. P∗P^* and HH are the published limitMatrix and deviationMatrix; their properties for substochastic matrices are milestones, not assumptions. VρV_\rho is a tsum with Veinott's extra factor β\beta; every theorem about it carries the hypotheses under which the series converges. The spectral radius is that of the complexified matrix. The sign ±\pm is a real parameter σ∈{1,−1}\sigma\in\{1,-1\}, and statements for σ=−1\sigma=-1 assume the transient case. The liminf in (27) is encoded as "for every ε>0\varepsilon>0, eventually ≥−ε\ge-\varepsilon", which is the extended-real liminf. Matrices with columns −1,…,n-1,\dots,n are functions of an integer column index read on [−1,n][-1,n].

A trivializing formalization would define Dn±D_n^\pm by comparison with stationary policies only, or directly as the lexicographic maximizers of Yn±Y_n^\pm; here Dn±D_n^\pm is defined by (27) against all policies, and the lexicographic characterization is a milestone.

Contributions welcome: proofs of the matrix results of §3 (reusable for any work on deviation matrices and Laurent expansions of Markov chains), of the Laurent expansions, and of the existence of ∞±\infty^\pm discount optimal stationary policies.

Selected references

17 thms1 active userReviewed
Dynamic ProgrammingOperations Research·Captain: mikedeng1

On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting 2: f Maximizes Gain and Then Bias Exactly When Its Averaged Finite-Horizon Returns Dominate Every Stationary Policy'sResearch Paper

Motivation

A Markov decision process with finitely many states and actions is usually run either with a discount factor β<1\beta<1 or under the long-run average criterion. Without discounting, the total return over an infinite horizon is typically infinite, and the average return per period ignores everything that happens in any finite stretch of time: two policies with equal gain (average return per period) can differ by a fixed amount of income forever, and the average criterion cannot tell them apart. Finer, undiscounted criteria that break such ties are a standard topic of the MDP literature (Puterman, Markov Decision Processes, Ch. 10), and the paper of this mission is one of their starting points.

Timeline. Howard (1960) introduced policy iteration for the average-return problem. Blackwell (1962) expanded the discounted return of a stationary policy near β=1\beta=1 as x(f)/(1−β)+y(f)+o(1)x(f)/(1-\beta)+y(f)+o(1), defined 1-optimal ("nearly optimal") policies, and showed that the stationary 1-optimal policies are exactly those that maximize the gain x(f)x(f) and then the bias y(f)y(f). Veinott (1966), the source of this mission, gave a finite algorithm for such policies and, in §5, a characterization of the same set by an undiscounted criterion: comparing the Cesàro averages of the finite-horizon total returns. Later work (Veinott 1969) developed the hierarchy of nn-discount optimality criteria from this starting point.

Setting

There are finitely many states ss and a finite set of actions; in state ss, action aa earns the income i(s,a)i(s,a) and moves the system to state s′s' with probability q(s′∣s,a)q(s'\mid s,a). A decision rule f∈Ff\in F chooses an action f(s)f(s) in each state; r(f)r(f) is the vector with entries i(s,f(s))i(s,f(s)), and Q(f)Q(f) is the Markov matrix with entries q(s′∣s,f(s))q(s'\mid s,f(s)). A policy is a sequence π=(f1,f2,… )\pi=(f_1,f_2,\dots) of decision rules, Qn(π)=Q(f1)⋯Q(fn)Q_n(\pi)=Q(f_1)\cdots Q(f_n) with Q0(π)=IQ_0(\pi)=I, and f∞=(f,f,… )f^\infty=(f,f,\dots) is the stationary policy that uses ff every period.

The limit matrix Q∗(f)=lim⁡N→∞N−1∑i=0N−1Q(f)iQ^*(f)=\lim_{N\to\infty}N^{-1}\sum_{i=0}^{N-1}Q(f)^i exists for every Markov matrix. The gain and bias of ff are

x(f)=Q∗(f) r(f),y(f)=H(f) r(f),H(f)=(I−Q(f)+Q∗(f))−1−Q∗(f).x(f)=Q^*(f)\,r(f),\qquad y(f)=H(f)\,r(f),\qquad H(f)=\bigl(I-Q(f)+Q^*(f)\bigr)^{-1}-Q^*(f).

Vectors are compared coordinatewise. The decision rules of maximal gain form

F′={f∈F:x(f)≥x(g) for all g∈F},F'=\{f\in F: x(f)\ge x(g)\text{ for all }g\in F\},

and those of maximal bias among them form

F′′={f∈F′:y(f)≥y(g) for all g∈F′}.F''=\{f\in F': y(f)\ge y(g)\text{ for all }g\in F'\}.

Finally, the nn-period total expected return of a policy π\pi, starting from each state, is

Vn(π)=∑i=0n−1Qi(π) r(fi+1).V^n(\pi)=\sum_{i=0}^{n-1}Q_i(\pi)\,r(f_{i+1}).

Formalization targets

Goal: Theorem 7

For every f∈Ff\in F,

f∈F′′  ⟺  lim⁡N→∞1N∑n=1N[Vn(f∞)−Vn(g∞)] ≥ 0for all g∈F,f\in F''\iff \lim_{N\to\infty}\frac1N\sum_{n=1}^{N}\bigl[V^n(f^\infty)-V^n(g^\infty)\bigr]\ \ge\ 0\quad\text{for all }g\in F,

where the inequality is coordinatewise and the limit is taken in [−∞,+∞][-\infty,+\infty].

Milestones

  1. Theorem 3 (Blackwell): Vβ(f∞)=x(f)/(1−β)+y(f)+ε(β,f)V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+\varepsilon(\beta,f) with ε(β,f)→0\varepsilon(\beta,f)\to0 as β→1−\beta\to1^-, where x(f)x(f) and y(f)y(f) are the unique solutions of [I−Q(f)]x=0, Q∗(f)x=Q∗(f)r(f)[I-Q(f)]x=0,\ Q^*(f)x=Q^*(f)r(f) and [I−Q(f)]y=r(f)−x(f), Q∗(f)y=0[I-Q(f)]y=r(f)-x(f),\ Q^*(f)y=0.
  2. The nn-step identity (p. 1293): y(f)=Vn(f∞)−n x(f)+Q(f)ny(f)y(f)=V^n(f^\infty)-n\,x(f)+Q(f)^n y(f) for every nn.
  3. (27): y(f)=lim⁡N→∞N−1∑n=1N[Vn(f∞)−n x(f)]y(f)=\lim_{N\to\infty}N^{-1}\sum_{n=1}^N[V^n(f^\infty)-n\,x(f)].
  4. (28): N−1∑n=1NVn(f∞)=N+12x(f)+y(f)+σ(N,f)N^{-1}\sum_{n=1}^N V^n(f^\infty)=\tfrac{N+1}{2}x(f)+y(f)+\sigma(N,f) with σ(N,f)→0\sigma(N,f)\to0.
  5. Theorem 4 (Blackwell): F′′F'' is nonempty and is exactly the set of ff for which f∞f^\infty is 1-optimal.

Significance

The result. Theorem 7 gives the set F′′F'', defined through the discount-factor expansion, an interpretation that involves no discounting at all: f∞f^\infty maximizes gain and then bias exactly when, from every starting state, its Cesàro-averaged finite-horizon returns are in the limit at least those of every other stationary policy. Combined with Theorem 4 it identifies the stationary 1-optimal policies with the stationary policies that are optimal under this average-overtaking comparison. The paper records a consequence (an optimal policy in the average-overtaking sense (26) that is stationary is 1-optimal) and conjectures the converse; that remark and conjecture are not part of this mission.

Formalizing it. The results are proved in the paper (Theorems 3 and 4 are Blackwell's). None of them is formalized: the Blackwell expansion (Theorem 3) is an open item on Prove2Me, referenced here, and Theorem 4, the nn-step identity, (27), (28) and Theorem 7 have no machine-checked proof. A complete development gives the first formal treatment of Cesàro-averaged finite-horizon returns of a finite MDP and their relation to gain and bias.

Difficulty

The paper calls Theorem 7 "an immediate consequence of the representation (28)". For the direction "the limit condition implies f∈F′′f\in F''" this is accurate: a state where x(f)<x(g)x(f)<x(g) would drive the average to −∞-\infty, so f∈F′f\in F', and then the constant terms give the bias comparison over F′F'. The converse is where the obvious argument stops. It must hold for every g∈Fg\in F, including g∉F′g\notin F'; at a state where x(f)s=x(g)sx(f)_s=x(g)_s for such a gg, (28) needs y(f)s≥y(g)sy(f)_s\ge y(g)_s, and the definition of F′′F'' only compares biases with gain-maximal rules. That inequality comes from 1-optimality of f∞f^\infty (Theorem 4) together with the expansion of Theorem 3, not from (28). Proving (27) itself requires the Cesàro convergence N−1∑n<NQ(f)n→Q∗(f)N^{-1}\sum_{n<N}Q(f)^n\to Q^*(f) and the identity Q∗(f)y(f)=0Q^*(f)y(f)=0, which rest on Blackwell's Lemma 1 about Markov matrices.

Formalization scope

The development builds on the published Lean model of Blackwell (1962): Model (states St, actions Act, incomes, transition law), Policy (indexed from 00, so π 0 is f1f_1), Qn, V, IsNearlyOptimal (= 1-optimal), limitMatrix, and the closed forms x, y. Conventions:

  • State and action sets are finite and nonempty, and every action is available in every state (As=AA_s=A).
  • Vectors are real functions on states with the pointwise order; limits of vectors are coordinatewise; limits in NN are along the natural numbers. The Cesàro mean in limitMatrix uses N+1N+1 terms rather than Veinott's NN; the limit is the same.
  • x(f)x(f) and y(f)y(f) are their closed forms; Theorem 3 asserts they are the unique solutions of Veinott's (2) and (3).
  • 1-optimality is Blackwell's "nearly optimal", formulated without U(β)U(\beta), against all policies.
  • In Theorem 7 the limit is an extended-real limit, stated as: for every gg and every state, the real sequence converges in [−∞,+∞][-\infty,+\infty] to some L≥0L\ge0. A real-valued limit would make the statement false whenever x(f)s≠x(g)sx(f)_s\ne x(g)_s; the comparison class is the stationary policies g∞g^\infty only, and it must not be narrowed to g∈F′g\in F'.

The shared module defines F′F' and F′′F''; this chunk defines Vn(π)V^n(\pi). Contributions are welcome for any milestone, and in particular for reusable lemmas about Cesàro means of powers of a Markov matrix, which the proofs of (27) and (28) and Blackwell's Lemma 1 share.

Selected references

11 thms1 active userReviewed
Dynamic ProgrammingMachine LearningProbability+1·Captain: mikedeng1

An Analysis of Temporal-Difference Learning with Function Approximation 1: Linear TD(λ) Converges with Probability 1 to the Fixed Point of ΠT^(λ), with Error ≤ ‖ΠJ* − J*‖_D/(1 − α(1−λ)/(1−αλ))Research Paper

Motivation

Temporal-difference learning, TD(λ\lambda), is the basic algorithm of reinforcement learning for estimating the expected discounted cost of a Markov chain from observed transitions (Sutton, 1988). On large or infinite state spaces it is run with a linear function approximator: the cost-to-go is represented as a weighted sum of KK fixed basis functions, and the algorithm updates the weights. With a lookup table (one basis function per state) its convergence follows from general results on contraction mappings. With function approximation that argument breaks down. Before 1996 there were only results on convergence in the mean (Dayan, 1992), sketches restricted to linearly independent feature vectors ϕ(i)\phi(i), and counterexamples in which related algorithms diverge.

Tsitsiklis and Van Roy (MIT report LIDS-P-2322, 1996; IEEE Trans. Automatic Control 42(5), 1997) proved that on-line TD(λ\lambda) with linear function approximation converges with probability 1 on finite or countably infinite ergodic chains. They identified the limit as the fixed point of a projected Bellman-type operator ΠT(λ)\Pi T^{(\lambda)} and bounded its error. This analysis is the reference point for later results: finite-time bounds for linear TD, the off-policy divergence examples, and the gradient-TD family.

Timeline:

  • 1988: Sutton introduces TD(λ\lambda) and proves convergence in the mean for TD(0) on absorbing chains with linearly independent features.
  • 1992: Dayan extends convergence in the mean to general λ\lambda.
  • 1994: Jaakkola, Jordan and Singh, and Tsitsiklis, prove almost-sure convergence for lookup tables, using maximum-norm contraction.
  • 1996: Tsitsiklis and Van Roy prove almost-sure convergence with linear function approximation and the error bound below.

Setting

A Markov chain i0,i1,…i_0, i_1, \dots lives on a finite or countably infinite state space SS, with transition matrix P=(pij)P = (p_{ij}). A transition from ii to jj costs g(i,j)g(i,j), and α∈(0,1)\alpha \in (0,1) is a discount factor. The cost-to-go is

J∗(i)=E[∑t=0∞αtg(it,it+1) ∣ i0=i].J^*(i) = E\Big[\sum_{t=0}^\infty \alpha^t g(i_t,i_{t+1}) \,\Big|\, i_0 = i\Big].

Basis functions ϕ1,…,ϕK:S→R\phi_1,\dots,\phi_K : S \to \mathbb R give the feature vector ϕ(i)∈RK\phi(i) \in \mathbb R^K and the approximation J~(i,r)=r′ϕ(i)\tilde J(i,r) = r'\phi(i), written Φ′r\Phi' r as a vector over SS.

Starting from an arbitrary r0r_0, TD(λ\lambda) with λ∈[0,1]\lambda \in [0,1] and step sizes γt\gamma_t forms the eligibility vector zt=∑k=0t(αλ)t−kϕ(ik)z_t = \sum_{k=0}^t (\alpha\lambda)^{t-k}\phi(i_k) and the temporal difference dt=g(it,it+1)+αϕ(it+1)′rt−ϕ(it)′rtd_t = g(i_t,i_{t+1}) + \alpha\phi(i_{t+1})'r_t - \phi(i_t)'r_t, and updates rt+1=rt+γtdtztr_{t+1} = r_t + \gamma_t d_t z_t.

Let π\pi be the invariant distribution, D=diag(π)D = \mathrm{diag}(\pi), ∥J∥D2=∑iπ(i)J(i)2\|J\|_D^2 = \sum_i \pi(i)J(i)^2, and L2(S,D)={J:∥J∥D<∞}L_2(S,D) = \{J : \|J\|_D < \infty\}. Write Π=Φ′(ΦDΦ′)−1ΦD\Pi = \Phi'(\Phi D\Phi')^{-1}\Phi D for the DD-orthogonal projection onto {Φ′r}\{\Phi'r\}. The operator T(λ)T^{(\lambda)} averages mm-stage truncated costs:

(T(λ)J)(i)=(1−λ)∑m=0∞λmE[∑t=0mαtg(it,it+1)+αm+1J(im+1) ∣ i0=i],(T^{(\lambda)}J)(i) = (1-\lambda)\sum_{m=0}^\infty \lambda^m E\Big[\sum_{t=0}^m \alpha^t g(i_t,i_{t+1}) + \alpha^{m+1}J(i_{m+1}) \,\Big|\, i_0 = i\Big],

for λ<1\lambda < 1, and T(1)J=J∗T^{(1)}J = J^*. The paper makes four assumptions:

  1. the chain has a unique invariant distribution with π(i)>0\pi(i) > 0, E0[g2]<∞E_0[g^2] < \infty, and finite J∗J^*;
  2. the ϕk\phi_k are linearly independent with E0[ϕk2]<∞E_0[\phi_k^2] < \infty;
  3. polynomial moment growth and summable mixing conditions, relative to coordinates σ(i)∈RN\sigma(i) \in \mathbb R^N of the states;
  4. nonnegative, nonincreasing step sizes with ∑γt=∞\sum\gamma_t = \infty and ∑γt2<∞\sum\gamma_t^2 < \infty.

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumptions 1–4: J∗∈L2(S,D)J^* \in L_2(S,D); for every λ∈[0,1]\lambda \in [0,1], TD(λ\lambda) converges with probability 1, from every initial state and every r0r_0, to a vector r∗r^*; r∗r^* is the unique solution of

ΠT(λ)(Φ′r∗)=Φ′r∗;\Pi T^{(\lambda)}(\Phi' r^*) = \Phi' r^*;

and

∥Φ′r∗−J∗∥D≤∥ΠJ∗−J∗∥D1−α(1−λ)/(1−λα).\|\Phi' r^* - J^*\|_D \le \frac{\|\Pi J^* - J^*\|_D}{1 - \alpha(1-\lambda)/(1-\lambda\alpha)}.

Milestones

  • Lemma 1: ∥PJ∥D≤∥J∥D\|PJ\|_D \le \|J\|_D.
  • Lemma 2: J∗J^* is finite, lies in L2(S,D)L_2(S,D), and J∗=∑t(αP)tgˉJ^* = \sum_t(\alpha P)^t\bar g.
  • Lemma 3: T(λ)T^{(\lambda)} maps L2(S,D)L_2(S,D) into itself and has a closed-form series.
  • Lemma 4: T(λ)T^{(\lambda)} is a ∥⋅∥D\|\cdot\|_D-contraction with modulus α(1−λ)/(1−αλ)\alpha(1-\lambda)/(1-\alpha\lambda).
  • Lemma 5: ΠT(λ)\Pi T^{(\lambda)} has a unique fixed point Φ′r∗\Phi'r^*, with the error bound above.
  • Lemma 6: steady-state moments of ϕ\phi and ztz_t.
  • Lemma 7: the steady-state mean step is E0[s(r,Xt)]=ΦD(T(λ)(Φ′r)−Φ′r)E_0[s(r,X_t)] = \Phi D(T^{(\lambda)}(\Phi'r) - \Phi'r).
  • Lemma 8: (r−r∗)′E0[s(r,Xt)]<0(r - r^*)'E_0[s(r,X_t)] < 0 for r≠r∗r \neq r^*.
  • Theorem 2: a stochastic approximation theorem with Markov noise.
  • §6: A=E0[A(Xt)]A = E_0[A(X_t)] is negative definite and Ar∗+b=0Ar^* + b = 0.

Significance

Theorem 1 says that TD(λ\lambda), run on-line along a single trajectory, converges for every λ\lambda, and that its limit has a precise meaning: the fixed point of the projected operator. The error bound shows that as λ→1\lambda \to 1 the limit approaches the best approximation ΠJ∗\Pi J^*, and that for smaller λ\lambda the error can grow by at most a factor (1−αλ)/(1−α)(1-\alpha\lambda)/(1-\alpha). The analysis also explains the failures of related schemes: the projection and the contraction must use the same norm, ∥⋅∥D\|\cdot\|_D, which holds only when states are sampled along the chain.

The result is proved on paper. To our knowledge no part of it has been machine-checked; it is not in Mathlib or on this platform. This mission produces:

  • a Lean model of countable-state Markov chains with costs, their path law, the weighted space L2(S,D)L_2(S,D) and the projection Π\Pi, which is reusable for later work on linear TD, LSTD and approximate policy evaluation;
  • the deterministic layer (Lemmas 1–5, 7, 8), which is self-contained functional analysis on L2(S,D)L_2(S,D);
  • Theorem 2, a stochastic approximation theorem with Markov noise, which the paper quotes from Benveniste, Métivier and Priouret (1987) without proof. A formal proof of it would be a library result in its own right.

Difficulty

The obvious approach treats TD(λ\lambda) as a noisy version of the deterministic iteration rˉt+1=rˉt+γtΦD(T(λ)(Φ′rˉt)−Φ′rˉt)\bar r_{t+1} = \bar r_t + \gamma_t\Phi D(T^{(\lambda)}(\Phi'\bar r_t) - \Phi'\bar r_t). It fails at the noise. The increments s(rt,Xt)s(r_t,X_t) are driven by the Markov process Xt=(it,it+1,zt)X_t = (i_t,i_{t+1},z_t), not by independent samples. They are not martingale differences, and on an infinite state space they are unbounded. The standard ODE method with martingale-difference noise therefore does not apply, and the bias from Markov dependence must be controlled through the mixing and growth conditions of Assumption 3. The algorithm also starts with z−1=0z_{-1} = 0 rather than in steady state, so the steady-state identities of Lemmas 6–8 must be transferred to the actual trajectory. The contraction argument needs care for a different reason: Π\Pi is a nonexpansion of ∥⋅∥D\|\cdot\|_D only because DD is the invariant distribution of the same chain that defines T(λ)T^{(\lambda)}.

Formalization scope

SS is a countable type with the discrete σ\sigma-algebra, PP a Markov kernel (pij=P(i)({j})p_{ij} = P(i)(\{j\}), PmP^m the kernel power), and the path law of the chain is Mathlib's Ionescu–Tulcea measure Kernel.trajMeasure. Standing conventions:

  • α∈(0,1)\alpha \in (0,1) and λ∈[0,1]\lambda \in [0,1];
  • "with probability 1" is almost-sure convergence under the path law from each deterministic initial state;
  • J∗J^* and T(λ)T^{(\lambda)} are defined by the page's path expectations, not by the series of Lemmas 2 and 3;
  • L2(S,D)L_2(S,D) membership is summability of π(i)J(i)2\pi(i)J(i)^2;
  • Assumption 1(c) means absolute integrability of the discounted cost series;
  • vector norms are Euclidean and matrix norms Frobenius (equivalent to the induced norm and used only under existential constants);
  • (ΦDΦ′)−1(\Phi D\Phi')^{-1} is Lean's matrix inverse, invertible under Assumptions 1(a) and 2;
  • the steady-state process of Lemmas 6–8 is any two-sided chain on a probability space with the stationary finite-dimensional distributions.

Lean's integral of a non-integrable function and sum of a non-summable series are 00. A trivializing formalization is excluded by stating every expectation and series with its integrability or summability: "well defined and finite" is always a conjunct or a hypothesis, never left to junk values.

The development needs the following:

  • Markov-chain path measures and stationary two-sided chains;
  • Bochner integrals of vector-valued functions;
  • the Cauchy–Schwarz inequality on L2(S,D)L_2(S,D);
  • a Markov-noise stochastic approximation theorem.

Contributions are welcome at every level: proofs of the deterministic lemmas, a construction of the stationary chain from π\pi and PP (showing that the steady-state hypotheses are satisfiable), and a proof of Theorem 2 or a stronger stochastic approximation result that implies it.

Selected references

13 thms1 active userReviewed
Dynamic ProgrammingOperations ResearchOptimization·Captain: mikedeng1

Inventory Control in a Fluctuating Demand Environment II: With a Fixed Order Cost, a World-Dependent (r, S) Policy Is Optimal and Lies within Veinott-Type BoundsResearch Paper

Motivation

Demand for many products is not stationary: it rises and falls with the economy, the season, a product's life cycle or a customer's state. Song and Zipkin (1993) (DOI 10.1287/opre.41.2.351) model this by a world-driven demand process: an exogenous Markov chain AA (the "state of the world") whose current state sets the rate of a Poisson demand stream. The model contains the classical stationary inventory model as the case of one world state, and it is a standard example of a Markov-modulated decision problem in operations research.

For stationary demand with a fixed order cost, optimal (s,S)(s, S) policies go back to Scarf (1960) for finite horizons and Iglehart (1963) for the infinite horizon; Veinott (1966) bounded the optimal parameters by quantities computed from the one-period cost alone. This mission formalizes the extension of both results to the fluctuating-demand model (§3.2 of the paper). A companion mission treats the linear order-cost case, in which a world-dependent basestock policy is optimal.

Setting

The world AA is a continuous-time Markov chain on a countable set II with generator (qij)(q_{ij}), qi=−qii=∑j≠iqijq_i = -q_{ii} = \sum_{j\neq i} q_{ij}, and bounded rates. While A=iA = i, unit demands arrive at Poisson rate λi\lambda_i; shortages are backlogged. An order arrives after a random lead time LL, independent of the world and the demand. The inventory position x∈Zx \in \mathbb Z is on-hand stock minus backorders plus stock on order.

Costs: a fixed cost Kˉ\bar K per order and a unit cost cˉ\bar c, both paid on arrival; a holding cost rate h>0h > 0 and a penalty cost rate p>0p > 0; a discount rate α>0\alpha > 0. With F~L(α)=E[e−αL]\tilde F_L(\alpha) = E[e^{-\alpha L}], the discounted costs are c=cˉF~L(α)c = \bar c\tilde F_L(\alpha) and K=KˉF~L(α)K = \bar K\tilde F_L(\alpha). If DLiD^i_L is the demand during a lead time from world state ii and C^(x)=max⁡{−px,hx}\hat C(x) = \max\{-px, hx\},

C(i,y)=E[e−αLC^(y−DLi)].C(i, y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big].

Uniformization at a rate μ≥sup⁡iqi+sup⁡iλi\mu \ge \sup_i q_i + \sup_i\lambda_i turns the problem into a discrete-time dynamic program with β=1/(μ+α)\beta = 1/(\mu+\alpha), γ=βμ\gamma = \beta\mu and the myopic cost G+(i,y)=(1−γ)cy+βC(i,y)G^+(i, y) = (1-\gamma)cy + \beta C(i, y). For a terminal cost W0W_0 the nn-stage costs satisfy the recursion (10):

Wn(i,x)=min⁡y≥x{Kδ(y−x)+Gn(i,y)},W_n(i, x) = \min_{y\ge x}\{K\delta(y-x) + G_n(i, y)\}, Gn(i,y)=G+(i,y)+βλic+β{λiWn−1(i,y−1)+∑j≠iqijWn−1(j,y)+(μ−λi−qi)Wn−1(i,y)},G_n(i, y) = G^+(i, y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i, y-1) + \sum_{j\neq i} q_{ij}W_{n-1}(j, y) + (\mu - \lambda_i - q_i)W_{n-1}(i, y)\Big\},

where δ(z)=1\delta(z) = 1 if z>0z > 0 and δ(0)=0\delta(0) = 0. Throughout, Assumption 1, αcˉ<p\alpha\bar c < p, holds and K>0K > 0. The terminal cost is the optimal cost W∞W_\infty of the linear model (K=0K = 0); its G∞G_\infty is written G0G_0, and y∗(i)y^*(i) is the smallest minimizer of G0(i,⋅)G_0(i, \cdot).

A function f:Z→Rf : \mathbb Z \to \mathbb R is KK-convex (Definition 2) if f(x)−f(x−b)ba+f(x)≤f(x+a)+K\frac{f(x)-f(x-b)}{b}a + f(x) \le f(x+a) + K for all xx and all integers a,b>0a, b > 0. The (r,S)(r, S) policy with parameters {(r(i),S(i))}\{(r(i), S(i))\} orders up to S(i)S(i) when x≤r(i)x \le r(i) and the world is in state ii, and does not order otherwise. With y+(i)y^+(i) the smallest minimizer of G+(i,⋅)G^+(i,\cdot) and ymin⁡+=min⁡iy+(i)y^+_{\min} = \min_i y^+(i), the paper defines

S+(i)=min⁡{y≥y+(i):G+(i,y)−G+(i,y+(i))>γK},r+(i)=max⁡{y<y+(i):G+(i,y)−G+(i,y+(i))>(1−γ)K},r−(i)=max⁡{y<y∗(i):G0(i,y)−G0(i,y∗(i))>K},r−−(i)=max⁡{y<ymin⁡+:G+(i,y)−G+(i,ymin⁡+)>K}.\begin{aligned} S^+(i) &= \min\{y \ge y^+(i) : G^+(i, y) - G^+(i, y^+(i)) > \gamma K\},\\ r^+(i) &= \max\{y < y^+(i) : G^+(i, y) - G^+(i, y^+(i)) > (1-\gamma)K\},\\ r^-(i) &= \max\{y < y^*(i) : G_0(i, y) - G_0(i, y^*(i)) > K\},\\ r^{--}(i) &= \max\{y < y^+_{\min} : G^+(i, y) - G^+(i, y^+_{\min}) > K\}. \end{aligned}

Formalization targets

Goal: Theorems 5(e) and 6

Let Sn∗(i)S^*_n(i) be the smallest minimizer of Gn(i,⋅)G_n(i,\cdot) and rn∗(i)r^*_n(i) the largest y<Sn∗(i)y < S^*_n(i) with Gn(i,y)>K+Gn(i,Sn∗(i))G_n(i, y) > K + G_n(i, S^*_n(i)). For every ii the sequence (rn∗(i),Sn∗(i))(r^*_n(i), S^*_n(i)) has limit points; for any choice of limit points (r∗(i),S∗(i))(r^*(i), S^*(i)), the world-dependent (r,S)(r, S) policy with these parameters is optimal for the infinite-horizon discounted problem, and

y∗(i)≤S∗(i)<S+(i),r−−(i)≤r−(i)≤r∗(i)≤r+(i).y^*(i) \le S^*(i) < S^+(i),\qquad r^{--}(i) \le r^-(i) \le r^*(i) \le r^+(i).

Milestones

Lemma 4 (uniform bounds on the iterates); Theorem 3 (KK-convexity of GnG_n, WnW_n and optimality of an (r,S)(r, S) rule for each nn-stage problem); Lemmas 5 and 6 (difference comparisons); Theorem 4 (the bounds above for every nn); Theorem 5(a)–(d) (convergence of WnW_n, GnG_n, the (r,S)(r, S) property of limit points, and the optimality equation (2)).

Significance

The result shows that the classical (s,S)(s, S) structure survives Markov modulation of demand with an infinite world space and stochastic lead times: a stationary policy whose two parameters depend only on the current world state is optimal over the infinite horizon. The bounds of Theorem 6 locate those parameters in an interval computed from the myopic cost G+G^+ and the linear model alone, uniformly in the horizon.

The results are proved in the paper, except that Theorem 5 refers to Iglehart (1963) and Lemma 4 to Song's thesis. To our knowledge none of them has a machine-checked proof. A formalization would also produce reusable machinery: KK-convexity on the integers, the Scarf-type inductive argument with a countable world state, and the passage from finite-horizon to infinite-horizon optimality for a nonnegative-cost Markov decision process with unbounded costs.

Difficulty

The one-period cost is unbounded in xx and the world space may be infinite, so the usual contraction argument for discounted dynamic programs does not apply. Convergence of WnW_n needs the uniform bound of Lemma 4. Optimality of the limit policy needs a separate argument, because a pointwise limit of (r,S)(r, S) rules need not exist: the parameter sequences are only known to have limit points. The lower bounds r−r^- and r−−r^{--} hold only because the terminal cost is the linear model's optimal cost, which makes the difference comparisons of Lemma 6 possible; the paper notes that Lemma 6 depends on this choice of W0W_0.

Formalization scope

All definitions live in the namespace SongZipkinFluct.FixedCost. Inventory positions and order-up-to levels are integers. The demand law DLiD^i_L is defined through uniformization at rate μ\mu, as an exact series representation of the Markov-modulated Poisson count, and the lead time is a probability law on [0,∞)[0,\infty) independent of the rest. The standing conventions h,p,α>0h, p, \alpha > 0, cˉ,Kˉ≥0\bar c, \bar K \ge 0, μ>0\mu > 0 and μ≥q∗+λ∗\mu \ge q^* + \lambda^* are hypotheses of the model. Assumption 1 and Kˉ>0\bar K > 0 are hypotheses of each theorem.

The iterates WnW_n are defined by the recursion (10), with the minimum written as an infimum over integers y≥xy \ge x. W∞W_\infty and G∞G_\infty are the suprema over nn, which are finite and equal the limits by Lemma 4 and Theorem 3. Every minimizer and every extremal integer (y+y^+, ymin⁡+y^+_{\min}, y∗y^*, Sn∗S^*_n, rn∗r^*_n, S+S^+, r+r^+, r−r^-, r−−r^{--}) is passed through its defining property, never through sInf/sSup on Z\mathbb Z. The goal also asserts that all of them exist, so its hypotheses can be met. A limit point of an integer sequence is a value taken infinitely often.

Optimality is over all deterministic history-dependent feasible policies and from every initial state. Costs are valued in [0,∞][0,\infty], and a policy's cost is the supremum of its finite-horizon discounted costs in the uniformized problem (1). Restricting the comparison to (r,S)(r, S) or stationary policies would trivialize the goal and is ruled out. KK-convexity is the integer version of Definition 2, not convexity over Z\mathbb Z-scalars.

Welcome contributions: KK-convexity calculus on Z\mathbb Z, convergence of the uniformized demand series, Lemma 4, and an Iglehart-type limit argument for countable-state Markov decision processes with nonnegative costs.

Selected references

  • J.-S. Song and P. Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. https://doi.org/10.1287/opre.41.2.351
  • H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
  • D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
  • A. F. Veinott, Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
  • D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
14 thms1 active userReviewed
ProbabilityStochastic Systems·Captain: mikedeng1

Random Walks in a Random Environment 2: lim X_n/n = (1 − Eσ)/(1 + Eσ) if Eσ < 1, −(1 − E(σ⁻¹))/(1 + E(σ⁻¹)) if E(σ⁻¹) < 1, and 0 OtherwiseResearch Paper

Motivation

A random walk in a random environment is a walk whose step probabilities are sampled once at each site and then reused whenever the walk returns there. Repeated visits therefore reveal the same local bias instead of drawing a fresh probability. This makes the walk different from an ordinary random walk with a single averaged step probability. Solomon's 1975 paper asks how the random environment changes the long-run direction and speed of a one-dimensional nearest-neighbor walk. Its Section 1 gives the speed law and the associated limits for first passage times. These results distinguish escape at a nonzero linear rate from escape or recurrence at zero linear rate. Solomon (1975)

The question matters whenever a particle repeatedly crosses the same heterogeneous medium. Averaging the local right-step probabilities predicts the drift of a homogeneous comparison walk, but it does not generally predict the speed in the sampled medium. Sites with a small right-step probability can hold up the walk through repeated excursions. The formula in Theorem (1.16) quantifies this effect using a moment of the ratio of left-step to right-step probability. Solomon (1975), pp. 7–8

Setting

An environment is a sequence α=(αz)z∈Z\alpha=(\alpha_z)_{z\in\mathbb Z} of numbers in [0,1][0,1]. In a fixed environment, a walk at site zz moves to z+1z+1 with probability αz\alpha_z and to z−1z-1 with probability βz=1−αz\beta_z=1-\alpha_z. It starts at X0=0X_0=0. For the random environment, the variables αz\alpha_z are independent and identically distributed. First the environment is sampled; then the walk moves according to the fixed probabilities at its sites. The probability law that averages over both choices is the annealed law PP. The mission's model records this law through every finite path cylinder, jointly with every measurable event concerning the environment. Solomon (1975), pp. 1–2

Write σz=βz/αz\sigma_z=\beta_z/\alpha_z for the ratio of leftward to rightward probability. At the endpoints, σz=∞\sigma_z=\infty when αz=0\alpha_z=0 and σz=0\sigma_z=0 when αz=1\alpha_z=1. Let e=Eσ0e=E\sigma_0 and e−=E(σ0−1)e_-=E(\sigma_0^{-1}); either may be infinite. For an integer site z≠0z\ne0, the passage time TzT_z is the first positive time at which XX visits zz, with Tz=∞T_z=\infty if the site is never reached; put T0=0T_0=0. The positive ladder times are τn=Tn−Tn−1\tau_n=T_n-T_{n-1} where the passage times are finite. Their joint sequence, rather than individual identically distributed variables alone, is relevant to the speed law. Solomon (1975), pp. 5–7

Formalization targets

The goal is the complete three-case statement of Theorem (1.16). All limits below hold almost surely. If e<1e<1, then

Tnn⟶1+e1−e,Xnn⟶1−e1+e.\frac{T_n}{n}\longrightarrow\frac{1+e}{1-e},\qquad \frac{X_n}{n}\longrightarrow\frac{1-e}{1+e}.

If e−<1e_-<1, the symmetric limits are

T−nn⟶1+e−1−e−,Xnn⟶−1−e−1+e−.\frac{T_{-n}}{n}\longrightarrow\frac{1+e_-}{1-e_-},\qquad \frac{X_n}{n}\longrightarrow-\frac{1-e_-}{1+e_-}.

In the remaining case, e−1≤1≤e−e^{-1}\le1\le e_-, both normalized passage times tend to infinity and Xn/nX_n/n tends to zero. The reciprocal inequality is understood in the extended nonnegative reals, including e=∞e=\infty. The milestone list follows the paper's supporting statements: a transience observation, a fixed-environment mean passage-time identity, a separated-block independence lemma, stationarity and ergodicity of ladder times, and the annealed mean ladder-time formula. Solomon (1975), pp. 3, 5–7

Significance

The theorem gives a numerical asymptotic speed in either direction when the corresponding ratio has mean below one. It also identifies a zero-speed regime through explicit conditions on the two reciprocal moments. The passage-time clauses say more than the final speed alone: they describe the time required to reach distant positive and negative sites and distinguish a finite linear time scale from an infinite one. The same section compares the speed with that of a homogeneous walk obtained by replacing every local probability with Eα0E\alpha_0; the random environment can slow the walk. Solomon (1975), pp. 7–8

Solomon proved these results in 1975. This mission asks for machine-checked proofs of the known statements and a reusable Lean description of the annealed nearest-neighbor model. The fixed-environment chain, first passage times, and the shift law of a sequence of ladder times are useful interfaces for further formal work on random media. No proof of these draft statements is claimed by the mission proposal. Solomon (1975)

Difficulty

The direct attempt to apply an ordinary law of large numbers to the step increments Xn−Xn−1X_n-X_{n-1} does not fit the model: those increments are not strictly stationary in a nonconstant environment. The walk revisits previously sampled site probabilities, so a later increment depends on the path's history through the sites it has encountered. The paper points out this obstruction before introducing ladder times. An additional issue is that a passage time need not be finite, and the means ee and e−e_- may also be infinite. Any argument that converts these quantities to ordinary real numbers too early loses the zero-speed cases. Solomon (1975), pp. 5, 7

Formalization scope

Lean represents sites by Z\mathbb Z and time indices by N\mathbb N. A probability space carries the jointly sampled environment and path. The environment lies in [0,1][0,1] pointwise and is independent and identically distributed across all integer sites. The path law is fixed by its joint finite-dimensional cylinder probabilities, which express the annealed construction from the paper. In particular, the path cannot be chosen independently of the environment merely because its one-step marginal probabilities look right. This rules out a trivializing model that forgets the dependence between the sampled medium and the walk.

The ratios σz\sigma_z, their reciprocal and their expectations take values in R≥0∪{∞}\mathbb R_{\ge0}\cup\{\infty\}. Passage times take values in N∪{∞}\mathbb N\cup\{\infty\}, and normalized passage-time limits are expressed in extended nonnegative reals. The position ratio Xn/nX_n/n has a real limit. The theorem permits both endpoint probabilities, αz=0\alpha_z=0 and αz=1\alpha_z=1, and imposes no nondegeneracy assumption. Each convergence statement is almost sure. The ergodicity milestone concerns the full joint law of the sequence (τn)n≥1(\tau_n)_{n\ge1} under the left shift; shift preservation supplies strict stationarity. Solomon (1975), pp. 1–2, 5–7

A complete development needs measure-theoretic probability, the fixed-environment chain and annealed cylinder law, extended-valued integration and first passage times, and ergodic theory for the ladder-time shift. The model and passage-time interfaces can be reused in later one-dimensional random-environment results. Contributions proving the listed milestones, sharpening their interfaces without changing their meaning, or supplying general probability lemmas used by the known proof are within scope.

Selected references

8 thms1 active userReviewed
ProbabilityStochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 6: n·Y_n → (1 − α)/α Almost Surely under PD(α, θ)Research Paper

Motivation

In a population divided into many species, a ranked frequency VnV_n is the fraction belonging to the nnth most common species. The Poisson–Dirichlet distribution is a model for such random ranked frequencies. It also arises from ranked jumps of a stable subordinator, which gives the model its connection to random interval partitions. Pitman and Yor's 1997 paper develops both descriptions and studies quantities derived from the ranked sequence. Its §7.3 asks how much of the remaining total mass belongs to the nnth ranked component when nn is large. This is the chain factor YnY_n, the quantity studied here. These interpretations and the result are in Pitman and Yor (1997).

For 0<α<10<\alpha<1, the paper first analyzes the tail ratio Σn\Sigma_n under PD(α,0)\mathrm{PD}(\alpha,0) through Proposition 11 and its Laplace transform. Proposition 14 relates PD(α,θ)\mathrm{PD}(\alpha,\theta) to that base law by a local-time density. The limiting behavior in Proposition 44 combines those two themes. The paper states both an almost-sure limit and a Gaussian fluctuation limit, but the variance printed for the latter conflicts with the variance of Σ1\Sigma_1 displayed immediately before it. The mission retains the paper's almost-sure assertion as its goal and records the corrected fluctuation assertion separately. Pitman and Yor (1997), pp. 863–865, 890–891.

Setting

Choose 0≤α<10\le\alpha<1 and θ>−α\theta> -\alpha. Let Y~1,Y~2,…\tilde Y_1,\tilde Y_2,\ldots be independent random variables, where Y~n\tilde Y_n has the beta distribution with parameters (1−α,θ+nα)(1-\alpha,\theta+n\alpha). Its density on (0,1)(0,1) is Γ(a+b)xa−1(1−x)b−1/(Γ(a)Γ(b))\Gamma(a+b)x^{a-1}(1-x)^{b-1}/(\Gamma(a)\Gamma(b)) for parameters a,b>0a,b>0. Form the stick-breaking lengths

V~1=Y~1,V~n=(1−Y~1)⋯(1−Y~n−1)Y~n(n≥2).\tilde V_1=\tilde Y_1,\qquad \tilde V_n=(1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n\quad(n\ge2).

Sort these lengths in decreasing order, retaining multiplicities. The law of the resulting sequence V1≥V2≥⋯V_1\ge V_2\ge\cdots is PD(α,θ)\mathrm{PD}(\alpha,\theta), exactly Definition 1 of the paper. Pitman and Yor (1997), p. 857.

For that ranked sequence, define the tail ratio and chain factor

Σn=Vn+1+Vn+2+⋯Vn,Yn=VnVn+Vn+1+⋯=11+Σn.\Sigma_n=\frac{V_{n+1}+V_{n+2}+\cdots}{V_n},\qquad Y_n=\frac{V_n}{V_n+V_{n+1}+\cdots}=\frac{1}{1+\Sigma_n}.

The distinction between YnY_n and the original independent factors Y~n\tilde Y_n matters: the former is computed after ranking and is generally dependent across indices. The paper also uses the function ψα(λ)=1+α∫01(1−e−λx)x−α−1 dx\psi_\alpha(\lambda)=1+\alpha\int_0^1(1-e^{-\lambda x})x^{-\alpha-1}\,dx for λ≥0\lambda\ge0. It appears in the Laplace transform of Σn\Sigma_n. Pitman and Yor (1997), pp. 863–865, 890.

Formalization targets

The central target is Proposition 44, display (150): for 0<α<10<\alpha<1 and θ>−α\theta> -\alpha,

nYn⟶1−ααalmost surely under PD(α,θ).nY_n\longrightarrow\frac{1-\alpha}{\alpha}\quad\text{almost surely under }\mathrm{PD}(\alpha,\theta).

The milestones state the distribution and Laplace transform of Σn\Sigma_n from Proposition 11(ii), its mean α/(1−α)\alpha/(1-\alpha), the almost-sure limit of Σn/n\Sigma_n/n under PD(α,0)\mathrm{PD}(\alpha,0), and Proposition 14's change-of-measure formula. The Gaussian companion records the central limit theorem for Σn/n\Sigma_n/n and the corrected version of Proposition 44's display (151):

n(nYn−1−αα)⟹N ⁣(0,(1−α)2α3(2−α)).\sqrt n\left(nY_n-\frac{1-\alpha}{\alpha}\right) \Longrightarrow N\!\left(0,\frac{(1-\alpha)^2}{\alpha^3(2-\alpha)}\right).

The printed variance in (151) is α−2(2−α)−2\alpha^{-2}(2-\alpha)^{-2}. It differs from the variance forced by the preceding Σn\Sigma_n central limit theorem: Var⁡(Σ1)=α/((2−α)(1−α)2)\operatorname{Var}(\Sigma_1)=\alpha/((2-\alpha)(1-\alpha)^2) and the derivative of x↦1/xx\mapsto1/x at α/(1−α)\alpha/(1-\alpha) give (1−α)2/(α3(2−α))(1-\alpha)^2/(\alpha^3(2-\alpha)). At α=1/2\alpha=1/2, the corrected and printed values are 4/34/3 and 16/916/9. The verbatim milestone text preserves the paper's wording; the companion theorem discloses the correction. Pitman and Yor (1997), pp. 890–891.

Significance

Display (150) identifies the almost-sure scale of the ranked chain factor: YnY_n behaves like a deterministic constant divided by nn. This makes the order of magnitude precise for every permitted θ\theta, despite the dependence among ranked components. The companion fluctuation statement gives a distributional scale around that limit and exposes a numerical inconsistency in the printed version. Neither conclusion is simply a statement about the independent beta factors Y~n\tilde Y_n; the paper compares the two sequences precisely because they have different limiting distributions. Pitman and Yor (1997), p. 891.

The result is proved in the paper, while its statements and their supporting definitions still need a machine-checked development. A completed formalization would make the ranked-frequency law, the tail-ratio limit, and the local-time change of measure available as separately reusable results. It would also settle the corrected variance at the level of a precise probability-law statement rather than silently adopting the paper's printed constant.

Difficulty

The tempting shortcut is to use Proposition 11(ii), which says that each Σn\Sigma_n has the law of a sum of nn independent copies of Σ1\Sigma_1, and invoke a strong law. That information concerns each one-dimensional law separately; it does not exhibit the whole sequence (Σn)(\Sigma_n) as partial sums of a single independent sequence. Almost-sure convergence is a statement about their joint coupling, so the shortcut leaves a gap. The Gaussian conclusion raises a different issue: its limit must survive the change from PD(α,0)\mathrm{PD}(\alpha,0) to PD(α,θ)\mathrm{PD}(\alpha,\theta), and its variance must be consistent with the displayed variance of Σ1\Sigma_1. These are the two substantive tasks beyond the calculation of the Laplace transform. Pitman and Yor (1997), pp. 864, 890–891.

Formalization scope

Lean represents a random ranked sequence as V:Ω→(N→R)V:\Omega\to(\mathbb N\to\mathbb R) on a probability space. Its index kk means the paper's n=k+1n=k+1. Thus the goal uses (k+1)Yk+1(k+1)Y_{k+1}, and the tail-ratio milestones use Σk+1/(k+1)\Sigma_{k+1}/(k+1). The paper's Definition 1 is represented by independent beta coordinate laws followed by a decreasing ranking. The ranking counts multiplicity using extended cardinality, so an infinite set of terms above a threshold cannot acquire a finite fallback count. The law of the ranked sequence is expressed through measurable preimages. This avoids treating a nonmeasurable ranking map as a zero measure through Measure.map.

All targets retain 0<α<10<\alpha<1; the θ\theta targets also retain θ>−α\theta> -\alpha. The beta law and integrals use these parameter ranges. Real expectations state integrability or square integrability where needed, preventing a nonintegrable Bochner integral or variance from supplying a fallback zero. The nonnegative change-of-measure identity uses extended nonnegative integrals, and its local time LL is identified by the almost-sure limit nVnαnV_n^\alpha rather than by an arbitrary extra weight or a limit operator with a default value. The Gaussian variances are positive on this parameter range, despite being represented by nonnegative real parameters in Mathlib. The formalization must use the actual tail ratio of the PD(α,θ)\mathrm{PD}(\alpha,\theta) sequence, not an independently assigned factor process.

The reusable infrastructure includes the ranked-value operation, the stick-breaking law, convolution powers, the tail-ratio and chain-factor definitions, and the bridge between PD(α,0)\mathrm{PD}(\alpha,0) and PD(α,θ)\mathrm{PD}(\alpha,\theta). Contributions that establish these interfaces or prove the displayed mean, strong law, and central limit assertions directly against them are within scope. Pitman and Yor (1997), Definition 1, Propositions 11, 14, 44.

Selected references

  • J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Annals of Probability 25(2):855–900, 1997. DOI: 10.1214/aop/1024404422.
8 thms1 active userReviewed
ProbabilityStochastic Systems·Captain: mikedeng1

On the Generalized “Birth-and-Death” Process 3: Given the Mean Growth n̄_t, the Rates λ = (n̄′/n̄)⁺, μ = (n̄′/n̄)⁻ Uniquely Minimize Var(n_t) for All tResearch Paper

Motivation

In a birth-and-death population model, an expected population curve does not determine the amount of random variation. Births and deaths can occur frequently while nearly canceling in the mean, or one of the two rates can vanish while giving the same mean. This distinction matters when a prescribed growth curve is used to model a population: two processes can agree on their expected size at every time and differ substantially in their uncertainty. In §6 of Kendall's 1948 paper, the question is posed directly: among time-varying birth and death rates giving a fixed mean curve, which choice minimizes the variance of the population size?

Kendall cites Arley's observation for constant rates with the same positive net growth. His §6 moves from that special case to an arbitrary prescribed mean curve and identifies a unique minimum-fluctuation rate pair. The paper also gives a logistic-growth example, connecting the stochastic rate choice to a familiar deterministic population law. The historical result is proved in the paper; this mission concerns its Lean formalization, including the exact time-dependent variance comparison and uniqueness claim.

Setting

The process starts with one ancestor. At time tt, each member gives birth at rate λ(t)\lambda(t) and dies at rate μ(t)\mu(t); the rates are nonnegative. Let ntn_t be the population size and nˉt\bar n_t its expectation. Kendall works with the population probabilities and their generating function rather than constructing sample paths. This mission likewise uses his explicit formulas for the mean and variance, so that the comparison has a precise real-valued expression.

Define the integrated net death rate and the fluctuation by

ρλ,μ(t)=∫0t(μ(τ)−λ(τ)) dτ,Vλ,μ(t)=e−2ρλ,μ(t)∫0teρλ,μ(τ)(λ(τ)+μ(τ)) dτ.\rho_{\lambda,\mu}(t)=\int_0^t\bigl(\mu(\tau)-\lambda(\tau)\bigr)\,d\tau, \qquad V_{\lambda,\mu}(t)=e^{-2\rho_{\lambda,\mu}(t)} \int_0^t e^{\rho_{\lambda,\mu}(\tau)} \bigl(\lambda(\tau)+\mu(\tau)\bigr)\,d\tau.

Kendall's equations (13) and (14c) identify nˉt=e−ρλ,μ(t)\bar n_t=e^{-\rho_{\lambda,\mu}(t)} and Vλ,μ(t)=Var⁡(nt)V_{\lambda,\mu}(t)=\operatorname{Var}(n_t) for the one-ancestor process. A pair (λ,μ)(\lambda,\mu) is admissible here when both rates are continuous and nonnegative on [0,∞)[0,\infty). It has mean nˉ\bar n when e−ρλ,μ(t)=nˉte^{-\rho_{\lambda,\mu}(t)}=\bar n_t for every t≥0t\ge0. In particular, the initial value is nˉ0=1\bar n_0=1. These definitions let the mission quantify over every admissible rate pair with the prescribed mean.

For a positive continuously differentiable mean curve, write g(t)=nˉt′/nˉtg(t)=\bar n_t'/\bar n_t. The minimum-fluctuation rates are λ∗(t)=max⁡{g(t),0}\lambda_*(t)=\max\{g(t),0\} and μ∗(t)=max⁡{−g(t),0}\mu_*(t)=\max\{-g(t),0\}. When the mean decreases, only deaths occur; when it increases, only births occur; when it is locally constant, both rates are zero. This is Kendall's equation (56), expressed without first naming intervals of monotonicity.

Formalization targets

The goal is the simultaneous variance bound

Vλ∗,μ∗(t)≤Vλ,μ(t)for every t≥0 and every admissible (λ,μ) with mean nˉ.V_{\lambda_*,\mu_*}(t)\le V_{\lambda,\mu}(t) \quad\text{for every }t\ge0 \text{ and every admissible }(\lambda,\mu)\text{ with mean }\bar n.

The statement also establishes that (λ∗,μ∗)(\lambda_*,\mu_*) is admissible and has the required mean. Its uniqueness clause says that if one admissible pair has the same variance as the candidate at every nonnegative time, then its two rates equal the candidate rates at every nonnegative time. Equality at only one selected time does not express Kendall's claim. The formal milestones record the fixed rate difference (55), the integral decomposition displayed in §6, and the nonnegative excess in variance that precedes (56). A companion statement covers the logistic example (58)–(60): for a>1a>1 and b>0b>0, nˉt=a/(1+(a−1)e−bt)\bar n_t=a/(1+(a-1)e^{-bt}) has minimum-fluctuation death rate zero and birth rate b(1−nˉt/a)b(1-\bar n_t/a).

Significance

The result distinguishes mean growth from population risk. Fixing λ−μ\lambda-\mu fixes the mean curve, but it leaves room for births and deaths that offset one another. Kendall's theorem determines the lowest variance compatible with the given curve and specifies the rate pair attaining it. The uniqueness statement identifies a model, rather than only a numerical lower bound. His logistic example shows the choice concretely: positive logistic growth is realized by a purely reproductive process in the minimum-fluctuation model.

The paper already derives these formulas. A complete formalization would connect the exact variance expression to a universal optimization claim over continuous nonnegative rate functions, and it would verify that equality throughout time identifies the rates. The definitions of the integrated rate, mean condition and variance functional can also support the other results in Kendall's paper. This proposal uses a local copy of ρ\rho because the geometric-solution mission is being drafted in parallel and its definition has not been published for import.

Difficulty

The constraint imposed by a given mean fixes the difference λ−μ\lambda-\mu but not either rate separately. The variance is an integral over the full past, multiplied by a term involving that same integrated difference. Consequently, a pointwise observation about the current sum λ(t)+μ(t)\lambda(t)+\mu(t) does not by itself state the required comparison of variances over every time horizon. The equality case is also global: a single time's variance cannot generally identify the rates at all earlier times. The formal result must keep the shared mean condition, the variance integral and the quantifiers over both rate pairs and all nonnegative times aligned.

Formalization scope

The Lean development represents rates and the prescribed mean as functions R→R\mathbb R\to\mathbb R. Every stochastic claim is restricted to t≥0t\ge0; the integrals are oriented interval integrals from zero. Both rates are continuous on all of R\mathbb R and nonnegative on nonnegative time. The mean is C1C^1, positive on all of R\mathbb R, and equals one at zero. Extending the regularity and positivity assumptions to negative time makes the total functions defining gg, λ∗\lambda_* and μ∗\mu_* continuous without changing any comparison on [0,∞)[0,\infty). These are explicit convenience assumptions beyond Kendall's wording. No denominator is used without the positivity assumption.

Kendall presents (56) after assuming that positive time splits into decreasing, increasing and constant intervals of nˉ\bar n. The goal uses positive and negative parts of gg and therefore covers any positive C1C^1 curve, including one without such a partition. On each of Kendall's three types of interval the formula agrees with his stated rates. The variance functional is exactly the last expression in (14c); its identification with the variance of the geometric population law is treated in the companion geometric-solution mission. The local statements do not construct a Markov process. The minimum is taken over all admissible continuous nonnegative rate pairs with the prescribed mean, not merely over the two candidate functions or over pointwise values of λ+μ\lambda+\mu.

The development needs real differentiation, continuity, exponentials and interval integrals from Mathlib. Contributions that relate the explicit functional to the population law, prove the comparison and its equality case, or extend the regularity regime while preserving Kendall's claim are within scope. The logistic example provides a concrete instance of the general result.

Selected references

  • D. G. Kendall, On the generalized “birth-and-death” process, Annals of Mathematical Statistics 19(1), 1–15, 1948. DOI: 10.1214/aoms/1177730285.
6 thms1 active userReviewed
Dynamic ProgrammingOperations ResearchReinforcement Learning·Captain: mikedeng1

Planning and Acting in Partially Observable Stochastic Domains: The Witness Theorem, a Set of Useful Policy Trees Is Incomplete iff Replacing One Subtree Improves on It at Some Belief StateResearch Paper

Motivation

A partially observable Markov decision process (POMDP) models an agent that acts in a stochastic world whose state it cannot see directly. The agent sees only noisy observations. POMDPs are the standard model for planning under uncertainty in robotics, dialogue systems, medical decision making and machine maintenance. The exact finite-horizon theory goes back to Smallwood and Sondik (1973), who showed that the optimal value function is piecewise linear and convex in the agent's belief, so that it can be represented by a finite set of vectors.

Kaelbling, Littman and Cassandra (1998) brought this theory to artificial intelligence. Their paper introduces policy trees as the objects behind those vectors and presents the witness algorithm, an exact value-iteration method. It is one of the most cited papers on POMDPs. The correctness of the witness algorithm rests on a single statement, Theorem A.1 of the paper's appendix, the witness theorem. This mission formalizes that theorem together with the lemmas its proof uses.

Timeline:

  • 1965: Åström reduces control with incomplete state information to control of the conditional state distribution.
  • 1973: Smallwood and Sondik prove that the finite-horizon value function is piecewise linear and convex and give the first exact algorithm.
  • 1980s: Cheng's linear support method. Lark and White's pruning.
  • 1994–1996: Littman, Cassandra and Kaelbling give the witness algorithm and its theorem (Littman's thesis, 1996).
  • 1998: the journal version studied here.

Setting

A POMDP is a tuple ⟨S,A,T,R,Ω,O⟩\langle S, A, T, R, \Omega, O\rangle with finite sets SS of states, AA of actions and Ω\Omega of observations. Taking action aa in state ss leads to state s′s' with probability T(s,a,s′)T(s, a, s') and earns expected reward R(s,a)R(s, a). The agent then observes oo with probability O(s′,a,o)O(s', a, o). Rewards are discounted by a factor γ\gamma with 0<γ≤10 < \gamma \le 1; γ=1\gamma = 1 is the plain finite-horizon problem.

A belief state bb is a probability vector on SS; BB denotes the set of all of them. After action aa and observation oo, the belief is updated by Bayes' rule to SE(b,a,o)SE(b, a, o). The normalizing constant of this update is Pr⁡(o∣a,b)\Pr(o \mid a, b).

A tt-step policy tree pp is a single action when t=1t = 1. For t≥2t \ge 2 it is a root action a(p)a(p) together with one (t−1)(t-1)-step subtree o(p)o(p) for each observation oo. Its value is defined by the recursion

Vp(s)=R(s,a(p))+γ∑s′T(s,a(p),s′)∑oO(s′,a(p),o) Vo(p)(s′),V_p(s) = R(s, a(p)) + \gamma \sum_{s'} T(s, a(p), s') \sum_{o} O(s', a(p), o)\, V_{o(p)}(s'),

and at a belief state it is Vp(b)=∑sb(s)Vp(s)=b⋅αpV_p(b) = \sum_s b(s) V_p(s) = b \cdot \alpha_p. The optimal tt-step value is Vt(b)=max⁡pVp(b)V_t(b) = \max_p V_p(b) over all tt-step trees.

A tree pp in a finite set V~\tilde V is useful if some belief state gives it a strictly larger value than every tree of V~\tilde V with a different value function. The useful trees form the parsimonious representation of V~\tilde V. Let Vt−1\mathcal V_{t-1} be the useful (t−1)(t-1)-step trees. The candidates CtaC^a_t are the tt-step trees with root aa and all subtrees in Vt−1\mathcal V_{t-1}, and Qta\mathcal Q^a_t is the set of trees useful in CtaC^a_t. The Q-function is

Qta(b)=∑sb(s)R(s,a)+γ∑oPr⁡(o∣a,b) Vt−1(SE(b,a,o)).Q^a_t(b) = \sum_s b(s) R(s, a) + \gamma \sum_o \Pr(o \mid a, b)\, V_{t-1}(SE(b, a, o)).

For a set UaU_a of candidates, Q^ta(b)=max⁡p∈UaVp(b)\hat Q^a_t(b) = \max_{p \in U_a} V_p(b) is the current approximation. For p∈Uap \in U_a, an observation oo and p′∈Vt−1p' \in \mathcal V_{t-1}, the tree pnewp_{\mathrm{new}} is pp with its subtree for oo replaced by p′p'.

Formalization targets

Goal: Theorem A.1

For a nonempty Ua⊆QtaU_a \subseteq \mathcal Q^a_t,

Ua≠Qta  ⟺  ∃ p∈Ua, o∗∈Ω, p′∈Vt−1, b∈B:Vpnew(b)>Vp~(b)  for all p~∈Ua.U_a \ne \mathcal Q^a_t \iff \exists\, p \in U_a,\ o^* \in \Omega,\ p' \in \mathcal V_{t-1},\ b \in B:\quad V_{p_{\mathrm{new}}}(b) > V_{\tilde p}(b) \ \text{ for all } \tilde p \in U_a .

Trees with the same value function are identified, as in the paper. The statement is exact, with no constants.

Milestones

  1. §3.3: Pr⁡(⋅∣a,b)\Pr(\cdot \mid a, b) is a distribution and SE(b,a,o)∈BSE(b, a, o) \in B when Pr⁡(o∣a,b)≠0\Pr(o \mid a, b) \ne 0.
  2. §4.1: VtV_t is convex on BB.
  3. §4.2: the useful trees represent the same upper surface and are contained, up to identification, in every representing subset.
  4. §4.3: for every belief and subtree there is a useful subtree that is at least as good.
  5. §4.4: Qta(b)Q^a_t(b) is the maximum of Vp(b)V_p(b) over all aa-rooted trees and over CtaC^a_t, and Vt(b)=max⁡aQta(b)V_t(b) = \max_a Q^a_t(b).
  6. §4.4.1: Q^ta≤Qta\hat Q^a_t \le Q^a_t on BB.
  7. Appendix A: if Vp∗(b)>Vp(b)V_{p^*}(b) > V_p(b) for trees with the same root, one subtree swap already improves on pp at bb.
  8. §4.4.2: the witness theorem in Q-function form: Q^ta≠Qta\hat Q^a_t \ne Q^a_t somewhere on BB iff a single-subtree replacement beats all of UaU_a at some belief.

Significance

The witness theorem is the stopping and growth criterion of the witness algorithm. If no single-subtree modification of the current trees beats all of them at some belief state, the current set represents the Q-function exactly. Otherwise the belief found is a witness and yields a new useful tree. Because each test is one linear program, the theorem turns an infinite search over belief space into finitely many linear programs. It is also the basis of the paper's complexity claim, polynomial time in ∣S∣|S|, ∣A∣|A|, ∣Ω∣|\Omega|, ∣Vt−1∣|\mathcal V_{t-1}| and ∣Qta∣|\mathcal Q^a_t|. Incremental pruning and later exact POMDP solvers rely on the same parsimonious-set machinery.

The theorem is proved in the paper; it has not been machine-checked. A formal development would also provide reusable infrastructure: policy trees, their value recursion, belief updates, and the existence and minimality of parsimonious representations of finite sets of linear functions on the simplex. That infrastructure is needed for any formal treatment of exact POMDP value iteration.

Difficulty

Most steps are finite algebra. The part that needs care is the "if" direction of the goal. A belief at which a new tree beats all of UaU_a shows that the true Q-function exceeds the approximation. It does not directly show that a useful tree is missing, because the maximizing tree at that belief may tie with other trees there. One needs the representation property of the parsimonious set (milestone 3): at every belief, the maximum over all candidates is attained by a useful one. Proving this means moving from a belief where several value functions tie to a nearby belief, inside the simplex, where exactly one of them is strictly largest. The proof on p. 131 also needs the Q-function to be attained on the candidate set, so that the improving subtree lies in Vt−1\mathcal V_{t-1} (milestones 4 and 5).

Formalization scope

  • SS, AA and Ω\Omega are finite, nonempty types with decidable equality. TT and OO are stochastic and 0<γ≤10 < \gamma \le 1; these are bundled in POMDP.IsValid.
  • PolicyTree A Ω n is the type of (n+1)(n+1)-step trees, so statements about tt-step trees with subtrees use t=n+2t = n + 2. The type is finite, and the set of all trees of a given depth is Finset.univ.
  • Values are defined by the recursion of p. 109, not by expectations over trajectories; everything is a finite sum.
  • Belief states are the points of stdSimplex ℝ S. Every "there is some belief state" ranges over the simplex, not over RS\mathbb R^S.
  • Usefulness is relative to a named finite set: all trees of a depth for Vt−1\mathcal V_{t-1}, and the candidates for Qta\mathcal Q^a_t. Qta\mathcal Q^a_t is constructed from Vt−1\mathcal V_{t-1}, not quantified over.
  • Maxima are Finset.sup' over nonempty finite sets, or IsGreatest.
  • SE(b,a,o)SE(b, a, o) is the zero vector when Pr⁡(o∣a,b)=0\Pr(o \mid a, b) = 0 (division by zero). Every use either assumes Pr⁡≠0\Pr \ne 0 or multiplies by Pr⁡\Pr.

The following encodings would make the theorem trivial or false, and are excluded: comparing trees by equality instead of by value function, letting bb range over all of RS\mathbb R^S, taking Qta\mathcal Q^a_t to be an arbitrary set, allowing Ua=∅U_a = \emptyset, and defining the true Q-function as Q^ta\hat Q^a_t itself.

Contributions are welcome at every level. The parsimonious-representation lemma (milestone 3) is the reusable geometric core. The subtree-swap lemma and the Q-function identity are the algebraic core.

Selected references

  • L. P. Kaelbling, M. L. Littman, A. R. Cassandra, Planning and acting in partially observable stochastic domains, Artificial Intelligence 101(1–2):99–134, 1998. https://doi.org/10.1016/S0004-3702(98)00023-X
  • R. D. Smallwood, E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
  • K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10:174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X
  • A. R. Cassandra, M. L. Littman, N. L. Zhang, Incremental pruning: a simple, fast, exact method for partially observable Markov decision processes, UAI 1997. https://arxiv.org/abs/1302.1525
11 thms1 active userReviewed
Algorithmic Game TheoryProbability·Captain: mikedeng1

The Evolution of Conventions I: In a Weakly Acyclic Game, Adaptive Play with k ≤ m/(L_Γ + 2) Converges Almost Surely to a ConventionResearch Paper

Motivation

A convention is a pattern of behaviour that is customary because everyone expects everyone else to follow it: driving on the right, or which party yields at a narrow bridge. Peyton Young's The Evolution of Conventions (Econometrica 61 (1993) 57–84) asks how such a pattern can emerge from decentralized play. The players have limited memory and limited information, and nobody coordinates them. The paper's model, adaptive play, is now a standard dynamic of learning in games. It is the starting point of the stochastic-stability theory of equilibrium selection (Foster and Young 1990; Kandori, Mailath and Rob 1993), which builds on the perturbation theory of Freidlin and Wentzell (1984).

This mission covers the first half of the paper: §3 (the model) and §4 (convergence when the players make no mistakes). Before mistakes can be added and stochastically stable conventions selected, the unperturbed process must be shown to settle at all. Theorem 1 gives the condition under which it does.

Setting

Let Γ\Gamma be a game with finitely many players ii, a finite nonempty strategy set SiS_i for each player, and payoffs ui(s)u_i(s) for strategy tuples s∈∏jSjs \in \prod_j S_j. Write (x,s−i)(x, s_{-i}) for ss with player ii's strategy replaced by xx.

  • A play is a strategy tuple. Fix a memory mm and a sample size kk with 1≤k≤m1 \le k \le m. The state h∈H=(∏jSj)mh \in H = (\prod_j S_j)^m is the sequence of the last mm plays, oldest first.
  • A successor of hh is obtained by deleting the oldest play and appending a new one.
  • A sample is a set of kk positions of hh. Player ii's best reply to a sample KK maximizes the total payoff ∑t∈Kui(x,(ht)−i)\sum_{t \in K} u_i(x, (h_t)_{-i}) against the sampled plays.
  • A best-reply distribution gives, for each ii and hh, a probability distribution pi(⋅∣h)p_i(\cdot \mid h) on SiS_i that is positive exactly on the strategies that are best replies to some sample of size kk. The sampling law itself is arbitrary.
  • Adaptive play P0P^0 is the Markov chain on HH that moves from hh to the successor with new play ss with probability ∏ipi(si∣h)\prod_i p_i(s_i \mid h).
  • A strict Nash equilibrium is a tuple ss from which every unilateral deviation is strictly worse. A convention is a state (s,s,…,s)(s, s, \dots, s) with ss a strict Nash equilibrium.
  • The best-reply graph has an edge s→(x,s−i)s \to (x, s_{-i}) whenever x≠six \ne s_i is a best reply of ii to s−is_{-i}. Γ\Gamma is weakly acyclic if from every ss a directed path leads to a sink. L(s)L(s) is the length of a shortest such path from ss to a strict Nash equilibrium, and LΓ=max⁡sL(s)L_\Gamma = \max_s L(s).

Formalization targets

Goal: Theorem 1 (p. 64)

If Γ\Gamma is weakly acyclic and k≤m/(LΓ+2)k \le m/(L_\Gamma + 2), then for every best-reply distribution and every initial state hh,

lim⁡t→∞∑h′ a convention((P0)t)hh′=1.\lim_{t\to\infty} \sum_{h' \text{ a convention}} \big((P^0)^t\big)_{hh'} = 1 .

Milestones

  1. Absorbing states (§4, p. 62): Phh0=1P^0_{hh} = 1 if and only if hh is a convention.
  2. Sinks (§4, p. 64): the sinks of the best-reply graph are exactly the strict Nash equilibria. Hence weak acyclicity means that one-player-at-a-time best replies can reach a strict equilibrium from every tuple.
  3. A run of best replies (proof of Theorem 1, p. 64): if m≥2k−1m \ge 2k-1, then with positive probability kk consecutive identical best replies to the last kk plays are appended.
  4. Uniform bound (proof of Theorem 1, p. 65): there is q>0q > 0 such that from every state a convention is reached within M=kLΓ+mM = kL_\Gamma + m periods with probability at least qq.
  5. Geometric tail (proof of Theorem 1, p. 64): such a uniform bound makes the probability of no convention after rMrM periods at most (1−q)r(1-q)^r.
  6. Example 2 (pp. 65–66, off the goal's path): in a Battle-of-the-Sexes game with complete sampling k=mk = m, a perfectly miscoordinated history stays miscoordinated forever.

Significance

Theorem 1 identifies a class of games, the weakly acyclic ones, in which boundedly rational players who best-reply to small random samples of the past almost surely lock in to a strict pure equilibrium. The paper's examples of weakly acyclic games (p. 63) are pure coordination games and games with common interests in which no two strategy tuples are payoff equivalent. Absorption is in behaviour, not just in empirical frequencies. Example 2 shows that this fails for fictitious-play-like complete sampling, so the sampling ratio k/mk/m is a real ingredient. The absorbing states identified in the first milestone are the states among which the stochastic-stability analysis of the paper's later sections selects.

The result is proved in the paper. To the best of our knowledge no machine-checked version exists. The mission asks for a formal proof of Theorem 1 and its milestones for an arbitrary best-reply distribution. That generality is the paper's own: non-uniform sampling is explicitly allowed. A formal proof also pins down the memory bookkeeping in the paper's proof (look-backs of 2k−12k-1, 3k−13k-1 and kr+2k−1kr + 2k - 1 periods), which the text checks only in words.

Difficulty

Adaptive play is a finite Markov chain. The obvious route through the generic theory of absorbing chains requires showing that a convention is reachable from every state, and that is where the argument becomes delicate. A best-reply path in the game cannot be followed directly: each player only sees a random sample, and the players who are not moving must keep playing their old strategies. The proof gets around this by having the non-moving players keep sampling older parts of the history, so those parts must still be in memory. This is what forces the bound k≤m/(LΓ+2)k \le m/(L_\Gamma+2). A uniform, state-independent constant is then needed to turn reachability into almost-sure convergence.

Formalization scope

Players form a finite type ι, strategies a family of finite nonempty types S i, and payoffs u : ι → (∀ i, S i) → ℝ. A state is Fin m → ∀ i, S i with position 0 the oldest play. A best-reply distribution is any p : ∀ i, H → S i → ℝ with the stated support. All statements quantify over every such p. Adaptive play is a Matrix H H ℝ, and "converges almost surely to a convention" is stated through matrix powers. That is equivalent to almost-sure absorption because conventions are absorbing. The condition k≤m/(LΓ+2)k \le m/(L_\Gamma+2) is k(LΓ+2)≤mk(L_\Gamma+2) \le m in ℕ. L(s)L(s) is an sInf on ℕ that is never empty under weak acyclicity.

The display (1) on p. 62 reads "the right-most element of hh". The formalization uses the right-most element of the successor h′h', the only reading under which the rule is meaningful.

The goal cannot be satisfied trivially. The sampling law is not fixed, the conclusion is a limit equal to 11 from every initial state (not "with positive probability" or "along some path"), and the hypotheses are jointly satisfiable, for example by a 2×22\times2 coordination game with uniform sampling. A best reply to a sample uses the joint empirical distribution of the sampled plays, not independent marginals.

A complete development needs elementary Markov-chain facts about matrix powers and absorbing sets, plus combinatorics of shifted histories. These parts are reusable for any finite-memory learning dynamic. Proofs of individual milestones are welcome independently.

Related platform work: stochastic fictitious play in potential games (StochFictPlay.*, Hofbauer–Sandholm 2002) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra 1997) formalize other learning dynamics. The perturbed process and the selection of risk-dominant conventions are the subject of the sibling missions The Evolution of Conventions II and III.

Selected references

22 thms1 active userReviewed
Graph TheoryProbability·Captain: mikedeng1

The Evolution of Conventions II: The Stochastically Stable States of a Regular Perturbation of a Finite Markov Chain Are the Recurrent Classes of Minimum Stochastic PotentialResearch Paper

Motivation

Many models in economics, biology and computer science are finite Markov chains that have several absorbing states or recurrent classes, so their long-run behaviour depends on where they start. Adding a small amount of noise (mistakes, mutations, experimentation) makes the chain irreducible, and the noisy chain then has a unique stationary distribution. As the noise vanishes, that distribution concentrates on some of the original recurrent classes. The stochastically stable states are the ones that keep positive weight in the limit; they are the states the system spends nearly all its time in when the noise is small but nonzero.

H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) proved a general finite-state characterization of these states, which he used to select among the equilibria of coordination games under adaptive play. The characterization rests on the theory of small random perturbations of Freidlin and Wentzell (1984), developed for diffusions, and on a combinatorial lemma of theirs expressing stationary distributions through spanning trees. Kandori, Mailath and Rob (1993) characterized the limit distribution by spanning trees on the whole state space for their model of learning with mutations; Young's Lemma 1 generalizes their Theorem 1 (p. 78), and his Lemma 2 reduces the computation to the much smaller graph of recurrent classes. Foster and Young (1990) introduced stochastic stability for evolutionary dynamics, and the equilibria it selects in 2×22\times 2 games coincide with the risk-dominant equilibria of Harsanyi and Selten (1988).

Setting

Let XX be a finite set and P0P^0 the transition matrix of a Markov chain on XX. A state yy is reachable from xx if (P0)xyn>0(P^0)^n_{xy} > 0 for some n≥0n \ge 0; xx is recurrent if every state reachable from xx can reach xx back; the recurrent communication classes X1,…,XJX_1, \dots, X_J are the communication classes of recurrent states.

A family (Pε)ε∈(0,a](P^\varepsilon)_{\varepsilon \in (0,a]} of Markov chains on XX is a regular perturbation of P0P^0 if for all x,yx, y:

  • (6) PεP^\varepsilon is aperiodic and irreducible for every ε∈(0,a]\varepsilon \in (0,a];
  • (7) Pxyε→Pxy0P^\varepsilon_{xy} \to P^0_{xy} as ε→0\varepsilon \to 0;
  • (8) if Pxyε>0P^\varepsilon_{xy} > 0 for some ε\varepsilon, there is r≥0r \ge 0 with 0<lim⁡ε→0ε−rPxyε<∞0 < \lim_{\varepsilon \to 0} \varepsilon^{-r} P^\varepsilon_{xy} < \infty.

The exponent r=r(x,y)r = r(x,y) is the resistance of the transition x→yx \to y. The graph GG has vertex set XX and an edge (x,y)(x,y) when Pxyε>0P^\varepsilon_{xy} > 0 for all small ε\varepsilon, weighted by r(x,y)r(x,y).

For z∈Xz \in X, a zz-tree is a spanning tree of edges of GG in which every x≠zx \ne z has a unique directed path to zz. The potential of zz is

γ(z)=min⁡T∈Tz∑(x,y)∈Tr(x,y).(9)\gamma(z) = \min_{T \in \mathcal T_z} \sum_{(x,y) \in T} r(x,y). \tag{9}

For classes i≠ji \ne j, rijr_{ij} is the least resistance of a path in GG from XiX_i to XjX_j. On the complete directed graph G\mathcal G with vertices 1,…,J1, \dots, J and edge weights rijr_{ij}, the stochastic potential γj\gamma_j of XjX_j is the least total weight of a jj-tree in G\mathcal G.

Formalization targets

Goal: Theorem 4 (p. 78)

If με\mu^\varepsilon is the stationary distribution of PεP^\varepsilon for ε∈(0,a]\varepsilon \in (0,a], then με→μ0\mu^\varepsilon \to \mu^0 as ε→0\varepsilon \to 0, where μ0\mu^0 is a stationary distribution of P0P^0, and

μx0>0  ⟺  x∈Xj for some j with γj=min⁡iγi.\mu^0_x > 0 \iff x \in X_j \text{ for some } j \text{ with } \gamma_j = \min_i \gamma_i .

Milestones, in the order of the paper's proof

  1. Resistance (p. 77). The exponent in (8) is unique; a transition positive for some ε\varepsilon is an edge of GG; and the edges of zero resistance are exactly the transitions with Pxy0>0P^0_{xy} > 0.
  2. Markov chain tree formula (p. 79). For an aperiodic irreducible chain P′P', μz′=pz′/∑xpx′\mu'_z = p'_z / \sum_x p'_x with pz′=∑T∈Tz∏(x,y)∈TPxy′p'_z = \sum_{T \in \mathcal T_z} \prod_{(x,y)\in T} P'_{xy} is the unique stationary distribution.
  3. Lemma 1 (p. 78). με→μ0\mu^\varepsilon \to \mu^0, μ0\mu^0 is stationary for P0P^0, and μx0>0\mu^0_x > 0 iff γ(x)≤γ(y)\gamma(x) \le \gamma(y) for all yy.
  4. (p. 80) A stationary distribution of a finite chain vanishes on non-recurrent states.
  5. (p. 80) All states of a recurrent class of P0P^0 have the same potential.
  6. Lemma 2 (p. 80). γ(x)=γj\gamma(x) = \gamma_j for every x∈Xjx \in X_j.

Significance

Theorem 4 turns a limit of stationary distributions into a finite optimization: compute least-resistance paths between the recurrent classes, then a minimum-weight arborescence on the reduced graph. The answer depends only on the orders of magnitude of the perturbations, not on their exact values, which is what makes the result usable when the noise model is known only qualitatively. It underlies the equilibrium-selection results of the same paper (risk dominance in 2×22\times 2 coordination games, Theorem 3) and much of the later stochastic evolutionary game theory literature.

The result is proved in the paper, with the tree formula imported from Freidlin and Wentzell. As far as is known, none of it is formalized: Mathlib has irreducible and primitive nonnegative matrices but neither the Markov chain tree formula, aperiodicity, recurrent classes of a finite chain, nor minimum arborescences. A complete development would produce these as reusable components.

Difficulty

The first idea is to take the limit in μεPε=με\mu^\varepsilon P^\varepsilon = \mu^\varepsilon: compactness and (7) give that every limit point of με\mu^\varepsilon is stationary for P0P^0, but P0P^0 has many stationary distributions, so this neither proves convergence nor identifies the support. Both come from the tree formula, which makes μzε\mu^\varepsilon_z a ratio of sums of products whose orders of magnitude are read off from the resistances; the absence of cancellation (all terms are nonnegative) is essential. The second difficulty is Lemma 2: an optimal xx-tree on the whole state space must be transformed, by the paper's tree surgery on junctions (pp. 80–83), into something comparable with a jj-tree on the class graph without increasing its resistance. The easy inequality γ(xj)≤γj\gamma(x_j) \le \gamma_j glues optimal paths and zero-resistance trees together; the reverse inequality is where the work lies.

Formalization scope

States form a Fintype X with decidable equality; chains are real matrices Matrix X X ℝ, row stochasticity is Matrix.rowStochastic, irreducibility is Mathlib's Matrix.IsIrreducible, and aperiodicity (every state has period 1) is defined in the mission. The family PεP^\varepsilon is a function ℝ → Matrix X X ℝ constrained only on (0,a](0, a]; all limits are one-sided (ε→0+\varepsilon \to 0^+), ε−r\varepsilon^{-r} is the real power, and "0<lim⁡<∞0 < \lim < \infty" is a real limit c>0c > 0. Distributions are row vectors and stationarity is μA=μ\mu A = \mu. Trees are parent maps with edges pointing toward the root. Potentials, class resistances and stochastic potentials are infima in EReal, where an empty infimum is +∞+\infty; under the hypotheses all of them are finite.

The goal quantifies over every regular perturbation, not a parametric family such as (1−ε)P0+εQ(1-\varepsilon)P^0 + \varepsilon Q, and over every family of stationary distributions of the PεP^\varepsilon (unique by (6)). The recurrent classes are computed from P0P^0, not supplied as data, and γj\gamma_j is computed on the class graph with weights rijr_{ij}; defining γj\gamma_j as γ(x)\gamma(x) for some x∈Xjx \in X_j would make Lemma 2 definitional and is ruled out.

Contributions welcome: the Markov chain tree formula and the uniqueness of stationary distributions for irreducible finite chains (both reusable well beyond this mission), recurrence and the support of stationary distributions, and the arborescence surgery of Lemma 2.

Selected references

11 thms1 active userReviewed
Dynamic ProgrammingOperations 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\|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≥1S\ge 1 states 1,…,S1,\dots,S. In state ss a finite nonempty set AsA_s of actions is available; taking action aa earns the real reward r(s,a)r(s,a) and assigns the transition weight p(t∣s,a)≥0p(t\mid s,a)\ge 0 to each state tt. No bound on ∑tp(t∣s,a)\sum_t p(t\mid s,a) is assumed. The set of decision rules is F=×s=1SAsF=\times_{s=1}^S A_s; for f∈Ff\in F, r(f)r(f) is the vector (r(s,f(s)))s(r(s,f(s)))_s and P(f)P(f) the matrix (p(t∣s,f(s)))s,t(p(t\mid s,f(s)))_{s,t}.

A policy is a sequence π=(f1,f2,… )\pi=(f_1,f_2,\dots) of decision rules. The policy f∞=(f,f,… )f^\infty=(f,f,\dots) is stationary; (g,π)=(g,f1,f2,… )(g,\pi)=(g,f_1,f_2,\dots) uses gg first and then follows π\pi; Nπ{}^N\pi repeats the first NN rules of π\pi forever and is called periodic. Let P0(π)=IP^0(\pi)=I and PN(π)=P(f1)⋯P(fN)P^N(\pi)=P(f_1)\cdots P(f_N). The policy π\pi is transient if ∑N≥0PN(π)\sum_{N\ge0}P^N(\pi) converges, and then its vector of total returns is

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

The one-step comparison v(g,π∗)=V(g,π∗)−V(π∗)v(g,\pi^*)=V(g,\pi^*)-V(\pi^*) measures the gain from deviating to gg for one step. Vectors are compared coordinatewise, and x>yx>y means x≥yx\ge y, x≠yx\ne y. For a matrix BB, ∥B∥=max⁡i∑j∣bij∣\|B\|=\max_i\sum_j|b_{ij}| and ∣σ(B)∣|\sigma(B)| is its spectral radius. Finally V∗=max⁡fV(f∞)V^*=\max_f V(f^\infty) and ℜV=max⁡g[r(g)+P(g)V]\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∈Ff\in F with

V(π)≤V(f∞)for every policy π.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

  1. Lemma 1. For transient π=(gi)\pi=(g_i) and π∗\pi^*: V(π)−V(π∗)=∑NPN(π) v(gN+1,π∗)V(\pi)-V(\pi^*)=\sum_N P^N(\pi)\,v(g_{N+1},\pi^*), and V(g∞)−V(π∗)=[I−P(g)]−1v(g,π∗)V(g^\infty)-V(\pi^*)=[I-P(g)]^{-1}v(g,\pi^*).
  2. Lemma 2. If every stationary policy is transient and f∈Ff\in F: either v(g,f∞)>0v(g,f^\infty)>0 for some gg, and then V(g∞)>V(f∞)V(g^\infty)>V(f^\infty), or v(g,f∞)≤0v(g,f^\infty)\le0 for all gg, which holds iff f∞f^\infty is best among stationary policies.
  3. Corollary 1. If every stationary policy is transient, some stationary policy maximizes VV over the stationary policies.
  4. Corollary 2. Under the same hypothesis, V∗V^* is the unique fixed point of ℜ\Re.
  5. Lemma 3 (Hoffman). For every ε>0\varepsilon>0 and every program there is a positively similar program with max⁡g∥P~(g)∥<max⁡g∣σ(P(g))∣+ε\max_g\|\tilde P(g)\|<\max_g|\sigma(P(g))|+\varepsilon.
  6. Corollary 4, read with "every" and with "some": stationary, periodic and arbitrary policies are transient together, and this is equivalent to ∥PN(π)∥<1\|P^N(\pi)\|<1 for some N≥1N\ge1; with ∥P(g)∥≤1\|P(g)\|\le1 also to ∥PS(π)∥<1\|P^S(\pi)\|<1.
  7. Theorem 1. If every stationary policy is transient and π∗\pi^* is any policy: v(g,π∗)>0v(g,\pi^*)>0 implies V(g∞)>V(π∗)V(g^\infty)>V(\pi^*), and v(⋅,π∗)≤0v(\cdot,\pi^*)\le0 iff V(π)≤V(π∗)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 ℜV=V\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(π)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)∥\|P(g)\| may exceed one for every gg, 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)NP(g)^N, whereas the goal concerns infinite products of different matrices P(f1)P(f2)⋯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 FF 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)∥≤1\|P(g)\|\le1.
  • Policies are deterministic Markov sequences ℕ → F, indexed from 00: π 0 is f1f_1. "All policies" means all such sequences.
  • Transience is Summable of N↦PN(π)N\mapsto P^N(\pi) in the entrywise topology. VV 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,∞][0,\infty].
  • V∗V^* and ℜ\Re are coordinatewise Finset.sup' over the finite set FF.

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 00, no statement compares VV 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=∑BN(I-B)^{-1}=\sum B^N, and finite-dimensional spectral theory relating ∣σ(B)∣<1|\sigma(B)|<1 to BN→0B^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

12 thms1 active userReviewed
Dynamic ProgrammingOperations Research·Captain: mikedeng1

Average Optimality in Dynamic Programming with General State Space: Under (W) or (S) and Bounded Relative Discounted Values, a Limit of Discount-Optimal Policies Is Average OptimalResearch Paper

Motivation

A Markov decision process with the average cost criterion asks for a policy that minimizes the long-run expected cost per unit time. The criterion is the natural one for inventory, queueing and maintenance systems that run indefinitely without a meaningful discount rate, and it is the standard benchmark in the theory of controlled Markov chains (Arapostathis et al. 1993, Hernández-Lerma and Lasserre 1996). Unlike the discounted criterion, it has no contraction to work with, and an average-optimal policy may fail to exist.

The classical route to average optimality is the vanishing discount approach: solve the β\beta-discounted problem, which is well behaved, and let β↑1\beta \uparrow 1. Schäl's paper gives conditions on a model with a general (Borel) state space under which this limit produces an average-optimal stationary policy.

Timeline. Taylor (1965) and Ross (1968) used the vanishing discount approach with equicontinuity via Arzelà–Ascoli. Sennott (1989) proved, for countable state spaces, that pointwise bounded relative discounted values yield an average cost optimality inequality and an average-optimal stationary policy. Schäl (1993, this mission) extended this to standard Borel state spaces under two alternative compactness–continuity conditions, (W) and (S). Later work, e.g. Feinberg, Kasyanov and Zadoianchuk (2012) and Feinberg and Liang (2022), weakened the compactness assumptions and studied when the inequality becomes an equation.

Setting

The model (S,A,A(⋅),q,c)(S, A, A(\cdot), q, c) consists of standard Borel spaces SS (states) and AA (actions); nonempty action sets A(x)⊆AA(x) \subseteq A whose graph {(x,a):a∈A(x)}\{(x, a) : a \in A(x)\} is measurable; a transition law q(⋅∣x,a)q(\cdot \mid x, a); and a measurable one-step cost c(x,a)∈[0,∞]c(x, a) \in [0, \infty]. A policy δ∈Δ\delta \in \Delta chooses, at each stage nn, a randomized action that may depend on the whole history and lies in A(xn)A(x_n) with probability one. A stationary policy f∈Ff \in \mathbb F is a measurable f:S→Af : S \to A with f(x)∈A(x)f(x) \in A(x).

For a policy δ\delta and initial state xx, Jn(δ,x)J^n(\delta, x) is the expected total cost of the first nn stages, and

Φ(δ,x)=lim sup⁡n→∞1nJn(δ,x),g=inf⁡x∈Sinf⁡δ∈ΔΦ(δ,x).\Phi(\delta, x) = \limsup_{n\to\infty} \tfrac1n J^n(\delta, x), \qquad g = \inf_{x \in S}\inf_{\delta \in \Delta} \Phi(\delta, x).

A policy is average optimal if Φ(δ,x)=g\Phi(\delta, x) = g for every xx. The General Assumption is g<∞g < \infty.

For 0<β<10 < \beta < 1, Jβ(δ,x)J_\beta(\delta, x) is the expected total β\beta-discounted cost, vβ(x)=inf⁡δJβ(δ,x)v_\beta(x) = \inf_\delta J_\beta(\delta, x), mβ=inf⁡xvβ(x)m_\beta = \inf_x v_\beta(x), and wβ=vβ−mβ≥0w_\beta = v_\beta - m_\beta \ge 0 is the relative discounted value function. The quantities gˉ\bar g and g‾\underline g are the upper and lower limits of (1−β)mβ(1-\beta)m_\beta as β↑1\beta \uparrow 1. Condition (B) requires sup⁡β<1wβ(x)<∞\sup_{\beta < 1} w_\beta(x) < \infty for each xx.

Condition (W): SS is locally compact with countable base, the A(x)A(x) are compact and x↦A(x)x \mapsto A(x) is upper semicontinuous, qq is weakly continuous on the graph of AA, and cc is lower semicontinuous there. Condition (S): the A(x)A(x) are compact, and for each fixed xx, a↦q(⋅∣x,a)a \mapsto q(\cdot \mid x, a) is setwise continuous and a↦c(x,a)a \mapsto c(x, a) is lower semicontinuous on A(x)A(x).

Formalization targets

Goal: Theorem 3.8

Under the General Assumption, (B), and (W) or (S):

∃f1∈F: Φ(f1,x)=g  ∀x∈S,g=lim⁡β→1(1−β)mβ=lim⁡β→1(1−β)vβ(x)  ∀x.\exists f_1 \in \mathbb F:\ \Phi(f_1, x) = g \ \ \forall x \in S, \qquad g = \lim_{\beta\to1}(1-\beta)m_\beta = \lim_{\beta \to 1}(1-\beta)v_\beta(x)\ \ \forall x.

Moreover, for every sequence β(k)↑1\beta(k) \uparrow 1 and every choice of β(k)\beta(k)-discount-optimal stationary policies fβ(k)f_{\beta(k)}, some average-optimal f1f_1 is a limit of them: under (W), f1(x)=lim⁡mfβm(xm)f_1(x) = \lim_m f_{\beta_m}(x_m) with βm\beta_m from {β(k)}\{\beta(k)\}, βm→1\beta_m \to 1 and xm→xx_m \to x; under (S), f1(x)=lim⁡mfβm(x)f_1(x) = \lim_m f_{\beta_m}(x).

Milestones

  1. Lemma 1.2: lim sup⁡β→1(1−β)Jβ(δ,x)≤Φ(δ,x)\limsup_{\beta\to1}(1-\beta)J_\beta(\delta, x) \le \Phi(\delta, x), and g‾≤gˉ≤g\underline g \le \bar g \le g.
  2. Proposition 1.3: a finite measurable w‾≥0\underline w \ge 0 and f1∈Ff_1 \in \mathbb F with w‾(x)+g‾≥c(x,f1(x))+∫w‾ dq(x,f1(x))\underline w(x) + \underline g \ge c(x, f_1(x)) + \int \underline w\, dq(x, f_1(x)) give Φ(f1,⋅)=g=g‾=gˉ\Phi(f_1, \cdot) = g = \underline g = \bar g.
  3. Proposition 2.1 and (2.2): existence of discount-optimal stationary policies, the discounted optimality equation and its relative form.
  4. Lemma 2.3: Fatou's lemma for setwise and for weakly converging measures.
  5. (3.2), Lemmas 3.3, 3.4: the lower limit w‾(x)=lim inf⁡k→∞,y→xwβ(k)(y)\underline w(x) = \liminf_{k\to\infty, y\to x} w_{\beta(k)}(y) is attained along measurable sequences.
  6. Proposition 3.5 and its (S) version (3.7): w‾\underline w and some f1f_1 satisfy the optimality inequality with g‾\underline g.

Significance

The theorem gives existence of an average-optimal stationary policy on a general state space from checkable model conditions plus pointwise bounds on relative values, without assuming a solution of the average cost optimality equation. It also identifies the optimal average cost as the Abelian limit of discounted values, and says how to compute an optimal policy: as a limit of discount-optimal ones. §4 of the paper verifies (B) through entrance-time bounds and applies the theorem to Assaf's invariant problem and to a finite-capacity inventory model.

The result is a published theorem; none of it is machine-checked. Formalizing it requires the measure-theoretic layer of Borel dynamic programming (canonical path measures of history-dependent policies, discounted optimality equations, measurable selection of minimizers and of accumulation points) and Fatou lemmas for varying measures. These components are reusable for any Borel-space MDP. Related platform work: the Feinberg–Liang average-cost optimality equation under an additional equicontinuity assumption is posed separately (FeinbergLiang.ACOE.acoe_of_assumptionEC); it is a different theorem.

Difficulty

The naive argument takes a pointwise limit of wβw_{\beta} as β→1\beta \to 1 in the relative optimality equation (2.2). Under (B) the family {wβ(x)}\{w_\beta(x)\} is only bounded pointwise, so no subsequence need converge, and even a pointwise lower limit loses the continuity needed to pass ∫wβ dq(x,fβ(x))\int w_\beta\, dq(x, f_\beta(x)) to the limit when qq is only weakly continuous. The generalized lower limit w‾(x)=lim inf⁡k,y→xw(k,y)\underline w(x) = \liminf_{k, y\to x} w(k, y) repairs this, but then the limit has to be realized along measurably chosen states and indices, and the limiting actions must be selected measurably as accumulation points. The second obstacle is that only an inequality survives, with the constant g‾\underline g; turning it into average optimality needs the Tauberian comparison of Lemma 1.2.

Formalization scope

The model reuses the published FeinbergLiang.ACOE.MDP (history-dependent randomized policies, the Ionescu-Tulcea path measure, JnJ^n, JβJ_\beta, Φ\Phi) with its constant lower = 0, and a local definition file adds action sets, admissibility, gg, vβv_\beta, mβm_\beta, gˉ\bar g, g‾\underline g, wβw_\beta, w‾\underline w and Conditions (W), (S), (B). Committed conventions:

  • All costs and values lie in [0,∞][0, \infty]; (1−β)(1-\beta) is a nonnegative extended real, and β→1\beta \to 1 means β↑1\beta \uparrow 1.
  • Every infimum defining gg and vβv_\beta runs over admissible policies only (actions in A(x)A(x) almost surely); qq and cc are defined on S×AS \times A, but only their values on the graph of AA enter.
  • wβw_\beta is a truncated difference, which equals vβ−mβv_\beta - m_\beta because the General Assumption gives mβ<∞m_\beta < \infty. The General Assumption is an explicit hypothesis of every statement that involves gg, g‾\underline g, gˉ\bar g, mβm_\beta or wβw_\beta.
  • Upper semicontinuity of A(⋅)A(\cdot) is Berge's. Condition (W)(0) is part of CondW: the topology on SS generates its σ-algebra and is locally compact, second countable and Hausdorff, hence metrizable; the metric ρ\rho of §3 is a metric-space instance. Under (S) no topology on SS is used, and the lower limit is lim inf⁡kwβ(k)(x)\liminf_k w_{\beta(k)}(x) (the discrete metric).
  • (W)(1) prints "A(x)∈C(x)A(x) \in \mathcal C(x)", read as C(A)\mathcal C(A). (3.2) prints inf⁡k≥nw‾k(k,x)\inf_{k\ge n}\underline w_k(k, x), which is false in general; the subscript-nn version used in the proof of Lemma 3.4 is stated. "{βm}⊂{β(k)}\{\beta_m\} \subset \{\beta(k)\}, βm→1\beta_m \to 1" is encoded as βm=β(km)\beta_m = \beta(k_m) with km→∞k_m \to \infty.
  • Theorem 3.8's "{β(k)}\{\beta(k)\} can be any sequence" is a universal quantifier over sequences and over choices of discount-optimal policies.

A formalization that assumes an average cost optimality inequality or equation, or that assumes the existence of the limit lim⁡(1−β)mβ\lim(1-\beta)m_\beta, proves Proposition 1.3 rather than the goal; the goal derives the inequality from (W) or (S), (B) and the General Assumption alone. Contributions to the shared infrastructure (Markov property of the canonical process, measurable selection theorems such as Brown–Purves, Fatou lemmas for varying measures) are welcome as separate theorems. §4 of the paper (entrance-time bounds for (B)) is outside this mission.

Selected references

  • M. Schäl, Average Optimality in Dynamic Programming with General State Space, Mathematics of Operations Research 18(1), 163–172, 1993. https://doi.org/10.1287/moor.18.1.163
  • M. Schäl, Conditions for optimality in dynamic programming and for the limit of n-stage optimal policies to be optimal, Z. Wahrscheinlichkeitstheorie verw. Gebiete 32, 179–196, 1975. https://doi.org/10.1007/BF00532612
  • L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Operations Research 37(4), 626–633, 1989. https://doi.org/10.1287/opre.37.4.626
  • R. F. Serfozo, Convergence of Lebesgue integrals with varying measures, Sankhyā Ser. A 44, 380–402, 1982.
  • A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2), 282–344, 1993. https://doi.org/10.1137/0331018
  • E. A. Feinberg, P. O. Kasyanov, N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 37(4), 591–607, 2012. https://doi.org/10.1287/moor.1120.0555
14 thms1 active userReviewed
Dynamic ProgrammingOperations ResearchProbability·Captain: mikedeng1

Inventory Control in a Fluctuating Demand Environment III: Under Stochastic Monotonicity, the Myopic and Optimal Basestock Levels Are Nondecreasing in the World StateResearch Paper

Motivation

Demand for many products does not arrive at a constant rate. It moves with an underlying environment: the economy, the season, a product's life-cycle stage, the state of a customer's own operations. Song and Zipkin (Oper. Res. 41(2):351–370, 1993) modelled this environment as a continuous-time Markov chain, the world, whose current state sets the Poisson demand rate, and showed that a basestock policy whose level depends on the current world state is optimal under linear order costs. Missions I and II of this series formalize those optimality results.

A practitioner who uses such a policy wants to know how the levels depend on the world. If a higher world state means more demand now and more demand later, a higher level should be kept. That is what intuition says, but the optimal level depends on the whole future of the world chain, not only on the current demand rate. §4 of the paper answers it for a world with an arbitrary partial order, which covers several independent demand drivers at once.

Setting

The world AA is a continuous-time Markov chain on a countable set I\mathbf I with generator Q=(qij)Q = (q_{ij}), qi=−qiiq_i = -q_{ii}, and bounded rates q∗=sup⁡iqiq^* = \sup_i q_i, λ∗=sup⁡iλi\lambda^* = \sup_i \lambda_i. While A=iA = i, unit demands arrive at rate λi\lambda_i, all demand is backlogged, and orders arrive after a random lead time LL that is independent of the world and the demand. Costs are discounted at rate α>0\alpha > 0. With the unit order cost cˉ\bar c, holding rate hh and penalty rate pp, set c=cˉ E[e−αL]c = \bar c\,E[e^{-\alpha L}] and

C^(x)=max⁡{−px, hx},C(i,y)=E[e−αLC^(y−DLi)],\hat C(x) = \max\{-px,\ hx\}, \qquad C(i,y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big],

where DLiD^i_L is the demand during a lead time when the world starts in ii. Uniformizing at a rate μ≥q∗+λ∗\mu \ge q^* + \lambda^* with β=1/(μ+α)\beta = 1/(\mu+\alpha) and γ=βμ\gamma = \beta\mu, the myopic cost is G+(i,y)=(1−γ)cy+βC(i,y)G^+(i,y) = (1-\gamma)cy + \beta C(i,y). The linear-cost model (K=0K = 0) is solved by value iteration from W0≡0W_0 \equiv 0:

Gn(i,y)=G+(i,y)+βλic+β{λiWn−1(i,y−1)+∑j≠iqijWn−1(j,y)+(μ−λi−qi)Wn−1(i,y)},G_n(i,y) = G^+(i,y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i,y-1) + \sum_{j\ne i} q_{ij}W_{n-1}(j,y) + (\mu-\lambda_i-q_i)W_{n-1}(i,y)\Big\},

Wn(i,x)=min⁡y≥xGn(i,y)W_n(i,x) = \min_{y\ge x} G_n(i,y), with limits G∞G_\infty and W∞W_\infty. The myopic level y+(i)y^+(i), the finite-horizon levels yn∗(i)y^*_n(i) and the optimal level y∗(i)y^*(i) are the smallest minimizers of G+(i,⋅)G^+(i,\cdot), Gn(i,⋅)G_n(i,\cdot) and G∞(i,⋅)G_\infty(i,\cdot), and y∞∗(i)=lim⁡nyn∗(i)y^*_\infty(i) = \lim_n y^*_n(i). Throughout, αcˉ<p\alpha\bar c < p (Assumption 1).

The world states carry a partial order ⪯\preceq. The chain is stochastically partial-monotone (display (14)) if for every i⪯ji \preceq j there is a probability space carrying copies of AA started at ii and at jj whose paths satisfy A(t)⪯A′(t)A(t) \preceq A'(t) for all t≥0t \ge 0 almost surely. Condition 1 requires this together with λi\lambda_i nondecreasing in ii.

Formalization targets

Goal: Theorem 8

Under Condition 1, the three families of levels exist and are nondecreasing along ⪯\preceq:

i⪯j ⟹ y+(i)≤y+(j),y∗(i)≤y∗(j),y∞∗(i)≤y∞∗(j).i \preceq j \ \Longrightarrow\ y^+(i) \le y^+(j),\qquad y^*(i) \le y^*(j),\qquad y^*_\infty(i) \le y^*_\infty(j).

Milestones

  • Lemma 8, with its fixed-lead-time form from the proof: D(l)D(l) given A(0)=iA(0)=i is stochastically smaller than given A(0)=jA(0)=j for each l≥0l \ge 0, and DLi≤stDLjD^i_L \le_{st} D^j_L.
  • Lemma 9: ΔC(i,y)≥ΔC(j,y)\Delta C(i,y) \ge \Delta C(j,y) for i⪯ji \preceq j.
  • Theorem 7: for all n≥1n \ge 1 and fixed xx, ΔWn−1(i,x)\Delta W_{n-1}(i,x) and ΔGn(i,x)\Delta G_n(i,x) are nonincreasing in ii, and yn∗(i)y^*_n(i) is nondecreasing in ii.
  • Theorem 9 (companion): if qij≠0q_{ij} \ne 0 only for j⪰ij \succeq i, then y∗(i)=y+(i)y^*(i) = y^+(i), so the myopic policy is optimal.
  • Theorem 10 (companion): with a fixed order cost K>0K > 0, the bounds S+(i)S^+(i), r+(i)r^+(i), r−(i)r^-(i), r−−(i)r^{--}(i) on the optimal (r,S)(r,S) parameters are nondecreasing in ii.

Significance

Theorem 8 turns an optimal policy into a structured one. A world-dependent basestock policy has one level per world state; monotonicity says the levels follow the order of the states, which reduces search, makes the levels interpretable, and gives sanity checks for computed solutions. Theorem 9 identifies when nothing beyond the one-step cost needs to be computed at all. Theorem 10 is the paper's substitute for an open question: the authors could not show that the optimal (r,S)(r,S) parameters are monotone, and instead bound them between monotone functions.

All of these results are proved in the paper. None of them has been machine-checked. The formalization requires a value-iteration argument for a model with unbounded one-period costs, a coupling argument for Markov-modulated Poisson demand, and the passage to the limit in the levels. These are the ingredients of most monotone-policy results in inventory theory with Markov-modulated demand.

Difficulty

The obvious argument fails at the generator. For a single scalar world, stochastic monotonicity is equivalent to the expectation inequality (15) for nondecreasing functions, and the inductive step of Theorem 7 only needs that. For a partial order, the expectation inequality is strictly weaker than the coupling (14) (Massey 1987). The induction must also handle the cross term ∑jqijΔWn−1(j,x)\sum_j q_{ij}\Delta W_{n-1}(j,x), which requires an embedded discrete-time chain whose one-step kernel preserves the order. The paper's Lemma 7 asserts that the embedded chain P=I+Q/νP = I + Q/\nu is monotone for every ν≥q∗\nu \ge q^*. As printed, this is false at ν=q∗\nu = q^*: for two states with q01=q10=1q_{01} = q_{10} = 1, PP swaps the states. A complete proof cannot rely on that lemma as printed.

A second difficulty is that the one-period cost is unbounded. The classical theorems that ordered differences survive value iteration (Denardo, Lovejoy) assume bounded costs, so the induction has to be carried out by hand, and the limits G∞G_\infty, y∞∗y^*_\infty must be justified by Lemma 4's uniform bounds.

Formalization scope

The Lean development lives in the namespace SongZipkinFluct.Monotone. World states form a countable nonempty type with a PartialOrder instance; no linear order is assumed. Inventory positions are integers. The demand-count law fi(d∣l)f_i(d\mid l) and the world transition function P(t)P(t) are defined by uniformization at the model's rate μ\mu, the paper's own device. The lead-time law is a probability measure on [0,∞)[0,\infty), and C(i,y)C(i,y) is the series ∑dgi(d∣α)C^(y−d)\sum_d g_i(d\mid\alpha)\hat C(y-d) of display (16). WnW_n uses an infimum over integers y≥xy \ge x, and W∞W_\infty, G∞G_\infty are suprema over nn, which equal the limits because the sequences are nondecreasing and bounded. Monotonicity in ii is Monotone/Antitone with respect to ⪯\preceq. Smallest minimizers, maxima and minima are IsLeast/IsGreatest characterizations, never sInf on Z\mathbb Z.

Condition 1(a) is encoded as the coupling (14) itself, with one probability space per pair i⪯ji \preceq j and copies identified by their finite-dimensional distributions. Replacing it by the expectation inequality (15), or the partial order by a total order, would change the theorem and is ruled out. Every goal statement asserts the existence of the levels it constrains before constraining them, so no conclusion holds vacuously. The standing hypotheses together with Condition 1 are satisfiable: a one-state instance is checked in Lean.

Lemma 7 is not included because it is false as printed. A guarded version (for instance with ν≥2q∗\nu \ge 2q^*) would be a welcome contribution. Reusable parts include the uniformized Markov-modulated Poisson process, the coupling definition of stochastic monotonicity for a countable partially ordered state space, and the usual stochastic order on N\mathbb N. Proofs of Lemma 9 and Theorem 7 that avoid Lemma 7 are particularly welcome.

Selected references

11 thms1 active userReviewed
Dynamic ProgrammingOperations ResearchOptimization·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 ii belongs to a nonempty countable set II. The world evolves according to a conservative continuous-time Markov generator Q=(qij)Q=(q_{ij}), with exit rate qi=−qiiq_i=-q_{ii}. When the world is in state ii, customers demand individual units at rate λi≥0\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∈Zx\in\mathbb Z, which includes outstanding orders, and chooses an order-up-to position y≥xy\ge x.

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

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

C(i,y)=E[e−αLC^(y−DLi)],G+(i,y)=(1−γ)cy+βC(i,y),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 μ>0\mu>0 is a uniformization rate at least sup⁡iqi+sup⁡iλi\sup_iq_i+\sup_i\lambda_i, β=(μ+α)−1\beta=(\mu+\alpha)^{-1}, and γ=βμ\gamma=\beta\mu. The paper's Assumption 1, αcˉ<p\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 ii is y+(i)y^+(i), and ymin⁡+=min⁡iy+(i)y^+_{\min}=\min_i y^+(i).

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

Formalization targets

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

0≤ymin⁡+≤y∗(i)≤y∞∗(i)≤y+(i),G∞(i,y∞∗(i))=min⁡z∈ZG∞(i,z).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∞∗(i)y^*_\infty(i) is the limit of the smallest finite-stage minimizers yn∗(i)y^*_n(i). Theorem 2(e) then asserts that π(y∗)\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=0K=0 and W0=0W_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 thms1 active userReviewed
Dynamic ProgrammingOperations ResearchProbability·Captain: mikedeng1

Some Monotonicity Results for Partially Observed Markov Decision Processes: MLR-Monotone Optimal Values and the Myopic Policy as a Lower Bound on the Optimal PolicyResearch Paper

Motivation

A partially observed Markov decision process (POMDP) models a controller that cannot see the state of the system it controls. It sees only noisy observations, and so it acts on a belief: a probability vector over the hidden states. Machine maintenance, medical screening, quality control and search problems all have this form. The dynamic program of a POMDP lives on the simplex of beliefs, a continuum, so computing exact optimal policies is expensive even when the state, action and observation sets are small. Structural results reduce that cost. A value function that is monotone in the belief, or a policy known to dominate a cheap reference policy, shrinks the space a computation must search. Such results also explain the model: they say when one belief is "better" than another.

W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes (Operations Research 35(5):736–743, 1987), provides such results by ordering beliefs with the monotone likelihood ratio (MLR) order instead of first-order stochastic dominance.

Timeline. Smallwood and Sondik (1973) set out the finite POMDP and its piecewise-linear value functions. White (1979, 1980) obtained monotone policies and values for machine replacement, for single-stage problems, and for the completely observed and completely unobserved extremes, all under first-order stochastic dominance. Albright (1979) treated the two-state case, where the usual orders coincide. Whitt (1979, 1982) developed the likelihood-ratio orders and showed that they are preserved by Bayesian updating. Lovejoy (1987) combined these into general monotonicity results for finite POMDPs, and the MLR order has since become the standard tool for structural results in POMDPs.

Setting

Let S={1,…,n}S=\{1,\dots,n\} (states) and O={1,…,m}O=\{1,\dots,m\} (observations) carry their natural orders, and let AA be a finite, completely ordered action set. For a finite chain XX, Π(X)\Pi(X) is the set of probability vectors on XX. For π,π′∈Π(X)\pi,\pi'\in\Pi(X), π≥sπ′\pi\ge_s\pi' (first-order stochastic dominance) means ∑i≥qπi≥∑i≥qπi′\sum_{i\ge q}\pi_i\ge\sum_{i\ge q}\pi'_i for every qq. π≥rπ′\pi\ge_r\pi' (MLR order) means πiπi′′≥πi′πi′\pi_i\pi'_{i'}\ge\pi_{i'}\pi'_i whenever i≥i′i\ge i'. For matrices f,gf,g on X×YX\times Y, f≥tpgf\ge_{tp}g means f(x∨x′,y∨y′) g(x∧x′,y∧y′)≥f(x,y) g(x′,y′)f(x\vee x',y\vee y')\,g(x\wedge x',y\wedge y')\ge f(x,y)\,g(x',y') for all pairs, and ff is TP₂ if f≥tpff\ge_{tp}f.

In each period the decision maker in state st=is_t=i chooses a∈Aa\in A and receives the reward g(i,a)g(i,a). The state moves to jj with probability pijap^a_{ij} (matrix PaP^a), and an observation kk arrives with probability rjkar^a_{jk} (matrix RaR^a, with row ra(j)∈Π(O)r^a(j)\in\Pi(O)), generated by the new state jj and the action aa. The paper assumes rjka>0r^a_{jk}>0 throughout. The discount factor is β≥0\beta\ge 0. From a belief π\pi, the observation kk has probability σ(k;π,a)=∑i,jπipijarjka\sigma(k;\pi,a)=\sum_{i,j}\pi_i p^a_{ij}r^a_{jk}, and the posterior is the Bayes update Tj(π,a,k)=∑iπipijarjka/σ(k;π,a)T_j(\pi,a,k)=\sum_i\pi_ip^a_{ij}r^a_{jk}/\sigma(k;\pi,a). With

h(π,a,V)=∑iπig(i,a)+β∑kσ(k;π,a) V(T(π,a,k)),h(\pi,a,V)=\sum_{i}\pi_i g(i,a)+\beta\sum_{k}\sigma(k;\pi,a)\,V(T(\pi,a,k)),

a finite horizon NN with salvage value gsg_s gives the optimal values VN+1∗(π)=∑iπigs(i)V^*_{N+1}(\pi)=\sum_i\pi_ig_s(i) and Vt∗(π)=max⁡ah(π,a,Vt+1∗)V^*_t(\pi)=\max_a h(\pi,a,V^*_{t+1}). For N=∞N=\infty and 0<β<10<\beta<1, V∗V^* is the bounded solution of V∗(π)=max⁡ah(π,a,V∗)V^*(\pi)=\max_a h(\pi,a,V^*). The myopic actions are α(π)=argmax⁡a∑iπig(i,a)\alpha(\pi)=\operatorname{argmax}_a\sum_i\pi_ig(i,a).

Formalization targets

Goal: Proposition 2 (myopic lower bound)

Under (a) gsg_s nondecreasing, (b) g(⋅,a)g(\cdot,a) nondecreasing, (c) Pa≥tpPa′P^a\ge_{tp}P^{a'} for a≥a′a\ge a', (d) ra(j)≥rra(j′)r^a(j)\ge_r r^a(j') for j≥j′j\ge j', (e) ra(j)≥sra′(j)r^a(j)\ge_s r^{a'}(j) for a≥a′a\ge a', and (f) rjkarj′ka′≥rjka′rj′kar^a_{jk}r^{a'}_{j'k}\ge r^{a'}_{jk}r^a_{j'k} for a≥a′a\ge a', j≥j′j\ge j': for every t≤Nt\le N (finite horizon), or for the infinite horizon with 0<β<10<\beta<1, and every π∈Π(S)\pi\in\Pi(S),

∀ δ∗(π) ∃ α(π)≤δ∗(π),∀ α(π) ∃ δ∗(π)≥α(π),\forall\,\delta^*(\pi)\ \exists\,\alpha(\pi)\le\delta^*(\pi),\qquad \forall\,\alpha(\pi)\ \exists\,\delta^*(\pi)\ge\alpha(\pi),

where δ∗(π)\delta^*(\pi) ranges over the maximizers of a↦h(π,a,Vt+1∗)a\mapsto h(\pi,a,V^*_{t+1}) (resp. h(π,a,V∗)h(\pi,a,V^*)).

Milestone: Proposition 1 (MLR-monotone values)

Under (a)–(d) with every PaP^a TP₂: π≥rπ′\pi\ge_r\pi' in Π(S)\Pi(S) implies Vt∗(π)≥Vt∗(π′)V^*_t(\pi)\ge V^*_t(\pi') for t=1,…,N+1t=1,\dots,N+1, and, without (a), V∗(π)≥V∗(π′)V^*(\pi)\ge V^*(\pi') for N=∞N=\infty.

Supporting milestones

The ordering facts behind both propositions: MLR implies stochastic dominance (§1), Lemma 1.1 (characterization of ≥s\ge_s), Lemma 1.3 (TP₂ prediction preserves ≥r\ge_r), Lemma 1.2 (the Bayes update is MLR-monotone in the observation, the prior and the action), the stochastic monotonicity of σ\sigma in the belief (proof of Proposition 1) and in the action (Lemma 2.3), the comparison of hh-increments with myopic increments (proof of Proposition 2), and Lemma 2.2 (dominated increments order maximizer sets).

Significance

The result. Proposition 2 makes the myopic policy, which solves a one-stage problem, a lower bound on an optimal policy for every belief and every period. In a search over policies, actions below α(π)\alpha(\pi) can be discarded. When gg also has isotone differences, α\alpha is nondecreasing, and the optimal policy is bounded below by a monotone function that is easy to compute. Proposition 1 gives MLR-monotone value functions, the input to many later structural results for POMDPs. Lemma 1.2 records the fact behind it: Bayesian updating respects the MLR order, while first-order stochastic dominance does not survive conditioning.

Formalizing it. These results are proved on paper. This mission produces machine-checked proofs, together with a reusable finite-POMDP layer (belief update, observation probabilities, Bellman operator, finite- and infinite-horizon values) and a library of the stochastic orders on finite chains. One statement in the paper is wrong: the printed "only if" direction of Lemma 1.2(1) is false. The mission states only the direction that is true and used.

Difficulty

The obvious induction on tt for Proposition 1 needs k↦V(T(π,a,k))k\mapsto V(T(\pi,a,k)) to be nondecreasing and σ(π,a)\sigma(\pi,a) to increase with π\pi. Both need a belief order that conditioning preserves. Under first-order stochastic dominance the posterior is not monotone in the prior, and the paper's counterexample (p. 740) shows that the induction then fails. The MLR order repairs this, but proving that the prediction step preserves it (Lemma 1.3) requires a total-positivity composition argument (Karlin–Rinott, Theorem 2.4) on product lattices. For Proposition 2 the difficulty is to compare continuation values across actions: the observation distribution and the posterior both change with the action, and two separate orderings (Lemma 2.3 and Lemma 1.2(3)) must be combined before the maximizer comparison applies. The infinite-horizon parts additionally need the Bellman fixed point characterized well enough to pass monotonicity to the limit.

Formalization scope

Everything is finite, so all probabilities and expectations are finite sums and no measure theory is involved. States, observations and actions are finite nonempty types with a LinearOrder (any finite chain is isomorphic to {1,…,n}\{1,\dots,n\}). Π(X)\Pi(X) is Mathlib's stdSimplex ℝ X. The orders ≥s,≥r,≥tp\ge_s,\ge_r,\ge_{tp} are plain relations (StochGE, MLRGE, TPGE) with the larger argument first, and every statement assumes simplex membership explicitly. The standing assumptions (stochastic rows of PaP^a and RaR^a, rjka>0r^a_{jk}>0, β≥0\beta\ge0) are fields of the structure POMDP. Vt∗V^*_t is computed by recursion (3) counted in steps to go, Vstar gs N t = valueToGo gs (N+1-t). The infinite-horizon V∗V^* is any function bounded on Π(S)\Pi(S) that solves the Bellman equation there. For 0<β<10<\beta<1 such a function exists and is unique on Π(S)\Pi(S), by contraction. The equivalence between recursion (3) and the optimum over history-dependent strategies is cited by the paper from the literature and is not part of this mission. Maximizer sets (argmaxSet) carry the "for all δ∗\delta^* / there exists α\alpha" quantifiers. Both halves of each part of Proposition 2 are ∀∃\forall\exists statements.

The goal is not to be read with Vt+1∗V^*_{t+1} or V∗V^* replaced by an arbitrary, or an arbitrary nondecreasing, value function. That reading would reduce Proposition 2 to Lemma 2.2 plus a hypothesis. The goal quantifies only over the value functions of recursion (3) and over bounded Bellman solutions.

A complete development needs finite total-positivity composition (Mathlib's four functions theorem is the natural starting point), Abel summation for Lemma 1.1, and a contraction argument for the infinite horizon. The order library and the finite POMDP layer are reusable beyond this paper. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1.3.

Selected references

  • W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes, Operations Research 35(5):736–743, 1987. https://doi.org/10.1287/opre.35.5.736
  • R. D. Smallwood and E. J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
  • W. Whitt, A Note on the Influence of the Sample on the Posterior Distribution, Journal of the American Statistical Association 74:424–426, 1979.
  • W. Whitt, Multivariate Monotone Likelihood Ratio and Uniform Conditional Stochastic Order, Journal of Applied Probability 19:695–701, 1982.
  • S. Karlin and Y. Rinott, Classes of Orderings of Measures and Related Correlation Inequalities. I. Multivariate Totally Positive Distributions, Journal of Multivariate Analysis 10(4):467–498, 1980. https://doi.org/10.1016/0047-259X(80)90065-2
  • C. White, Optimal Control-limit Strategies for a Partially Observed Replacement Problem, International Journal of Systems Science 10:321–331, 1979 (the machine-replacement model of §5).
  • S. C. Albright, Structural Results for Partially Observable Markov Decision Processes, Operations Research 27(5):1041–1053, 1979. https://doi.org/10.1287/opre.27.5.1041
16 thms1 active userReviewed
ProbabilityStochastic Systems·Captain: mikedeng1

On the Generalized “Birth-and-Death” Process 1: For Rates λ(t), μ(t) ≥ 0 the Population Size Is Geometric with a Modified Zero Term, ξ_t = 1 − e^{−ρ}/W, η_t = 1 − 1/WResearch Paper

Motivation

Population models often allow each individual to produce a new individual or die at rates that change over time. Seasonal conditions, exposure to an epidemic, and changing conditions in a laboratory population all make a constant rate a restrictive assumption. In Kendall's 1948 paper, the question is how the entire distribution of the population size evolves when the per-individual birth and death rates are prescribed functions of time. The distribution matters even when its mean is known: a population can have a stable expected size while still having a substantial chance of extinction. Kendall presents the varying-rate model as a generalization of the constant-rate process discussed by Feller in 1939 (Kendall 1948, §1).

This mission concerns Kendall's solution for a population descended from one ancestor. It includes the explicit distribution, the forward equations that connect it to the birth and death model, and the formulas for its mean, variance, and chance of eventual extinction. The paper has no numbered theorems; its results are identified here by its equation numbers and printed pages.

Setting

At time t≥0t\ge0, let ntn_t be the number of individuals. Each individual gives birth at instantaneous rate λ(t)\lambda(t) and dies at rate μ(t)\mu(t), so a population of size nn moves to n+1n+1 at rate nλ(t)n\lambda(t) and to n−1n-1 at rate nμ(t)n\mu(t). Both rates are nonnegative. The initial state is n0=1n_0=1. Write Pn(t)P_n(t) for the probability that nt=nn_t=n. The forward equations in §2, (2)–(4), p. 2 are

P0′(t)=μ(t)P1(t),Pn′(t)=(n+1)μ(t)Pn+1(t)+(n−1)λ(t)Pn−1(t)−n(λ(t)+μ(t))Pn(t)(n≥1).P_0'(t)=\mu(t)P_1(t),\qquad P_n'(t)=(n+1)\mu(t)P_{n+1}(t)+(n-1)\lambda(t)P_{n-1}(t) -n(\lambda(t)+\mu(t))P_n(t)\quad(n\ge1).

The formula for P0′P_0' reflects that a population already at zero cannot reproduce. The n−1n-1 term vanishes at n=1n=1, as it must. The model is expressed through these real-valued probability functions; it does not require a sample-space construction of a stochastic process.

Define the integrated rate difference ρ(t)\rho(t) and the function W(t)W(t) by §2, (10a)–(11), p. 4:

ρ(t)=∫0t(μ(τ)−λ(τ)) dτ,W(t)=e−ρ(t)(1+∫0teρ(τ)μ(τ) dτ).\rho(t)=\int_0^t(\mu(\tau)-\lambda(\tau))\,d\tau,\qquad W(t)=e^{-\rho(t)}\left(1+\int_0^t e^{\rho(\tau)}\mu(\tau)\,d\tau\right).

Set ξt=1−e−ρ(t)/W(t)\xi_t=1-e^{-\rho(t)}/W(t) and ηt=1−1/W(t)\eta_t=1-1/W(t). Kendall's modified-zero geometric law is P0(t)=ξtP_0(t)=\xi_t and Pn(t)=(1−ξt)(1−ηt)ηtn−1P_n(t)=(1-\xi_t)(1-\eta_t)\eta_t^{n-1} for n≥1n\ge1. The zero state has its own mass; the positive states form a geometric tail. For the nonnegative rates in this mission, W(t)≥1W(t)\ge1 and 0≤ηt<10\le\eta_t<1 on t≥0t\ge0, so the displayed formulas have their ordinary probabilistic meaning.

Formalization targets

The geometric transient law

The goal is the full claim of §2, (8), (10a)–(12), pp. 3–4: the explicit Pn(t)P_n(t) starts from one ancestor, is nonnegative and sums to one for every t≥0t\ge0, and satisfies the forward equations above. In symbols, the distribution part is

P0(t)=ξt,Pn(t)=(1−ξt)(1−ηt)ηtn−1 (n≥1),∑n=0∞Pn(t)=1.P_0(t)=\xi_t,\qquad P_n(t)=(1-\xi_t)(1-\eta_t)\eta_t^{n-1}\ (n\ge1),\qquad \sum_{n=0}^{\infty}P_n(t)=1.

The milestones record the paper's intermediate statements in reading order: the rational generating function ϕ(z,t)\phi(z,t) in (9); the pair of equations for ξ\xi and η\eta obtained from the generating-function equation (6); the equations for U=1−ξU=1-\xi and V=1−ηV=1-\eta; the differential equation and integral representation of WW; the alternate formulas (10b)–(10c); and the explicit expressions (12). Each is a statement made in the source, with the page and equation displayed beside its milestone.

Extinction and moments

The companion target from §3, (18)–(19), p. 6 writes J(t)=∫0teρ(τ)μ(τ) dτJ(t)=\int_0^t e^{\rho(\tau)}\mu(\tau)\,d\tau and states

P0(t)=J(t)1+J(t),P0(t)⟶1 ⟺ J(t)⟶+∞.P_0(t)=\frac{J(t)}{1+J(t)},\qquad P_0(t)\longrightarrow1\ \Longleftrightarrow\ J(t)\longrightarrow+\infty.

When J(t)J(t) has finite limit II, the limiting extinction chance is I/(1+I)I/(1+I). Companion statements also retain the mean nˉt=e−ρ(t)\bar n_t=e^{-\rho(t)}, all three expressions for the variance in (14c), the criterion that extinction has zero chance exactly when μ\mu vanishes identically, and the necessary divergence of ∫0∞μ\int_0^\infty\mu for almost-sure extinction (Kendall 1948, pp. 4, 6–7).

Significance

The geometric law supplies every finite-time population probability from the rate functions. Its zero mass yields an extinction probability without taking limits of an unspecified process, while its first two moments quantify expected growth and fluctuations. The extinction criterion distinguishes a population that dies out with probability one from one that retains a positive chance of survival even when its eventual mean behavior is simple. The variance formulas give later sections of Kendall's paper a way to compare rate schedules with the same expected population (§§3, 6).

The result was proved in the 1948 paper. The work here is to state its model and conclusions precisely in Lean, preserving the initial condition, normalization, boundary state, and time-dependent rate conventions. The current files are theorem statements with proof placeholders; a successful build checks their syntax and types, not the mathematical proofs. Once proved, the definitions and the moment and extinction statements can also support formal work on time-dependent branching and population models.

Difficulty

Knowing the expected population is insufficient to determine the distribution. The forward equation for each PnP_n couples it to both neighboring states, producing an infinite system. A direct finite truncation would change the birth rate at its upper boundary and would therefore no longer be Kendall's model. The zero state also behaves differently from positive states: a purely geometric law on all n≥0n\ge0 does not capture its mass. The generating function has a rational form, but its time dependence must still agree with the forward system for every state and with a normalized probability law. The extinction statement adds an improper integral, whose finite and divergent regimes require distinct limits.

Formalization scope

Lean represents λ,μ:R→R\lambda,\mu:\mathbb R\to\mathbb R as continuous functions that are nonnegative for t≥0t\ge0. The paper calls the rates specified functions and assumes their nonnegativity; global continuity is an explicit convenience for the two-sided derivatives and interval integrals. Only nonnegative time appears in the probabilistic statements. The oriented intervalIntegral from zero to tt represents every finite integral. HasDerivAt expresses each derivative, and HasSum expresses both normalization and the moment and generating-function series. The law lives on natural-number states, with P0P_0 handled separately. The coefficient at state n=1n=1 is the real number n−1n-1, not an implicit extension to a negative state.

The positivity of WW on nonnegative time must follow from the rates. The definitions are total Lean real functions, so a result that relies on a division states the hypotheses that keep its denominator nonzero. The limit J(t)→+∞J(t)\to+\infty expresses divergence of the paper's improper integral. No uniqueness of solutions to the forward equations is included, because the cited passage does not establish that claim. The goal requires the explicit law to solve the forward equations and to be a probability law; merely expanding its generating function would leave the population model unformalized. Contributions that prove the formulas, establish the required positivity and convergence facts, or develop reusable lemmas for time-dependent linear birth and death equations all fit the scope.

Selected references

  • D. G. Kendall, On the generalized “birth-and-death” process, Annals of Mathematical Statistics 19(1), 1–15, 1948. DOI: 10.1214/aoms/1177730285.
8 thms1 active userReviewed
ProbabilityStochastic Systems·Captain: mikedeng1

Ergodic Theorems for Weakly Interacting Infinite Systems and the Voter Model: The Discrete-Time Proximity Process Is Dual to the Branching Process with InterferenceResearch Paper

Motivation

Many models in probability, statistical physics and the theory of stochastic networks are interacting particle systems: infinitely many sites, each in state 0 or 1, each updating at random according to the states of a few other sites. A basic question about such a system is ergodicity: does it have a unique stationary distribution, and does its law converge to it from every initial configuration? For infinite systems the question is hard, because the state space {0,1}I\{0,1\}^I is uncountable and standard Markov chain arguments do not apply.

Holley and Liggett (Ann. Probab. 3 (1975), 643–663) introduced a class of such systems, the proximity processes, which arise from a coupling of more general weakly interacting systems (the settings of Vasershtein (1969), Dobrushin (1971) and Chover (1974)), and showed that each proximity process is dual to a process of finite sets, the branching process with interference. Duality turns a question about an infinite-dimensional process into a question about a process whose states are finite sets. The paper uses it to give short proofs of ergodicity criteria and, in its §5, to study the invariant measures of the voter model. Duality of this kind became one of the main tools of the field; see Liggett, Interacting Particle Systems (Springer, 1985).

This mission formalizes the discrete-time half of the paper: the duality theorem (1.6) and its first applications, Corollary (3.1) and Corollary (4.1).

Setting

Let II be a countable set of sites and S={0,1}IS=\{0,1\}^I the set of configurations η:I→{0,1}\eta:I\to\{0,1\}, with the product σ\sigma-algebra. For η∈S\eta\in S, C(η)={i∈I:η(i)=1}C(\eta)=\{i\in I:\eta(i)=1\} is the set of occupied sites.

The data of the model are, for each site ii, a sequence Ni,0=∅,Ni,1,Ni,2,…N_{i,0}=\emptyset,N_{i,1},N_{i,2},\dots of finite subsets of II and a probability distribution fif_i on {0,1,2,… }\{0,1,2,\dots\}.

The proximity process ηn\eta_n is the Markov chain on SS whose transition function is the product measure

Q(η,⋅)=∏i∈Iνα(i,η),i,α(i,η)=∑k: Ni,k∩C(η)≠∅fi(k),Q(\eta,\cdot)=\prod_{i\in I}\nu_{\alpha(i,\eta),i},\qquad \alpha(i,\eta)=\sum_{k:\,N_{i,k}\cap C(\eta)\neq\emptyset}f_i(k),

where νρ,i\nu_{\rho,i} puts mass ρ\rho on 11. In words: each site ii independently picks an index kk with probability fi(k)f_i(k) and becomes 11 exactly when the set Ni,kN_{i,k} contains an occupied site. Pη(ηn∈⋅)P_\eta(\eta_n\in\cdot) denotes the law at time nn started from η\eta.

The branching process with interference (b.p.i.) AnA_n is the Markov chain on the collection T\mathcal T of finite subsets of II with transition function

Q~(A,B)=∑′∏i∈Afi(ki),\tilde Q(A,B)=\sum{}'\prod_{i\in A}f_i(k_i),

the sum over all sequences (ki)i∈A(k_i)_{i\in A} with ⋃i∈ANi,ki=B\bigcup_{i\in A}N_{i,k_i}=B: each particle at ii splits into particles on Ni,kN_{i,k} with probability fi(k)f_i(k), and particles landing on the same site merge. PFP_F denotes probabilities for the chain started at FF.

For F∈TF\in\mathcal T, B(F)={η∈S:η(i)=0 for all i∈F}B(F)=\{\eta\in S:\eta(i)=0\ \text{for all } i\in F\}.

Formalization targets

Goal: Theorem (1.6)

For all n≥0n\ge0, η∈S\eta\in S and F∈TF\in\mathcal T,

Pη(ηn∈B(F))=PF(An∩C(η)=∅).P_\eta(\eta_n\in B(F))=P_F(A_n\cap C(\eta)=\emptyset).

Milestones

The proof is an induction on nn whose steps are four displayed identities on p. 647:

  1. (2.3) the one-step law of the proximity process on B(F)B(F): Pη(η1∈B(F))=∑′∏i∈Ffi(ki)P_\eta(\eta_1\in B(F))=\sum'\prod_{i\in F}f_i(k_i), the sum over sequences with Ni,ki∩C(η)=∅N_{i,k_i}\cap C(\eta)=\emptyset for all i∈Fi\in F;
  2. (2.4) the same expression for PF(A1∩C(η)=∅)P_F(A_1\cap C(\eta)=\emptyset);
  3. (2.5) the first-step decomposition PF(An+1∩C(η)=∅)=∑(ki)P⋃i∈FNi,ki(An∩C(η)=∅)∏i∈Ffi(ki)P_F(A_{n+1}\cap C(\eta)=\emptyset)=\sum_{(k_i)}P_{\bigcup_{i\in F}N_{i,k_i}}(A_n\cap C(\eta)=\emptyset)\prod_{i\in F}f_i(k_i);
  4. (2.8) the last-step decomposition Pη(ηn+1∈B(F))=∑(ki)Pη(ηn∈B(⋃i∈FNi,ki))∏i∈Ffi(ki)P_\eta(\eta_{n+1}\in B(F))=\sum_{(k_i)}P_\eta(\eta_n\in B(\bigcup_{i\in F}N_{i,k_i}))\prod_{i\in F}f_i(k_i).

Applications

  • Corollary (3.1): if ∑k∣Ni,k∣fi(k)≤λ<1\sum_k|N_{i,k}|f_i(k)\le\lambda<1 for all ii, then
Pη(ηn∈B(F))≥1−λn∣F∣,P_\eta(\eta_n\in B(F))\ge1-\lambda^n|F|,

and the point mass on the all-zero configuration is the only stationary distribution; along the way, (3.5): PF(An≠∅)≤EF∣An∣≤λn∣F∣P_F(A_n\neq\emptyset)\le E_F|A_n|\le\lambda^n|F|.

  • (4.5): for the §4 model on Z\mathbb Z, PF∪G(At≠∅)≤PF(At≠∅)+PG(At≠∅)−PF∩G(At≠∅)P_{F\cup G}(A_t\neq\emptyset)\le P_F(A_t\neq\emptyset)+P_G(A_t\neq\emptyset)-P_{F\cap G}(A_t\neq\emptyset).
  • Corollary (4.1): on I=ZI=\mathbb Z with Ni,1={i−1,i+1}N_{i,1}=\{i-1,i+1\}, fi(0)=1−λf_i(0)=1-\lambda, fi(1)=λf_i(1)=\lambda, and h(λ)=2λ+2λ2−7λ3+5λ4−λ5h(\lambda)=2\lambda+2\lambda^2-7\lambda^3+5\lambda^4-\lambda^5,
Pη(ηt∈B(F))≥1−[h(λ)](t−1)/2∣F∣(t≥1).P_\eta(\eta_t\in B(F))\ge1-[h(\lambda)]^{(t-1)/2}|F|\qquad(t\ge1).

Significance

The duality identity expresses every finite-dimensional "all vacant" probability of the proximity process, which determine its law, through a chain on finite sets. Consequences in the paper: a sufficient condition for convergence to the all-zero configuration (Corollary (3.1)), which in the nearest-neighbour example on Z\mathbb Z gives λ<12\lambda<\tfrac12; the sharper range h(λ)<1h(\lambda)<1, i.e. λ<0.6527\lambda<0.6527, for that example (Corollary (4.1)), which the interference term makes possible; and, in continuous time, the analysis of the invariant measures of the voter model.

The results are classical and proved; a search of Prove2Me and Mathlib found no machine-checked proof of any of them. A formalization contributes a Lean model of an infinite-product Markov kernel on {0,1}I\{0,1\}^I with its nn-step laws, a model of a set-valued branching chain, and the duality between them, which are reusable for other duality arguments (contact process, voter model, coalescing random walks).

Difficulty

The two sides of (1.7) are defined independently and live on different spaces. The left side is the time-nn law of a chain on the uncountable space {0,1}I\{0,1\}^I, obtained by iterating an infinite product kernel; the right side comes from a transition matrix on the countable set of finite subsets of II, whose entries are themselves infinite sums over sequences indexed by a finite set. Neither side can be computed in closed form beyond n=1n=1, so no direct evaluation proves the identity for general nn.

Two technical points stand in the way of a naive argument. Evaluating a product kernel on a cylinder event and integrating it against a previous law requires the kernel to be measurable in η\eta, a statement about cylinder sets of an infinite product that a hand proof passes over. And the natural recursion for nn-step probabilities of the b.p.i. adds the new step at the end, while the comparison with the proximity process needs information about the first step; the two orders agree only by a Chapman–Kolmogorov argument over a countable state space with [0,∞][0,\infty]-valued sums. Corollary (4.1) further needs quantitative estimates of survival probabilities for specific initial sets on Z\mathbb Z.

Formalization scope

All objects are in the namespace HolleyLiggett.Duality, in one definitions file.

  • {0,1}\{0,1\} is Bool (true = 1), SS is Config I := I → Bool with the product σ\sigma-algebra, T\mathcal T is Finset I.
  • Standing assumptions on every theorem: [Countable I], N : I → ℕ → Finset I (finite sets) with N i 0 = ∅, and f : I → PMF ℕ (probability distributions). A finite collection Ni,0,…,Ni,mN_{i,0},\dots,N_{i,m} is the case fi(k)=0f_i(k)=0 for k>mk>m.
  • The kernel (1.1) is Measure.infinitePi of the two-point measures; the nn-step law is proxLaw, iterating Measure.bind from the point mass at η\eta. Measurability of the kernel is a true fact that solvers must prove; it is not assumed.
  • The b.p.i. nn-step probabilities bpiProb follow the last-step recursion PF(An+1=B)=∑GPF(An=G)Q~(G,B)P_F(A_{n+1}=B)=\sum_GP_F(A_n=G)\tilde Q(G,B). All probabilities are in ℝ≥0∞, and each ∑′\sum' over sequences is an unconditional sum over ↥F → ℕ.
  • The page's "η(1)=1\eta(1)=1" in (1.2) is read as η(i)=1\eta(i)=1. Corollary (4.1) carries the added hypothesis t≥1t\ge1: at t=0t=0 the printed bound fails when h(λ)>1h(\lambda)>1, and the proof starts at t=1t=1. Inequality (4.5) uses the §4 model on Z\mathbb Z, with the subtracted term moved across.
  • The goal relates the two chains defined by (1.1) and (1.4). A statement through the coupling Xi,nX_{i,n} of the proof, about an arbitrary process with the right one-step behaviour, or for n=1n=1 only, is not the theorem.

The continuous-time duality (Theorem (2.12)), Corollaries (3.9) and (4.15) and the voter model of §5 are out of scope. Contributions welcome: the measurability and probability facts for proxStep, Chapman–Kolmogorov for bpiProb, and proofs of the milestones.

Selected references

  • R. A. Holley and T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, Ann. Probab. 3(4) (1975), 643–663. https://doi.org/10.1214/aop/1176996306
  • T. M. Liggett, Interacting Particle Systems, Grundlehren der mathematischen Wissenschaften 276, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
  • R. L. Dobrushin, Markov processes with a large number of locally interacting components (Russian), Problems of Information Transmission 7(2) (1971), 70–87 (as cited by Holley and Liggett).
  • O. N. Stavskaya and I. I. Pyatetskii-Shapiro, On homogeneous nets of spontaneously active elements, Systems Theory Research 20 (1971), 75–88 (as cited by Holley and Liggett).
  • L. N. Vasershtein, Processes over denumerable products of spaces, describing large systems, Problems of Information Transmission 3 (1969), 47–52 (as cited by Holley and Liggett).
6 thms1 active userReviewed
Dynamic ProgrammingOperations Research·Captain: mikedeng1

Denumerable State Markovian Decision Processes—Average Cost Criterion: Every Limit Point of Policy Improvement Is a Deterministic Stationary Rule That Is Optimal over All RulesResearch Paper

Motivation

Markovian decision processes with the long-run average cost criterion model systems run indefinitely: inventories, queues, maintenance schedules, communication links. For a finite state space the theory was settled by the early 1960s. Howard's policy improvement (policy iteration) procedure (1960) finds an optimal stationary rule in finitely many steps, and Gillette (1957) and Derman (1962) showed that a stationary deterministic rule is optimal over all rules, history-dependent and randomized included (Derman 1962).

Many models of interest, such as queues with unbounded buffers and inventories with unbounded backlog, have a denumerable state space, and there the finite theory breaks down. Derman's paper (Ann. Math. Statist. 37 (1966) 1545–1553) gives two counterexamples in §2, both under bounded costs and finitely many decisions per state. In the first, due to Maitra, no optimal rule exists. In the second, a randomized stationary rule beats every deterministic one. It then gives sufficient conditions under which a stationary deterministic optimal rule exists and policy improvement finds it.

Timeline:

  • 1960: Howard introduces policy iteration for finite average-cost problems.
  • 1962: Derman proves that deterministic stationary rules are optimal for finite state spaces; Blackwell develops the finite discounted and near-discount theory.
  • 1963–1965: Iglehart (inventory) and Taylor (replacement) treat the average cost criterion in special infinite-state models; Derman's §3 proof follows part of Iglehart's argument.
  • 1964–1965: Blackwell, Maitra, Strauch and Derman (J. Math. Anal. Appl. 1965) treat infinite state spaces under the discounted criterion, where with Ki<∞K_i < \infty and bounded costs an optimal rule of C′′C'' always exists.
  • 1966: Derman (this paper) gives the bounded-solution verification theorem and the convergence of policy improvement on a denumerable state space.
  • 1967 onward: Derman and Veinott (announced in §5 of this paper), and later Ross, Sennott, and Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (1993), give conditions for the existence of solutions of the optimality equation.

Setting

The system is observed at times t=0,1,2,…t = 0, 1, 2, \dots in a state YtY_t of a denumerable set II. At state ii one of Ki<∞K_i < \infty decisions kk is made (condition (A)). It costs wikw_{ik}, and the next state is jj with probability qij(k)q_{ij}(k). The costs are bounded (condition (B)) and may have either sign. A rule RR chooses the decision at each time with probabilities that may depend on the whole history. The class of all rules is CC, and C′′C'' is the class of stationary deterministic rules ("make decision kik_i at state ii"). The average cost of RR from Y0=iY_0 = i is

QR(i)=lim sup⁡T→∞1T+1∑t=0TERWt,Wt=wYtΔt.Q_R(i) = \limsup_{T\to\infty} \frac{1}{T+1}\sum_{t=0}^{T} E_R W_t, \qquad W_t = w_{Y_t \Delta_t}.

A rule is optimal over CC if QR(i)≤QR′(i)Q_R(i) \le Q_{R'}(i) for every R′∈CR' \in C and every ii.

The optimality equation (1) asks for a number gg and a bounded {vj}\{v_j\} with

g+vi=min⁡k{wik+∑j∈Iqij(k)vj},i∈I,g + v_i = \min_k \Big\{w_{ik} + \sum_{j\in I} q_{ij}(k) v_j\Big\}, \qquad i \in I,

and equation (2) is its version for one rule R∈C′′R \in C'', with kik_i in place of the minimum. Condition (C): every R∈C′′R \in C'' induces an irreducible Markov chain all of whose states are positive recurrent. Condition (E): every R∈C′′R \in C'' has a solution {gR,vjR}\{g^R, v^R_j\} of (2), bounded uniformly in jj and RR. Condition (F): for every jj the Cesàro limits πij(R)\pi_{ij}(R) of P{Yt=j∣Y0=i}P\{Y_t = j \mid Y_0 = i\} satisfy inf⁡R∈C′′,i∈Iπij(R)>0\inf_{R\in C'', i \in I} \pi_{ij}(R) > 0. One policy improvement iteration replaces RR by a rule R′R' whose decisions minimize wik+∑jqij(k)vjRw_{ik} + \sum_j q_{ij}(k) v_j^R at every state.

Formalization targets

Goal: Theorem 4

Under (A), (B), (C), (E) and (F), let R1,R2,…R_1, R_2, \dots be any sequence of policy improvement iterations from an arbitrary R1∈C′′R_1 \in C''. Then the sequence has a limit point R∗∈C′′R^* \in C'', and every limit point satisfies

QR∗(i)≤QR(i)for all R∈C, i∈I,Q_{R^*}(i) \le Q_R(i) \qquad \text{for all } R \in C,\ i \in I,

with gRn→QR∗(i)g^{R_n} \to Q_{R^*}(i).

Milestones

  • Display (4): a rule of C′′C'' solving (2) with bounded vv has QR≡gQ_R \equiv g, the limit existing.
  • Display (6): a bounded solution of (1) gives ∣gn(i)−ng−vi∣≤M|g_n(i) - ng - v_i| \le M for the value iteration gng_n of (5).
  • §3: gn(i)g_n(i) is the least expected cost over the periods 0,…,n0, \dots, n among all rules.
  • Theorem 1: a bounded solution of (1) makes every minimizing rule R∗∈C′′R^* \in C'' optimal over CC, with QR∗≡gQ_{R^*} \equiv g.
  • Lemma 1 and the remark after it: a strict improvement at a nonempty set of states lowers QQ at every initial state, by exactly ∑iπiεi\sum_i \pi_i \varepsilon_i.
  • Theorems 2 and 3: under (C), optimality over C′′C'' implies optimality over CC; under (C) and (E), an optimal rule of C′′C'' exists.
  • Lemma 2: along policy improvement the gaps εiRn\varepsilon_i^{R_n} tend to 00 at every state.

Significance

Theorem 1 is the countable-state verification theorem. It is the template for all later average-cost theory on infinite state spaces, which replaces boundedness of vv by growth or Lyapunov conditions. Theorem 4 extends policy improvement, the standard algorithm for finite average-cost problems, to denumerable state spaces, under conditions that do not reduce the problem to a finite one.

Derman proved these results in 1966. None of them has been machine-checked: the platform has finite-state average-cost policy iteration and finite-state verification theorems, but no countable-state result of this kind. A formal development checks the analytic steps that the paper treats briefly. These are the interchange of limits and infinite sums in (3), (9) and (11), and the identification of the Cesàro limits of a positive recurrent chain with its steady-state probabilities.

Difficulty

On a finite state space, policy improvement terminates because there are finitely many rules and the average cost strictly decreases. On a denumerable state space C′′C'' is uncountable, so neither step works. The sequence need not terminate. With ties in the minimization it need not converge either. A strict decrease of gRng^{R_n} does not force the gaps to vanish. That needs (F), a uniform positive lower bound on the long-run occupation of each state. Passing to the limit in (2) along a subsequence requires a limit interchange in an infinite sum, which works only because {vR}\{v^R\} is uniformly bounded. Finally, comparing with history-dependent randomized rules needs the finite-horizon argument behind (6). A stationary-rule comparison is not enough.

Formalization scope

The model is the published Markov decision chain SennottDP.AvgFinite.MDC: a countable state type, a finite nonempty Finset of decisions at each state (so (A) is built in), and transition probabilities in [0,∞][0,\infty] summing to one. History-dependent randomized rules are Policy M, and C′′C'' is StationaryPolicy M. The chain notions (irreducibility, positive recurrence, steady state 1/mjj1/m_{jj}) come from the published SennottDP.MarkovCost.Chain. The conventions are as follows.

  • Costs are a separate signed function w with (B). The nonnegative cost field of MDC is unused, and w≥0w \ge 0 is not assumed.
  • ERWtE_R W_t is the genuine expectation against the history law, and QRQ_R is the real limsup with the paper's normalization (T+1)−1(T+1)^{-1}.
  • Every use of (1) or (2) assumes vv bounded, so the series ∑jqij(k)vj\sum_j q_{ij}(k) v_j converge absolutely. The bound is part of the paper's hypotheses: without it Theorem 1 is false on infinite II.
  • (E) is an explicit family gR,vRg^R, v^R, and the improvement step is taken against it, with arbitrary tie-breaking. (D) follows from (E) and is not a separate hypothesis.
  • (F) is stated with Cesàro limits. That they equal the steady-state probabilities under (C) is a proof obligation.
  • "Converges" in Theorem 4 is read as: a limit point exists, and every limit point is optimal over CC. Whole-sequence convergence is not claimed, because the paper's proof does not establish it.
  • Sequences are indexed from 00.

Two trivializing formalizations are ruled out: optimality is over all history-dependent randomized rules, never only over C′′C'', and QRQ_R is computed from the process law, never defined through (2).

A complete development needs Cesàro convergence of tt-step probabilities to 1/mjj1/m_{jj} for positive recurrent chains, dominated convergence for bounded functions against stochastic kernels, the finite-horizon dynamic programming principle for history-dependent rules, and a diagonal (Tychonoff) argument in ∏i{1,…,Ki}\prod_i \{1,\dots,K_i\}. The first and third are reusable well beyond this paper. Contributions of these lemmas as separate theorems are welcome.

Selected references

  • C. Derman, Denumerable State Markovian Decision Processes—Average Cost Criterion, Ann. Math. Statist. 37(6) (1966) 1545–1553. https://doi.org/10.1214/aoms/1177699146
  • C. Derman, On Sequential Decisions and Markov Chains, Management Sci. 9(1) (1962) 16–24. https://doi.org/10.1287/mnsc.9.1.16
  • R. A. Howard, Dynamic Programming and Markov Processes, Wiley, New York, 1960.
  • D. L. Iglehart, Dynamic programming and stationary analysis of inventory problems, Ch. 1 of Multistage Inventory Models and Techniques (H. Scarf, D. Gilford, M. Shelly, eds.), Stanford Univ. Press, 1963.
  • K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, 1960. https://doi.org/10.1007/978-3-642-49686-8
  • A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
13 thms1 active userReviewed