Theorems · Theorem · probability

MeasureTheory.isProjectiveMeasureFamily_inducedFamily

∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)),
  (∀ (a b : ℕ) (hab : a ≤ b), MeasureTheory.Measure.map (Preorder.frestrictLe₂ hab) (μ b) = μ a) →
    MeasureTheory.IsProjectiveMeasureFamily (MeasureTheory.inducedFamily μ)

Given a family of measures μ : (n : ℕ) → Measure (Π i : Iic n, X i), the induced family will be projective only if μ is projective, in the sense that if a ≤ b, then projecting μ b gives μ a.

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.Traj

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace