Theorems · Theorem · measure theory

MeasureTheory.Measure.pi_eq

∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  {μ' : MeasureTheory.Measure ((i : ι) → α i)},
  (∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (s i)) → μ' (Set.univ.pi s) = ∏ i, (μ i) (s i)) →
    MeasureTheory.Measure.pi μ = μ'

A measure on a finite product space equals the product measure if they are equal on rectangles.

Defined in

Mathlib.MeasureTheory.Constructions.Pi

Cited by

19 results in Mathlib

Foundations

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

Assumes

FintypeMeasurableSpaceMeasureTheory.SigmaFinite