Theorems · Definition · measure theory

MeasureTheory.Measure.infinitePi

{ι : Type u_1} →
  {X : ι → Type u_2} →
    {mX : (i : ι) → MeasurableSpace (X i)} →
      ((i : ι) → MeasureTheory.Measure (X i)) → MeasureTheory.Measure ((i : ι) → X i)

The product measure of an arbitrary family of probability measures. It is defined as the unique extension of the function which gives to cylinders the measure given by the associated product measure. It is defined via an if ... then ... else so that it can be manipulated without carrying a proof that the measures are probability measures.

Defined in

Mathlib.Probability.ProductMeasure

Cited by

48 results in Mathlib

Foundations

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