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

@[simp]
def measure_theory.pi_premeasure {ι : Type u_1} [fintype ι] {α : ι → Type u_2} (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} [fintype ι] {α : ι → Type u_2} {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} [fintype ι] {α : ι → Type u_2} {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} [fintype ι] {α : ι → Type u_2} {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} [fintype ι] {α : ι → Type u_2} {m : Π (i : ι), measure_theory.outer_measure (α i)} [nonempty ι] {s : set (Π (i : ι), α i)} :
def measure_theory.outer_measure.pi {ι : Type u_1} [fintype ι] {α : ι → Type u_2} (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} [fintype ι] {α : ι → Type u_2} (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} [fintype ι] {α : ι → Type u_2} {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_3} {π : δ → Type u_4} [Π (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_3} {π : δ → Type u_4} [Π (x : δ), measurable_space («π» x)] (μ : Π (i : δ), measure_theory.measure («π» i)) :
@[simp]
theorem measure_theory.measure.tprod_cons {δ : Type u_3} {π : δ → Type u_4} [Π (x : δ), measurable_space («π» x)] (i : δ) (l : list δ) (μ : Π (i : δ), measure_theory.measure («π» i)) :
@[instance]
def measure_theory.measure.sigma_finite_tprod {δ : Type u_3} {π : δ → Type u_4} [Π (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_3} {π : δ → Type u_4} [Π (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_3} {π : δ → Type u_4} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (i : ι), measurable_space (α i)] (μ : Π (i : ι), measure_theory.measure (α i)) :
def measure_theory.measure.pi {ι : Type u_1} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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)
theorem measure_theory.measure.pi_eval_preimage_null {ι : Type u_1} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] {β : ι → Type u_3} {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} [fintype ι] {α : ι → Type u_2} [Π (i : ι), measurable_space (α i)] {μ : Π (i : ι), measure_theory.measure (α i)} [∀ (i : ι), measure_theory.sigma_finite (μ i)] {β : ι → Type u_3} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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} [fintype ι] {α : ι → Type u_2} [Π (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)) :