mathlib documentation

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

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.prod t for sets s : set α and t : set β.

@[simp]
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) = ∏ (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)} [nonempty ι] {s : Π (i : ι), set (α i)} :
measure_theory.pi_premeasure m (set.univ.pi s) = ∏ (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)} [nonempty ι] {s : set (Π (i : ι), α i)} :
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)) :
(measure_theory.outer_measure.pi m) (set.univ.pi s) ∏ (i : ι), (m i) (s 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) ∏ (i : ι), (m i) (s i)
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
@[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)) :
@[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)} (hs : ∀ (i : δ), measurable_set (s i)) :
(measure_theory.measure.tprod l μ) (set.tprod l s) = (list.map (λ (i : δ), (μ i) (s i)) l).prod
theorem measure_theory.measure.tprod_tprod_le {δ : 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
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)} (hs : ∀ (i : ι), measurable_set (s i)) :
(measure_theory.measure.pi' μ) (set.univ.pi s) = ∏ (i : ι), (μ i) (s i)
theorem measure_theory.measure.pi'_pi_le {ι : 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) ∏ (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)) :
def measure_theory.measure.pi {ι : Type u_1} {α : ι → Type u_3} [fintype ι] [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α 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
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)) (hs : ∀ (i : ι), measurable_set (s i)) :
(measure_theory.measure.pi μ) (set.univ.pi s) = ∏ (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)) (hC : ∀ (i : ι) (s : set (α i)), s C imeasurable_set s) :

μ.prod ν 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) = ∏ (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) = ∏ (i : ι), (μ i) (s i)) :

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

@[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_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_infi_comap {ι : 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.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.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.

@[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)] :
@[instance]
def measure_theory.measure.pi.measure_theory.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 : ι), opens_measurable_space (α i)] [∀ (i : ι), measure_theory.locally_finite_measure (μ i)] :
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)) (hs : ∀ (i : ι), measurable_set (s i)) :