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 #
measure_theory.measure.pi: The product of finitely many σ-finite measures. Givenμ : Π i : ι, measure (α i)for[fintype ι]it has typemeasure (Π i : ι, α i).
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[encodable ι]. - Using this, we have an equivalence
measurable_equiv.pi_measurable_equiv_tprodbetweenΠ ι, α iand an iterated product ofα i, calledlist.tprod α lfor some listl. - On this iterated product we can easily define a product measure
measure_theory.measure.tprodby iteratingmeasure_theory.measure.prod - Using the previous two steps we construct
measure_theory.measure.pi'onΠ ι, α ifor encodableι. - We know that
measure_theory.measure.pi'sends products of sets to products of measures, and sincemeasure_theory.measure.piis 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 formeasure_theory.measure.pi.
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)] :
measurable_space.generate_from (set.univ.pi '' set.univ.pi (λ (i : ι), {s : set (α i) | measurable_set s})) = measurable_space.pi
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
- measure_theory.pi_premeasure m s = ∏ (i : ι), ⇑(m i) (function.eval i '' s)
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)} :
measure_theory.pi_premeasure m (set.univ.pi (λ (i : ι), function.eval i '' s)) = measure_theory.pi_premeasure m s
@[protected]
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 : ι}.
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)} :
@[protected]
def
measure_theory.measure.tprod
{δ : Type u_4}
{π : δ → Type u_5}
[Π (x : δ), measurable_space («π» x)]
(l : list δ)
(μ : Π (i : δ), measure_theory.measure («π» i)) :
measure_theory.measure (list.tprod «π» l)
A product of measures in tprod α l.
Equations
- measure_theory.measure.tprod l μ = list.rec (measure_theory.measure.dirac punit.star) (λ (i : δ) (l : list δ) (ih : measure_theory.measure (list.tprod «π» l)), (μ i).prod ih) l
@[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)) :
measure_theory.measure.tprod (i :: l) μ = (μ i).prod (measure_theory.measure.tprod l μ)
@[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)}
(hs : ∀ (i : δ), measurable_set (s i)) :
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)) :
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.
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)) :
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)} :
theorem
measure_theory.measure.pi_caratheodory
{ι : Type u_1}
{α : ι → Type u_3}
[fintype ι]
[Π (i : ι), measurable_space (α i)]
(μ : Π (i : ι), measure_theory.measure (α i)) :
measurable_space.pi ≤ (measure_theory.outer_measure.pi (λ (i : ι), (μ i).to_outer_measure)).caratheodory
@[protected]
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
- measure_theory.measure.pi μ = (measure_theory.outer_measure.pi (λ (i : ι), (μ i).to_outer_measure)).to_measure _
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)) :
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 i → measurable_set s) :
μ.prod ν has finite spanning sets in rectangles of finite spanning sets.
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.
@[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_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) :
⇑(measure_theory.measure.pi μ) (function.eval 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 : ι} :
filter.tendsto (function.eval i) (measure_theory.measure.pi μ).ae (μ i).ae
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)] :
(measure_theory.measure.pi μ).ae ≤ ⨅ (i : ι), filter.comap (function.eval 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 ∈ I → s i ≤ᵐ[μ i] t i) :
I.pi s ≤ᵐ[measure_theory.measure.pi μ] I.pi t
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 ∈ I → s i =ᵐ[μ i] t i) :
I.pi s =ᵐ[measure_theory.measure.pi μ] 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 : ι), 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} :
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} :
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} :
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} :
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} :
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} :
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} :
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} :
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.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)] :
@[protected, instance]
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
{ι : Type u_1}
{α : ι → Type u_3}
[fintype ι]
[Π (i : ι), measure_theory.measure_space (α 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)) :
⇑measure_theory.measure_space.volume (set.univ.pi s) = ∏ (i : ι), ⇑measure_theory.measure_space.volume (s i)