The almost-sure renewal law of large numbers

For pairwise independent, identically distributed nonnegative increments that are not almost surely zero, the number of arrivals per unit time converges almost surely to the reciprocal of the extended mean increment. The reciprocal is taken before conversion to a real number, so infinite mean gives rate zero. Zero increments, including genuine arrivals at time zero, are allowed.

The deterministic inversion theorem transfers a limit for reciprocal arrival averages to a limit for the count at all real nonnegative times, not only at integer times. The probabilistic result applies the ordinary strong law for finite mean and the truncated strong law for infinite mean. It works on any realization of the increments.

References

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

theorem TauCeti.Probability.tendsto_renewalCountNat_div_of_tendsto {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} {r : ℝ} (hω : Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop) (h : Filter.Tendsto (fun (n : ℕ) => ↑n / ↑(arrival T n ω)) Filter.atTop (nhds r)) : Filter.Tendsto (fun (t : NNReal) => ↑(renewalCountNat T t ω) / ↑t) Filter.atTop (nhds r)

Inverting arrival times preserves the limit of reciprocal averages. The hypothesis of nonexplosion permits zero increments and ensures that the natural-valued count is the true count.

theorem TauCeti.Probability.ae_tendsto_natCast_div_arrival {Ω : Type u_1} {T : ℕ → Ω → NNReal} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (T i) (T j) P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hzero : P {ω : Ω | T 0 ω = 0} < 1) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (n : ℕ) => ↑n / ↑(arrival T n ω)) Filter.atTop (nhds (∫⁻ (ω : Ω), ↑(T 0 ω) ∂P)⁻¹.toReal)

The reciprocal arrival averages converge almost surely to the reciprocal extended mean. This includes infinite mean, where the limit is zero.

theorem TauCeti.Probability.ae_tendsto_renewalCountNat_div {Ω : Type u_1} {T : ℕ → Ω → NNReal} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (T i) (T j) P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hzero : P {ω : Ω | T 0 ω = 0} < 1) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (t : NNReal) => ↑(renewalCountNat T t ω) / ↑t) Filter.atTop (nhds (∫⁻ (ω : Ω), ↑(T 0 ω) ∂P)⁻¹.toReal)

Almost-sure renewal law of large numbers. The count per unit time converges to the reciprocal of the extended mean increment, with rate zero for infinite mean. The convergence holds along the full nonnegative real time axis on a single event of probability one. Pairwise independence suffices; the identical-distribution hypothesis supplies almost-everywhere measurability of the increments.