Theorems · Theorem · probability

MeasureTheory.isProjectiveLimit_nat_iff

∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {μ : (I : Finset ℕ) → MeasureTheory.Measure ((i : ↥I) → X ↑i)},
  MeasureTheory.IsProjectiveMeasureFamily μ →
    ∀ (ν : MeasureTheory.Measure ((n : ℕ) → X n)),
      MeasureTheory.IsProjectiveLimit ν μ ↔
        ∀ (n : ℕ), MeasureTheory.Measure.map (Preorder.frestrictLe n) ν = μ (Finset.Iic n)

To check that a measure ν is the projective limit of a projective family of measures indexed by Finset ℕ, it is enough to check on intervals of the form Iic n.

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.Traj

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace