English
The kernel traj κ a x0 is the projective limit of the family of partial trajectories (partialTraj κ a n x0) with the inducedFamily structure.
Русский
Ядро traj κ a x0 является проективной границей для семейства частичных траекторий (partialTraj κ a n x0) с использованием структуры inducedFamily.
LaTeX
$$$\\text{IsProjectiveLimit}\\bigl(\\text{trajFun }\\kappa\\ a\\ x_0\\bigr)\\bigl(\\text{inducedFamily }(n\\mapsto\\ partialTraj\\ kappa\\ a\\ n\\ x_0)\\bigr)$$$
Lean4
theorem isProjectiveLimit_trajFun (a : ℕ) (x₀ : Π i : Iic a, X i) :
IsProjectiveLimit (trajFun κ a x₀) (inducedFamily (fun n ↦ partialTraj κ a n x₀)) :=
by
refine isProjectiveLimit_nat_iff (isProjectiveMeasureFamily_partialTraj κ x₀) _ |>.2 fun n ↦ ?_
ext s ms
rw [Measure.map_apply (measurable_frestrictLe n) ms, trajFun, AddContent.measure_eq, trajContent,
projectiveFamilyContent_congr _ (frestrictLe n ⁻¹' s) rfl ms]
· exact generateFrom_measurableCylinders.symm
· exact cylinder_mem_measurableCylinders _ _ ms
