English
The projective limit of the finite-dimensional distributions of a stochastic process equals the law of the process itself. Formally, the push-forward measure along the full process equals the projective limit of the finite-dimensional push-forwards.
Русский
Проективный предел конечномерных распределений стахостического процесса равен распределению самого процесса.
LaTeX
$$$\text{If } X_t ext{ is a process and } P ext{ its law, then } \varphi_I = P\circ X|_I \text{ forms a projective limit with } \varphi_I = P\circ (I\text{ restriction of } X)$. Thus, the projective limit of the family $(\varphi_I)_{I}$ equals $P$.$$
Lean4
/-- The projective limit of the finite-dimensional distributions of a stochastic process is the law
of the process. -/
theorem isProjectiveLimit_map (hX : AEMeasurable (fun ω ↦ (X · ω)) P) :
IsProjectiveLimit (P.map (fun ω ↦ (X · ω))) (fun I ↦ P.map (fun ω ↦ I.restrict (X · ω))) :=
by
intro I
rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict _).aemeasurable hX, Function.comp_def]
