English
Two processes are identically distributed if and only if they have the same finite-dimensional distributions. This is characterized by the equality of all finite restrictions under a common dominating measure P.
Русский
Два процесса имеют одинаковое распределение тогда и только тогда, когда их конечномерные распределения совпадают.
LaTeX
$$$\text{IdentDistrib}(X,Y,P,P) \iff \forall I, \text{IdentDistrib}(X|_I,Y|_I,P,P).$$$
Lean4
/-- Two stochastic processes are identically distributed iff they have the same
finite-dimensional distributions. -/
theorem identDistrib_iff_forall_finset_identDistrib [IsFiniteMeasure P] (hX : AEMeasurable (fun ω ↦ (X · ω)) P)
(hY : AEMeasurable (fun ω ↦ (Y · ω)) P) :
IdentDistrib (fun ω ↦ (X · ω)) (fun ω ↦ (Y · ω)) P P ↔
∀ I : Finset T, IdentDistrib (fun ω ↦ I.restrict (X · ω)) (fun ω ↦ I.restrict (Y · ω)) P P :=
by
refine ⟨fun h I ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ⟨hX, hY, ?_⟩⟩
· exact (Finset.measurable_restrict _).comp_aemeasurable hX
· exact (Finset.measurable_restrict _).comp_aemeasurable hY
· exact (map_eq_iff_forall_finset_map_restrict_eq hX hY).mp h.map_eq I
· exact (map_eq_iff_forall_finset_map_restrict_eq hX hY).mpr (fun I ↦ (h I).map_eq)
