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.iUnion_le_nat : ⋃ (n : ℕ), {i : ℕ | i ≤ n} = univ

structure FiniteExhaustion {α : Type u_1} (s : Set α) : Type u_1

• toFun : ℕ → Set α
• Finite' (n : ℕ) : Finite ↑(self.toFun n)
• subset_succ' (n : ℕ) : self.toFun n ⊆ self.toFun (n + 1)
• iUnion_eq' : ⋃ (n : ℕ), self.toFun n = s

instance FiniteExhaustion.instFunLikeNatSet {α : Type u_1} {s : Set α} : FunLike (FiniteExhaustion s) ℕ (Set α)

Equations

• FiniteExhaustion.instFunLikeNatSet = { coe := FiniteExhaustion.toFun, coe_injective' := ⋯ }

instance FiniteExhaustion.instRelHomClassNatSetLeSubset {α : Type u_1} {s : Set α} : RelHomClass (FiniteExhaustion s) LE.le Subset

instance FiniteExhaustion.instFiniteElemCoeNatSet {α : Type u_1} {s : Set α} {K : FiniteExhaustion s} {n : ℕ} : Finite ↑(K n)

@[simp]

theorem FiniteExhaustion.toFun_eq_coe {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) : K.toFun = ⇑K

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

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

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

theorem FiniteExhaustion.iUnion_eq {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) : ⋃ (n : ℕ), K n = s

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

noncomputable def FiniteExhaustion.choice {α : Type u_2} (s : Set α) [Countable ↑s] : FiniteExhaustion s

Equations

• FiniteExhaustion.choice s = Classical.choice ⋯

def FiniteExhaustion.prod {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) {β : Type u_2} {t : Set β} (K' : FiniteExhaustion t) : FiniteExhaustion (s ×ˢ t)

Equations

• K.prod K' = { toFun := fun (n : ℕ) => K n ×ˢ K' n, Finite' := ⋯, subset_succ' := ⋯, iUnion_eq' := ⋯ }

theorem FiniteExhaustion.prod_apply {α : Type u_1} {s : Set α} (K : FiniteExhaustion s) {β : Type u_2} {t : Set β} (K' : FiniteExhaustion t) (n : ℕ) : (K.prod K') n = K n ×ˢ K' n

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 : HasBoundedInternalCoveringNumber 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 : HasBoundedInternalCoveringNumber U c d) (hX : IsAEKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hdq_lt : d < q) (hβ_pos : 0 < β) (T' : Set T) [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 : HasBoundedInternalCoveringNumber 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) < ⊤