The renewal measure and the renewal function

For a measure F on an additive monoid, the renewal measure is the sum of its convolution powers,

U = ∑ n, F^{∗n} = δ₀ + F + F ∗ F + ⋯,

where F^{∗0} = δ₀ is Measure.convolutionPower F 0. It satisfies the renewal equation U = δ₀ + F ∗ U. When F is the law of the increments of a renewal process, F^{∗n} is the law of the n-th arrival time, so U s is the expected number of arrival times in s, counting the artificial arrival at time zero. This file proves that identity for the intervals [0, t].

On the half-line ℝ≥0, the renewal function is m t = (F ∗ U) [0, t] = ∑_{n ≥ 1} F^{∗n} [0, t]. For independent increments with law F, it is the expected count 𝔼[N t] of the renewal process, and U [0, t] = 1 + m t; this holds also when F has an atom at zero. If F is a probability measure with F {0} < 1, the finite moments of the renewal counts show that m t is finite. Hence U is finite on bounded intervals, and m is nondecreasing and right-continuous. The renewal measure and the renewal function are the objects of the renewal limit theorems and of the solution g = h ∗ U of the renewal equation g = h + g ∗ F.

Main definitions

• MeasureTheory.Measure.renewalMeasure — the renewal measure ∑ n, F^{∗n}.
• MeasureTheory.Measure.renewalFunction — the renewal function t ↦ (F ∗ U) [0, t] on ℝ≥0.

Main results

• MeasureTheory.Measure.convolutionPower_le_renewalMeasure, MeasureTheory.Measure.summable_convolutionPower_real — each F^{∗n} is dominated by U, and the masses F^{∗n} s are summable when U s is finite.
• MeasureTheory.Measure.isLocallyFiniteMeasure_of_renewalMeasure — F is locally finite when U is.
• MeasureTheory.Measure.renewalMeasure_eq_dirac_add_conv — the renewal equation U = δ₀ + F ∗ U.
• MeasureTheory.Measure.renewalFunction_eq_tsum — m t = ∑_{n ≥ 1} F^{∗n} [0, t].
• MeasureTheory.Measure.renewalMeasure_Iic — U [0, t] = 1 + m t.
• TauCeti.Probability.lintegral_renewalCount — 𝔼[N t] = m t for i.i.d. increments, and TauCeti.Probability.integral_renewalCountNat, its real form for the natural-valued count.
• MeasureTheory.Measure.renewalFunction_lt_top, MeasureTheory.Measure.isLocallyFiniteMeasure_renewalMeasure — local finiteness when F {0} < 1.
• MeasureTheory.Measure.continuousWithinAt_renewalFunction_Ici — right continuity of m.

References

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

The renewal measure

noncomputable def MeasureTheory.Measure.renewalMeasure {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) : Measure α

The renewal measure ∑ n, μ^{∗n} of a measure μ: the sum of all its convolution powers, including the point mass μ^{∗0} = δ₀. For the law μ of the increments of a renewal process, its mass on [0, t] is one more than the expected number of arrivals in [0, t] (renewalMeasure_Iic and TauCeti.Probability.lintegral_renewalCount).

theorem MeasureTheory.Measure.renewalMeasure_def {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) : μ.renewalMeasure = sum μ.convolutionPower

theorem MeasureTheory.Measure.renewalMeasure_apply {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) {s : Set α} : μ.renewalMeasure s = ∑' (n : ℕ), (μ.convolutionPower n) s

theorem MeasureTheory.Measure.map_renewalMeasure {α : Type u_1} [MeasurableSpace α] [AddMonoid α] {β : Type u_2} [MeasurableSpace β] [AddMonoid β] [MeasurableAdd₂ α] [MeasurableAdd₂ β] (μ : Measure α) [SFinite μ] (f : α →+ β) (hf : Measurable ⇑f) : map (⇑f) μ.renewalMeasure = (map (⇑f) μ).renewalMeasure

A measurable additive homomorphism transports the renewal measure to the renewal measure of the transported increment law.

theorem MeasureTheory.Measure.convolutionPower_le_renewalMeasure {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) (n : ℕ) : μ.convolutionPower n ≤ μ.renewalMeasure

Each convolution power is dominated by the renewal measure.

theorem MeasureTheory.Measure.le_renewalMeasure {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (μ : Measure α) [SFinite μ] : μ ≤ μ.renewalMeasure

An s-finite measure is dominated by its renewal measure, of which it is the term μ^{∗1}.

theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_renewalMeasure {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] [TopologicalSpace α] (μ : Measure α) [SFinite μ] [IsLocallyFiniteMeasure μ.renewalMeasure] : IsLocallyFiniteMeasure μ

An s-finite measure whose renewal measure is locally finite is itself locally finite.

theorem MeasureTheory.Measure.summable_convolutionPower_real {α : Type u_1} [MeasurableSpace α] [AddMonoid α] {μ : Measure α} {s : Set α} (hU : μ.renewalMeasure s ≠ ⊤) : Summable fun (n : ℕ) => (μ.convolutionPower n).real s

The masses of a set s under the convolution powers are summable when the renewal measure gives s finite mass. No measurability of s is needed.

instance MeasureTheory.Measure.sfinite_renewalMeasure {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) [SFinite μ] : SFinite μ.renewalMeasure

The renewal measure of an s-finite measure is s-finite.

theorem MeasureTheory.Measure.conv_renewalMeasure {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (μ : Measure α) [SFinite μ] : μ.conv μ.renewalMeasure = sum fun (n : ℕ) => μ.convolutionPower (n + 1)

Convolving the renewal measure with μ removes the term μ^{∗0} = δ₀: μ ∗ U = ∑ n, μ^{∗(n + 1)}.

theorem MeasureTheory.Measure.renewalMeasure_eq_dirac_add_conv {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (μ : Measure α) [SFinite μ] : μ.renewalMeasure = dirac 0 + μ.conv μ.renewalMeasure

The renewal equation U = δ₀ + μ ∗ U for the renewal measure U of μ.

The renewal function on the half-line

noncomputable def MeasureTheory.Measure.renewalFunction (μ : Measure NNReal) (t : NNReal) : ENNReal

The renewal function t ↦ (μ ∗ U) [0, t] of a measure μ on ℝ≥0, where U is the renewal measure of μ. It equals ∑_{n ≥ 1} μ^{∗n} [0, t] (renewalFunction_eq_tsum), and for independent increments with law μ it is the expected count of the renewal process (TauCeti.Probability.lintegral_renewalCount).

theorem MeasureTheory.Measure.renewalFunction_def (μ : Measure NNReal) (t : NNReal) : μ.renewalFunction t = (μ.conv μ.renewalMeasure) (Set.Iic t)

theorem MeasureTheory.Measure.renewalFunction_eq_tsum (μ : Measure NNReal) [SFinite μ] (t : NNReal) : μ.renewalFunction t = ∑' (n : ℕ), (μ.convolutionPower (n + 1)) (Set.Iic t)

The renewal function is the sum of the masses of [0, t] under the positive convolution powers.

theorem MeasureTheory.Measure.renewalMeasure_Iic (μ : Measure NNReal) [SFinite μ] (t : NNReal) : μ.renewalMeasure (Set.Iic t) = 1 + μ.renewalFunction t

The renewal measure of [0, t] is one more than the renewal function at t: the extra unit is the point mass μ^{∗0} = δ₀.

theorem MeasureTheory.Measure.monotone_renewalFunction (μ : Measure NNReal) : Monotone μ.renewalFunction

The renewal function is nondecreasing in time.

theorem TauCeti.Probability.lintegral_renewalCount {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {T : ℕ → Ω → NNReal} (hindep : ProbabilityTheory.iIndepFun T P) (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P) (t : NNReal) : ∫⁻ (ω : Ω), renewalCount T t ω ∂P = (MeasureTheory.Measure.map (T 0) P).renewalFunction t

The renewal function is the expected count. For independent, identically distributed increments, the expected number of arrivals in [0, t] is the renewal function of the common law of the increments. No assumption is made on the atom of the law at zero, and both sides may be infinite.

theorem TauCeti.Probability.integral_renewalCountNat {Ω : 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) : ∫ (ω : Ω), ↑(renewalCountNat T t ω) ∂P = ((MeasureTheory.Measure.map (T 0) P).renewalFunction t).toReal

The real form of TauCeti.Probability.lintegral_renewalCount: for independent, identically distributed increments that are not almost surely zero, the mean of the natural-valued count at time t is the renewal function of the increment law.

theorem MeasureTheory.Measure.renewalFunction_lt_top (μ : Measure NNReal) [IsProbabilityMeasure μ] (hμ : μ {0} < 1) (t : NNReal) : μ.renewalFunction t < ⊤

The renewal function is finite. For a probability measure μ on ℝ≥0 that is not the point mass at zero, the renewal function is finite at every time. No assumption is made on the mean of μ.

theorem MeasureTheory.Measure.renewalMeasure_Iic_lt_top (μ : Measure NNReal) [IsProbabilityMeasure μ] (hμ : μ {0} < 1) (t : NNReal) : μ.renewalMeasure (Set.Iic t) < ⊤

The renewal measure of a probability measure on ℝ≥0 other than the point mass at zero is finite on every bounded interval [0, t].

theorem MeasureTheory.Measure.isLocallyFiniteMeasure_renewalMeasure (μ : Measure NNReal) [IsProbabilityMeasure μ] (hμ : μ {0} < 1) : IsLocallyFiniteMeasure μ.renewalMeasure

The renewal measure of a probability measure on ℝ≥0 other than the point mass at zero is locally finite.

theorem MeasureTheory.Measure.continuousWithinAt_renewalFunction_Ici (μ : Measure NNReal) [IsProbabilityMeasure μ] (t : NNReal) : ContinuousWithinAt μ.renewalFunction (Set.Ici t) t

Right continuity of the renewal function of a probability measure on ℝ≥0. For the point mass at zero the renewal function is constantly infinite.