Theorems · Theorem · probability

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

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

Defined in

Mathlib.Probability.Process.FiniteDimensionalLaws

Cited by

0 results in Mathlib

Foundations

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