Finite moments of the renewal counts

Let T 0, T 1, … be independent, identically distributed nonnegative increments that are not almost surely zero, with arrival times arrival T n and counts renewalCount T t as in TauCeti.Probability.Renewal.Basic. This file shows that every count has finite moments of every order, without any assumption on the mean of the increments: the mean may be infinite.

The argument is a Chernoff bound for the lower tail of the arrival times. Writing ρ(s) = 𝔼[exp (-s T 0)] for the Laplace transform of the increment law at rate s ≥ 0, Markov's inequality and independence give

P(n ≤ N t) = P(arrival T n ≤ t) ≤ exp (s t) · ρ(s) ^ n,

and ρ(s) < 1 for s > 0 because the increments are not almost surely zero. So the tail of N t decays geometrically. Past M ≈ L t arrivals, with L chosen so that e · ρ(1) ^ L ≤ 1, the factor exp t is absorbed, which gives 𝔼[(N t) ^ p] ≤ C (t + 1) ^ p with C independent of t. Since the count is nondecreasing in time, these moments also bound the counts on every bounded time interval. Finite moments supply the local integrability used for the renewal function m t = 𝔼[N t], and their polynomial growth gives the uniform integrability of N t / t behind the elementary renewal theorem.

Main results

• TauCeti.Probability.measureReal_arrival_le_le_exp_mul_mgf_pow — the Chernoff bound P(arrival T n ≤ t) ≤ exp (s t) · mgf (T 0) P (-s) ^ n.
• TauCeti.Probability.exists_lintegral_renewalCount_pow_le — ∫⁻ (N t) ^ p ≤ C (t + 1) ^ p for a constant C independent of t.
• TauCeti.Probability.lintegral_renewalCount_pow_lt_top — ∫⁻ (N t) ^ p < ∞ for every p : ℕ.
• TauCeti.Probability.memLp_toReal_renewalCount — the real-valued count lies in Lᵖ for every finite p.
• TauCeti.Probability.integrable_toReal_renewalCount — the real-valued count is integrable.

References

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

theorem TauCeti.Probability.measureReal_arrival_le_le_exp_mul_mgf_pow {Ω : 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) {s : ℝ} (hs : 0 ≤ s) (t : NNReal) (n : ℕ) : P.real {ω : Ω | arrival T n ω ≤ t} ≤ Real.exp (s * ↑t) * ProbabilityTheory.mgf (fun (ω : Ω) => ↑(T 0 ω)) P (-s) ^ n

Chernoff bound for the arrival times. For independent, identically distributed increments and every rate s ≥ 0, the probability that the n-th arrival is at most t is at most exp (s t) times the n-th power of the Laplace transform mgf (T 0) P (-s) of the increment law. By natCast_le_renewalCount_iff this is also a bound on P(n ≤ renewalCount T t).

theorem TauCeti.Probability.exists_lintegral_renewalCount_pow_le {Ω : 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) (p : ℕ) : ∃ (C : NNReal), ∀ (t : NNReal), ∫⁻ (ω : Ω), renewalCount T t ω ^ p ∂P ≤ ↑C * ↑(t + 1) ^ p

Polynomial growth of the moments of the renewal counts. For independent, identically distributed increments that are not almost surely zero, the p-th moment of the count grows at most like the p-th power of time: there is a constant C with ∫⁻ (N t) ^ p ≤ C * (t + 1) ^ p for every t. No assumption is made on the mean of the increments.

theorem TauCeti.Probability.lintegral_renewalCount_pow_lt_top {Ω : 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) (t : NNReal) (p : ℕ) : ∫⁻ (ω : Ω), renewalCount T t ω ^ p ∂P < ⊤

Finite moments of the renewal counts. For independent, identically distributed increments that are not almost surely zero, every count renewalCount T t has a finite moment of every order p. No assumption is made on the mean of the increments.

theorem TauCeti.Probability.memLp_toReal_renewalCount {Ω : 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) (t : NNReal) {p : ENNReal} (hp : p ≠ ⊤) : MeasureTheory.MemLp (fun (ω : Ω) => (renewalCount T t ω).toReal) p P

For independent, identically distributed increments that are not almost surely zero, the real-valued count (renewalCount T t).toReal lies in Lᵖ for every finite exponent p. It agrees almost surely with the count, which is almost surely finite.

theorem TauCeti.Probability.integrable_toReal_renewalCount {Ω : 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) (t : NNReal) : MeasureTheory.Integrable (fun (ω : Ω) => (renewalCount T t ω).toReal) P

For independent, identically distributed increments that are not almost surely zero, the real-valued count (renewalCount T t).toReal is integrable.