Stochastic processes satisfying the Kolmogorov condition

structure ProbabilityTheory.IsKolmogorovProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] (X : T → Ω → E) (P : MeasureTheory.Measure Ω) (p q M : NNReal) : Prop

• aemeasurablePair (s t : T) : AEMeasurable (fun (ω : Ω) => (X s ω, X t ω)) P
• kolmogorovCondition (s t : T) : ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ ↑p ∂P ≤ ↑M * edist s t ^ ↑q

theorem ProbabilityTheory.IsKolmogorovProcess.aemeasurable {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] {p q M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E} (hX : IsKolmogorovProcess X P p q M) (s : T) : AEMeasurable (X s) P

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

theorem ProbabilityTheory.IsKolmogorovProcess.mk_of_secondCountableTopology {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] {p q M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E} [SecondCountableTopology E] (h_meas : ∀ (s : T), AEMeasurable (X s) P) (h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ ↑p ∂P ≤ ↑M * edist s t ^ ↑q) : IsKolmogorovProcess X P p q M

theorem ProbabilityTheory.IsKolmogorovProcess.aestronglyMeasurable_edist {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 : IsKolmogorovProcess X P p q M) {s t : T} : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => edist (X s ω) (X t ω)) P

theorem ProbabilityTheory.IsKolmogorovProcess.aemeasurable_edist {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 : IsKolmogorovProcess X P p q M) {s t : T} : AEMeasurable (fun (ω : Ω) => edist (X s ω) (X t ω)) P

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] [MeasurableSpace E] [BorelSpace E] {p q M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E} (hX : IsKolmogorovProcess 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] [MeasurableSpace E] [BorelSpace E] {p q M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E} (hX : IsKolmogorovProcess X P p q M) {J : Finset T} {a c : ENNReal} {n : ℕ} (hJ_card : ↑J.card ≤ a ^ n) (ha : 1 < a) (hc : c ≠ 0) : ∫⁻ (ω : Ω), ⨆ (s : T), ⨆ (t : T), ⨆ (_ : s ∈ J), ⨆ (_ : t ∈ J), ⨆ (_ : edist s t ≤ c), edist (X s ω) (X t ω) ^ ↑p ∂P ≤ 2 ^ ↑p * a * ↑J.card * ↑M * (c * ↑n) ^ ↑q