Documentation

Mathlib.Probability.Process.FiniteDimensionalLaws

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 #

theorem ProbabilityTheory.isProjectiveMeasureFamily_map_restrict {T : Type u_1} {Ω : Type u_2} {𝓧 : TType u_3} { : MeasurableSpace Ω} { : (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} {𝓧 : TType u_3} { : MeasurableSpace Ω} { : (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} {𝓧 : TType u_3} { : MeasurableSpace Ω} { : (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} {𝓧 : TType u_3} { : MeasurableSpace Ω} { : (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} {𝓧 : TType u_3} { : MeasurableSpace Ω} { : (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} {𝓧 : TType u_3} { : MeasurableSpace Ω} { : (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.