Kolmogorov-Chentsov theorem

def ProbabilityTheory.constL (T : Type u_4) [PseudoEMetricSpace T] (c : ENNReal) (d p q β : NNReal) : ENNReal

Equations

• ProbabilityTheory.constL T c d p q β = sorry

theorem ProbabilityTheory.constL_lt_top {T : Type u_1} [PseudoEMetricSpace T] {c : ENNReal} {d p q β : NNReal} : constL T c d p q β < ⊤

theorem ProbabilityTheory.finite_kolmogorov_chentsov {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] {X : T → Ω → E} {c : ENNReal} {d p q M β : NNReal} {P : MeasureTheory.Measure Ω} (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hX : IsKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_pos : 0 < β) (hβ_lt : β < (q - d) / p) (T' : Set T) (hT' : T'.Finite) : ∫⁻ (ω : Ω), ⨆ (s : T), ⨆ (t : T), ⨆ (_ : s ∈ T'), ⨆ (_ : t ∈ T'), edist (X s ω) (X t ω) ^ ↑p / edist s t ^ (↑β * ↑p) ∂P ≤ ↑M * constL T c d p q β

theorem ProbabilityTheory.countable_kolmogorov_chentsov {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] {X : T → Ω → E} {c : ENNReal} {d p q M β : NNReal} {P : MeasureTheory.Measure Ω} (hT : HasBoundedInternalCoveringNumber Set.univ c d) (hX : IsKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_pos : 0 < β) (hβ_lt : β < (q - d) / p) (T' : Set T) (hT' : T'.Countable) : ∫⁻ (ω : Ω), ⨆ (s : T), ⨆ (t : T), ⨆ (_ : s ∈ T'), ⨆ (_ : t ∈ T'), edist (X s ω) (X t ω) ^ ↑p / edist s t ^ (↑β * ↑p) ∂P ≤ ↑M * constL T c d p q β