Kolmogorov-Chentsov theorem

theorem Asymptotics.IsEquivalent.rpow_of_nonneg {α : Type u_1} {t u : α → ℝ} (hu : 0 ≤ u) {l : Filter α} (h : IsEquivalent l t u) {r : ℝ} : IsEquivalent l (t ^ r) (u ^ r)

theorem Set.FiniteExhaustion.subset {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) (n : ℕ) : K n ⊆ s

theorem measure_add_ge_le_add_measure_ge {Ω : Type u_1} {x✝ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {f g : Ω → ENNReal} {x u : ENNReal} (hu : u ≤ x) : P {ω : Ω | x ≤ f ω + g ω} ≤ P {ω : Ω | u ≤ f ω} + P {ω : Ω | x - u ≤ g ω}

theorem measure_add_ge_le_add_measure_ge_half {Ω : Type u_1} {x✝ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {f g : Ω → ENNReal} {x : ENNReal} : P {ω : Ω | x ≤ f ω + g ω} ≤ P {ω : Ω | x / 2 ≤ f ω} + P {ω : Ω | x / 2 ≤ g ω}

theorem ProbabilityTheory.lintegral_div_edist_le_sum_integral_edist_le {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {X : T → Ω → E} {p q : ℝ} {M β : NNReal} {P : MeasureTheory.Measure Ω} {U : Set T} [PseudoEMetricSpace T] [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] (hT : EMetric.diam U < ⊤) (hX : IsAEKolmogorovProcess X P p q M) (hβ : 0 < β) {J : Set T} [Countable ↑J] (hJU : J ⊆ U) : ∫⁻ (ω : Ω), ⨆ (s : ↑J), ⨆ (t : ↑J), edist (X (↑s) ω) (X (↑t) ω) ^ p / edist s t ^ (↑β * p) ∂P ≤ ∑' (k : ℕ), 2 ^ (↑k * ↑β * p) * ∫⁻ (ω : Ω), ⨆ (s : ↑J), ⨆ (t : { t : ↑J // edist s t ≤ 2 * 2⁻¹ ^ k * (EMetric.diam U + 1) }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P

noncomputable def ProbabilityTheory.constL (T : Type u_4) [PseudoEMetricSpace T] (c : ENNReal) (d p q β : ℝ) (U : Set T) : ENNReal

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.constL_lt_top {T : Type u_1} {c : ENNReal} {d p q : ℝ} {β : NNReal} {U : Set T} [PseudoEMetricSpace T] (hT : EMetric.diam U < ⊤) (hc : c ≠ ⊤) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) (hβ_lt : ↑β < (q - d) / p) : constL T c d p q (↑β) U < ⊤

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

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

theorem ProbabilityTheory.IsKolmogorovProcess.ae_iSup_rpow_edist_div_lt_top {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {X : T → Ω → E} {c : ENNReal} {d p q : ℝ} {M β : NNReal} {P : MeasureTheory.Measure Ω} {U : Set T} [PseudoEMetricSpace T] [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] (hT : HasBoundedCoveringNumber U c d) (hX : IsKolmogorovProcess X P p q M) (hc : c ≠ ⊤) (hd_pos : 0 < d) (hdq_lt : d < q) (hβ_pos : 0 < β) (hβ_lt : ↑β < (q - d) / p) {T' : Set T} (hT' : T'.Countable) (hT'U : T' ⊆ U) : ∀ᵐ (ω : Ω) ∂P, ⨆ (s : ↑T'), ⨆ (t : ↑T'), edist (X (↑s) ω) (X (↑t) ω) ^ p / edist s t ^ (↑β * p) < ⊤