English
Let X be a family of random variables. For every finite index set I, the finite-dimensional distribution μ_I = P.map(ω ↦ (I.restrict(X(·, ω)))) forms a projective family with respect to the restriction maps, i.e., μ_J restricted to I equals μ_I whenever I ⊆ J.
Русский
Пусть имеется семейство случайных величин. Для каждого конечного подмножества индексов I конечного множества 𝕀 распределения μ_I = P.map(ω ↦ (I.restrict (X(·, ω)))) образуют проективную семью относительно отображений ограничений: если I ⊆ J то ограничение μ_J до μ_I равно μ_I.
LaTeX
$$$\{ \mu_I : I \subseteq_{fin} 𝕀 \}$ является проективной семью, где $\mu_I = P\circ (X|_I)\!_\ast$, то есть $\mu_J|_I = \mu_I$ для всех $I\subseteq J$.$$
Lean4
/-- The finite-dimensional distributions of a stochastic process are a projective measure family. -/
theorem isProjectiveMeasureFamily_map_restrict (hX : ∀ t, AEMeasurable (X t) P) :
IsProjectiveMeasureFamily (fun I ↦ P.map (fun ω ↦ I.restrict (X · ω))) :=
by
intro I J hJI
rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict₂ _).aemeasurable]
· simp [Finset.restrict_def, Finset.restrict₂_def, Function.comp_def]
· exact aemeasurable_pi_lambda _ fun _ ↦ hX _
