map_restrict_eq_of_forall_ae_eq — Mathlib

English

If two stochastic processes are modifications of each other, then they have the same finite-dimensional distributions (hence the same law).

Русский

Если два процесса являются модификациями друг друга, то их конечномерные распределения совпадают (значит и закон равны).

LaTeX

$$$\text{If } X_t =\!\! Y_t \quad \text{a.e. under } P, \text{ then } \; P\circ X|_I = P\circ Y|_I \text{ for all finite } I$.$$

Lean4

/-- If two processes are modifications of each other, then they have the same finite-dimensional
distributions. -/
theorem map_restrict_eq_of_forall_ae_eq (h : ∀ t, X t =ᵐ[P] Y t) (I : Finset T) :
    P.map (fun ω ↦ I.restrict (X · ω)) = P.map (fun ω ↦ I.restrict (Y · ω)) :=
  by
  have h' : ∀ᵐ ω ∂P, ∀ (i : I), X i ω = Y i ω :=
    by
    rw [MeasureTheory.ae_all_iff]
    exact fun i ↦ h i
  refine Measure.map_congr ?_
  filter_upwards [h'] with ω h using funext h

Похожие утверждения