The renewal central limit theorem

Let T 0, T 1, … be independent, identically distributed nonnegative waiting times on a probability space (Ω, P) whose common law has finite second moment and strictly positive variance σ² = Var[T 0; P] ≠ 0 (in Mathlib, Var[X; P] vanishes outside L², so Var[T 0; P] ≠ 0 encodes both MemLp (T 0) 2 P and 0 < σ²). Then the increments are not almost surely zero, their extended mean ∫⁻ ω, (T 0 ω : ℝ≥0∞) ∂P is finite and strictly positive, and its real value agrees with the Bochner expectation μ = P[fun ω ↦ (T 0 ω : ℝ)] > 0.

Writing N_t = renewalCountNat T t for the natural-valued renewal count at time t : ℝ≥0, this file proves that as t → ∞,

((N_t : ℝ) - t / μ) / (σ * √(t / μ ^ 3))  ⟶  𝒩(0, 1)

in distribution (MeasureTheory.TendstoInDistribution).

Proof outline

Following Feller's inversion argument, fix x : ℝ and set

u(t) = t / μ + x * σ * √(t / μ ^ 3),     m(t) = ⌊u(t)⌋₊ + 1.

1. Pathwise inversion (renewalCountNat_sub_div_le_iff): on a nonexplosive path, once t > 0 and u(t) ≥ 0, the count inequality ((N_t : ℝ) - t / μ) / (σ * √(t / μ ^ 3)) ≤ x is equivalent to N_t < m(t), hence by le_renewalCountNat_iff to t < arrival T (m(t)), which after centering by m(t) * μ and scaling by σ * √(m(t)) becomes -(arrival T (m(t)) - m(t) * μ) / (σ * √(m(t))) < (m(t) * μ - t) / (σ * √(m(t))).
2. Rounding asymptotics (tendsto_natFloor_add_one_div_add_mul_sqrt_atTop, tendsto_natFloor_add_one_mul_sub_div_sqrt_atTop): as t → ∞, m(t) → ∞, m(t) / (t / μ) → 1, and the rounding remainder m(t) - u(t) ∈ (0, 1] becomes negligible when divided by √(m(t)), so the threshold (m(t) * μ - t) / (σ * √(m(t))) converges to x.
3. Comparison with the scalar i.i.d. central limit theorem: applying Mathlib's ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum to the standardized negated increments -(T k - μ) / σ and sandwiching the threshold via MeasureTheory.tendsto_cdf_of_eventually_ae_le_iff_lt and continuity of the standard Gaussian cumulative distribution function yields pointwise CDF convergence (tendsto_cdf_renewalCountNat_sub_div), from which weak convergence follows by MeasureTheory.TendstoInDistribution.of_tendsto_cdf.

Both the ℝ≥0 real-time limit (with both P[T 0] and (∫⁻ T 0 ∂P).toReal formulations) and the ℝ real-time limit are provided; precomposing with MeasureTheory.TendstoInDistribution.comp_tendsto specializes them along any time family t_i → ∞ (in particular any sequence t_n → ∞). Zero waiting times are permitted.

Main statements

• TauCeti.Probability.renewalCountNat_sub_div_le_iff — pathwise inversion of the standardized count sublevel event into a standardized arrival-time event.
• TauCeti.Probability.tendsto_natFloor_add_one_div_add_mul_sqrt_atTop, TauCeti.Probability.tendsto_natFloor_add_one_mul_sub_div_sqrt_atTop — divergence of the arrival index m(s) = ⌊s / μ + x * σ * √(s / μ ^ 3)⌋₊ + 1 and convergence of the threshold (m(s) * μ - s) / (σ * √(m(s))) to x.
• TauCeti.Probability.tendsto_cdf_renewalCountNat_sub_div — pointwise convergence of the CDFs of the standardized renewal counts to cdf (gaussianReal 0 1).
• TauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div — the renewal central limit theorem along atTop : Filter ℝ≥0, together with its extended-mean form tendstoInDistribution_renewalCountNat_sub_div_toReal_lintegral and its real-axis form tendstoInDistribution_renewalCountNat_toNNReal_sub_div.

References

• William Feller, An Introduction to Probability Theory and Its Applications, vol. II, 2nd edition, Wiley, 1971, Chapter XI, §5, Theorem 5.
• Vincent Tassion, Applied Stochastic Processes, lecture notes, ETH Zürich, 2025, Chapter 5.

Pathwise inversion and rounding asymptotics

theorem TauCeti.Probability.renewalCountNat_sub_div_le_iff {Ω : Type u_1} {T : ℕ → Ω → NNReal} {ω : Ω} (hω : Filter.Tendsto (fun (n : ℕ) => arrival T n ω) Filter.atTop Filter.atTop) {μ σ : ℝ} (hμ : 0 < μ) (hσ : 0 < σ) (x : ℝ) {t : NNReal} (ht : 0 < t) (hu : 0 ≤ ↑t / μ + x * σ * √(↑t / μ ^ 3)) : have m := ⌊↑t / μ + x * σ * √(↑t / μ ^ 3)⌋₊ + 1; (↑(renewalCountNat T t ω) - ↑t / μ) / (σ * √(↑t / μ ^ 3)) ≤ x ↔ -(↑(arrival T m ω) - ↑m * μ) / (σ * √↑m) < (↑m * μ - ↑t) / (σ * √↑m)

Pathwise inversion for the standardized renewal count. On a nonexplosive path, once t > 0 and u = t / μ + x * σ * √(t / μ ^ 3) ≥ 0, the standardized count at time t is at most x if and only if the standardized negated m-th arrival time (with m = ⌊u⌋₊ + 1) lies strictly below the rounded threshold (m * μ - t) / (σ * √m).

theorem TauCeti.Probability.tendsto_natFloor_add_one_div_add_mul_sqrt_atTop {μ σ : ℝ} (hμ : 0 < μ) (x : ℝ) : Filter.Tendsto (fun (s : ℝ) => ⌊s / μ + x * σ * √(s / μ ^ 3)⌋₊ + 1) Filter.atTop Filter.atTop

The integer arrival index ⌊s / μ + x * σ * √(s / μ ^ 3)⌋₊ + 1 in the renewal inversion tends to infinity as s → ∞.

theorem TauCeti.Probability.tendsto_natFloor_add_one_mul_sub_div_sqrt_atTop {μ σ : ℝ} (hμ : 0 < μ) (hσ : 0 < σ) (x : ℝ) : Filter.Tendsto (fun (s : ℝ) => (↑(⌊s / μ + x * σ * √(s / μ ^ 3)⌋₊ + 1) * μ - s) / (σ * √↑(⌊s / μ + x * σ * √(s / μ ^ 3)⌋₊ + 1))) Filter.atTop (nhds x)

Rounding estimate for the renewal central limit theorem. For μ > 0, σ > 0, and x : ℝ, setting m(s) = ⌊s / μ + x * σ * √(s / μ ^ 3)⌋₊ + 1, the standardized threshold (m(s) * μ - s) / (σ * √(m(s))) converges to x as s → ∞.

The renewal central limit theorem

theorem TauCeti.Probability.tendsto_cdf_renewalCountNat_sub_div {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {T : ℕ → Ω → NNReal} (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hvar : ProbabilityTheory.variance (fun (ω : Ω) => ↑(T 0 ω)) P ≠ 0) (x : ℝ) : have μ := ∫ (x : Ω), (fun (ω : Ω) => ↑(T 0 ω)) x ∂P; have σ := √(ProbabilityTheory.variance (fun (ω : Ω) => ↑(T 0 ω)) P); Filter.Tendsto (fun (t : NNReal) => ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (ω : Ω) => (↑(renewalCountNat T t ω) - ↑t / μ) / (σ * √(↑t / μ ^ 3))) P)) x) Filter.atTop (nhds (↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x))

Pointwise CDF convergence in the renewal central limit theorem. For i.i.d. nonnegative increments with nonzero variance, the cumulative distribution function of the standardized renewal count at x converges to cdf (gaussianReal 0 1) x as t → ∞ in ℝ≥0.

theorem TauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {T : ℕ → Ω → NNReal} {Z : Ω' → ℝ} (hZ : ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) P') (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hvar : ProbabilityTheory.variance (fun (ω : Ω) => ↑(T 0 ω)) P ≠ 0) : MeasureTheory.TendstoInDistribution (fun (t : NNReal) (ω : Ω) => (↑(renewalCountNat T t ω) - ↑t / ∫ (x : Ω), (fun (ω : Ω) => ↑(T 0 ω)) x ∂P) / (√(ProbabilityTheory.variance (fun (ω : Ω) => ↑(T 0 ω)) P) * √(↑t / (∫ (x : Ω), (fun (ω : Ω) => ↑(T 0 ω)) x ∂P) ^ 3))) Filter.atTop Z (fun (x : NNReal) => P) P'

The renewal central limit theorem. Let T 0, T 1, … be independent, identically distributed nonnegative waiting times with nonzero variance σ² = Var[T 0; P] and expectation μ = P[T 0]. As t → ∞ in ℝ≥0, the standardized renewal count ((N_t : ℝ) - t / μ) / (σ * √(t / μ ^ 3)) converges in distribution to any standard normal random variable Z. Precomposing with MeasureTheory.TendstoInDistribution.comp_tendsto gives convergence along any time family (in particular any sequence) tending to atTop.

theorem TauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div_toReal_lintegral {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {T : ℕ → Ω → NNReal} {Z : Ω' → ℝ} (hZ : ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) P') (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hvar : ProbabilityTheory.variance (fun (ω : Ω) => ↑(T 0 ω)) P ≠ 0) : MeasureTheory.TendstoInDistribution (fun (t : NNReal) (ω : Ω) => (↑(renewalCountNat T t ω) - ↑t / (∫⁻ (ω : Ω), ↑(T 0 ω) ∂P).toReal) / (√(ProbabilityTheory.variance (fun (ω : Ω) => ↑(T 0 ω)) P) * √(↑t / (∫⁻ (ω : Ω), ↑(T 0 ω) ∂P).toReal ^ 3))) Filter.atTop Z (fun (x : NNReal) => P) P'

The renewal central limit theorem (extended-mean formulation). Same limit as tendstoInDistribution_renewalCountNat_sub_div, written in terms of the extended mean (∫⁻ ω, (T 0 ω : ℝ≥0∞) ∂P).toReal of the waiting-time distribution.

theorem TauCeti.Probability.tendstoInDistribution_renewalCountNat_toNNReal_sub_div {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {T : ℕ → Ω → NNReal} {Z : Ω' → ℝ} (hZ : ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) P') (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (hvar : ProbabilityTheory.variance (fun (ω : Ω) => ↑(T 0 ω)) P ≠ 0) : MeasureTheory.TendstoInDistribution (fun (t : ℝ) (ω : Ω) => (↑(renewalCountNat T t.toNNReal ω) - t / ∫ (x : Ω), (fun (ω : Ω) => ↑(T 0 ω)) x ∂P) / (√(ProbabilityTheory.variance (fun (ω : Ω) => ↑(T 0 ω)) P) * √(t / (∫ (x : Ω), (fun (ω : Ω) => ↑(T 0 ω)) x ∂P) ^ 3))) Filter.atTop Z (fun (x : ℝ) => P) P'

The renewal central limit theorem on the real time axis. As t → ∞ in ℝ, the standardized renewal count at t.toNNReal converges in distribution to a standard normal law.