Documentation

BrownianMotion.Continuity.IsKolmogorovProcess

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 : β), iI, f i b iI, ⨆ (b : β), f i b
theorem Finset.sup_le_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid β] [LinearOrder β] [OrderBot β] [IsOrderedAddMonoid β] (s : Finset α) (f : αβ) (hfs : is, 0 f i) :
s.sup f as, f a
theorem log2_le_logb_two (n : ) :
n.log2 Real.logb 2 n
structure ProbabilityTheory.IsMeasurableKolmogorovProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] (X : TΩE) (P : MeasureTheory.Measure Ω) (p q : ) (M : NNReal) :
Instances For
    def ProbabilityTheory.IsKolmogorovProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] (X : TΩE) (P : MeasureTheory.Measure Ω) (p q : ) (M : NNReal) :
    Equations
    Instances For
      noncomputable def ProbabilityTheory.IsKolmogorovProcess.mk {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} (X : TΩE) (h : IsKolmogorovProcess X P p q M) :
      TΩE
      Equations
      Instances For
        theorem ProbabilityTheory.IsKolmogorovProcess.ae_eq_mk {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (h : IsKolmogorovProcess X P p q M) (t : T) :
        X t =ᵐ[P] mk X h t
        theorem ProbabilityTheory.IsKolmogorovProcess.congr {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X Y : TΩE} (hX : IsKolmogorovProcess X P p q M) (h : ∀ (t : T), X t =ᵐ[P] Y t) :
        theorem ProbabilityTheory.IsKolmogorovProcess.kolmogorovCondition {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsKolmogorovProcess X P p q M) (s t : T) :
        ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p P M * edist s t ^ q
        theorem ProbabilityTheory.IsMeasurableKolmogorovProcess.measurable {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} [MeasurableSpace E] [BorelSpace E] (hX : IsMeasurableKolmogorovProcess X P p q M) (s : T) :
        theorem ProbabilityTheory.IsKolmogorovProcess.aemeasurable {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} [MeasurableSpace E] [BorelSpace E] (hX : IsKolmogorovProcess X P p q M) (s : T) :
        AEMeasurable (X s) P
        theorem ProbabilityTheory.measurable_pair_of_measurable {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : 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} { : 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.IsMeasurableKolmogorovProcess.mk_of_secondCountableTopology {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (h_meas : ∀ (s : T), Measurable (X s)) (h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p P M * edist s t ^ q) :
        theorem ProbabilityTheory.IsMeasurableKolmogorovProcess.stronglyMeasurable_edist {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsMeasurableKolmogorovProcess X P p q M) {s t : T} :
        MeasureTheory.StronglyMeasurable fun (ω : Ω) => edist (X s ω) (X t ω)
        theorem ProbabilityTheory.IsKolmogorovProcess.aestronglyMeasurable_edist {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsKolmogorovProcess X P p q M) {s t : T} :
        MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => edist (X s ω) (X t ω)) P
        theorem ProbabilityTheory.IsMeasurableKolmogorovProcess.measurable_edist {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsMeasurableKolmogorovProcess X P p q M) {s t : T} :
        Measurable fun (ω : Ω) => edist (X s ω) (X t ω)
        theorem ProbabilityTheory.IsKolmogorovProcess.aemeasurable_edist {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsKolmogorovProcess X P p q M) {s t : T} :
        AEMeasurable (fun (ω : Ω) => edist (X s ω) (X t ω)) P
        theorem ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsKolmogorovProcess X P p q M) (hp : 0 < p) (hq : 0 < q) {s t : T} (h : edist s t = 0) :
        ∀ᵐ (ω : Ω) P, edist (X s ω) (X t ω) = 0
        theorem ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero_of_M_eq_zero {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsKolmogorovProcess X P p q 0) (hp : 0 < p) {s t : T} :
        ∀ᵐ (ω : Ω) P, edist (X s ω) (X t ω) = 0
        theorem ProbabilityTheory.IsKolmogorovProcess.lintegral_sup_rpow_edist_eq_zero {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsKolmogorovProcess X P p q M) (hp : 0 < p) (hq : 0 < q) {T' : Set T} (hT' : T'.Countable) (h : sT', tT', edist s t = 0) :
        ∫⁻ (ω : Ω), ⨆ (s : T'), ⨆ (t : T'), edist (X (↑s) ω) (X (↑t) ω) ^ p P = 0
        theorem ProbabilityTheory.IsKolmogorovProcess.lintegral_sup_rpow_edist_eq_zero' {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hX : IsKolmogorovProcess X P p q M) (hp : 0 < p) (hq : 0 < q) {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] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hq : 0 q) (hX : IsKolmogorovProcess X P p q M) {ε : ENNReal} (C : Finset (T × T)) (hC : uC, edist u.1 u.2 ε) :
        ∫⁻ (ω : Ω), ⨆ (u : { x : T × T // x 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] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} (hp : 0 < p) (hq : 0 q) (hX : IsKolmogorovProcess 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
        theorem ProbabilityTheory.lintegral_sup_rpow_edist_cover_of_dist_le {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} {J : Set T} (hp : 0 < p) (hq : 0 q) (hX : IsKolmogorovProcess 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)
        theorem ProbabilityTheory.lintegral_sup_rpow_edist_cover_rescale {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} {J : Set T} (hp : 0 < p) (hq : 0 q) (hX : IsKolmogorovProcess 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)
        theorem ProbabilityTheory.lintegral_sup_rpow_edist_succ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} {J : Set T} {C : Finset T} {ε : ENNReal} {j k : } (hq : 0 q) (hX : IsKolmogorovProcess 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
        theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_sum_rpow {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : 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 : IsKolmogorovProcess 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 (∑ iFinset.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
        theorem ProbabilityTheory.lintegral_sup_rpow_edist_le_sum {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : 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 : IsKolmogorovProcess X P p q M) (hq : 0 q) (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 * (∑ iFinset.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] { : 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 : IsKolmogorovProcess X P p q M) ( : ∀ (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 : } (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 M * c₁ * (∑ jFinset.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] { : 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 : IsKolmogorovProcess X P p q M) {ε₀ : ENNReal} ( : ε₀ 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 : } (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) / 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] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} {J : Set T} {C : Finset T} {ε : ENNReal} {k m : } (hp_pos : 0 < p) (hp : p 1) (hX : IsKolmogorovProcess 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 iFinset.range (k - m), ∫⁻ (ω : Ω), ⨆ (t : { x : T // x C k }), edist (X (chainingSequence hC (m + i)) ω) (X (chainingSequence hC (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] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} {J : Set T} {C : Finset T} {ε : ENNReal} {k m : } (hp_pos : 0 < p) (hp : p 1) (hq : 0 q) (hX : IsKolmogorovProcess 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 * iFinset.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] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} {J : Set T} {C : Finset T} {ε : ENNReal} {k m : } (hp_pos : 0 < p) (hp : p 1) (hX : IsKolmogorovProcess X P p q M) ( : ∀ (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 : } (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 M * c₁ * jFinset.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] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} {J : Set T} {C : Finset T} {k m : } (hp_pos : 0 < p) (hp : p 1) (hX : IsKolmogorovProcess X P p q M) {ε₀ : ENNReal} ( : ε₀ 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)
        noncomputable def ProbabilityTheory.Cp (d p q : ) :
        Equations
        Instances For
          theorem ProbabilityTheory.second_term_bound {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {p q : } {M : NNReal} {P : MeasureTheory.Measure Ω} {X : TΩE} {J : Set T} {C : Finset T} {k m : } (hp_pos : 0 < p) (hX : IsKolmogorovProcess X P p q M) {ε₀ : ENNReal} ( : ε₀ 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
          theorem ProbabilityTheory.lintegral_sup_cover_eq_of_lt_iInf_dist {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : MeasurableSpace Ω} [PseudoEMetricSpace E] {P : MeasureTheory.Measure Ω} {X : TΩE} {M : NNReal} {p q : } {J : Set T} {δ : ENNReal} {C : Finset T} {ε : ENNReal} (hX : IsKolmogorovProcess X P p q M) (hp : 0 < p) (hq : 0 < q) (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
          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
          theorem ProbabilityTheory.scale_change_lintegral_iSup {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : 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 : IsKolmogorovProcess X P p q M) (hp : 0 p) (δ : 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
          theorem ProbabilityTheory.finite_set_bound_of_edist_le_of_diam_le {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : 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 : IsKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hp_pos : 0 < p) (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
          theorem ProbabilityTheory.finite_set_bound_of_edist_le_of_le_diam {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : 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 : IsKolmogorovProcess X P p q M) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) ( : δ 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)
          theorem ProbabilityTheory.finite_set_bound_of_edist_le_of_le_diam' {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : 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 : IsKolmogorovProcess X P p q M) (hc : c ) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) ( : δ 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)
          theorem ProbabilityTheory.finite_set_bound_of_edist_le {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] { : 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 : IsKolmogorovProcess X P p q M) (hc : c ) (hd_pos : 0 < d) (hp_pos : 0 < p) (hdq_lt : d < q) ( : δ 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)