Poisson processes

12 fully proved

Probability Theory

StructurePoisson process#✓fully proved

N : ℝ≥0 → Ω → ℕ is a Poisson process of rate r under P (Kingman 1993, ch. 4; Karlin–Taylor 1975, ch. 4): N 0 = 0 and the paths are nondecreasing almost surely, the increments over consecutive intervals are independent, and for s ≤ t the increment N t - N s has the Poisson law of mean r (t - s).

structure IsPoissonProcess (N : ℝ≥0 → Ω → ℕ) (r : ℝ≥0) (P : Measure Ω := by volume_tac) :
    Prop where
  /-- The process starts at `0` almost surely. -/
  ae_zero : ∀ᵐ ω ∂P, N 0 ω = 0
  /-- Almost every path is nondecreasing. -/
  ae_monotone : ∀ᵐ ω ∂P, Monotone fun t ↦ N t ω
  /-- Increments over consecutive intervals are independent. -/
  hasIndepIncrements : HasIndepIncrements N P
  /-- The increment over `(s, t]` has the Poisson law of mean `r (t - s)`. -/
  hasLaw_sub : ∀ ⦃s t : ℝ≥0⦄, s ≤ t →
    HasLaw (fun ω ↦ N t ω - N s ω) (poissonMeasure (r * (t - s))) P

Used by 3

Used bySuperposition · Exponential interarrivals give a Poisson process · Thinning

Poisson Process

DefinitionArrival times from interarrival times#✓fully proved

The n-th arrival time S n = T 0 + ⋯ + T (n - 1) of the interarrival times T.

noncomputable def arrivalTime (T : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
  ∑ i ∈ Finset.range n, T i ω

Used by 6

Used byCounting process has nondecreasing paths almost surely · Counting process starts at zero almost surely · Counting process of interarrival times · Arrival times of exponential interarrivals are Erlang · Arrival counts of exponential interarrivals are Poisson · Independent Poisson increments of the counting process

DefinitionCounting process of interarrival times#✓fully proved

The counting process of the interarrival times T: count T t ω is the number of arrivals n ≥ 1 with S n ≤ t. When that set is infinite (a null event for exponential interarrivals of positive rate) Set.ncard returns 0.

noncomputable def count (T : ℕ → Ω → ℝ) (t : ℝ≥0) (ω : Ω) : ℕ :=
  {n : ℕ | arrivalTime T (n + 1) ω ≤ t}.ncard

Uses 1 · Used by 5

Statement usesArrival times from interarrival times

Used byCounting process has nondecreasing paths almost surely · Counting process starts at zero almost surely · Arrival counts of exponential interarrivals are Poisson · Independent Poisson increments of the counting process · Exponential interarrivals give a Poisson process

TheoremArrival times of exponential interarrivals are Erlang#✓fully proved

The (n + 1)-th arrival time of i.i.d. rate-r exponential interarrivals has the Gamma (Erlang) law with shape n + 1 and rate r (Karlin–Taylor 1975, §4.2).

theorem hasLaw_arrivalTime {T : ℕ → Ω → ℝ} {r : ℝ≥0} (hr : 0 < r)
    (hT : ∀ i, HasLaw (T i) (expMeasure r) P) (hind : iIndepFun T P) (n : ℕ) :
    HasLaw (arrivalTime T (n + 1)) (gammaMeasure (n + 1) r) P

Uses 1 · Used by 1

Statement usesArrival times from interarrival times

Used byArrival counts of exponential interarrivals are Poisson

TheoremArrival counts of exponential interarrivals are Poisson#✓fully proved

The number of arrivals in [0, t] of i.i.d. rate-r exponential interarrivals has the Poisson law of mean r t (Karlin–Taylor 1975, §4.2, Theorem 2.1).

theorem hasLaw_count {T : ℕ → Ω → ℝ} {r : ℝ≥0} (hr : 0 < r)
    (hT : ∀ i, HasLaw (T i) (expMeasure r) P) (hind : iIndepFun T P) (t : ℝ≥0) :
    HasLaw (count T t) (poissonMeasure (r * t)) P

Uses 3 · Used by 1

Statement usesCounting process of interarrival times

Proof usesArrival times from interarrival times · Arrival times of exponential interarrivals are Erlang

Used byIndependent Poisson increments of the counting process

TheoremCounting process starts at zero almost surely#✓fully proved

The counting process of i.i.d. rate-r exponential interarrivals starts at 0 almost surely (all interarrival times are positive almost surely).

theorem ae_count_zero {T : ℕ → Ω → ℝ} {r : ℝ≥0} (hr : 0 < r)
    (hT : ∀ i, HasLaw (T i) (expMeasure r) P) : ∀ᵐ ω ∂P, count T 0 ω = 0

Uses 2 · Used by 1

Statement usesCounting process of interarrival times

Proof usesArrival times from interarrival times

Used byExponential interarrivals give a Poisson process

TheoremCounting process has nondecreasing paths almost surely#✓fully proved

The counting process of i.i.d. rate-r exponential interarrivals has nondecreasing paths almost surely (the arrival times tend to infinity almost surely, so every arrival set in [0, t] is finite).

theorem ae_count_monotone {T : ℕ → Ω → ℝ} {r : ℝ≥0} (hr : 0 < r)
    (hT : ∀ i, HasLaw (T i) (expMeasure r) P) (hind : iIndepFun T P) :
    ∀ᵐ ω ∂P, Monotone fun t ↦ count T t ω

Uses 2 · Used by 2

Statement usesCounting process of interarrival times

Proof usesArrival times from interarrival times

Used byIndependent Poisson increments of the counting process · Exponential interarrivals give a Poisson process

Probability Theory

TheoremSuperposition#✓fully proved

Superposition (Kingman 1993, §2.2): the sum of two independent Poisson processes of rates r₁ and r₂ is a Poisson process of rate r₁ + r₂. Independence is of the two processes as random paths.

theorem IsPoissonProcess.add {N₁ N₂ : ℝ≥0 → Ω → ℕ} {r₁ r₂ : ℝ≥0}
    (h₁ : IsPoissonProcess N₁ r₁ P) (h₂ : IsPoissonProcess N₂ r₂ P)
    (hind : IndepFun (fun ω t ↦ N₁ t ω) (fun ω t ↦ N₂ t ω) P) :
    IsPoissonProcess (N₁ + N₂) (r₁ + r₂) P

Uses 1

Statement usesPoisson process

DefinitionThinning of a Poisson process#✓fully proved

The thinning of N by the marks B: the number of indices i < N t with B i, i.e. the number of points of N in [0, t] that are kept when the i-th point (in time order, from 0) is kept iff B i.

noncomputable def PoissonProcess.thinning (N : ℝ≥0 → Ω → ℕ) (B : ℕ → Ω → Bool) (t : ℝ≥0)
    (ω : Ω) : ℕ :=
  ((Finset.range (N t ω)).filter fun i ↦ B i ω).card

Used by 1

Used byThinning

TheoremThinning#✓fully proved

Thinning (Kingman 1993, §5.1; Karlin–Taylor 1975, §4.1): keeping each point of a Poisson process of rate r independently with probability p, independently of the process, gives a Poisson process of rate p r. The marks B i are i.i.d. with P(B i) = p and independent of N as a random path.

theorem IsPoissonProcess.thinning {N : ℝ≥0 → Ω → ℕ} {r p : ℝ≥0} {B : ℕ → Ω → Bool}
    [IsProbabilityMeasure P] (hN : IsPoissonProcess N r P) (hp : p ≤ 1)
    (hBm : ∀ i, Measurable (B i)) (hB : ∀ i, P.real {ω | B i ω = true} = p)
    (hBind : iIndepFun B P) (hNB : IndepFun (fun ω t ↦ N t ω) (fun ω i ↦ B i ω) P) :
    IsPoissonProcess (PoissonProcess.thinning N B) (p * r) P

Uses 2

Statement usesPoisson process · Thinning of a Poisson process

Poisson Process

TheoremIndependent Poisson increments of the counting process#✓fully proved

The increments of the counting process of i.i.d. rate-r exponential interarrivals over consecutive intervals (t i, t (i + 1)] are independent with the Poisson laws of means r (t (i + 1) - t i): the increment vector has the product law (Kingman 1993, ch. 4; Karlin–Taylor 1975, ch. 4).

theorem hasLaw_count_increments {T : ℕ → Ω → ℝ} {r : ℝ≥0} (hr : 0 < r)
    (hT : ∀ i, HasLaw (T i) (expMeasure r) P) (hind : iIndepFun T P) (n : ℕ)
    (t : Fin (n + 1) → ℝ≥0) (ht : Monotone t) :
    HasLaw (fun ω (i : Fin n) ↦ count T (t i.succ) ω - count T (t i.castSucc) ω)
      (Measure.pi fun i ↦ poissonMeasure (r * (t i.succ - t i.castSucc))) P

Uses 4 · Used by 1

Statement usesCounting process of interarrival times

Proof usesCounting process has nondecreasing paths almost surely · Arrival times from interarrival times · Arrival counts of exponential interarrivals are Poisson

Used byExponential interarrivals give a Poisson process

TheoremExponential interarrivals give a Poisson process#✓fully proved

Exponential interarrivals give a Poisson process (Kingman 1993, ch. 4; Karlin–Taylor 1975, ch. 4): the counting process of i.i.d. rate-r exponential interarrival times is a Poisson process of rate r.

theorem isPoissonProcess_count {T : ℕ → Ω → ℝ} {r : ℝ≥0} (hr : 0 < r)
    (hT : ∀ i, HasLaw (T i) (expMeasure r) P) (hind : iIndepFun T P) :
    IsPoissonProcess (count T) r P

Uses 5

Statement usesPoisson process · Counting process of interarrival times

Proof usesCounting process has nondecreasing paths almost surely · Counting process starts at zero almost surely · Independent Poisson increments of the counting process

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.