The Swiss Army Formula of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest of the book runs on. Its subject is the relation between two ways of looking at the same stationary system: from a clock fixed in time, and from a customer arriving into it. The two are not the same — the interval a random instant falls into is longer than a typical interval, a fact every queueing student meets as the inspection paradox — and the object that makes the difference precise is the Palm probability P⁰_N.

The chapter defines P⁰_N by the Matthes definition in terms of counting,

λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ],                          (1.2.1)

and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the inversion formula and the goal theorem would inherit that emptiness.

From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift (1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4), which relates two point processes stationary for the same flow; and the Miyazawa rate conservation principle (1.3.10), which balances the drift of a process between its jumps against the rate at which it jumps.

The goal

§1.3.7 then collects all of them into one identity. Its name is the book's own:

Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.

Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A, departures {τ_n} with counting measure D — not assumed ordered — sojourn times W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative process {Z(t)}, all compatible with a measurable flow under which P is invariant:

λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ].              (1.3.28)

Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law, here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other choices give the inversion formula, the Miyazawa conservation principle and the rate conservation law.

The local meaning of P⁰_N

One milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of P⁰_N as "what an arriving customer sees":

lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0.                       (1.5.3)

The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.

What this mission provides

Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.

Formalization scope

• The flow {θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].
• P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula would make the milestones and the goal trivial and is ruled out.
• Every "for all non-negative measurable" formula (Mecke, inversion, mean-value, Neveu, Wald, the goal) is stated in [0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded or integrable ones.
• Three hypotheses the book uses without listing them are explicit: the Swiss army formula assumes the integrator {B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails); it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.
• Theorem 1.5.1 keeps the supremum over all events inside the limit (one δ for every A).

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$, $T_{iG}\ge 1$ is the first passage time to $G$. The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$. The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$. The mean first passage time is $m_{iG}=E[T_{iG}]$, infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$. A state $i$ is positive recurrent when $m_{ii}<\infty$, and the steady state probability is $\pi_i=m_{ii}^{-1}$. On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$. The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$. Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$, and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$, a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$. The quantities of $\Gamma_N$ are written $m_{iG}(N)$, $c_{iG}(N)$, $\pi_i(N)$ and $J(i)(N)$. An AS is conforming (for a $z$ standard $\Gamma$) if, for large $N$, $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$. It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$:

$$P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in S_N.$$

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$.

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$,

$$\text{every ATAS that sends excess probability to } G \text{ is conforming},$$

and if $G\subseteq R$ it is also conforming on $R$. No rate of convergence and no constants are involved, and $G$ need not contain $z$.

Milestones

1. Proposition C.4.2: for fixed $t$, $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$.
2. Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$.
3. Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$.
4. Proposition C.4.6: on a positive recurrent class, convergence of $\pi$, of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$, of $c_{zz}$ and of all $c_{iG}$ are equivalent.
5. Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$, and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$.

Further results

6. Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$, the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$.
7. Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$, the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$. First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$, a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$, and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$, $c_{iG}$, $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$. $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$, the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$. $\Gamma_N$ is built as an MC on the subtype of $S_N$, and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$. Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ($N<N_0$ or a state outside $S_N$). For fixed states this affects finitely many $N$, and all statements are limits, $\liminf$s or eventual equalities. All convergence is in $[0,\infty]$. The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$.

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$, is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$, and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
• L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
• L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
• D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).

Motivation

A Markov chain Monte Carlo sampler is often assembled from simpler parts. A practitioner who has several proposal mechanisms $Q_1, Q_2, \dots$ for a Metropolis–Hastings sampler can combine them in two ways. Either each $Q_i$ drives its own Metropolis–Hastings kernel $P_i$ and the sampler picks kernel $P_i$ with probability $\beta_i$ at each step, or the mixture $Q = \sum_i \beta_i Q_i$ is used as a single proposal inside one Metropolis–Hastings kernel. Both samplers leave the target $\pi$ invariant, so the choice is about efficiency.

Section 4 of Tierney (1998) settles the comparison: when both samplers use the maximal acceptance probability, the second never does worse in terms of asymptotic variances of sample-path averages. The statement that carries this is Proposition 5, an ordering of kernels in Peskun's off-diagonal order; the variance comparison then follows from Theorem 4 of the same paper, the general-state-space extension of Peskun (1973).

Timeline. Peskun (1973) introduced off-diagonal domination for finite state spaces and showed that the Metropolis–Hastings acceptance probability is maximal in that order. A version of Proposition 5 for discrete chains appears in the appendix of Tierney (1991) and in the rejoinder of Besag, Green, Higdon and Mengersen (1995). Tierney (1998) states and proves it for general state spaces, using the measure-theoretic description of Metropolis–Hastings kernels from §2 of the same paper.

Setting

Let $(E, \mathcal E)$ be a measurable space and $\pi$ a probability measure on it, the target. A proposal kernel $Q(x, dy)$ is a Markov kernel on $E$. Given a measurable acceptance probability $\alpha : E \times E \to [0,1]$, the Metropolis–Hastings kernel is

$$P(x, dy) = Q(x, dy)\,\alpha(x, y) + \delta_x(dy) \int \bigl(1 - \alpha(x, u)\bigr)\, Q(x, du),$$

where $\delta_x$ is the point mass at $x$ (mhKernel Q α).

Put $\mu(dx, dy) = \pi(dx) Q(x, dy)$ and $\mu^T(dx, dy) = \mu(dy, dx)$. With $\nu = \mu + \mu^T$ and $h = d\mu/d\nu$ (canonDensity), let

$$R = \{(x, y) : h(x, y) > 0,\ h(y, x) > 0\},\qquad r(x, y) = h(x, y)/h(y, x) \text{ on } R,\quad r = 1 \text{ on } R^c$$

(canonR, canonRatio). The set $R$ is symmetric, $\mu$ and $\mu^T$ are mutually absolutely continuous on $R$ and mutually singular off it (Proposition 1 of the paper). The Metropolis–Hastings acceptance probability is

$$\alpha_{MH}(x, y) = \min\{1, r(y, x)\} \text{ if } (x, y) \in R, \qquad \alpha_{MH}(x, y) = 0 \text{ otherwise}$$

(alphaMH π Q), and the kernel with $\alpha = \alpha_{MH}$ is the maximal Metropolis–Hastings kernel for $Q$ (maxMHKernel π Q).

For kernels $P_1, P_2$ on $E$, $P_1$ dominates $P_2$ off the diagonal, $P_1 \succeq P_2$ (OffDiagDominates π P₁ P₂), if for $\pi$-almost every $x$, $P_1(x, A \setminus \{x\}) \ge P_2(x, A \setminus \{x\})$ for all $A \in \mathcal E$. For a countable family of kernels $K_i$ and weights $\beta_i \ge 0$, the mixture $\sum_i \beta_i K_i$ is the kernel $x \mapsto \sum_i \beta_i K_i(x, \cdot)$ (mixKernel β K).

Formalization targets

Goal: Proposition 5

Let $Q_i$ be a finite or countable family of proposal kernels and $\beta_i \ge 0$ with $\sum_i \beta_i = 1$. Let $P_i$ be the maximal Metropolis–Hastings kernel for $Q_i$ and $P$ the maximal Metropolis–Hastings kernel for $Q = \sum_i \beta_i Q_i$. Then

$$P \succeq \sum_i \beta_i P_i .$$

Both sides use maximal kernels: $P$ uses $\alpha_{MH}$ of the mixture proposal, each $P_i$ its own $\alpha^{(i)}_{MH}$, and the same weights $\beta_i$ form both mixtures.

Milestones

1. The construction in the proof of Proposition 1 (p. 2) yields a set $R$ and ratio $r$ with the properties of Proposition 1 for $\mu = \pi \otimes Q$.
2. $\alpha_{MH}$ satisfies conditions (i) and (ii) of Theorem 2 (p. 3): $\alpha_{MH} = 0$ $\mu$-a.e. on $R^c$, and $\alpha_{MH}(x, y) r(x, y) = \alpha_{MH}(y, x)$ $\mu$-a.e. on $R$.
3. The maximal kernel satisfies detailed balance, $\pi(dx) P(x, dy) = \pi(dy) P(y, dx)$.
4. For any symmetric $\sigma$-finite $\nu$ dominating $\mu$, with $h = d\mu/d\nu$:

$$\pi(dx) Q(x, dy)\, \alpha_{MH}(x, y) = \min\{h(y, x), h(x, y)\}\, \nu(dx, dy).$$

5. As measures on $E \times E$:

$$\pi(dx) Q(x, dy)\, \alpha_{MH}(x, y) \ge \sum_i \beta_i\, \pi(dx) Q_i(x, dy)\, \alpha^{(i)}_{MH}(x, y).$$

A companion item states the maximality of $\alpha_{MH}$ (§3, p. 7): every measurable acceptance probability $\alpha$ whose kernel is reversible satisfies $\alpha \le \alpha_{MH}$ $\mu$-a.e., so the maximal kernel dominates every reversible Metropolis–Hastings kernel with the same proposal.

Significance

The result. Proposition 5, combined with Theorem 4 of the paper (off-diagonal domination orders asymptotic variances of reversible kernels), shows that for every function $f$ with finite variance the asymptotic variance of $\frac1n \sum_{k} f(X_k)$ under the mixture-proposal sampler is at most that under the mixture of samplers. Per-iteration cost can be higher for the mixture proposal, since $\alpha_{MH}$ then needs the densities of all components; Proposition 5 isolates the statistical side of that trade-off. The maximality companion states the fact behind the name "maximal kernel": $\alpha_{MH}$ is the largest acceptance probability that keeps a Metropolis–Hastings kernel reversible.

Formalizing it. The paper's proof is a computation of about six lines with Radon–Nikodym densities. A formal version must make explicit what the computation leaves implicit: that $\alpha_{MH}$, defined from one dominating measure, has the same density form for every symmetric dominating measure; that the measure inequality on $E \times E$ passes to the kernel-level statement with one null set for all $A$; and that the mixture proposal and the mixture of kernels are handled as countable sums of kernels. As of September 2026 neither Mathlib nor this platform has a machine-checked version of Proposition 5, of the maximality of $\alpha_{MH}$, or of reversibility of the Metropolis–Hastings kernel on a general state space; only finite-state Metropolis chains have been formalized on the platform.

Difficulty

The obvious argument works pointwise with densities: write every kernel as a density against a common reference measure and compare $\min\{\cdot, \cdot\}$ of sums with sums of minima. On a general state space there is no common reference measure given in advance, and $\alpha_{MH}$ is only defined up to $\mu$-null sets, through a Radon–Nikodym derivative with respect to $\mu + \mu^T$, a measure that differs for $Q$ and for each $Q_i$. The step that needs care is relating these different versions: the densities $h_i$ of the $\mu_i$ against a common symmetric $\nu$, the density of $\mu = \sum_i \beta_i \mu_i$, and the transpose densities $h(y, x)$, which are densities of $\mu^T$ only because $\nu$ is symmetric.

The second difficulty is the passage from measures to kernels. The inequality between measures on $E \times E$ gives, for each fixed $A$, the kernel inequality for $\pi$-almost every $x$, with a null set that depends on $A$. The order $\succeq$ requires one null set for all $A$, and the diagonal must be removed, which needs the diagonal to be measurable.

Formalization scope

The formalization is in Lean 4 with Mathlib, in the namespace TierneyMH.Mixture. The state space is a type E with a σ-algebra; π is a probability measure; proposal kernels are Markov kernels Kernel E E. Acceptance probabilities and densities take values in $[0, \infty]$ (ℝ≥0∞); a general $\alpha$ is assumed measurable with $\alpha \le 1$. $\mu$ is π ⊗ₘ Q, $\mu^T$ its image under Prod.swap, detailed balance is Kernel.IsReversible. Mixtures are indexed by a countable type ("a sequence", which includes finite families), with weights in ℝ≥0 and HasSum β 1.

Added hypotheses, both labelled in the statements: singletons are measurable (implicit in the paper's $A \setminus \{x\}$ and $\delta_x$), on the goal and the maximality companion; and, on the goal only, the σ-algebra of $E$ is countably generated. The second is an addition to the paper: it is what makes the exceptional null set in $\succeq$ uniform over $A$ in the passage from the measure inequality to the kernels. It is not assumed in the measure-level milestones.

$\alpha_{MH}$ is one fixed version, built from Mathlib's rnDeriv exactly as in the proof of Proposition 1 (with $\nu = \mu + \mu^T$, not an arbitrary dominating measure), and all statements are insensitive to the version. The ratio $r$ is set to 1 on the null subset of $R$ where $h$ is infinite, so that $0 < r < \infty$ and $r(x, y) = 1/r(y, x)$ hold everywhere, as Proposition 1 asks.

Trivializations ruled out: $\alpha_{MH}$ is the indicator of $R$ times $\min\{1, r(y, x)\}$, never an arbitrary acceptance function or a single $\alpha$ shared by all components; $\succeq$ compares $A \setminus \{x\}$, not $A$ (on $A$ the rejection masses differ and the comparison is false); and the conclusion is about the Metropolis–Hastings kernels themselves, not about the measure identity alone. All hypotheses are satisfiable, for instance on $E$ = Bool with $\pi$ uniform, two proposals $Q_1 = \pi$ and $Q_2 = \delta_x$ and weights $(1/2, 1/2)$.

Needed infrastructure, reusable for other Metropolis–Hastings results: Radon–Nikodym calculus for product measures and their transposes, countable sums of kernels, and a monotone-class argument over a countable generating family. The Metropolis–Hastings kernel, $R$, $r$ and off-diagonal domination are defined identically in the companion missions I (detailed balance, Theorem 2) and II (Peskun ordering, Theorem 4) of this series. Proofs of milestones in any order, and proofs of the goal from the milestones, are welcome.

Selected references

• L. Tierney, A Note on Metropolis–Hastings Kernels for General State Spaces, The Annals of Applied Probability 8(1), 1998, 1–9. https://doi.org/10.1214/aoap/1027961031
• P. H. Peskun, Optimum Monte Carlo sampling using Markov chains, Biometrika 60(3), 1973, 607–612. https://doi.org/10.1093/biomet/60.3.607
• J. Besag, P. Green, D. Higdon, K. Mengersen, Bayesian computation and stochastic systems (with discussion), Statistical Science 10(1), 1995, 3–66. https://doi.org/10.1214/ss/1177010123
• W. K. Hastings, Monte Carlo sampling methods using Markov chains and their applications, Biometrika 57(1), 1970, 97–109. https://doi.org/10.1093/biomet/57.1.97
• N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, E. Teller, Equations of state calculations by fast computing machines, J. Chemical Physics 21, 1953, 1087–1091. https://doi.org/10.1063/1.1699114

Motivation

The discrete logarithm problem modulo a prime asks, given a prime $p$, a generator $g$ of the multiplicative group modulo $p$, and a nonzero residue $x$, for the exponent $r$ with $g^r\equiv x \pmod p$. Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time $\exp(O((\log p)^{1/3}(\log\log p)^{2/3}))$.

In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which $r$ can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least $1/480$. This mission formalizes that bound and the three estimates it is assembled from.

Setting

Let $p$ be a prime and $g$ a generator of $(\mathbb Z/p\mathbb Z)^\times$, so that $1,g,\dots,g^{p-2}$ are all the nonzero residues. Fix the unknown $r$ with $0\le r<p-1$ and put $x=g^r$. Let $q=2^l$ be the power of $2$ with $p<q<2p$.

The Fourier matrix $A_q$ is the $q\times q$ matrix with entries $(A_q)_{a,c}=q^{-1/2}\exp(2\pi i\,ac/q)$ for $0\le a,c<q$ (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.

The algorithm uses three registers: two holding numbers $0\le a,b<q$ and one holding a nonzero residue modulo $p$. It starts from the state

$$\frac{1}{p-1}\sum_{a=0}^{p-2}\sum_{b=0}^{p-2}|a,b,g^ax^{-b}\ (\mathrm{mod}\ p)\rangle \qquad (6.1)$$

(preFourierState), applies $A_q$ to each of the first two registers (finalState), and measures all three registers. The probability of observing $|c,d,y\rangle$ is the squared modulus of its amplitude (outcomeProb).

For integers $z$ and $q>0$, the symmetric residue $\{z\}_q$ is the residue of $z$ modulo $q$ in $(-q/2,q/2]$ (symmRes). Put

$$T=rc+d-\frac{r}{p-1}\{c(p-1)\}_q .$$

An observed state $|c,d,y\rangle$ is good (IsGood) when

$$|\{T\}_q|\le\tfrac12 \quad (6.10) \qquad\text{and}\qquad |\{c(p-1)\}_q|\le q/12 \quad (6.11).$$

Goodness depends only on $(c,d)$.

Formalization targets

Goal: a good output with probability at least $1/480$ (§6, p. 1504)

$$\sum_{\substack{0\le c,d<q\\ (c,d)\ \text{good}}}\ \sum_{y\in(\mathbb Z/p)^\times}\Pr[c,d,y]\ \ge\ \frac1{480}.$$

The constant is the one the page carries forward. The goal fixes no threshold on $p$: it is stated for every prime $p$ that admits a power of two strictly between $p$ and $2p$.

Milestones

1. The output distribution, eq. (6.4). For $0\le k<p-1$,

$$\Pr[c,d,g^k]=\left|\frac{1}{(p-1)q}\sum_{\substack{0\le a,b\le p-2\\ a-rb\equiv k\ (p-1)}}\exp\Bigl(\frac{2\pi i}{q}(ac+bd)\Bigr)\right|^2 .$$

2. Each good state is likely, eq. (6.17). If $(c,d)$ is good, then $\Pr[c,d,y]\ge 1/(20q^2)$ for every $y$.
3. Many good pairs (p. 1504). At least $q/12$ pairs $(c,d)$ are good.
4. Each good $c$ is likely (p. 1504). If $(c,d)$ is good for some $d$, then $\sum_{d',y}\Pr[c,d',y]\ge(p-1)/(20q^2)\ge1/(40q)$.

Significance

The result. The bound $1/480$ is what turns the circuit into an algorithm. Repeating the circuit $O(1)$ times in expectation yields a good output, and from a good pair $(c,d)$ one reads off an equation that determines $r$ modulo divisors of $p-1$ (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.

Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term $O(W/(pq))$ whose constant is not given, yet states $1/(20q^2)$ for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of $q^2\Pr[c,d,y]$ over good states is about $0.49$ for all primes $p<90$, so the unconditional claim is not in doubt for small $p$. The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.

Difficulty

The exponential sum (6.4) runs over pairs $(a,b)$ satisfying a congruence modulo $p-1$, while the phases are taken modulo $q$. The two moduli are unrelated: $q$ is a power of two and $p-1$ is arbitrary. Eliminating $a$ through the congruence introduces a floor function $\lfloor(br+k)/(p-1)\rfloor$, and the resulting phase is not linear in $b$. The obvious estimate treats the sum as a geometric series in $b$ and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to $|\{c(p-1)\}_q|$. Condition (6.11) only keeps this perturbation within $\pi/6$ of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in $p$, $r$ and $k$, including small primes where the paper's integral approximation gives no explicit control.

The count of good pairs needs a separate argument about how often a multiple $c(p-1)$ lies within $q/12$ of a multiple of $q$ when $\gcd(p-1,q)$ is large.

Formalization scope

• States are functions Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over $\{0,\dots,q-1\}$; the third over the units modulo $p$.
• Matrix convention. Following §2, rows are inputs, so the amplitude of $|c,d,y\rangle$ after the transforms is $\sum_{a,b}\psi(a,b,y)(A_q)_{a,c}(A_q)_{b,d}$. finalState is defined this way from (6.1) and $A_q$. It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.
• Probability of a basis state is the squared norm of its amplitude, with no normalization hypothesis.
• Parameters. $p$ is prime (Fact p.Prime). The generator is encoded as orderOf g = p - 1. $r<p-1$ is a parameter, with $x=g^r$. $q$ is given by q = 2 ^ l together with $p<q<2p$. No large-$p$ threshold is added anywhere.
• Arithmetic. $x^{-b}$ is x⁻¹ ^ b in the unit group. $p-1$ is computed in $\mathbb Z$ and $\mathbb R$ inside $T$ and the congruences, and as natural-number subtraction only where $p\ge2$ makes it exact. $T$ is real.
• Condition (6.10) is stated as "some integer $j$ has $|T-jq|\le\frac12$". Because $q\ge4$, this is equivalent to the page's form with $j$ the closest integer to $T/q$.
• Not formalized. The preparation of (6.1) by testing and restarting is not formalized; the state (6.1) is taken as displayed. The printed test "whether the number is less than $p$" should read $p-1$, as the sums in (6.1) show. Also out of scope: the recovery of $r$ (eqs. (6.18)–(6.20)), the repetition count "$480t$", and all running-time claims.
• Printed slips.
  • The page asserts that for each $c$ there is exactly one $d$ satisfying (6.10). At a tie $\{T\}_q=\pm\frac12$ there can be two such $d$. Milestone 3 states only the count, which needs at least one.
  • The page's intermediate bound "at least $p/(240q)$" should be $(p-1)/(240q)$. The conclusion $1/480$ is unaffected, since $q$ and $2p$ are both even and so $q\le 2(p-1)$. Only $1/480$ is stated.

Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of $\mathbb Z/q$. The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization $\sum\Pr=1$, and of auxiliary lemmas about symmRes are welcome.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172 (preprint: https://arxiv.org/abs/quant-ph/9508027)
• D. M. Gordon, Discrete logarithms in GF(p) using the number field sieve, SIAM J. Discrete Math. 6(1):124–138, 1993. https://doi.org/10.1137/0406010
• W. Diffie and M. E. Hellman, New directions in cryptography, IEEE Trans. Inform. Theory 22(6):644–654, 1976. https://doi.org/10.1109/TIT.1976.1055638
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511976667

Motivation

Classical generalization bounds control the gap between the expected loss of a learned hypothesis and its average loss on the training sample. The average is sensitive to outliers: when a non-negligible fraction of the sample is corrupted, the mean loss stops describing the quality of a solution, and quantile-type summaries such as the median become the natural measurement. Quantile losses have long been used for this reason in statistics and econometrics (Koenker and Bassett 1978; Huber 1981). The standard tools for proving generalization bounds — symmetrization, Rademacher and VC arguments — are built around the expected loss and do not extend to quantiles in any direct way.

Xu and Mannor (Mach Learn 86 (2012) 391–423) introduced algorithmic robustness: an algorithm is robust if the sample space can be partitioned into finitely many cells such that a test point falling in the same cell as a training point incurs a similar loss. Because the argument works cell by cell and needs no symmetrization, it transfers to loss functionals other than the mean. Sect. 4.1 of the paper uses this to bound the quantile value and the truncated mean of the testing error, and Sect. 5 relaxes robustness to pseudo robustness, which only asks the cell condition for a subset of the training samples. This mission formalizes the resulting Theorem 5 (p. 402), whose proof is Appendix C (pp. 415–418).

Setting

Let $\mathcal Z$ be a measurable sample space, $\mathcal H$ a set of hypotheses and $l : \mathcal H \times \mathcal Z \to [0, M]$ a loss, with each $l(h, \cdot)$ measurable. A training set $\mathbf s = (s_1, \dots, s_n)$ consists of $n$ i.i.d. draws from a probability measure $\mu$ on $\mathcal Z$; its empirical distribution is $\mu_{\mathrm{emp}} = \frac1n \sum_i \delta_{s_i}$. A learning algorithm is a map $\mathcal A : \mathcal Z^n \to \mathcal H$, and $\mathcal A_{\mathbf s}$ is the hypothesis learned from $\mathbf s$.

For a real random variable $X$ and a level $\beta$, the $\beta$-quantile value is

$$\mathbb Q^\beta(X) = \inf\{ c \in \mathbb R : \Pr(X \le c) \ge \beta \},$$

and, writing $Q = \mathbb Q^\beta(X)$, the $\beta$-truncated mean is

$$\mathbb T^\beta(X) = \mathbb E[X \cdot \mathbf 1(X < Q)] + \big(\beta - \Pr[X < Q]\big)\, Q,$$

where the second term vanishes when $\Pr[X = Q] = 0$. It is the contribution to $\mathbb E X$ of the leftmost $\beta$ fraction of the distribution. For a hypothesis $h$ and a measure $\nu$ on $\mathcal Z$ put $\mathcal Q(h, \beta, \nu) = \mathbb Q^\beta(l(h, z))$ and $\mathcal T(h, \beta, \nu) = \mathbb T^\beta(l(h, z))$ with $z \sim \nu$.

The algorithm is $(K, \epsilon(\cdot), \hat n(\cdot))$ pseudo robust, with $\epsilon : \mathcal Z^n \to \mathbb R$ and $\hat n : \mathcal Z^n \to \{1, \dots, n\}$, if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$, fixed in advance, such that every training set $\mathbf s$ has a subset $\hat{\mathbf s}$ of $\hat n(\mathbf s)$ samples with: whenever $s \in \hat{\mathbf s}$ and $z \in \mathcal Z$ lie in a common cell, $|l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s)$. With $\hat n \equiv n$ this is $(K, \epsilon(\cdot))$-robustness.

Formalization targets

Goal: Theorem 5 (p. 402)

Let $\lambda_0 = \sqrt{(2K \ln 2 + 2 \ln(1/\delta))/n}$ and $r(\mathbf s) = (n - \hat n(\mathbf s))/n$. If $\mathcal A$ is $(K, \epsilon(\cdot), \hat n(\cdot))$ pseudo robust, $\beta \in (0,1)$ and $\delta > 0$, then with probability at least $1 - \delta$: whenever $0 \le \beta - \lambda_0 - r(\mathbf s)$ and $\beta + \lambda_0 + r(\mathbf s) \le 1$,

$$\mathcal Q(\mathcal A_{\mathbf s}, \beta - \lambda_0 - r(\mathbf s), \mu_{\mathrm{emp}}) - \epsilon(\mathbf s) \le \mathcal Q(\mathcal A_{\mathbf s}, \beta, \mu) \le \mathcal Q(\mathcal A_{\mathbf s}, \beta + \lambda_0 + r(\mathbf s), \mu_{\mathrm{emp}}) + \epsilon(\mathbf s),$$ $$\mathcal T(\mathcal A_{\mathbf s}, \beta - \lambda_0 - r(\mathbf s), \mu_{\mathrm{emp}}) - \epsilon(\mathbf s) \le \mathcal T(\mathcal A_{\mathbf s}, \beta, \mu) \le \mathcal T(\mathcal A_{\mathbf s}, \beta + \lambda_0 + r(\mathbf s), \mu_{\mathrm{emp}}) + \epsilon(\mathbf s).$$

The constants are the paper's, and $K$, $\epsilon$, $\hat n$, $M$, $\mu$, $\delta$ and the algorithm are arbitrary.

Milestones (Appendix C)

1. Property 1 (p. 415): for a nonnegative $X$ and levels $0 \le \beta_2 \le \beta_1 \le 1$ (with $\beta_1 = 1$ only for $X$ bounded above), $\mathbb Q^{\beta_1}(X) \ge \mathbb Q^{\beta_2}(X)$ and $\mathbb T^{\beta_1}(X) \ge \mathbb T^{\beta_2}(X)$.
2. Property 2 (p. 415): if $\Pr(Y \ge a) \ge \Pr(X \ge a)$ for all $a$, then $\mathbb Q^\beta(Y) \ge \mathbb Q^\beta(X)$ and $\mathbb T^\beta(Y) \ge \mathbb T^\beta(X)$ for $\beta \in [0,1]$.
3. The event $\mathcal E$ (pp. 415–416): with $N_i$ the indices of samples in $C_i$, $\sum_i \big| |N_i|/n - \mu(C_i) \big| \le \lambda_0$ with probability at least $1 - \delta$.

Significance

The result. Theorem 5 shows that any pseudo-robust algorithm has a testing-error quantile and truncated mean that are bracketed by the empirical ones at levels shifted by $\lambda_0 + (n - \hat n(\mathbf s))/n$, up to the robustness tolerance $\epsilon(\mathbf s)$. The quantile of the testing error can therefore be estimated from training data for every algorithm to which the robustness framework applies — among them majority voting, SVMs, Lasso and principal component analysis (Sect. 6 of the paper) — without a separate complexity analysis of the loss class. The pseudo-robust form covers algorithms that are robust only away from a small set of training samples, which is the typical situation in the presence of outliers. The robust case $\hat n \equiv n$ is the paper's Theorem 2 (p. 400).

Formalizing it. The paper states Theorem 5 and proves it in Appendix C; no machine-checked proof exists. The appendix contains misprints (see Formalization scope) and the argument uses minimizers of the loss over each cell, which need not exist; a formal proof settles which steps are sound as written. The definitions of quantile value and truncated mean of a law on $\mathbb R$ developed here are reusable beyond this mission.

Difficulty

The concentration step is the same as for the expected loss: on the event $\mathcal E$ the empirical cell frequencies are close to the cell probabilities. The difficulty is converting this into a statement about quantiles. Quantile values are not linear in the distribution and are discontinuous in the level, so the triangle-inequality argument that bounds the mean-loss gap does not apply. Mass that moves between cells shifts every level of the quantile function, and the up to $n - \hat n(\mathbf s)$ samples outside $\hat{\mathbf s}$ carry no guarantee at all, so an arbitrary fraction $r(\mathbf s)$ of the empirical law is uncontrolled. For the truncated mean this must be done for the whole lower tail up to level $\beta$, not just at one point, and the atoms of the loss distribution (the second branch of the definition) have to be accounted for exactly.

Formalization scope

• The Lean namespace is XuMannorRobust.Quantile. $\mathcal Z$ is a type with a measurable space structure, $\mathcal H$ an arbitrary type, a training set a function Fin n → Z, and the i.i.d. law the product measure Measure.pi (fun _ => μ).
• "With probability at least $1 - \delta$" is encoded as: the outer measure of the set of training sets on which the claim fails is at most $\delta$. No measurability of $\mathbf s \mapsto \mathcal A_{\mathbf s}$ is needed.
• Added measurability. The paper ignores measurability; the formalization requires each $l(h,\cdot)$ and each cell $C_i$ to be measurable.
• Corrected Definition 3. The paper prints the second branch of the truncated mean as $\big(\beta - \Pr[X < Q]\big)/\Pr[X = Q] \cdot Q$. That contradicts its own worked example on p. 399, where the $0.63$-truncated mean of a uniform law on $c_1 < \dots < c_{10}$ is $0.1(\sum_{i \le 6} c_i + 0.3 c_7)$, and its verbal description. The formalization drops the division, as the example requires; with the printed formula $\mathbb T^\beta$ would not even be monotone in $\beta$.
• $\mathbb Q^\beta$ and $\mathbb T^\beta$ are defined on the law of the random variable, a measure on $\mathbb R$. Lean returns $0$ for the infimum of an empty set or of a set unbounded below, so $\mathbb Q^0 = 0$ (the paper's value is $-\infty$). This never helps: $\mathcal Q(\mathcal A_{\mathbf s}, \beta, \mu) \ge 0$ and $\epsilon(\mathbf s) \ge 0$, so the goal's inequalities remain meaningful at level $0$. The goal keeps every level in $[0,1]$ through the paper's side condition, which depends on $\hat n(\mathbf s)$ and is therefore placed inside the probability event as a premise. The codomain $\{1, \dots, n\}$ of $\hat n$ is part of the definition: with $\hat n(\mathbf s) = 0$ nothing would constrain $\epsilon(\mathbf s)$.
• The partition is fixed before the training set; the good subset $\hat{\mathbf s}$ may depend on $\mathbf s$ and is a set of indices. Choosing the partition after $\mathbf s$ would make pseudo robustness trivial and is ruled out.
• Properties 1 and 2 are stated for nonnegative laws and levels in $[0,1]$. The level $1$ is admitted only for a variable bounded above (for property 2, the dominating one). For an unbounded variable, $\mathbb Q^1$ is $+\infty$ in the paper, where the inequality is trivial, and a junk $0$ in Lean. Property 3 of Appendix C (p. 415) is misprinted (with the constraint $\sum \alpha_i \le \beta$ the minimum is $0$) and is not formalized.
• Needed infrastructure: the Bretagnolle–Huber–Carol inequality for multinomial frequencies (van der Vaart and Wellner 1996, Prop. A.6.6) (or a direct concentration argument), and elementary order properties of lower quantile values and truncated means of laws on $\mathbb R$. Contributions of these as separate lemmas are welcome.

Selected references

• H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86(3):391–423, 2012. https://doi.org/10.1007/s10994-011-5268-1
• R. Koenker and G. Bassett, Regression Quantiles, Econometrica 46(1):33–50, 1978. https://doi.org/10.2307/1913643
• P. J. Huber, Robust Statistics, Wiley, 1981. https://doi.org/10.1002/0471725250
• A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Proposition A.6.6). https://doi.org/10.1007/978-1-4757-2545-2