Arrival times and counts of an ordinary renewal process

Let T 0, T 1, … be nonnegative increments, with T i the waiting time between the i-th and the (i + 1)-st renewal. This file defines the arrival times and the counting process

arrival T n = T 0 + ⋯ + T (n - 1),     renewalCount T t = #{n ≥ 1 | arrival T n ≤ t},

so that arrival T 0 = 0 is the artificial arrival at time zero, which is not counted, while genuine arrivals at time zero (zero increments) are counted with multiplicity. Time and increments live in ℝ≥0. The count is extended-valued, renewalCount T t ω : ℝ≥0∞, so that it is defined and measurable before one knows that it is finite.

The deterministic part of the file relates the two objects: n ≤ renewalCount T t ω exactly when arrival T n ω ≤ t; the count equals n exactly when arrival T n ω ≤ t < arrival T (n + 1) ω; it is infinite exactly when every arrival is at most t; it is nondecreasing and right-continuous in t; and it is finite for every t exactly when the arrival times tend to infinity.

The probabilistic part shows that the process does not explode: if the increments are independent and identically distributed and not almost surely zero, then almost surely the arrival times tend to infinity, and hence almost surely renewalCount T t is finite simultaneously for all t. The proof applies the second Borel–Cantelli lemma to the events {a ≤ T n} for a threshold a > 0 of positive probability. For i.i.d. increments with common law F, the n-th arrival time has law the convolution power F^{∗n}. Finally, the law of each count depends only on F: it is the law of the count of the coordinate process under the product measure Measure.infinitePi (fun _ ↦ F), on which Mathlib's iIndepFun_infinitePi constructs the increments.

Main definitions

• TauCeti.Probability.arrival — the n-th arrival time ∑ i ∈ Finset.range n, T i.
• TauCeti.Probability.renewalCount — the extended number of arrivals with index n ≥ 1 in [0, t].

Main results

• TauCeti.Probability.natCast_le_renewalCount_iff — n ≤ N t ↔ arrival n ≤ t.
• TauCeti.Probability.renewalCount_eq_natCast_iff — N t = n ↔ arrival n ≤ t < arrival (n + 1).
• TauCeti.Probability.continuousWithinAt_renewalCount_Ici — right continuity of the count.
• TauCeti.Probability.tendsto_arrival_atTop_iff — nonexplosion is finiteness of every count.
• TauCeti.Probability.ae_tendsto_arrival_atTop, TauCeti.Probability.ae_renewalCount_lt_top — i.i.d. increments that are not almost surely zero do not explode.
• TauCeti.Probability.hasLaw_arrival — for i.i.d. increments with law F, the n-th arrival time has law the convolution power F^{∗n}, and TauCeti.Probability.hasLaw_arrival_shift, the same for the process restarted at the m-th arrival.
• TauCeti.Probability.map_renewalCount_eq_infinitePi_map — the law of a count is computed on the canonical product space.

References

• William Feller, An Introduction to Probability Theory and Its Applications, vol. II, 2nd edition, Wiley, 1971, Chapter XI, §1.

Arrival times

def TauCeti.Probability.arrival {Ω : Type u_1} (T : ℕ → Ω → NNReal) (n : ℕ) (ω : Ω) : NNReal

The n-th arrival time T 0 + ⋯ + T (n - 1) of the renewal process with increments T. The artificial arrival at time zero is arrival T 0 = 0.

theorem TauCeti.Probability.arrival_def {Ω : Type u_1} (T : ℕ → Ω → NNReal) (n : ℕ) (ω : Ω) : arrival T n ω = ∑ i ∈ Finset.range n, T i ω

@[simp]

theorem TauCeti.Probability.arrival_zero {Ω : Type u_1} (T : ℕ → Ω → NNReal) (ω : Ω) : arrival T 0 ω = 0

theorem TauCeti.Probability.arrival_succ {Ω : Type u_1} (T : ℕ → Ω → NNReal) (n : ℕ) (ω : Ω) : arrival T (n + 1) ω = arrival T n ω + T n ω

theorem TauCeti.Probability.arrival_add {Ω : Type u_1} (T : ℕ → Ω → NNReal) (m k : ℕ) (ω : Ω) : arrival T (m + k) ω = arrival T m ω + arrival (fun (i : ℕ) => T (m + i)) k ω

The (m + k)-th arrival time is the m-th one plus the k-th arrival time of the renewal process restarted at the m-th arrival, whose increments are T m, T (m + 1), ….

theorem TauCeti.Probability.monotone_arrival {Ω : Type u_1} (T : ℕ → Ω → NNReal) (ω : Ω) : Monotone fun (n : ℕ) => arrival T n ω

The arrival times are nondecreasing.

theorem TauCeti.Probability.strictMono_arrival_succ {Ω : Type u_1} (T : ℕ → Ω → NNReal) {ω : Ω} (hT : ∀ (n : ℕ), 0 < T (n + 1) ω) : StrictMono fun (n : ℕ) => arrival T (n + 1) ω

Positive increments after the first give strictly increasing positive-index arrivals. The first increment may vanish.

theorem TauCeti.Probability.measurable_arrival_of_lt {Ω : Type u_1} {x✝ : MeasurableSpace Ω} {T : ℕ → Ω → NNReal} {n : ℕ} (hT : ∀ i < n, Measurable (T i)) : Measurable (arrival T n)

The n-th arrival time is measurable as soon as the increments T 0, …, T (n - 1) are.

theorem TauCeti.Probability.measurable_arrival {Ω : Type u_1} [MeasurableSpace Ω] {T : ℕ → Ω → NNReal} (hT : ∀ (n : ℕ), Measurable (T n)) (n : ℕ) : Measurable (arrival T n)

theorem TauCeti.Probability.aemeasurable_arrival {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {T : ℕ → Ω → NNReal} (hT : ∀ (n : ℕ), AEMeasurable (T n) P) (n : ℕ) : AEMeasurable (arrival T n) P

If every increment is almost-everywhere measurable, so is every arrival time.

theorem TauCeti.Probability.arrival_congr_ae {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {T T' : ℕ → Ω → NNReal} (h : ∀ (n : ℕ), T n =ᵐ[P] T' n) : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), arrival T n ω = arrival T' n ω

If two increment sequences agree almost everywhere at each index, then almost everywhere all of their arrival times agree.

The counting process

noncomputable def TauCeti.Probability.renewalCount {Ω : Type u_1} (T : ℕ → Ω → NNReal) (t : NNReal) (ω : Ω) : ENNReal

The number #{n ≥ 1 | arrival T n ω ≤ t} of arrivals in [0, t], counted with multiplicity, as an extended nonnegative number. The artificial arrival arrival T 0 = 0 is not counted.

theorem TauCeti.Probability.renewalCount_def {Ω : Type u_1} (T : ℕ → Ω → NNReal) (t : NNReal) (ω : Ω) : renewalCount T t ω = ∑' (n : ℕ), if arrival T (n + 1) ω ≤ t then 1 else 0

theorem TauCeti.Probability.measurable_renewalCount {Ω : Type u_1} [MeasurableSpace Ω] {T : ℕ → Ω → NNReal} (hT : ∀ (n : ℕ), Measurable (T n)) (t : NNReal) : Measurable (renewalCount T t)

@[simp]

theorem TauCeti.Probability.natCast_le_renewalCount_iff {Ω : Type u_1} {T : ℕ → Ω → NNReal} {t : NNReal} {ω : Ω} {n : ℕ} : ↑n ≤ renewalCount T t ω ↔ arrival T n ω ≤ t

At least n arrivals occur in [0, t] exactly when the n-th arrival time is at most t. For n = 0 both sides hold trivially.

theorem TauCeti.Probability.renewalCount_eq_natCast_iff {Ω : Type u_1} {T : ℕ → Ω → NNReal} {t : NNReal} {ω : Ω} {n : ℕ} : renewalCount T t ω = ↑n ↔ arrival T n ω ≤ t ∧ t < arrival T (n + 1) ω

The count at time t equals n exactly when arrival T n ω ≤ t < arrival T (n + 1) ω.

@[simp]

theorem TauCeti.Probability.renewalCount_eq_top_iff {Ω : Type u_1} {T : ℕ → Ω → NNReal} {t : NNReal} {ω : Ω} : renewalCount T t ω = ⊤ ↔ ∀ (n : ℕ), arrival T n ω ≤ t

The count at time t is infinite exactly when every arrival time is at most t.

@[simp]

theorem TauCeti.Probability.renewalCount_lt_top_iff {Ω : Type u_1} {T : ℕ → Ω → NNReal} {t : NNReal} {ω : Ω} : renewalCount T t ω < ⊤ ↔ ∃ (n : ℕ), t < arrival T n ω

The count at time t is finite exactly when some arrival time exceeds t.

theorem TauCeti.Probability.exists_renewalCount_eq_natCast {Ω : Type u_1} {T : ℕ → Ω → NNReal} {t : NNReal} {ω : Ω} (h : renewalCount T t ω ≠ ⊤) : ∃ (n : ℕ), renewalCount T t ω = ↑n

A finite count is a natural number.

theorem TauCeti.Probability.monotone_renewalCount {Ω : Type u_1} {T : ℕ → Ω → NNReal} (ω : Ω) : Monotone fun (t : NNReal) => renewalCount T t ω

The count is nondecreasing in time.

theorem TauCeti.Probability.eventually_renewalCount_eq_nhdsGE {Ω : Type u_1} {T : ℕ → Ω → NNReal} (t : NNReal) (ω : Ω) : ∀ᶠ (s : NNReal) in nhdsWithin t (Set.Ici t), renewalCount T s ω = renewalCount T t ω

The count is locally constant to the right of every time.

theorem TauCeti.Probability.continuousWithinAt_renewalCount_Ici {Ω : Type u_1} {T : ℕ → Ω → NNReal} (t : NNReal) (ω : Ω) : ContinuousWithinAt (fun (s : NNReal) => renewalCount T s ω) (Set.Ici t) t

The count is right-continuous in time.

theorem TauCeti.Probability.tendsto_arrival_atTop_iff {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} : Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop ↔ ∀ (t : NNReal), renewalCount T t ω < ⊤

The process does not explode at ω, i.e. its arrival times tend to infinity, exactly when every count is finite.

theorem TauCeti.Probability.tendsto_arrival_atTop_of_frequently_le {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} {a : NNReal} (ha : 0 < a) (h : ∃ᶠ (n : ℕ) in Filter.atTop, a ≤ T n ω) : Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop

If infinitely many increments are at least a > 0, the arrival times tend to infinity.

Nonexplosion for i.i.d. increments

theorem TauCeti.Probability.ae_tendsto_arrival_atTop {Ω : Type u_1} {T : ℕ → Ω → NNReal} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hzero : P {ω : Ω | T 0 ω = 0} < 1) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop

Nonexplosion of a renewal process. If the increments are independent, identically distributed and not almost surely zero, then almost surely the arrival times tend to infinity.

theorem TauCeti.Probability.ae_renewalCount_lt_top {Ω : Type u_1} {T : ℕ → Ω → NNReal} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hzero : P {ω : Ω | T 0 ω = 0} < 1) : ∀ᵐ (ω : Ω) ∂P, ∀ (t : NNReal), renewalCount T t ω < ⊤

Finiteness of the renewal counts. For independent, identically distributed increments that are not almost surely zero, almost surely every count renewalCount T t is finite. The almost-sure quantifier is outside the quantifier over all times.

theorem TauCeti.Probability.hasLaw_arrival {Ω : Type u_1} {T : ℕ → Ω → NNReal} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (n : ℕ) : ProbabilityTheory.HasLaw (arrival T n) ((MeasureTheory.Measure.map (T 0) P).convolutionPower n) P

For independent increments with common law F = P.map (T 0), the n-th arrival time arrival T n has law the convolution power F^{∗n}.

theorem TauCeti.Probability.hasLaw_arrival_shift {Ω : Type u_1} {T : ℕ → Ω → NNReal} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (m k : ℕ) : ProbabilityTheory.HasLaw (arrival (fun (i : ℕ) => T (m + i)) k) ((MeasureTheory.Measure.map (T 0) P).convolutionPower k) P

For independent increments with common law F = P.map (T 0), the renewal process restarted at the m-th arrival, with increments T m, T (m + 1), …, has the same arrival-time laws: its k-th arrival time arrival T (m + k) - arrival T m has law F^{∗k}.

theorem TauCeti.Probability.map_renewalCount_eq_infinitePi_map {Ω : Type u_1} {T : ℕ → Ω → NNReal} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} (hT : ∀ (n : ℕ), Measurable (T n)) (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (t : NNReal) : MeasureTheory.Measure.map (renewalCount T t) P = MeasureTheory.Measure.map (renewalCount (fun (n : ℕ) (w : ℕ → NNReal) => w n) t) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.Measure.map (T 0) P)

Transfer to the canonical product space. For independent, identically distributed increments, the law of renewalCount T t is the law of the count of the coordinate process under the product measure whose factors are the common law of the increments.