mathlib documentation

measure_theory.constructions.pi

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 #

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:

Tags #

finitary product measure

We start with some measurability properties

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} [fintype ι] {C : Π (i : ι), set (set (α i))} (hC : ∀ (i : ι), is_countably_spanning (C i)) :

Boxes of countably spanning sets are countably spanning.

theorem generate_from_pi_eq {ι : Type u_1} {α : ι → Type u_3} [fintype ι] {C : Π (i : ι), set (set (α i))} (hC : ∀ (i : ι), is_countably_spanning (C 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} [fintype ι] [h : Π (i : ι), measurable_space (α i)] {C : Π (i : ι), set (set (α i))} (hC : ∀ (i : ι), measurable_space.generate_from (C i) = h i) (h2C : ∀ (i : ι), is_countably_spanning (C 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} [fintype ι] [Π (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 : ι), measure_theory.outer_measure (α 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 : ι), measure_theory.outer_measure (α i)} {s : Π (i : ι), set (α i)} (hs : (set.univ.pi s).nonempty) :
measure_theory.pi_premeasure m (set.univ.pi s) = finset.univ.prod (λ (i : ι), (m i) (s i))
theorem measure_theory.pi_premeasure_pi' {ι : Type u_1} {α : ι → Type u_3} [fintype ι] {m : Π (i : ι), measure_theory.outer_measure (α i)} {s : Π (i : ι), set (α i)} :
measure_theory.pi_premeasure m (set.univ.pi s) = finset.univ.prod (λ (i : ι), (m i) (s i))
theorem measure_theory.pi_premeasure_pi_mono {ι : Type u_1} {α : ι → Type u_3} [fintype ι] {m : Π (i : ι), measure_theory.outer_measure (α 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 : ι), measure_theory.outer_measure (α i)} {s : set (Π (i : ι), α i)} :
@[protected]
noncomputable def measure_theory.outer_measure.pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] (m : Π (i : ι), measure_theory.outer_measure (α i)) :
measure_theory.outer_measure (Π (i : ι), α 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 : ι), measure_theory.outer_measure (α i)) (s : Π (i : ι), set (α i)) :
theorem measure_theory.outer_measure.le_pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] {m : Π (i : ι), measure_theory.outer_measure (α i)} {n : measure_theory.outer_measure (Π (i : ι), α i)} :
n measure_theory.outer_measure.pi m ∀ (s : Π (i : ι), set (α i)), (set.univ.pi s).nonemptyn (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 : δ), measure_theory.measure (π 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 : δ), measure_theory.measure (π i)) :
@[simp]
theorem measure_theory.measure.tprod_cons {δ : Type u_4} {π : δ → Type u_5} [Π (x : δ), measurable_space (π x)] (i : δ) (l : list δ) (μ : Π (i : δ), measure_theory.measure (π i)) :
@[protected, instance]
def measure_theory.measure.sigma_finite_tprod {δ : Type u_4} {π : δ → Type u_5} [Π (x : δ), measurable_space (π x)] (l : list δ) (μ : Π (i : δ), measure_theory.measure (π i)) [∀ (i : δ), measure_theory.sigma_finite (μ i)] :
theorem measure_theory.measure.tprod_tprod {δ : Type u_4} {π : δ → Type u_5} [Π (x : δ), measurable_space (π x)] (l : list δ) (μ : Π (i : δ), measure_theory.measure (π i)) [∀ (i : δ), measure_theory.sigma_finite (μ i)] (s : Π (i : δ), set (π i)) :
(measure_theory.measure.tprod l μ) (set.tprod l 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 : ι), measure_theory.measure (α 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 : ι), measure_theory.measure (α i)) [encodable ι] [∀ (i : ι), measure_theory.sigma_finite (μ i)] (s : Π (i : ι), set (α i)) :
(measure_theory.measure.pi' μ) (set.univ.pi s) = 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 : ι), measure_theory.measure (α i)) :
theorem measure_theory.measure.pi_pi_aux {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] (s : Π (i : ι), set (α i)) (hs : ∀ (i : ι), measurable_set (s i)) :
(measure_theory.measure.pi μ) (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 : ι), measure_theory.measure (α 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 : ι), measure_theory.measure (α i)} {C : Π (i : ι), set (set (α i))} (hC : ∀ (i : ι), measurable_space.generate_from (C i) = _inst_3 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ 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 : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] [encodable ι] :
@[simp]
theorem measure_theory.measure.pi_pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] (s : Π (i : ι), set (α i)) :
(measure_theory.measure.pi μ) (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 : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] :
theorem measure_theory.measure.pi_ball {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), metric_space (α i)] (x : Π (i : ι), α i) {r : } (hr : 0 < r) :
(measure_theory.measure.pi μ) (metric.ball x 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 : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), metric_space (α i)] (x : Π (i : ι), α i) {r : } (hr : 0 r) :
@[protected, instance]
def measure_theory.measure.pi.sigma_finite {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] :
theorem measure_theory.measure.pi_of_empty {α : Type u_1} [is_empty α] {β : α → Type u_2} {m : Π (a : α), measurable_space (β a)} (μ : Π (a : α), measure_theory.measure (β 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 : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] {i : ι} {s : set (α i)} (hs : (μ i) s = 0) :
theorem measure_theory.measure.pi_hyperplane {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] (i : ι) [measure_theory.has_no_atoms (μ i)] (x : α i) :
(measure_theory.measure.pi μ) {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 : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] (i : ι) [measure_theory.has_no_atoms (μ i)] (x : α i) :
∀ᵐ (y : Π (i : ι), α i)measure_theory.measure.pi μ, y i x
theorem measure_theory.measure.tendsto_eval_ae_ae {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] {i : ι} :
theorem measure_theory.measure.ae_pi_le_pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] :
(measure_theory.measure.pi μ).ae filter.pi (λ (i : ι), (μ i).ae)
theorem measure_theory.measure.ae_eq_pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] {β : ι → Type u_2} {f f' : Π (i : ι), α iβ i} (h : ∀ (i : ι), f i =ᵐ[μ i] f' i) :
(λ (x : Π (i : ι), α i) (i : ι), f i (x i)) =ᵐ[measure_theory.measure.pi μ] λ (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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ 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)) ≤ᵐ[measure_theory.measure.pi μ] λ (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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] {I : set ι} {s t : Π (i : ι), set (α i)} (h : ∀ (i : ι), i Is i ≤ᵐ[μ i] t i) :
theorem measure_theory.measure.ae_eq_set_pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] {I : set ι} {s t : Π (i : ι), set (α i)} (h : ∀ (i : ι), i Is i =ᵐ[μ i] t i) :
theorem measure_theory.measure.pi_Iio_ae_eq_pi_Iic {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {s : set ι} {f : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Iio (f i)) =ᵐ[measure_theory.measure.pi μ] 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {s : set ι} {f : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ioi (f i)) =ᵐ[measure_theory.measure.pi μ] 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {f : Π (i : ι), α i} :
theorem measure_theory.measure.univ_pi_Ioi_ae_eq_Ici {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {f : Π (i : ι), α i} :
theorem measure_theory.measure.pi_Ioo_ae_eq_pi_Icc {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {s : set ι} {f g : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ioo (f i) (g i)) =ᵐ[measure_theory.measure.pi μ] 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {s : set ι} {f g : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ioo (f i) (g i)) =ᵐ[measure_theory.measure.pi μ] 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {f g : Π (i : ι), α i} :
set.univ.pi (λ (i : ι), set.Ioo (f i) (g i)) =ᵐ[measure_theory.measure.pi μ] set.Icc f g
theorem measure_theory.measure.pi_Ioc_ae_eq_pi_Icc {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {s : set ι} {f g : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ioc (f i) (g i)) =ᵐ[measure_theory.measure.pi μ] 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {f g : Π (i : ι), α i} :
set.univ.pi (λ (i : ι), set.Ioc (f i) (g i)) =ᵐ[measure_theory.measure.pi μ] set.Icc f g
theorem measure_theory.measure.pi_Ico_ae_eq_pi_Icc {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {s : set ι} {f g : Π (i : ι), α i} :
s.pi (λ (i : ι), set.Ico (f i) (g i)) =ᵐ[measure_theory.measure.pi μ] 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), partial_order (α i)] [∀ (i : ι), measure_theory.has_no_atoms (μ i)] {f g : Π (i : ι), α i} :
set.univ.pi (λ (i : ι), set.Ico (f i) (g i)) =ᵐ[measure_theory.measure.pi μ] set.Icc f g
theorem measure_theory.measure.pi_has_no_atoms {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [h : nonempty ι] [∀ (i : ι), measure_theory.has_no_atoms (μ 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 : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), topological_space (α i)] [∀ (i : ι), measure_theory.is_locally_finite_measure (μ i)] :
@[protected, instance]
def measure_theory.measure.pi.is_add_left_invariant {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ 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 : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), group (α i)] [∀ (i : ι), has_measurable_mul (α i)] [∀ (i : ι), (μ i).is_mul_left_invariant] :
@[protected, instance]
def measure_theory.measure.pi.is_inv_invariant {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ 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 : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] [Π (i : ι), add_group (α i)] [∀ (i : ι), has_measurable_neg (α i)] [∀ (i : ι), (μ i).is_neg_invariant] :
@[protected, instance]
noncomputable def measure_theory.measure_space.pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measure_theory.measure_space (α i)] :
measure_theory.measure_space (Π (i : ι), α i)
Equations
theorem measure_theory.volume_pi_pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measure_theory.measure_space (α i)] [∀ (i : ι), measure_theory.sigma_finite measure_theory.measure_space.volume] (s : Π (i : ι), set (α i)) :
theorem measure_theory.volume_pi_ball {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measure_theory.measure_space (α i)] [∀ (i : ι), measure_theory.sigma_finite measure_theory.measure_space.volume] [Π (i : ι), metric_space (α i)] (x : Π (i : ι), α i) {r : } (hr : 0 < r) :
theorem measure_theory.volume_pi_closed_ball {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measure_theory.measure_space (α i)] [∀ (i : ι), measure_theory.sigma_finite measure_theory.measure_space.volume] [Π (i : ι), metric_space (α i)] (x : Π (i : ι), α i) {r : } (hr : 0 r) :
@[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 : ι), measure_theory.measure (α i)) [∀ (i : ι), measure_theory.sigma_finite (μ i)] (p : ι → Prop) [decidable_pred p] :
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)), measure_theory.measure (α i)) [∀ (i : fin (n + 1)), measure_theory.sigma_finite (μ i)] (i : fin (n + 1)) :