English
Two processes have the same law if and only if they have the same finite-dimensional distributions. Precisely, P.map preserves equality if and only if all finite-dimensional restrictions coincide.
Русский
Два процесса имеют одинаковое распределение тогда и только тогда, когда совпадают их конечномерные распределения.
LaTeX
$$$P\text{-map equality } = P\text{ map equality} \iff \forall I, P\circ (X|_I) = P\circ (Y|_I).$$$
Lean4
/-- Two stochastic processes have same law iff they have the same
finite-dimensional distributions. -/
theorem map_eq_iff_forall_finset_map_restrict_eq [IsFiniteMeasure P] (hX : AEMeasurable (fun ω ↦ (X · ω)) P)
(hY : AEMeasurable (fun ω ↦ (Y · ω)) P) :
P.map (fun ω ↦ (X · ω)) = P.map (fun ω ↦ (Y · ω)) ↔
∀ I : Finset T, P.map (fun ω ↦ I.restrict (X · ω)) = P.map (fun ω ↦ I.restrict (Y · ω)) :=
by
refine ⟨fun h I ↦ ?_, fun h ↦ ?_⟩
· have hX' : P.map (fun ω ↦ I.restrict (X · ω)) = (P.map (fun ω ↦ (X · ω))).map I.restrict := by
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX, Function.comp_def]
have hY' : P.map (fun ω ↦ I.restrict (Y · ω)) = (P.map (fun ω ↦ (Y · ω))).map I.restrict := by
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hY, Function.comp_def]
rw [hX', hY', h]
· have hX' := isProjectiveLimit_map hX
simp_rw [h] at hX'
exact hX'.unique (isProjectiveLimit_map hY)
