map_eq_of_forall_ae_eq — Mathlib

English

If two processes are modifications of each other, then their laws coincide; more precisely, their pushforward measures under the process maps are equal.

Русский

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

LaTeX

$$$P\circ X|_I = P\circ Y|_I\quad\forall I\subseteq_{fin} 𝕋$.$$

Lean4

/-- If two processes are modifications of each other, then they have the same distribution. -/
theorem map_eq_of_forall_ae_eq [IsFiniteMeasure P] (hX : AEMeasurable (fun ω ↦ (X · ω)) P)
    (hY : AEMeasurable (fun ω ↦ (Y · ω)) P) (h : ∀ t, X t =ᵐ[P] Y t) :
    P.map (fun ω ↦ (X · ω)) = P.map (fun ω ↦ (Y · ω)) :=
  by
  rw [map_eq_iff_forall_finset_map_restrict_eq hX hY]
  exact fun I ↦ map_restrict_eq_of_forall_ae_eq h I

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