Documentation

BrownianMotion.Continuity.IsKolmogorovProcess

Stochastic processes satisfying the Kolmogorov condition #

source
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
source
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
source
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 ω)
source
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
source
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
source
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
source
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 : { x : T × T // x ∈ C }), edist (X (↑u).1 ω) (X (↑u).2 ω) ^ p ∂P ≤ ↑C.card * ↑M * ε ^ q
source
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) (ha : 1 < a) :
∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ J }), ⨆ (t : { t : { x : T // x ∈ J } // edist s t ≤ c }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ p * a * ↑J.card * ↑M * (c * ↑n) ^ q
source
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} {ε : ENNReal} (hC_card : ↑C.card = internalCoveringNumber ε J) {c : ENNReal} :
∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C }), ⨆ (t : { t : { x : T // x ∈ C } // edist s t ≤ c }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ (p + 1) * ↑M * (2 * c * ↑(internalCoveringNumber ε J).toNat.log2) ^ q * ↑(internalCoveringNumber ε J)
source
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} {ε₀ : ENNReal} (hε₀ : ε₀ ≠ ⊤) (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε₀ * 2⁻¹ ^ i) J) (hC_subset : ∀ (i : ℕ), ↑(C i) ⊆ J) (hC_card : ∀ (i : ℕ), ↑(C i).card = internalCoveringNumber (ε₀ * 2⁻¹ ^ i) J) {δ : ENNReal} (hδ_pos : 0 < δ) (hδ_le : δ ≤ ε₀ * 4) {k m : ℕ} (hm₁ : ε₀ * 2⁻¹ ^ m ≤ δ) (hm₂ : δ ≤ ε₀ * 4 * 2⁻¹ ^ m) (hmk : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C k }), ⨆ (t : { t : { x : T // x ∈ C k } // edist s t ≤ δ }), edist (X (chainingSequence hC ⋯ m) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ 2 ^ (p + 1) * ↑M * (16 * δ * ↑(internalCoveringNumber (δ / 4) J).toNat.log2) ^ q * ↑(internalCoveringNumber (δ / 4) J)
source
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} {ε : ℕ → ENNReal} {j k : ℕ} (hX : IsAEKolmogorovProcess X P p q M) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hjk : j < k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (chainingSequence hC ⋯ j) ω) (X (chainingSequence hC ⋯ (j + 1)) ω) ^ p ∂P ≤ ↑(C (j + 1)).card * ↑M * ε j ^ q
source
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} {J : Set T} {C : ℕ → Finset T} {ε : ℕ → ENNReal} {k m : ℕ} (hp : 1 ≤ p) (hX : IsAEKolmogorovProcess X P p q M) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J) (hm : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ (∑ i ∈ Finset.range (k - m), (∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (chainingSequence hC ⋯ (m + i)) ω) (X (chainingSequence hC ⋯ (m + i + 1)) ω) ^ p ∂P) ^ (1 / p)) ^ p
source
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} {ε : ℕ → ENNReal} {k m : ℕ} (hp : 1 ≤ p) (hX : IsAEKolmogorovProcess X P p q M) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hm : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ ↑M * (∑ i ∈ Finset.range (k - m), ↑(C (m + i + 1)).card ^ (1 / p) * ε (m + i) ^ (q / p)) ^ p
source
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} {ε : ℕ → ENNReal} {k m : ℕ} (hp : 1 ≤ p) (hX : IsAEKolmogorovProcess X P p q M) (hε : ∀ (n : ℕ), ε n ≤ EMetric.diam J) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε n) J) {c₁ : ENNReal} {d : ℝ} (h_cov : HasBoundedInternalCoveringNumber J c₁ d) (hm : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ ↑M * c₁ * (∑ j ∈ Finset.range (k - m), ε (m + j + 1) ^ (-d / p) * ε (m + j) ^ (q / p)) ^ p
source
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) {ε₀ : ENNReal} (hε : ε₀ ≤ EMetric.diam J) (hε' : ε₀ ≠ ⊤) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε₀ * 2⁻¹ ^ n) J) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε₀ * 2⁻¹ ^ n) J) {c₁ : ENNReal} {d : ℝ} (hdq : d < q) (h_cov : HasBoundedInternalCoveringNumber J c₁ d) (hm : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ 2 ^ d * ↑M * c₁ * (2 * ε₀ * 2⁻¹ ^ m) ^ (q - d) / (2 ^ ((q - d) / p) - 1) ^ p
source
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} {J : Set T} {C : ℕ → Finset T} {ε : ℕ → ENNReal} {k m : ℕ} (hp : p ≤ 1) (hX : IsAEKolmogorovProcess X P p q M) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J) (hm : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ ∑ i ∈ Finset.range (k - m), ∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (chainingSequence hC ⋯ (m + i)) ω) (X (chainingSequence hC ⋯ (m + i + 1)) ω) ^ p ∂P
source
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} {ε : ℕ → ENNReal} {k m : ℕ} (hp : p ≤ 1) (hX : IsAEKolmogorovProcess X P p q M) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hm : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ ↑M * ∑ i ∈ Finset.range (k - m), ↑(C (m + i + 1)).card * ε (m + i) ^ q
source
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} {ε : ℕ → ENNReal} {k m : ℕ} (hp : p ≤ 1) (hX : IsAEKolmogorovProcess X P p q M) (hε : ∀ (n : ℕ), ε n ≤ EMetric.diam J) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε n) J) {c₁ : ENNReal} {d : ℝ} (h_cov : HasBoundedInternalCoveringNumber J c₁ d) (hm : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ ↑M * c₁ * ∑ j ∈ Finset.range (k - m), ε (m + j + 1) ^ (-d) * ε (m + j) ^ q
source
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) {ε₀ : ENNReal} (hε : ε₀ ≤ EMetric.diam J) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε₀ * 2⁻¹ ^ n) J) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε₀ * 2⁻¹ ^ n) J) {c₁ : ENNReal} {d : ℝ} (hd_pos : 0 < d) (hdq : d < q) (h_cov : HasBoundedInternalCoveringNumber J c₁ d) (hm : m ≤ k) :
∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ 2 ^ d * ↑M * c₁ * (2 * ε₀ * 2⁻¹ ^ m) ^ (q - d) / (2 ^ (q - d) - 1)
source
noncomputable def ProbabilityTheory.Cp (d p q : ℝ) :
ENNReal
Equations
Instances For
    source
    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) {ε₀ : ENNReal} (hε : ε₀ ≤ EMetric.diam J) (hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε₀ * 2⁻¹ ^ n) J) (hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J) (hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε₀ * 2⁻¹ ^ n) J) {c₁ : ENNReal} {d : ℝ} (hd_pos : 0 < d) (hdq : d < q) (h_cov : HasBoundedInternalCoveringNumber J c₁ d) (hm : m ≤ k) :
    ∫⁻ (ω : Ω), ⨆ (t : { x : T // x ∈ C k }), edist (X (↑t) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P ≤ 2 ^ d * ↑M * c₁ * (2 * ε₀ * 2⁻¹ ^ m) ^ (q - d) * Cp d p q
    source
    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} {δ : ENNReal} {C : Finset T} {ε : ENNReal} (hX : IsAEKolmogorovProcess X P p q M) (hJ : J.Finite) (hC : IsCover (↑C) ε J) (hC_subset : ↑C ⊆ J) (hε_lt : ε < ⨅ (s : ↑J), ⨅ (t : ↑J), ⨅ (_ : 0 < edist s t), edist s t) :
    ∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C }), ⨆ (t : { t : { x : T // x ∈ 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
    source
    theorem ProbabilityTheory.exists_nat_pow_lt_iInf {T : Type u_1} [PseudoEMetricSpace T] {J : Set T} (hJ : EMetric.diam J < ⊤) (hJ_finite : J.Finite) (hJ_nonempty : J.Nonempty) :
    ∃ (k : ℕ), EMetric.diam J * 2⁻¹ ^ k < ⨅ (s : ↑J), ⨅ (t : ↑J), ⨅ (_ : 0 < edist s t), edist s t
    source
    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 : ℝ} {J : Set T} {C : ℕ → Finset T} {ε : ℕ → ENNReal} (hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) J) (hX : IsAEKolmogorovProcess X P p q M) (δ : ENNReal) (m k : ℕ) :
    ∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C k }), ⨆ (t : { t : { x : T // x ∈ C k } // edist s t ≤ δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ p * ∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C k }), ⨆ (t : { t : { x : T // x ∈ C k } // edist s t ≤ δ }), edist (X (chainingSequence hC ⋯ m) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P + 4 ^ p * ∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C k }), edist (X (↑s) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P
    source
    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} (hJ : HasBoundedInternalCoveringNumber J c d) (hJ_finite : J.Finite) (hX : IsAEKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hdq_lt : d < q) (hδ_le : EMetric.diam 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
    source
    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} (hJ : HasBoundedInternalCoveringNumber 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 ≤ EMetric.diam 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 * ↑(internalCoveringNumber (δ / 4) J).toNat.log2 ^ q * ↑(internalCoveringNumber (δ / 4) J) + c * Cp d p q)
    source
    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} (hJ : HasBoundedInternalCoveringNumber 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 ≤ EMetric.diam 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 * δ.toReal⁻¹ ^ d)) ^ q + Cp d p q)
    source
    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} (hJ : HasBoundedInternalCoveringNumber 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 * δ.toReal⁻¹ ^ d)) ^ q + Cp d p q)