isProbabilityMeasure_trajFun — Mathlib

English

If η is a kernel such that for every b, η.map (frestrictLe b) = partialTraj κ a b, then η equals traj κ a.

Русский

Если для каждого b, η.map (frestrictLe b) = partialTraj κ a b, то η совпадает с traj κ a.

LaTeX

$$$\\forall b,\\ η.map(\\mathrm{frestrictLe}\\ b) = partialTraj\\ κ\\ a\\ b \\Rightarrow η = traj\\ κ\\ a$$$

Lean4

theorem isProbabilityMeasure_trajFun (a : ℕ) (x₀ : Π i : Iic a, X i) : IsProbabilityMeasure (trajFun κ a x₀) where
  measure_univ :=
    by
    rw [← cylinder_univ (Iic 0), trajFun, AddContent.measure_eq, trajContent_cylinder .univ, measure_univ]
    · exact generateFrom_measurableCylinders.symm
    · exact cylinder_mem_measurableCylinders _ _ .univ

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