Theorems · Theorem · measure theory

MeasureTheory.Measure.eq_infinitePi

∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {ν : MeasureTheory.Measure ((i : ι) → X i)},
  (∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
      (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)) →
    ν = MeasureTheory.Measure.infinitePi μ

To prove that a measure is equal to the product measure it is enough to check that it it gives the same measure to measurable boxes.

Defined in

Mathlib.Probability.ProductMeasure

Cited by

6 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure