Prove2Me

The waiting-time density has total mass one

Proved
waiting_time_mass_eq_one

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

analysisintegralprobability

Waiting-time density has total mass 1. For integers 0≤m<N0 \le m < N and rate λ>0\lambda > 0, the Siegel waiting-time density f(t)=N(N−1m)(1−e−λt)m(e−λt)N−mλf(t) = N\binom{N-1}{m}(1-e^{-\lambda t})^m (e^{-\lambda t})^{N-m}\lambda integrates to 11 over (0,∞)(0,\infty): ∫0∞f(t) dt=1\int_0^\infty f(t)\,dt = 1. This is the normalization (probability-measure) property of the waiting time T=min⁡{s:XN(s)≥m+1}T = \min\{s : X_N(s) \ge m+1\} for NN independent rate-λ\lambda exponential clocks, established by the fundamental theorem of calculus from the CDF F(t)=∑k=m+1N(Nk)(1−e−λt)k(e−λt)N−kF(t)=\sum_{k=m+1}^{N}\binom{N}{k}(1-e^{-\lambda t})^k (e^{-\lambda t})^{N-k} (which satisfies F(0)=0F(0)=0 and F(t)→1F(t)\to 1 as t→∞t\to\infty).

Preamble
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.MeasureTheory.Integral.IntegralEqImproper
import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Order.Filter.AtTopBot.Field

set_option autoImplicit false
open scoped BigOperators
open Finset MeasureTheory Set Filter Topology
Formal statement
theorem waiting_time_mass_eq_one (N m : ℕ) (lam : ℝ) (h : m < N) (hlam : 0 < lam) :
    ∫ s in Set.Ioi (0:ℝ),
      ((N : ℝ) * (Nat.choose (N-1) m : ℝ) * (1 - Real.exp (-(lam * s))) ^ m
        * (Real.exp (-(lam * s))) ^ (N - m) * lam) = 1 := by sorry
Source
Siegel, "Median Bounds and their Application", J. Algorithms 38:184-236, 2001, §2.1.1 (Theorem 2.2 setup); the density fTf_T on p.6. Mass-1 is the statement that FF is a CDF.

View graph