Product measures #
In this file we define and prove properties about finite products of measures (and at some point, countable products of measures).
Main definition #
MeasureTheory.Measure.pi
: The product of finitely many σ-finite measures. Givenμ : (i : ι) → Measure (α i)
for[Fintype ι]
it has typeMeasure ((i : ι) → α i)
.
To apply Fubini's theorem or Tonelli's theorem along some subset, we recommend using the marginal
construction MeasureTheory.lmarginal
and (todo) MeasureTheory.marginal
. This allows you to
apply the theorems without any bookkeeping with measurable equivalences.
Implementation Notes #
We define MeasureTheory.OuterMeasure.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 MeasureTheory.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
MeasurableEquiv.piMeasurableEquivTProd
between∀ ι, α i
and an iterated product ofα i
, calledList.tprod α l
for some listl
. - On this iterated product we can easily define a product measure
MeasureTheory.Measure.tprod
by iteratingMeasureTheory.Measure.prod
- Using the previous two steps we construct
MeasureTheory.Measure.pi'
on(i : ι) → α i
for countableι
. - We know that
MeasureTheory.Measure.pi'
sends products of sets to products of measures, and sinceMeasureTheory.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 forMeasureTheory.Measure.pi
.
Tags #
finitary product measure
We start with some measurability properties
Boxes formed by π-systems form a π-system.
Boxes form a π-system.
Boxes of countably spanning sets are countably spanning.
The product of generated σ-algebras is the one generated by boxes, if both generating sets are countably spanning.
If C
and D
generate the σ-algebras on α
resp. β
, then rectangles formed by C
and D
generate the σ-algebra on α × β
.
The product σ-algebra is generated from boxes, i.e. s ×ˢ t
for sets s : set α
and
t : set β
.
An upper bound for the measure in a finite product space. It is defined to by taking the image of the set under all projections, and taking the product of the measures of these images. For measurable boxes it is equal to the correct measure.
Equations
- MeasureTheory.piPremeasure m s = Finset.prod Finset.univ fun (i : ι) => ↑(m i) (Function.eval i '' s)
Instances For
OuterMeasure.pi m
is the finite product of the outer measures {m i | i : ι}
.
It is defined to be 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 : ι}
.
Equations
Instances For
A product of measures in tprod α l
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The product measure on an encodable finite type, defined by mapping Measure.tprod
along the
equivalence MeasurableEquiv.piMeasurableEquivTProd
.
The definition MeasureTheory.Measure.pi
should be used instead of this one.
Equations
Instances For
Measure.pi μ
is the finite product of the measures {μ i | i : ι}
.
It is defined to be measure corresponding to MeasureTheory.OuterMeasure.pi
.
Instances For
Equations
- MeasureTheory.MeasureSpace.pi = MeasureTheory.MeasureSpace.mk (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume)
Measure.pi μ
has finite spanning sets in rectangles of finite spanning sets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A measure on a finite product space equals the product measure if they are equal on rectangles with as sides sets that generate the corresponding σ-algebras.
A measure on a finite product space equals the product measure if they are equal on rectangles.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If one of the measures μ i
has no atoms, them Measure.pi µ
has no atoms. The instance below assumes that all μ i
have no atoms.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
We intentionally restrict this only to the nondependent function space, since
type-class inference cannot find an instance for ι → ℝ
when this is stated for dependent function
spaces.
Equations
- ⋯ = ⋯
We intentionally restrict this only to the nondependent function space, since type-class
inference cannot find an instance for ι → ℝ
when this is stated for dependent function spaces.
Equations
- ⋯ = ⋯
We intentionally restrict this only to the nondependent function space, since
type-class inference cannot find an instance for ι → ℝ
when this is stated for dependent function
spaces.
Equations
- ⋯ = ⋯
We intentionally restrict this only to the nondependent function space, since type-class
inference cannot find an instance for ι → ℝ
when this is stated for dependent function spaces.
Equations
- ⋯ = ⋯
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 MeasureTheory.measurePreserving
prefix.