mk_of_secondCountableTopology — Mathlib

English

Under second countable topology on E and measurability hypotheses, the mk construction yields an Is Kolmogorov Process.

Русский

При условии второй счётности топологии на E и измеримых предпосылок конструкция mk даёт Is Kolmogorov Process.

LaTeX

$$$\\text{SecondCountableTopology } E \\to (\\forall h\\, Measurable, \\forall h_k\\, Kolmogorov) \\Rightarrow IsKolmogorovProcess$$$

Lean4

theorem mk_of_secondCountableTopology [SecondCountableTopology E] (h_meas : ∀ s, Measurable (X s))
    (h_kol : ∀ s t : T, ∫⁻ ω, (edist (X s ω) (X t ω)) ^ p ∂P ≤ M * edist s t ^ q) (hp : 0 < p) (hq : 0 < q) :
    IsKolmogorovProcess X P p q M
    where
  measurablePair s
    t := by
    suffices Measurable (fun ω ↦ (X s ω, X t ω)) by rwa [Prod.borelSpace.measurable_eq] at this
    fun_prop
  kolmogorovCondition := h_kol
  p_pos := hp
  q_pos := hq

Похожие утверждения