Stochastic processes satisfying the Kolmogorov condition #
A stochastic process X : T → Ω → E on an index space T and a measurable space Ω
with measure P is said to satisfy the Kolmogorov condition with exponents p, q and constant M
if for all s, t : T, the pair (X s, X t) is measurable for the Borel sigma-algebra on E × E
and the following condition holds:
∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P ≤ M * edist s t ^ q.
This condition is the main assumption of the Kolmogorov-Chentsov theorem, which gives the existence of a continuous modification of the process.
The measurability condition on pairs ensures that the distance edist (X s ω) (X t ω) is
measurable in ω for fixed s, t. In a space with second-countable topology, the measurability
of pairs can be obtained from measurability of each X t.
Main definitions #
IsKolmogorovProcess: property of being a stochastic process that satisfies the Kolmogorov condition.IsAEKolmogorovProcess: a stochastic process satisfiesIsAEKolmogorovProcessif it is a modification of a process satisfying the Kolmogorov condition.
Main statements #
IsKolmogorovProcess.mk_of_secondCountableTopology: in a space with second-countable topology, a process is a Kolmogorov process if eachX tis measurable and the Kolmogorov condition holds.
structure
ProbabilityTheory.IsKolmogorovProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
(X : T → Ω → E)
(P : MeasureTheory.Measure Ω)
(p q : ℝ)
(M : NNReal)
:
A stochastic process X : T → Ω → E on an index space T and a measurable space Ω
with measure P is said to satisfy the Kolmogorov condition with exponents p, q and constant M
if for all s, t : T, the pair (X s, X t) is measurable for the Borel sigma-algebra on E × E
and the following condition holds: ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P ≤ M * edist s t ^ q.
- measurablePair (s t : T) : Measurable fun (ω : Ω) => (X s ω, X t ω)
Instances For
def
ProbabilityTheory.IsAEKolmogorovProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
(X : T → Ω → E)
(P : MeasureTheory.Measure Ω)
(p q : ℝ)
(M : NNReal)
:
Property of being a modification of a stochastic process that satisfies the Kolmogorov
condition (IsKolmogorovProcess).
Equations
- ProbabilityTheory.IsAEKolmogorovProcess X P p q M = ∃ (Y : T → Ω → E), ProbabilityTheory.IsKolmogorovProcess Y P p q M ∧ ∀ (t : T), X t =ᵐ[P] Y t
Instances For
theorem
ProbabilityTheory.IsKolmogorovProcess.IsAEKolmogorovProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
:
ProbabilityTheory.IsAEKolmogorovProcess X P p q M
noncomputable def
ProbabilityTheory.IsAEKolmogorovProcess.mk
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
(X : T → Ω → E)
(h : IsAEKolmogorovProcess X P p q M)
:
T → Ω → E
A process with the property IsKolmogorovProcess such that ∀ t, X t =ᵐ[P] h.mk X t.
Equations
Instances For
theorem
ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(h : IsAEKolmogorovProcess X P p q M)
:
IsKolmogorovProcess (IsAEKolmogorovProcess.mk X h) P p q M
theorem
ProbabilityTheory.IsAEKolmogorovProcess.ae_eq_mk
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(h : IsAEKolmogorovProcess X P p q M)
(t : T)
:
theorem
ProbabilityTheory.IsAEKolmogorovProcess.kolmogorovCondition
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsAEKolmogorovProcess X P p q M)
(s t : T)
:
theorem
ProbabilityTheory.IsAEKolmogorovProcess.p_pos
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsAEKolmogorovProcess X P p q M)
:
theorem
ProbabilityTheory.IsAEKolmogorovProcess.q_pos
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsAEKolmogorovProcess X P p q M)
:
theorem
ProbabilityTheory.IsAEKolmogorovProcess.congr
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
(hX : IsAEKolmogorovProcess X P p q M)
(h : ∀ (t : T), X t =ᵐ[P] Y t)
:
IsAEKolmogorovProcess Y P p q M
theorem
ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
{s t : T}
:
MeasureTheory.StronglyMeasurable fun (ω : Ω) => edist (X s ω) (X t ω)
theorem
ProbabilityTheory.IsAEKolmogorovProcess.aestronglyMeasurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsAEKolmogorovProcess X P p q M)
{s t : T}
:
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => edist (X s ω) (X t ω)) P
theorem
ProbabilityTheory.IsKolmogorovProcess.measurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
{s t : T}
:
Measurable fun (ω : Ω) => edist (X s ω) (X t ω)
theorem
ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsAEKolmogorovProcess X P p q M)
{s t : T}
:
AEMeasurable (fun (ω : Ω) => edist (X s ω) (X t ω)) P
theorem
ProbabilityTheory.IsKolmogorovProcess.measurable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[BorelSpace E]
(hX : IsKolmogorovProcess X P p q M)
(s : T)
:
Measurable (X s)
theorem
ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[BorelSpace E]
(hX : IsAEKolmogorovProcess X P p q M)
(s : T)
:
AEMeasurable (X s) P
theorem
ProbabilityTheory.IsKolmogorovProcess.mk_of_secondCountableTopology
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
(h_meas : ∀ (s : T), Measurable (X s))
(h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q)
(hp : 0 < p)
(hq : 0 < q)
:
IsKolmogorovProcess X P p q M
theorem
ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsAEKolmogorovProcess X P p q M)
{s t : T}
(h : edist s t = 0)
:
theorem
ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
{s t : T}
(h : edist s t = 0)
:
theorem
ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsAEKolmogorovProcess X P p q 0)
(s t : T)
:
theorem
ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero_of_const_eq_zero
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q 0)
(s t : T)
: