Spitzer's Formula¶
Recover an i.i.d. random walk's running-maximum laws from positive-part partial-sum laws through Spitzer's time-generating-function identity.
Core Idea¶
Spitzer's formula describes the running maximum of a random walk through the distributions of its partial sums. For independent, identically distributed increments, write \(S_n=X_1+\cdots+X_n\), \(M_n=\max(0,S_1,\ldots,S_n)\), and \(S_\ell^+=\max(0,S_\ell)\). A verified one-sided form says that, for \(|u|<1\) and real \(t\),[^ref-7915df671cf5]
This is an ordinary generating function in the time index. It connects a path statistic, \(M_n\), to the one-time laws of \(S_\ell^+\). The original 1956 work is the historical source, but its full joint two-sided expression was not directly accessible for this draft, so only the verified one-sided theorem is stated.[ref-7915df671cf5][ref-a9e611e4439e]
Scope of Application¶
The theorem applies to an i.i.d. partial-sum walk, or to an applied quantity proved equal in distribution to its running maximum. A documented example is waiting time in an initially empty single-server queue with i.i.d. service-minus-interarrival increments. A second example is a stylized discrete insurance reserve with i.i.d. net-loss increments, where finite-horizon ruin can be expressed as a maximum crossing event.[^ref-7915df671cf5]
The insurance crossing relation is a model deduction, not a measured result in the paper. The theorem does not by itself give a closed-form ultimate ruin probability.[^ref-7915df671cf5]
Clarity¶
Keep \(S_n\) (terminal sum), \(S_\ell^+\) (positive part at one time), and \(M_n\) (maximum over a path) separate. The theorem uses the positive-part laws to determine maximum transforms; replacing them with signed partial sums changes the equality.[^ref-7915df671cf5]
The queue waiting time is a maximum of reversed increments. With i.i.d. increments it has the same distribution as the forward maximum, but is not necessarily equal to that forward maximum on each realized path. The author's later bounded-left integer-step Proposition 2 is also narrower than the stated general Theorem 1.[^ref-7915df671cf5]
Manages Complexity¶
Directly describing a running maximum requires considering whole paths. The identity organizes all finite-horizon maximum transforms from expectations involving individual partial sums. One still needs the model's partial-sum distributions and, to obtain probabilities, suitable coefficient extraction and inversion.[^ref-7915df671cf5]
Abstract Reasoning¶
First state and check the i.i.d. increment assumption. Define \(S_n\), \(S_n^+\) and \(M_n\) with the zero convention. Then prove the applied quantity is the maximum or has its law; only afterward apply the transform at \(|u|<1\). For a threshold event, specify the level and horizon before turning the maximum law into a probability.[^ref-7915df671cf5]
A similar-looking maximum with dependent increments needs a separate result. One should not extend a finite-horizon statement to infinite time without an additional limiting argument.[^ref-7915df671cf5]
Knowledge Transfer¶
The formal roles transfer from queue congestion to an insurance capital model. Queue service minus interarrival time supplies net-workload increments, and reversal in distribution supplies the maximum. Insurance claims minus premiums supply net-loss increments, and a reserve threshold turns the maximum into a ruin event. The two models differ, but the same i.i.d. random-walk theorem is used.[^ref-7915df671cf5]
The proposed direct parent is live Formal Theorem: this is a proved equality with specific random-walk roles. A generic “highest so far” pattern is not enough to instantiate this formula.
Example¶
Single-server queue. With i.i.d. \(X_{n+1}=B_n-C_n\), waiting time obeys \(W_{n+1}=(W_n+X_{n+1})^+\). Its reversed-sum maximum is equal in law to forward \(M_n\). Mapped roles: increments → service minus interarrival; sums → cumulative net workload; maximum → waiting-time law; positive parts → \(S_\ell^+\); equality → maximum transform.[^ref-7915df671cf5]
Finite-horizon insurance crossing. Let surplus after \(k\) periods be \(U_k=r-S_k\), with i.i.d. claims-minus-premium net-loss increments and \(r\geq0\). If ruin means strictly negative surplus, ruin by \(n\) is exactly \(\{M_n>r\}\). Mapped roles: increments → net losses; sums → cumulative losses; maximum → greatest loss by \(n\); positive parts → positive partial sums; equality → the transform used to recover the crossing probability. A nonpositive-surplus ruin convention changes \(>r\) to \(\geq r\).[^ref-7915df671cf5]
Relationships to Other Abstractions¶
Current abstraction Spitzer's Formula Domain-specific
Parents (1) — more general patterns this builds on
-
Spitzer's Formula is a kind of Formal theorem Domain-specific
Spitzer's formula is a proved theorem specialized to an i.i.d. walk maximum and positive-part transform equality.
Hierarchy paths (2) — routes to 2 parentless roots
- Spitzer's Formula → Formal theorem → Formal System → Formalization → Representation → Abstraction
- Spitzer's Formula → Formal theorem → Formal System → Formalization → Transformation → Function (Mapping)
Neighborhood in Abstraction Space¶
Spitzer's Formula sits in a sparse region of the domain-specific corpus (69th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Foundations of Probability & Inference (29 abstractions)
Nearest neighbors
- Lorden's Inequality — 0.86
- Average Order of an Arithmetic Function — 0.84
- Random Variable — 0.83
- Kolmogorov's Three-Series Theorem — 0.83
- Brownian Skorokhod Embedding — 0.83
Computed from structural-signature embeddings · 2026-10-08
Not to Be Confused With¶
A formula for the terminal sum alone; a pathwise equality between forward maximum and queue waiting time; an exponential generating function; a theorem for arbitrary dependent increments; a claim that the narrow discrete Proposition 2 proves every case; the unverified precise two-sided seed formula; or an automatic ultimate-ruin result.[ref-7915df671cf5][ref-a9e611e4439e]
References¶
[^ref-7915df671cf5]: A. J. E. M. Janssen and J. S. H. van Leeuwaarden, “Spitzer's Identity for Discrete Random Walks”, original author research paper (2017), Introduction and Lindley recursion Eq. (1.1) on PDF pp. 1–2, general Theorem 1 Eq. (1.2) on p. 2, and narrower Proposition 2 Eq. (1.4) on p. 3. Full text inspected. The paper restates the general named identity and proves a narrower integer-valued bounded-left version by a new method; its insurance-capital mention supports model context, while the finite-horizon ruin equivalence above is an explicit derivation. [^ref-a9e611e4439e]: Frank Spitzer, “A Combinatorial Lemma and Its Application to Probability Theory”, Transactions of the American Mathematical Society 82 (1956): 323–339. Original publisher/NDL bibliographic record verified; its full article was not accessible for direct formula comparison. The precise one-sided theorem statement here is checked in Janssen and van Leeuwaarden's full-text original research paper, which attributes it to Spitzer.