English
trajContent κ x0 is defined as the additive content on measurable cylinders obtained from the projective measure family corresponding to the trajectory; it uses projectiveFamilyContent built from the projective limit property.
Русский
trajContent κ x0 задаёт добавочное содержимое по измеримым цилиндрам для траектории, используя проектное семейство мер.
LaTeX
$$$\\text{trajContent}\\;\\kappa\\; x_0 = \\text{projectiveFamilyContent}\\bigl(\\text{isProjectiveMeasureFamilyPartialTraj }\\kappa\\ x_0\\bigr)$$$
Lean4
/-- Given a family of kernels `κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))`, and the
trajectory up to time `a` we can construct an additive content over cylinders. It corresponds
to composing the kernels, starting at time `a + 1`. -/
noncomputable def trajContent {a : ℕ} (x₀ : Π i : Iic a, X i) : AddContent (measurableCylinders X) :=
projectiveFamilyContent (isProjectiveMeasureFamily_partialTraj κ x₀)
