Markov chains and renewal processes
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremNonexplosion of a renewal process#
If the increments are independent, identically distributed and not almost surely zero, then almost surely the arrival times tend to infinity.
TauCeti.Probability.ae_tendsto_arrival_atTop.{u_1} {Ω : 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,
Filter.Tendsto (fun n => TauCeti.Probability.arrival T n ω) Filter.atTop Filter.atTop
TheoremFiniteness of the renewal counts#
For independent, identically distributed increments
that are not almost surely zero, almost surely every count renewalCount T t is finite. The
almost-sure quantifier is outside the quantifier over all times.
TauCeti.Probability.ae_renewalCount_lt_top.{u_1} {Ω : 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), TauCeti.Probability.renewalCount T t ω < ⊤
Uses 2 · Used by 2
TheoremFinite 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.
TauCeti.Probability.lintegral_renewalCount_pow_lt_top.{u_1} {Ω : 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 : ℕ) : ∫⁻ (ω : Ω), TauCeti.Probability.renewalCount T t ω ^ p ∂P < ⊤
Lean
Formalized in Tau Ceti as TauCeti.Probability.lintegral_renewalCount_pow_lt_top.
Sources
Uses 4 · Used by 1
TheoremChernoff 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).
TauCeti.Probability.measureReal_arrival_le_le_exp_mul_mgf_pow.{u_1} {Ω : 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 {ω | TauCeti.Probability.arrival T n ω ≤ t} ≤
Real.exp (s * ↑t) * ProbabilityTheory.mgf (fun ω => ↑(T 0 ω)) P (-s) ^ n
Lean
Formalized in Tau Ceti as TauCeti.Probability.measureReal_arrival_le_le_exp_mul_mgf_pow.
Sources
Used by 2
TheoremUniqueness of the path law#
For a finite initial measure ν, a measure on path space whose
time-zero marginal is ν and whose prefix laws satisfy the Markov recursion of
markovChainLaw_map_prefix_succ_eq_compProd is the path law markovChainLaw ν κ.
MeasureTheory.Measure.eq_markovChainLaw.{u_1} {α : Type u_1} [MeasurableSpace α]
(ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α)
[ProbabilityTheory.IsMarkovKernel κ] [MeasureTheory.IsFiniteMeasure ν]
{μ : MeasureTheory.Measure (ℕ → α)} (h₀ : MeasureTheory.Measure.map (fun x => x 0) μ = ν)
(hstep :
∀ (n : ℕ),
MeasureTheory.Measure.map (fun x => (fun i => x ↑i, x (n + 1))) μ =
(MeasureTheory.Measure.map (fun x i => x ↑i) μ).compProd
(κ.comap (fun w => w (Fin.last n)) ⋯)) :
μ = TauCeti.Probability.markovChainLaw ν κ
TheoremThe time-n marginal of the chain#
the state at time n has law (κ ^ n) ∘ₘ ν, the
initial law propagated by the n-step transition kernel. This holds for every initial measure
ν.
MeasureTheory.Measure.markovChainLaw_map_eval.{u_1} {α : Type u_1} [MeasurableSpace α]
(ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α)
[ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) :
MeasureTheory.Measure.map (fun w => w n) (TauCeti.Probability.markovChainLaw ν κ) =
ν.bind ⇑(κ ^ n)
Uses 1
DefinitionThe path-law kernel of a homogeneous Markov chain#
the kernel sending a state x to the law
markovChainLaw (Measure.dirac x) κ of the chain started at x (markovChainKernel_apply). Being
a kernel, it records that this law depends measurably on the starting state, and every path law of
the chain is its mixture over the initial law (markovChainLaw_eq_comp).
ProbabilityTheory.Kernel.markovChainKernel.{u_1} {α : Type u_1} [MeasurableSpace α]
(κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] :
ProbabilityTheory.Kernel α (ℕ → α)
Used by 1
DefinitionTauCeti.Probability.renewalCount#
The number #{n ≥ 1 | arrival T n ω ≤ t} of arrivals in [0, t], counted with multiplicity,
as an extended nonnegative number. The artificial arrival arrival T 0 = 0 is not counted.
TauCeti.Probability.renewalCount.{u_1} {Ω : Type u_1} (T : ℕ → Ω → NNReal) (t : NNReal) (ω : Ω) :
ENNReal
TheoremTauCeti.Probability.renewalCount_eq_natCast_iff#
The count at time t equals n exactly when arrival T n ω ≤ t < arrival T (n + 1) ω.
TauCeti.Probability.renewalCount_eq_natCast_iff.{u_1} {Ω : Type u_1} {T : ℕ → Ω → NNReal}
{t : NNReal} {ω : Ω} {n : ℕ} :
TauCeti.Probability.renewalCount T t ω = ↑n ↔
TauCeti.Probability.arrival T n ω ≤ t ∧ t < TauCeti.Probability.arrival T (n + 1) ω
Lean
Formalized in Tau Ceti as TauCeti.Probability.renewalCount_eq_natCast_iff.
Sources
Uses 1 · Used by 3
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.