Eq. (2.57) — the Poisson steady-state law of the M/M/∞ queue

Proved

QueueingFundamentals.BirthDeath.mminf_steady_state

by mikedeng1 · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

infinite-serverp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1queueingstationary-distribution

The $M/M/\infty$ queue is the birth–death process with $\lambda_n = \lambda > 0$ and $\mu_n = n\mu$ , $\mu > 0$ . Let $r = \lambda/\mu$ . For all such $\lambda$ and $\mu$ a steady-state solution exists, and it is unique: $\{p_n\}$ is a steady-state solution if and only if

p_n = \frac{r^n e^{-r}}{n!} \qquad (n \ge 0),

the Poisson distribution with mean $r$ .

Unlike the $M/M/1$ and $M/M/c$ queues, no stability condition on $\lambda/\mu$ is needed.

Preamble

import Mathlib
import Definitions.Def_QueueingFundamentals_BirthDeath_Balance

Formal statement

namespace QueueingFundamentals.BirthDeath

/-- Eq. (2.57), p.84. The `M/M/∞` queue is the birth–death process with `λ_n = λ` and `μ_n = nμ`.
For every `λ, μ > 0` it has a steady-state solution, and `{p_n}` is a steady-state solution
exactly when `p_n = r^n e^{−r} / n!` for all `n ≥ 0`, with `r = λ/μ` (Poisson with mean `r`). -/
theorem mminf_steady_state (lam mu r : ℝ) (hlam : 0 < lam) (hmu : 0 < mu) (hr : r = lam / mu) :
    (∃ p : ℕ → ℝ, IsSteadyState (fun _ => lam) (infDeath mu) p) ∧
      ∀ p : ℕ → ℝ, IsSteadyState (fun _ => lam) (infDeath mu) p ↔
        ∀ n : ℕ, p n = r ^ n * Real.exp (-r) / (n.factorial : ℝ) := by sorry

end QueueingFundamentals.BirthDeath

Source

Gross, Shortle, Thompson & Harris, Fundamentals of Queueing Theory, 4th ed., Wiley 2008, DOI 10.1002/9781118625651, p.84, Eq. (2.57)

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph