Stochastic processes satisfying the Kolmogorov condition

theorem Finset.iSup_sum_le {α : Type u_1} {ι : Type u_2} {β : Sort u_3} [CompleteLattice α] [AddCommMonoid α] [IsOrderedAddMonoid α] {I : Finset ι} (f : ι → β → α) : ⨆ (b : β), ∑ i ∈ I, f i b ≤ ∑ i ∈ I, ⨆ (b : β), f i b

theorem Finset.sup_le_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid β] [LinearOrder β] [OrderBot β] [IsOrderedAddMonoid β] (s : Finset α) (f : α → β) (hfs : ∀ i ∈ s, 0 ≤ f i) : s.sup f ≤ ∑ a ∈ s, f a

theorem ProbabilityTheory.measurable_pair_of_measurable {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {X : T → Ω → E} [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (hX : ∀ (s : T), Measurable (X s)) (s t : T) : Measurable fun (ω : Ω) => (X s ω, X t ω)

theorem ProbabilityTheory.aemeasurable_pair_of_aemeasurable {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : T → Ω → E} [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (hX : ∀ (s : T), AEMeasurable (X s) P) (s t : T) : AEMeasurable (fun (ω : Ω) => (X s ω, X t ω)) P

theorem ProbabilityTheory.IsAEKolmogorovProcess.lintegral_sup_rpow_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) {T' : Set T} (hT' : T'.Countable) (h : ∀ s ∈ T', ∀ t ∈ T', edist s t = 0) : ∫⁻ (ω : Ω), ⨆ (s : ↑T'), ⨆ (t : ↑T'), edist (X (↑s) ω) (X (↑t) ω) ^ p ∂P = 0

theorem ProbabilityTheory.IsAEKolmogorovProcess.lintegral_sup_rpow_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) {J : Set T} (hJ : J.Countable) {δ : ENNReal} (h : ∀ (s : ↑J) (t : { t : ↑J // edist s t ≤ δ }), edist s ↑t = 0) : ∫⁻ (ω : Ω), ⨆ (s : ↑J), ⨆ (t : { t : ↑J // edist s t ≤ δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P = 0

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_card_mul_rpow {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) {ε : ENNReal} (C : Finset (T × T)) (hC : ∀ u ∈ C, edist u.1 u.2 ≤ ε) : ∫⁻ (ω : Ω), ⨆ (u : ↥C), edist (X (↑u).1 ω) (X (↑u).2 ω) ^ p ∂P ≤ ↑C.card * ↑M * ε ^ q

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_card_mul_rpow_of_dist_le {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) {J : Finset T} {a c : ENNReal} {n : ℕ} (hJ_card : ↑J.card ≤ a ^ n) : ∫⁻ (ω : Ω), ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ p * a * ↑J.card * ↑M * (c * ↑n) ^ q

theorem ProbabilityTheory.lintegral_sup_rpow_edist_cover_of_dist_le {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} {J : Set T} (hX : IsAEKolmogorovProcess X P p q M) {C : Finset T} {ε : NNReal} (hC_card : ↑C.card = Metric.coveringNumber ε J) {c : ENNReal} : ∫⁻ (ω : Ω), ⨆ (s : ↥C), ⨆ (t : { t : ↥C // edist s t ≤ c }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ (p + 1) * ↑M * (2 * c * ↑(Metric.coveringNumber ε J).toNat.log2) ^ q * ↑(Metric.coveringNumber ε J)

theorem ProbabilityTheory.lintegral_sup_rpow_edist_cover_rescale {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} {J : Set T} (hX : IsAEKolmogorovProcess X P p q M) (hJ : J.Finite) {C : ℕ → Finset T} {ε₀ : NNReal} (hC : ∀ (i : ℕ), Metric.IsCover (ε₀ * 2⁻¹ ^ i) J ↑(C i)) (hC_subset : ∀ (i : ℕ), ↑(C i) ⊆ J) (hC_card : ∀ (i : ℕ), ↑(C i).card = Metric.coveringNumber (ε₀ * 2⁻¹ ^ i) J) {δ : NNReal} (hδ_pos : 0 < δ) (hδ_le : δ ≤ ε₀ * 4) {k m : ℕ} (hm₁ : ε₀ * 2⁻¹ ^ m ≤ δ) (hm₂ : δ ≤ ε₀ * 4 * 2⁻¹ ^ m) (hmk : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (s : ↥(C k)), ⨆ (t : { t : ↥(C k) // edist s t ≤ ↑δ }), edist (X (chainingSeq C (↑s) k m) ω) (X (chainingSeq C (↑↑t) k m) ω) ^ p ∂P ≤ 2 ^ (p + 1) * ↑M * (16 * ↑δ * ↑(Metric.coveringNumber (δ / 4) J).toNat.log2) ^ q * ↑(Metric.coveringNumber (δ / 4) J)

theorem ProbabilityTheory.lintegral_sup_rpow_edist_succ {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} {J : Set T} {C : ℕ → Finset T} {ε : ℕ → NNReal} {j k : ℕ} (hX : IsAEKolmogorovProcess X P p q M) (hC : ∀ (n : ℕ), Metric.IsCover (ε n) J ↑(C n)) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hjk : j < k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (chainingSeq C (↑t) k j) ω) (X (chainingSeq C (↑t) k (j + 1)) ω) ^ p ∂P ≤ ↑(C (j + 1)).card * ↑M * ↑(ε j) ^ q

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_sum_rpow {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} {C : ℕ → Finset T} {k m : ℕ} (hp : 1 ≤ p) (hX : IsAEKolmogorovProcess X P p q M) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ (∑ i ∈ Finset.range (k - m), (∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (chainingSeq C (↑t) k (m + i)) ω) (X (chainingSeq C (↑t) k (m + i + 1)) ω) ^ p ∂P) ^ (1 / p)) ^ p

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_sum {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} {J : Set T} {C : ℕ → Finset T} {ε : ℕ → NNReal} {k m : ℕ} (hp : 1 ≤ p) (hX : IsAEKolmogorovProcess X P p q M) (hC : ∀ (n : ℕ), Metric.IsCover (ε n) J ↑(C n)) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ ↑M * (∑ i ∈ Finset.range (k - m), ↑(C (m + i + 1)).card ^ (1 / p) * ↑(ε (m + i)) ^ (q / p)) ^ p

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_of_minimal_cover {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} {J : Set T} {C : ℕ → Finset T} {ε : ℕ → NNReal} {k m : ℕ} (hp : 1 ≤ p) (hX : IsAEKolmogorovProcess X P p q M) (hε : ∀ (n : ℕ), ↑(ε n) ≤ Metric.ediam J) (hC : ∀ (n : ℕ), Metric.IsCover (ε n) J ↑(C n)) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = Metric.coveringNumber (ε n) J) {c₁ : ENNReal} {d : ℝ} (h_cov : Metric.HasCoveringExponent J c₁ d) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ ↑M * c₁ * (∑ j ∈ Finset.range (k - m), ↑(ε (m + j + 1)) ^ (-d / p) * ↑(ε (m + j)) ^ (q / p)) ^ p

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_of_minimal_cover_two {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} {J : Set T} {C : ℕ → Finset T} {k m : ℕ} (hp : 1 ≤ p) (hX : IsAEKolmogorovProcess X P p q M) {ε₀ : NNReal} (hε : ↑ε₀ ≤ Metric.ediam J) (hC : ∀ (n : ℕ), Metric.IsCover (ε₀ * 2⁻¹ ^ n) J ↑(C n)) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = Metric.coveringNumber (ε₀ * 2⁻¹ ^ n) J) {c₁ : ENNReal} {d : ℝ} (hdq : d < q) (h_cov : Metric.HasCoveringExponent J c₁ d) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ 2 ^ d * ↑M * c₁ * (2 * ↑ε₀ * 2⁻¹ ^ m) ^ (q - d) / (2 ^ ((q - d) / p) - 1) ^ p

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_sum_rpow_of_le_one {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} {C : ℕ → Finset T} {k m : ℕ} (hp : p ≤ 1) (hX : IsAEKolmogorovProcess X P p q M) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ ∑ i ∈ Finset.range (k - m), ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (chainingSeq C (↑t) k (m + i)) ω) (X (chainingSeq C (↑t) k (m + i + 1)) ω) ^ p ∂P

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_sum_of_le_one {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} {J : Set T} {C : ℕ → Finset T} {ε : ℕ → NNReal} {k m : ℕ} (hp : p ≤ 1) (hX : IsAEKolmogorovProcess X P p q M) (hC : ∀ (n : ℕ), Metric.IsCover (ε n) J ↑(C n)) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ ↑M * ∑ i ∈ Finset.range (k - m), ↑(C (m + i + 1)).card * ↑(ε (m + i)) ^ q

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_of_minimal_cover_of_le_one {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} {J : Set T} {C : ℕ → Finset T} {ε : ℕ → NNReal} {k m : ℕ} (hp : p ≤ 1) (hX : IsAEKolmogorovProcess X P p q M) (hε : ∀ (n : ℕ), ↑(ε n) ≤ Metric.ediam J) (hC : ∀ (n : ℕ), Metric.IsCover (ε n) J ↑(C n)) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = Metric.coveringNumber (ε n) J) {c₁ : ENNReal} {d : ℝ} (h_cov : Metric.HasCoveringExponent J c₁ d) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ ↑M * c₁ * ∑ j ∈ Finset.range (k - m), ↑(ε (m + j + 1)) ^ (-d) * ↑(ε (m + j)) ^ q

theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_of_minimal_cover_two_of_le_one {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} {J : Set T} {C : ℕ → Finset T} {k m : ℕ} (hp : p ≤ 1) (hX : IsAEKolmogorovProcess X P p q M) {ε₀ : NNReal} (hε : ↑ε₀ ≤ Metric.ediam J) (hC : ∀ (n : ℕ), Metric.IsCover (ε₀ * 2⁻¹ ^ n) J ↑(C n)) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = Metric.coveringNumber (ε₀ * 2⁻¹ ^ n) J) {c₁ : ENNReal} {d : ℝ} (hdq : d < q) (h_cov : Metric.HasCoveringExponent J c₁ d) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ 2 ^ d * ↑M * c₁ * (2 * ↑ε₀ * 2⁻¹ ^ m) ^ (q - d) / (2 ^ (q - d) - 1)

noncomputable def ProbabilityTheory.Cp (d p q : ℝ) : ENNReal

Equations

• ProbabilityTheory.Cp d p q = max (1 / (2 ^ ((q - d) / p) - 1) ^ p) (1 / (2 ^ (q - d) - 1))

theorem ProbabilityTheory.second_term_bound {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} {J : Set T} {C : ℕ → Finset T} {k m : ℕ} (hX : IsAEKolmogorovProcess X P p q M) {ε₀ : NNReal} (hε : ↑ε₀ ≤ Metric.ediam J) (hC : ∀ (n : ℕ), Metric.IsCover (ε₀ * 2⁻¹ ^ n) J ↑(C n)) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = Metric.coveringNumber (ε₀ * 2⁻¹ ^ n) J) {c₁ : ENNReal} {d : ℝ} (hdq : d < q) (h_cov : Metric.HasCoveringExponent J c₁ d) (hm : m ≤ k) : ∫⁻ (ω : Ω), ⨆ (t : ↥(C k)), edist (X (↑t) ω) (X (chainingSeq C (↑t) k m) ω) ^ p ∂P ≤ 2 ^ d * ↑M * c₁ * (2 * ↑ε₀ * 2⁻¹ ^ m) ^ (q - d) * Cp d p q

theorem ProbabilityTheory.lintegral_sup_cover_eq_of_lt_iInf_dist {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : T → Ω → E} {M : NNReal} {p q : ℝ} {J : Set T} {δ : NNReal} {C : Set T} {ε : NNReal} (hX : IsAEKolmogorovProcess X P p q M) (hJ : J.Finite) (hC : Metric.IsCover ε J C) (hC_subset : C ⊆ J) (hε_lt : ↑ε < ⨅ (s : ↑J), ⨅ (t : ↑J), ⨅ (_ : 0 < edist s t), edist s t) : ∫⁻ (ω : Ω), ⨆ (s : ↑C), ⨆ (t : { t : ↑C // edist s t ≤ ↑δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P = ∫⁻ (ω : Ω), ⨆ (s : ↑J), ⨆ (t : { t : ↑J // edist s t ≤ ↑δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P

theorem ProbabilityTheory.exists_nat_pow_lt_iInf {T : Type u_1} [PseudoEMetricSpace T] {J : Set T} (hJ : Metric.ediam J < ⊤) (hJ_finite : J.Finite) (hJ_nonempty : J.Nonempty) : ∃ (k : ℕ), Metric.ediam J * 2⁻¹ ^ k < ⨅ (s : ↑J), ⨅ (t : ↑J), ⨅ (_ : 0 < edist s t), edist s t

theorem ProbabilityTheory.scale_change_lintegral_iSup {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : T → Ω → E} {M : NNReal} {p q : ℝ} {C : ℕ → Finset T} (hX : IsAEKolmogorovProcess X P p q M) (δ : ENNReal) (m k : ℕ) : ∫⁻ (ω : Ω), ⨆ (s : ↥(C k)), ⨆ (t : { t : ↥(C k) // edist s t ≤ δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ p * ∫⁻ (ω : Ω), ⨆ (s : ↥(C k)), ⨆ (t : { t : ↥(C k) // edist s t ≤ δ }), edist (X (chainingSeq C (↑s) k m) ω) (X (chainingSeq C (↑↑t) k m) ω) ^ p ∂P + 4 ^ p * ∫⁻ (ω : Ω), ⨆ (s : ↥(C k)), edist (X (↑s) ω) (X (chainingSeq C (↑s) k m) ω) ^ p ∂P

theorem ProbabilityTheory.finite_set_bound_of_edist_le_of_diam_le {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : T → Ω → E} {M : NNReal} {d p q : ℝ} {J : Set T} {c : ENNReal} {δ : NNReal} (hJ : Metric.HasCoveringExponent J c d) (hJ_finite : J.Finite) (hX : IsAEKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hdq_lt : d < q) (hδ_le : Metric.ediam J ≤ ↑δ / 4) : ∫⁻ (ω : Ω), ⨆ (s : ↑J), ⨆ (t : { t : ↑J // edist s t ≤ ↑δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 4 ^ p * 2 ^ q * ↑M * c * ↑δ ^ (q - d) * Cp d p q

theorem ProbabilityTheory.finite_set_bound_of_edist_le_of_le_diam {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : T → Ω → E} {M : NNReal} {d p q : ℝ} {J : Set T} {c : ENNReal} {δ : NNReal} (hJ : Metric.HasCoveringExponent J c d) (hJ_finite : J.Finite) (hX : IsAEKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hdq_lt : d < q) (hδ : δ ≠ 0) (hδ_le : ↑δ / 4 ≤ Metric.ediam J) : ∫⁻ (ω : Ω), ⨆ (s : ↑J), ⨆ (t : { t : ↑J // edist s t ≤ ↑δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ (2 * p + 4 * q + 1) * ↑M * ↑δ ^ (q - d) * (↑δ ^ d * ↑(Metric.coveringNumber (δ / 4) J).toNat.log2 ^ q * ↑(Metric.coveringNumber (δ / 4) J) + c * Cp d p q)

theorem ProbabilityTheory.finite_set_bound_of_edist_le_of_le_diam' {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : T → Ω → E} {M : NNReal} {d p q : ℝ} {J : Set T} {c : ENNReal} {δ : NNReal} (hJ : Metric.HasCoveringExponent J c d) (hJ_finite : J.Finite) (hX : IsAEKolmogorovProcess X P p q M) (hc : c ≠ ⊤) (hd_pos : 0 < d) (hdq_lt : d < q) (hδ : δ ≠ 0) (hδ_le : ↑δ / 4 ≤ Metric.ediam J) : ∫⁻ (ω : Ω), ⨆ (s : ↑J), ⨆ (t : { t : ↑J // edist s t ≤ ↑δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ (2 * p + 4 * q + 1) * ↑M * c * ↑δ ^ (q - d) * (4 ^ d * ENNReal.ofReal (Real.logb 2 (c.toReal * 4 ^ d * (↑δ)⁻¹ ^ d)) ^ q + Cp d p q)

theorem ProbabilityTheory.finite_set_bound_of_edist_le {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : T → Ω → E} {M : NNReal} {d p q : ℝ} {J : Set T} {c : ENNReal} {δ : NNReal} (hJ : Metric.HasCoveringExponent J c d) (hJ_finite : J.Finite) (hX : IsAEKolmogorovProcess X P p q M) (hc : c ≠ ⊤) (hd_pos : 0 < d) (hdq_lt : d < q) (hδ : δ ≠ 0) : ∫⁻ (ω : Ω), ⨆ (s : ↑J), ⨆ (t : { t : ↑J // edist s t ≤ ↑δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ (2 * p + 4 * q + 1) * ↑M * c * ↑δ ^ (q - d) * (4 ^ d * ENNReal.ofReal (Real.logb 2 (c.toReal * 4 ^ d * (↑δ)⁻¹ ^ d)) ^ q + Cp d p q)