The elementary renewal theorem

Let T 0, T 1, … be independent, identically distributed nonnegative increments that are not almost surely zero, with extended mean μ = 𝔼[T 0] ∈ (0, ∞] and rate r = (μ⁻¹).toReal, so that r = 0 when the mean is infinite. The almost-sure renewal law of large numbers (TauCeti.Probability.ae_tendsto_renewalCountNat_div) says that N t / t → r almost surely. This file upgrades it to convergence in L¹ and deduces the elementary renewal theorem: the renewal function m t = 𝔼[N t] satisfies m t / t → r as t → ∞, also when the mean is infinite.

The upgrade is Vitali's convergence theorem. The family N t / t, t ≥ 1, is uniformly integrable because its second moments are bounded: 𝔼[(N t) ^ 2] grows at most quadratically in t (TauCeti.Probability.exists_lintegral_renewalCount_pow_le), and a family bounded in L² is uniformly integrable by the de la Vallée Poussin criterion. Mathlib's Vitali theorem is stated for sequences, and the continuous-time limit follows by testing along every sequence of times tending to infinity.

Main results

• TauCeti.Probability.uniformIntegrable_renewalCountNat_div — the family N t / t, t ≥ 1, is uniformly integrable.
• TauCeti.Probability.tendsto_eLpNorm_renewalCountNat_div_sub — N t / t → r in L¹.
• TauCeti.Probability.tendsto_integral_renewalCountNat_div — 𝔼[N t] / t → r.
• MeasureTheory.Measure.tendsto_renewalFunction_div — the elementary renewal theorem m t / t → r for the renewal function of a probability measure on ℝ≥0 other than the point mass at zero.

References

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

theorem TauCeti.Probability.uniformIntegrable_renewalCountNat_div {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {T : ℕ → Ω → NNReal} (hT : ∀ (n : ℕ), Measurable (T n)) (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hzero : P {ω : Ω | T 0 ω = 0} < 1) : MeasureTheory.UniformIntegrable (fun (t : ↑(Set.Ici 1)) (ω : Ω) => ↑(renewalCountNat T (↑t) ω) / ↑↑t) 1 P

Uniform integrability of the renewal counts per unit time. For independent, identically distributed increments that are not almost surely zero, the family N t / t, t ≥ 1, is uniformly integrable. No assumption is made on the mean of the increments.

theorem TauCeti.Probability.tendsto_eLpNorm_renewalCountNat_div_sub {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {T : ℕ → Ω → NNReal} (hT : ∀ (n : ℕ), Measurable (T n)) (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hzero : P {ω : Ω | T 0 ω = 0} < 1) : Filter.Tendsto (fun (t : NNReal) => MeasureTheory.eLpNorm (fun (ω : Ω) => ↑(renewalCountNat T t ω) / ↑t - (∫⁻ (ω : Ω), ↑(T 0 ω) ∂P)⁻¹.toReal) 1 P) Filter.atTop (nhds 0)

The renewal law of large numbers in L¹. For independent, identically distributed increments that are not almost surely zero, N t / t converges in L¹ to the reciprocal of the extended mean increment, with rate zero for infinite mean.

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

The elementary renewal theorem, on any realization of the increments: for independent, identically distributed increments that are not almost surely zero, the expected count per unit time converges to the reciprocal of the extended mean increment, with rate zero for infinite mean.

theorem MeasureTheory.Measure.tendsto_renewalFunction_div (μ : Measure NNReal) [IsProbabilityMeasure μ] (hμ : μ {0} < 1) : Filter.Tendsto (fun (t : NNReal) => (μ.renewalFunction t).toReal / ↑t) Filter.atTop (nhds (∫⁻ (x : NNReal), ↑x ∂μ)⁻¹.toReal)

The elementary renewal theorem. For a probability measure μ on ℝ≥0 other than the point mass at zero, the renewal function satisfies m t / t → (𝔼 μ)⁻¹ as t → ∞, where the reciprocal of the extended mean is taken before conversion to a real number, so that the limit is zero for infinite mean.