Finite-dimensional distributions of a stochastic process

For a stochastic process X : T → Ω → 𝓧 and a finite measure P on Ω, the law of the process is P.map (fun ω ↦ (X · ω)), and its finite-dimensional distributions are P.map (fun ω ↦ I.restrict (X · ω)) for I : Finset T.

We show that two stochastic processes have the same laws if and only if they have the same finite-dimensional distributions.

Main statements

• map_eq_iff_forall_finset_map_restrict_eq: two processes have the same law if and only if their finite-dimensional distributions are equal.
• identDistrib_iff_forall_finset_identDistrib: same statement, but stated in terms of IdentDistrib.
• map_restrict_eq_of_forall_ae_eq: if two processes are modifications of each other, then their finite-dimensional distributions are equal.
• map_eq_of_forall_ae_eq: if two processes are modifications of each other, then they have the same law.

theorem ProbabilityTheory.isProjectiveMeasureFamily_map_restrict {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)} {X : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} (hX : ∀ (t : T), AEMeasurable (X t) P) : MeasureTheory.IsProjectiveMeasureFamily fun (I : Finset T) => MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P

The finite-dimensional distributions of a stochastic process are a projective measure family.

theorem ProbabilityTheory.isProjectiveLimit_map {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)} {X : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} (hX : AEMeasurable (fun (ω : Ω) (x : T) => X x ω) P) : MeasureTheory.IsProjectiveLimit (MeasureTheory.Measure.map (fun (ω : Ω) (x : T) => X x ω) P) fun (I : Finset T) => MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P

The projective limit of the finite-dimensional distributions of a stochastic process is the law of the process.

theorem ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)} {X Y : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (hX : AEMeasurable (fun (ω : Ω) (x : T) => X x ω) P) (hY : AEMeasurable (fun (ω : Ω) (x : T) => Y x ω) P) : MeasureTheory.Measure.map (fun (ω : Ω) (x : T) => X x ω) P = MeasureTheory.Measure.map (fun (ω : Ω) (x : T) => Y x ω) P ↔ ∀ (I : Finset T), MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P = MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => Y x ω) P

Two stochastic processes have same law iff they have the same finite-dimensional distributions.

theorem ProbabilityTheory.identDistrib_iff_forall_finset_identDistrib {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)} {X Y : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (hX : AEMeasurable (fun (ω : Ω) (x : T) => X x ω) P) (hY : AEMeasurable (fun (ω : Ω) (x : T) => Y x ω) P) : IdentDistrib (fun (ω : Ω) (x : T) => X x ω) (fun (ω : Ω) (x : T) => Y x ω) P P ↔ ∀ (I : Finset T), IdentDistrib (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) (fun (ω : Ω) => I.restrict fun (x : T) => Y x ω) P P

Two stochastic processes are identically distributed iff they have the same finite-dimensional distributions.

theorem ProbabilityTheory.map_restrict_eq_of_forall_ae_eq {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)} {X Y : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} (h : ∀ (t : T), X t =ᵐ[P] Y t) (I : Finset T) : MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P = MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => Y x ω) P

If two processes are modifications of each other, then they have the same finite-dimensional distributions.

theorem ProbabilityTheory.map_eq_of_forall_ae_eq {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)} {X Y : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (hX : AEMeasurable (fun (ω : Ω) (x : T) => X x ω) P) (hY : AEMeasurable (fun (ω : Ω) (x : T) => Y x ω) P) (h : ∀ (t : T), X t =ᵐ[P] Y t) : MeasureTheory.Measure.map (fun (ω : Ω) (x : T) => X x ω) P = MeasureTheory.Measure.map (fun (ω : Ω) (x : T) => Y x ω) P

If two processes are modifications of each other, then they have the same distribution.