Theorems · Theorem · probability

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 Ω},
  AEMeasurable (fun ω x => X x ω) P →
    MeasureTheory.IsProjectiveLimit (MeasureTheory.Measure.map (fun ω x => X x ω) P) fun I =>
      MeasureTheory.Measure.map (fun ω => I.restrict fun x => X x ω) P

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

Defined in

Mathlib.Probability.Process.FiniteDimensionalLaws

Cited by

1 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound