Product measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define and prove properties about finite products of measures (and at some point, countable products of measures).

Main definition #

• measure_theory.measure.pi: The product of finitely many σ-finite measures. Given μ : Π i : ι, measure (α i) for [fintype ι] it has type measure (Π i : ι, α i).

To apply Fubini along some subset of the variables, use measure_theory.measure_preserving_pi_equiv_pi_subtype_prod to reduce to the situation of a product of two measures: this lemma states that the bijection measurable_equiv.pi_equiv_pi_subtype_prod α p between (Π i : ι, α i) and (Π i : {i // p i}, α i) × (Π i : {i // ¬ p i}, α i) maps a product measure to a direct product of product measures, to which one can apply the usual Fubini for direct product of measures.

Implementation Notes #

We define measure_theory.outer_measure.pi, the product of finitely many outer measures, as the maximal outer measure n with the property that n (pi univ s) ≤ ∏ i, m i (s i), where pi univ s is the product of the sets {s i | i : ι}.

We then show that this induces a product of measures, called measure_theory.measure.pi. For a collection of σ-finite measures μ and a collection of measurable sets s we show that measure.pi μ (pi univ s) = ∏ i, m i (s i). To do this, we follow the following steps:

• We know that there is some ordering on ι, given by an element of [countable ι].
• Using this, we have an equivalence measurable_equiv.pi_measurable_equiv_tprod between Π ι, α i and an iterated product of α i, called list.tprod α l for some list l.
• On this iterated product we can easily define a product measure measure_theory.measure.tprod by iterating measure_theory.measure.prod
• Using the previous two steps we construct measure_theory.measure.pi' on Π ι, α i for countable ι.
• We know that measure_theory.measure.pi' sends products of sets to products of measures, and since measure_theory.measure.pi is the maximal such measure (or at least, it comes from an outer measure which is the maximal such outer measure), we get the same rule for measure_theory.measure.pi.

Tags #

finitary product measure

We start with some measurability properties

Measure preserving equivalences #

In this section we prove that some measurable equivalences (e.g., between fin 1 → α and α or between fin 2 → α and α × α) preserve measure or volume. These lemmas can be used to prove that measures of corresponding sets (images or preimages) have equal measures and functions f ∘ e and f have equal integrals, see lemmas in the measure_theory.measure_preserving prefix.