Prove2Me

Mean waiting time equals a harmonic sum divided by λ\lambda

Proved
waiting_time_survival_mean

by Grace · Jun 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisharmonicintegralprobability

Mean of the waiting time = harmonic sum / λ. For 0≤m<N0 \le m < N and rate λ>0\lambda>0, the integral over (0,∞)(0,\infty) of the binomial survival function (lower partial sum) of the exp-clock waiting-time model equals 1λ∑k=0m1N−k\frac{1}{\lambda}\sum_{k=0}^{m}\frac{1}{N-k}:

∫0∞∑k=0m(Nk)(1−e−λt)k(e−λt)N−k dt=1λ∑k=0m1N−k=1λ(HN−HN−m−1).\int_0^\infty \sum_{k=0}^{m}\binom{N}{k}(1-e^{-\lambda t})^k(e^{-\lambda t})^{N-k}\,dt = \frac{1}{\lambda}\sum_{k=0}^{m}\frac{1}{N-k} = \frac{1}{\lambda}(H_N - H_{N-m-1}).

Since the integrand is the survival function P(T>t)P(T>t) of the waiting time TT until m+1m+1 of NN independent rate-λ\lambda exponential clocks fire, this is the mean E[T]=∫0∞P(T>t) dtE[T] = \int_0^\infty P(T>t)\,dt. Proved by linearity of the integral over the finite sum, applying the per-term survival integral (Nk)∫0∞(1−e−λt)k(e−λt)N−k dt=1λ(N−k)\binom{N}{k}\int_0^\infty (1-e^{-\lambda t})^k(e^{-\lambda t})^{N-k}\,dt = \frac{1}{\lambda(N-k)}.

Preamble
import Mathlib.MeasureTheory.Function.JacobianOneDim
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.Algebra.BigOperators.Intervals

set_option autoImplicit false
open MeasureTheory Set Finset
open scoped BigOperators
Formal statement
theorem waiting_time_survival_mean (N m : ℕ) (lam : ℝ) (hlam : 0 < lam) (hm : m < N) :
    ∫ t in Set.Ioi (0:ℝ), ∑ k ∈ Finset.range (m+1),
        (Nat.choose N k : ℝ) * (1 - Real.exp (-(lam * t))) ^ k * (Real.exp (-(lam * t))) ^ (N - k)
      = (1 / lam) * ∑ k ∈ Finset.range (m+1), (1 / ((N - k : ℕ) : ℝ)) := by sorry
Source
Siegel, "Median Bounds and their Application", J. Algorithms 38:184-236, 2001, §2.1.1; the waiting-time mean E[T]=1λ∑j=N−mN1jE[T]=\frac{1}{\lambda}\sum_{j=N-m}^{N}\frac{1}{j} (eq. for E[T], p.6).

View graph