∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {X : T → Ω → E} {P : MeasureTheory.Measure Ω} {p q : ℝ} {M : NNReal},
  ProbabilityTheory.IsKolmogorovProcess X P p q M → 0 < q