Determination of Skorokhod laws by finite-dimensional distributions #
Cylinder generation and uniqueness of projective limits identify path laws.
theorem
BGW.Skorokhod.ext_of_finiteDimensional
{T : ℝ}
{E : Type u_1}
[MetricSpace E]
[TopologicalSpace.SeparableSpace E]
[MeasurableSpace E]
[BorelSpace E]
{P Q : MeasureTheory.ProbabilityMeasure (D T E)}
{S : Set ↑(Set.Icc 0 T)}
(hS : Dense S)
(hT0 : 0 ≤ T)
(hTS : ⟨T, ⋯⟩ ∈ S)
(h :
∀ (s : Finset ↑(Set.Icc 0 T)),
↑s ⊆ S → (P.map fun (f : D T E) (t : ↥s) => f ↑t) = Q.map fun (f : D T E) (t : ↥s) => f ↑t)
:
Laws on D are determined by their finite-dimensional distributions at times of a dense
set containing the terminal time (C12(1)).