Eq. (2.54) — the Erlang-B recursion

Proved

QueueingFundamentals.BirthDeath.erlang_b_recursion

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

erlang-bp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1queueing

Let $r > 0$ and let $B(c, r)$ be the Erlang-B formula. Then $B(0, r) = 1$ and, for every $c \ge 1$ ,

B(c, r) = \frac{r\,B(c-1, r)}{c + r\,B(c-1, r)}.

The recursion computes $B(c, r)$ without the factorials of (2.53), which overflow in floating point for large $c$ .

Preamble

import Mathlib
import Definitions.Def_QueueingFundamentals_BirthDeath_Erlang

Formal statement

namespace QueueingFundamentals.BirthDeath

/-- Eq. (2.54), p.82. For an offered load `r > 0`, the Erlang-B formula satisfies
`B(c, r) = r B(c − 1, r) / (c + r B(c − 1, r))` for `c ≥ 1`, with `B(0, r) = 1`. -/
theorem erlang_b_recursion (r : ℝ) (hr : 0 < r) :
    erlangB 0 r = 1 ∧
      ∀ c : ℕ, 1 ≤ c →
        erlangB c r = r * erlangB (c - 1) r / ((c : ℝ) + r * erlangB (c - 1) r) := by sorry

end QueueingFundamentals.BirthDeath

Source

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

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