# mathlib3documentation

measure_theory.constructions.pi

# 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

theorem is_pi_system.pi {ι : Type u_1} {α : ι Type u_3} {C : Π (i : ι), set (set (α i))} (hC : (i : ι), is_pi_system (C i)) :

Boxes formed by π-systems form a π-system.

theorem is_pi_system_pi {ι : Type u_1} {α : ι Type u_3} [Π (i : ι), measurable_space (α i)] :
is_pi_system (set.univ.pi '' set.univ.pi (λ (i : ι), {s : set (α i) | measurable_set s}))

Boxes form a π-system.

theorem is_countably_spanning.pi {ι : Type u_1} {α : ι Type u_3} [finite ι] {C : Π (i : ι), set (set (α i))} (hC : (i : ι), ) :

Boxes of countably spanning sets are countably spanning.

theorem generate_from_pi_eq {ι : Type u_1} {α : ι Type u_3} [finite ι] {C : Π (i : ι), set (set (α i))} (hC : (i : ι), ) :

The product of generated σ-algebras is the one generated by boxes, if both generating sets are countably spanning.

theorem generate_from_eq_pi {ι : Type u_1} {α : ι Type u_3} [finite ι] [h : Π (i : ι), measurable_space (α i)] {C : Π (i : ι), set (set (α i))} (hC : (i : ι), = h i) (h2C : (i : ι), ) :

If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D` generate the σ-algebra on `α × β`.

theorem generate_from_pi {ι : Type u_1} {α : ι Type u_3} [finite ι] [Π (i : ι), measurable_space (α i)] :

The product σ-algebra is generated from boxes, i.e. `s ×ˢ t` for sets `s : set α` and `t : set β`.

@[simp]
noncomputable def measure_theory.pi_premeasure {ι : Type u_1} {α : ι Type u_3} [fintype ι] (m : Π (i : ι), ) (s : set (Π (i : ι), α i)) :

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
theorem measure_theory.pi_premeasure_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] {m : Π (i : ι), } {s : Π (i : ι), set (α i)} (hs : (set.univ.pi s).nonempty) :
= finset.univ.prod (λ (i : ι), (m i) (s i))
theorem measure_theory.pi_premeasure_pi' {ι : Type u_1} {α : ι Type u_3} [fintype ι] {m : Π (i : ι), } {s : Π (i : ι), set (α i)} :
= finset.univ.prod (λ (i : ι), (m i) (s i))
theorem measure_theory.pi_premeasure_pi_mono {ι : Type u_1} {α : ι Type u_3} [fintype ι] {m : Π (i : ι), } {s t : set (Π (i : ι), α i)} (h : s t) :
theorem measure_theory.pi_premeasure_pi_eval {ι : Type u_1} {α : ι Type u_3} [fintype ι] {m : Π (i : ι), } {s : set (Π (i : ι), α i)} :
(set.univ.pi (λ (i : ι), '' s)) =
@[protected]
noncomputable def measure_theory.outer_measure.pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] (m : Π (i : ι), ) :

`outer_measure.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
theorem measure_theory.outer_measure.pi_pi_le {ι : Type u_1} {α : ι Type u_3} [fintype ι] (m : Π (i : ι), ) (s : Π (i : ι), set (α i)) :
finset.univ.prod (λ (i : ι), (m i) (s i))
theorem measure_theory.outer_measure.le_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] {m : Π (i : ι), } {n : measure_theory.outer_measure (Π (i : ι), α i)} :
(s : Π (i : ι), set (α i)), (set.univ.pi s).nonempty n (set.univ.pi s) finset.univ.prod (λ (i : ι), (m i) (s i))
@[protected]
noncomputable def measure_theory.measure.tprod {δ : Type u_4} {π : δ Type u_5} [Π (x : δ), measurable_space (π x)] (l : list δ) (μ : Π (i : δ), ) :

A product of measures in `tprod α l`.

Equations
Instances for `measure_theory.measure.tprod`
@[simp]
theorem measure_theory.measure.tprod_nil {δ : Type u_4} {π : δ Type u_5} [Π (x : δ), measurable_space (π x)] (μ : Π (i : δ), ) :
@[simp]
theorem measure_theory.measure.tprod_cons {δ : Type u_4} {π : δ Type u_5} [Π (x : δ), measurable_space (π x)] (i : δ) (l : list δ) (μ : Π (i : δ), ) :
μ = (μ i).prod
@[protected, instance]
def measure_theory.measure.sigma_finite_tprod {δ : Type u_4} {π : δ Type u_5} [Π (x : δ), measurable_space (π x)] (l : list δ) (μ : Π (i : δ), ) [ (i : δ), ] :
theorem measure_theory.measure.tprod_tprod {δ : Type u_4} {π : δ Type u_5} [Π (x : δ), measurable_space (π x)] (l : list δ) (μ : Π (i : δ), ) [ (i : δ), ] (s : Π (i : δ), set (π i)) :
s) = (list.map (λ (i : δ), (μ i) (s i)) l).prod
noncomputable def measure_theory.measure.pi' {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [encodable ι] :
measure_theory.measure (Π (i : ι), α i)

The product measure on an encodable finite type, defined by mapping `measure.tprod` along the equivalence `measurable_equiv.pi_measurable_equiv_tprod`. The definition `measure_theory.measure.pi` should be used instead of this one.

Equations
theorem measure_theory.measure.pi'_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [encodable ι] [ (i : ι), ] (s : Π (i : ι), set (α i)) :
= finset.univ.prod (λ (i : ι), (μ i) (s i))
theorem measure_theory.measure.pi_caratheodory {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) :
@[protected, irreducible]
noncomputable def measure_theory.measure.pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) :
measure_theory.measure (Π (i : ι), α i)

`measure.pi μ` is the finite product of the measures `{μ i | i : ι}`. It is defined to be measure corresponding to `measure_theory.outer_measure.pi`.

Equations
Instances for `measure_theory.measure.pi`
theorem measure_theory.measure.pi_pi_aux {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] (s : Π (i : ι), set (α i)) (hs : (i : ι), measurable_set (s i)) :
(set.univ.pi s) = finset.univ.prod (λ (i : ι), (μ i) (s i))
def measure_theory.measure.finite_spanning_sets_in.pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } {C : Π (i : ι), set (set (α i))} (hμ : Π (i : ι), (μ i).finite_spanning_sets_in (C i)) :

`measure.pi μ` has finite spanning sets in rectangles of finite spanning sets.

Equations
theorem measure_theory.measure.pi_eq_generate_from {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } {C : Π (i : ι), set (set (α i))} (hC : (i : ι), = _inst_2 i) (h2C : (i : ι), is_pi_system (C i)) (h3C : Π (i : ι), (μ i).finite_spanning_sets_in (C i)) {μν : measure_theory.measure (Π (i : ι), α i)} (h₁ : (s : Π (i : ι), set (α i)), ( (i : ι), s i C i) μν (set.univ.pi s) = finset.univ.prod (λ (i : ι), (μ i) (s i))) :

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.

theorem measure_theory.measure.pi_eq {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] {μ' : measure_theory.measure (Π (i : ι), α i)} (h : (s : Π (i : ι), set (α i)), ( (i : ι), measurable_set (s i)) μ' (set.univ.pi s) = finset.univ.prod (λ (i : ι), (μ i) (s i))) :

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

theorem measure_theory.measure.pi'_eq_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [encodable ι] :
@[simp]
theorem measure_theory.measure.pi_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] (s : Π (i : ι), set (α i)) :
(set.univ.pi s) = finset.univ.prod (λ (i : ι), (μ i) (s i))
theorem measure_theory.measure.pi_univ {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] :
= finset.univ.prod (λ (i : ι), (μ i) set.univ)
theorem measure_theory.measure.pi_ball {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), metric_space (α i)] (x : Π (i : ι), α i) {r : } (hr : 0 < r) :
r) = finset.univ.prod (λ (i : ι), (μ i) (metric.ball (x i) r))
theorem measure_theory.measure.pi_closed_ball {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), metric_space (α i)] (x : Π (i : ι), α i) {r : } (hr : 0 r) :
= finset.univ.prod (λ (i : ι), (μ i) (metric.closed_ball (x i) r))
@[protected, instance]
def measure_theory.measure.pi.sigma_finite {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] :
theorem measure_theory.measure.pi_of_empty {α : Type u_1} [is_empty α] {β : α Type u_2} {m : Π (a : α), measurable_space (β a)} (μ : Π (a : α), ) (x : (Π (a : α), β a) := is_empty_elim) :
theorem measure_theory.measure.pi_eval_preimage_null {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] {i : ι} {s : set (α i)} (hs : (μ i) s = 0) :
⁻¹' s) = 0
theorem measure_theory.measure.pi_hyperplane {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] (i : ι) [measure_theory.has_no_atoms (μ i)] (x : α i) :
{f : Π (i : ι), α i | f i = x} = 0
theorem measure_theory.measure.ae_eval_ne {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] (i : ι) [measure_theory.has_no_atoms (μ i)] (x : α i) :
∀ᵐ (y : Π (i : ι), α i) , y i x
theorem measure_theory.measure.tendsto_eval_ae_ae {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] {i : ι} :
(μ i).ae
theorem measure_theory.measure.ae_pi_le_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] :
filter.pi (λ (i : ι), (μ i).ae)
theorem measure_theory.measure.ae_eq_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] {β : ι Type u_2} {f f' : Π (i : ι), α i β i} (h : (i : ι), f i =ᵐ[μ i] f' i) :
(λ (x : Π (i : ι), α i) (i : ι), f i (x i)) =ᵐ[] λ (x : Π (i : ι), α i) (i : ι), f' i (x i)
theorem measure_theory.measure.ae_le_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] {β : ι Type u_2} [Π (i : ι), preorder (β i)] {f f' : Π (i : ι), α i β i} (h : (i : ι), f i ≤ᵐ[μ i] f' i) :
(λ (x : Π (i : ι), α i) (i : ι), f i (x i)) ≤ᵐ[] λ (x : Π (i : ι), α i) (i : ι), f' i (x i)
theorem measure_theory.measure.ae_le_set_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] {I : set ι} {s t : Π (i : ι), set (α i)} (h : (i : ι), i I s i ≤ᵐ[μ i] t i) :
I.pi s ≤ᵐ[] I.pi t
theorem measure_theory.measure.ae_eq_set_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] {I : set ι} {s t : Π (i : ι), set (α i)} (h : (i : ι), i I s i =ᵐ[μ i] t i) :
I.pi s =ᵐ[] I.pi t
theorem measure_theory.measure.pi_Iio_ae_eq_pi_Iic {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {s : set ι} {f : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Iio (f i)) =ᵐ[] s.pi (λ (i : ι), set.Iic (f i))
theorem measure_theory.measure.pi_Ioi_ae_eq_pi_Ici {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {s : set ι} {f : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ioi (f i)) =ᵐ[] s.pi (λ (i : ι), set.Ici (f i))
theorem measure_theory.measure.univ_pi_Iio_ae_eq_Iic {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {f : Π (i : ι), α i} :
set.univ.pi (λ (i : ι), set.Iio (f i)) =ᵐ[]
theorem measure_theory.measure.univ_pi_Ioi_ae_eq_Ici {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {f : Π (i : ι), α i} :
set.univ.pi (λ (i : ι), set.Ioi (f i)) =ᵐ[]
theorem measure_theory.measure.pi_Ioo_ae_eq_pi_Icc {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {s : set ι} {f g : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ioo (f i) (g i)) =ᵐ[] s.pi (λ (i : ι), set.Icc (f i) (g i))
theorem measure_theory.measure.pi_Ioo_ae_eq_pi_Ioc {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {s : set ι} {f g : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ioo (f i) (g i)) =ᵐ[] s.pi (λ (i : ι), set.Ioc (f i) (g i))
theorem measure_theory.measure.univ_pi_Ioo_ae_eq_Icc {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {f g : Π (i : ι), α i} :
set.univ.pi (λ (i : ι), set.Ioo (f i) (g i)) =ᵐ[] g
theorem measure_theory.measure.pi_Ioc_ae_eq_pi_Icc {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {s : set ι} {f g : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ioc (f i) (g i)) =ᵐ[] s.pi (λ (i : ι), set.Icc (f i) (g i))
theorem measure_theory.measure.univ_pi_Ioc_ae_eq_Icc {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {f g : Π (i : ι), α i} :
set.univ.pi (λ (i : ι), set.Ioc (f i) (g i)) =ᵐ[] g
theorem measure_theory.measure.pi_Ico_ae_eq_pi_Icc {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {s : set ι} {f g : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ico (f i) (g i)) =ᵐ[] s.pi (λ (i : ι), set.Icc (f i) (g i))
theorem measure_theory.measure.univ_pi_Ico_ae_eq_Icc {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), partial_order (α i)] [ (i : ι), ] {f g : Π (i : ι), α i} :
set.univ.pi (λ (i : ι), set.Ico (f i) (g i)) =ᵐ[] g
theorem measure_theory.measure.pi_has_no_atoms {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] (i : ι) [measure_theory.has_no_atoms (μ i)] :

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.

@[protected, instance]
def measure_theory.measure.pi.measure_theory.has_no_atoms {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [h : nonempty ι] [ (i : ι), ] :
@[protected, instance]
def measure_theory.measure.pi.measure_theory.is_locally_finite_measure {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), } [ (i : ι), ] [Π (i : ι), topological_space (α i)] [ (i : ι), ] :
@[protected, instance]
def measure_theory.measure.pi.is_add_left_invariant {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), add_group (α i)] [ (i : ι), has_measurable_add (α i)] [ (i : ι), (μ i).is_add_left_invariant] :
@[protected, instance]
def measure_theory.measure.pi.is_mul_left_invariant {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), group (α i)] [ (i : ι), has_measurable_mul (α i)] [ (i : ι), (μ i).is_mul_left_invariant] :
@[protected, instance]
def measure_theory.measure.pi.is_mul_right_invariant {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), group (α i)] [ (i : ι), has_measurable_mul (α i)] [ (i : ι), (μ i).is_mul_right_invariant] :
@[protected, instance]
def measure_theory.measure.pi.is_add_right_invariant {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), add_group (α i)] [ (i : ι), has_measurable_add (α i)] [ (i : ι), (μ i).is_add_right_invariant] :
@[protected, instance]
def measure_theory.measure.pi.is_inv_invariant {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), group (α i)] [ (i : ι), has_measurable_inv (α i)] [ (i : ι), (μ i).is_inv_invariant] :
@[protected, instance]
def measure_theory.measure.pi.is_neg_invariant {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), add_group (α i)] [ (i : ι), has_measurable_neg (α i)] [ (i : ι), (μ i).is_neg_invariant] :
@[protected, instance]
def measure_theory.measure.pi.is_open_pos_measure {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), topological_space (α i)] [ (i : ι), (μ i).is_open_pos_measure] :
@[protected, instance]
def measure_theory.measure.pi.is_finite_measure_on_compacts {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), topological_space (α i)] [ (i : ι), ] :
@[protected, instance]
def measure_theory.measure.pi.is_add_haar_measure {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), add_group (α i)] [Π (i : ι), topological_space (α i)] [ (i : ι), (μ i).is_add_haar_measure] [ (i : ι), has_measurable_add (α i)] :
@[protected, instance]
def measure_theory.measure.pi.is_haar_measure {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), ) [ (i : ι), ] [Π (i : ι), group (α i)] [Π (i : ι), topological_space (α i)] [ (i : ι), (μ i).is_haar_measure] [ (i : ι), has_measurable_mul (α i)] :
@[protected, instance]
noncomputable def measure_theory.measure_space.pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), ] :
Equations
theorem measure_theory.volume_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), ] :
theorem measure_theory.volume_pi_pi {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), ] (s : Π (i : ι), set (α i)) :
= finset.univ.prod (λ (i : ι),
theorem measure_theory.volume_pi_ball {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), ] [Π (i : ι), metric_space (α i)] (x : Π (i : ι), α i) {r : } (hr : 0 < r) :
= finset.univ.prod (λ (i : ι),
theorem measure_theory.volume_pi_closed_ball {ι : Type u_1} {α : ι Type u_3} [fintype ι] [Π (i : ι), ] [Π (i : ι), metric_space (α i)] (x : Π (i : ι), α i) {r : } (hr : 0 r) :
= finset.univ.prod (λ (i : ι),
@[protected, instance]

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.

@[protected, instance]

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.

@[protected, instance]

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.

@[protected, instance]

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.

### 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.

theorem measure_theory.measure_preserving_pi_equiv_pi_subtype_prod {ι : Type u} {α : ι Type v} [fintype ι] {m : Π (i : ι), measurable_space (α i)} (μ : Π (i : ι), ) [ (i : ι), ] (p : ι Prop)  :
((measure_theory.measure.pi (λ (i : subtype p), μ i)).prod (measure_theory.measure.pi (λ (i : {i // ¬p i}), μ i)))
theorem measure_theory.volume_preserving_pi_equiv_pi_subtype_prod {ι : Type u_1} (α : ι Type u_2) [fintype ι] [Π (i : ι), ] (p : ι Prop)  :
theorem measure_theory.measure_preserving_pi_fin_succ_above_equiv {n : } {α : fin (n + 1) Type u} {m : Π (i : fin (n + 1)), measurable_space (α i)} (μ : Π (i : fin (n + 1)), ) [ (i : fin (n + 1)), ] (i : fin (n + 1)) :
((μ i).prod (measure_theory.measure.pi (λ (j : fin n), μ ((i.succ_above) j))))
theorem measure_theory.volume_preserving_pi_fin_succ_above_equiv {n : } (α : fin (n + 1) Type u) [Π (i : fin (n + 1)), ] (i : fin (n + 1)) :
theorem measure_theory.measure_preserving_fun_unique {β : Type u} {m : measurable_space β} (μ : measure_theory.measure β) (α : Type v) [unique α] :
(measure_theory.measure.pi (λ (a : α), μ)) μ
theorem measure_theory.measure_preserving_pi_fin_two {α : fin 2 Type u} {m : Π (i : fin 2), measurable_space (α i)} (μ : Π (i : fin 2), ) [ (i : fin 2), ] :
((μ 0).prod (μ 1))
theorem measure_theory.measure_preserving_pi_empty {ι : Type u} {α : ι Type v} [is_empty ι] {m : Π (i : ι), measurable_space (α i)} (μ : Π (i : ι), ) :
theorem measure_theory.volume_preserving_pi_empty {ι : Type u} (α : ι Type v) [is_empty ι] [Π (i : ι), ] :