Natural-valued renewal counts

renewalCountNat T t is the number of positive-index arrivals by time t on paths whose arrival times tend to infinity. On every other path it is zero at all times. Using one exceptional event for the whole path preserves monotonicity and right continuity everywhere. Zero increments are allowed, so genuine arrivals at zero are retained.

On a nonexplosive path the natural count agrees with the extended count renewalCount and satisfies the inverse relations with arrival. In particular it can be used as an arrival index when defining the excess waiting time. For nondegenerate i.i.d. increments the two counts agree almost surely, simultaneously at all times. Whenever nonexplosion holds almost surely, any other natural-valued version agreeing on the nonexplosion event has the same process law. The process law also transfers to the canonical product realization of the increments.

References

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

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

The natural-valued renewal count, equal to the extended count on nonexplosive paths and zero at every time on explosive paths. The artificial arrival at index zero is omitted.

theorem TauCeti.Probability.renewalCountNat_def {Ω : Type u_1} (T : ℕ → Ω → NNReal) (t : NNReal) (ω : Ω) : renewalCountNat T t ω = if Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop then ⌊(renewalCount T t ω).toReal⌋₊ else 0

@[simp]

theorem TauCeti.Probability.renewalCountNat_eq_zero_of_not_tendsto {Ω : Type u_1} (T : ℕ → Ω → NNReal) {ω : Ω} (hω : ¬Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop) (t : NNReal) : renewalCountNat T t ω = 0

The exceptional value is zero for the entire explosive path.

@[simp]

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

On a nonexplosive path the natural count is exactly the extended count.

theorem TauCeti.Probability.natCast_renewalCountNat_le {Ω : Type u_1} (T : ℕ → Ω → NNReal) (t : NNReal) (ω : Ω) : ↑(renewalCountNat T t ω) ≤ renewalCount T t ω

The natural-valued count never exceeds the extended count: they agree on nonexplosive paths, and the natural-valued count is zero on the others.

theorem TauCeti.Probability.le_renewalCountNat_iff {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} (hω : Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop) {t : NNReal} {n : ℕ} : n ≤ renewalCountNat T t ω ↔ arrival T n ω ≤ t

The natural count reaches n exactly when the n-th arrival has occurred.

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

On a nonexplosive path the number of arrivals tends to infinity with time.

theorem TauCeti.Probability.renewalCountNat_eq_iff {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} (hω : Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop) {t : NNReal} {n : ℕ} : renewalCountNat T t ω = n ↔ arrival T n ω ≤ t ∧ t < arrival T (n + 1) ω

The count equals n exactly between the n-th and (n + 1)-st arrivals, including the left endpoint and excluding the right endpoint.

@[simp]

theorem TauCeti.Probability.renewalCountNat_const {Ω : Type u_1} {a : NNReal} (ha : 0 < a) (t : NNReal) (ω : Ω) : renewalCountNat (fun (x : ℕ) (x_1 : Ω) => a) t ω = ⌊t / a⌋₊

Deterministic positive increments give the usual floor count, including an arrival exactly at time t and excluding the artificial arrival at zero.

theorem TauCeti.Probability.arrival_renewalCountNat_le {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} (hω : Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop) (t : NNReal) : arrival T (renewalCountNat T t ω) ω ≤ t

The arrival indexed by the count has already occurred.

theorem TauCeti.Probability.lt_arrival_renewalCountNat_succ {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} (hω : Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop) (t : NNReal) : t < arrival T (renewalCountNat T t ω + 1) ω

The arrival immediately after the count is strictly in the future.

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

The natural count is nondecreasing, including on explosive paths.

theorem TauCeti.Probability.renewalCountNat_eq_sum_range_of_le {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} {s t : NNReal} (hst : s ≤ t) : renewalCountNat T s ω = ∑ k ∈ Finset.range (renewalCountNat T t ω), if arrival T (k + 1) ω ≤ s then 1 else 0

Before the observation time, the natural count is the finite sum over the completed arrivals at that time. The artificial arrival at index zero is omitted. On explosive paths both sides are zero by the count's exceptional-path convention.

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

The natural count is locally constant to the right, even on the exceptional event.

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

Every natural-count path is right-continuous.

@[simp]

theorem TauCeti.Probability.renewalCountNat_comp {Ω : Type u_1} (T : ℕ → Ω → NNReal) {Ω' : Type u_2} (f : Ω' → Ω) (t : NNReal) (ω : Ω') : renewalCountNat (fun (n : ℕ) (ω : Ω') => T n (f ω)) t ω = renewalCountNat T t (f ω)

Forming the count commutes with a change of sample space.

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

The natural-valued count is measurable.

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

If every increment is almost-everywhere measurable, so is the natural-valued renewal count at every time t.

theorem TauCeti.Probability.ae_natCast_renewalCountNat {Ω : 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), ↑(renewalCountNat T t ω) = renewalCount T t ω

For nondegenerate i.i.d. increments, the natural and extended counts agree almost surely on one event for all times.

theorem TauCeti.Probability.map_renewalCountNat_eq_of_nonexplosion {Ω : Type u_1} {T : ℕ → Ω → NNReal} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} (hP : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop) {N : NNReal → Ω → ℕ} (hN : ∀ (ω : Ω), Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop → ∀ (t : NNReal), ↑(N t ω) = renewalCount T t ω) : MeasureTheory.Measure.map (fun (ω : Ω) (t : NNReal) => renewalCountNat T t ω) P = MeasureTheory.Measure.map (fun (ω : Ω) (t : NNReal) => N t ω) P

Changing the natural-valued count on explosive paths does not change its process law when nonexplosion holds almost surely. This equality of pushforwards needs no measurability assumption on the chosen version.

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

The entire natural-count process has the same law in any i.i.d. realization as on the canonical product space. This includes its exceptional-path convention and all finite-time joint distributions.