Products of finite measures and probability measures #
This file introduces binary products of finite measures and probability measures. The constructions are obtained from special cases of products of general measures. Taking products nevertheless has specific properties in the cases of finite measures and probability measures, notably the fact that the product measures depend continuously on their factors in the topology of weak convergence when the underlying space is metrizable and separable.
Main definitions #
MeasureTheory.FiniteMeasure.prod: The product of two finite measures.MeasureTheory.ProbabilityMeasure.prod: The product of two probability measures.
Todo #
- Add continuous dependence of the product measures on the factors.
noncomputable def
MeasureTheory.FiniteMeasure.prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
:
MeasureTheory.FiniteMeasure (α × β)
The binary product of finite measures.
Equations
- MeasureTheory.FiniteMeasure.prod μ ν = { val := MeasureTheory.Measure.prod ↑μ ↑ν, property := (_ : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.prod ↑μ ↑ν)) }
Instances For
@[simp]
theorem
MeasureTheory.FiniteMeasure.toMeasure_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
:
↑(MeasureTheory.FiniteMeasure.prod μ ν) = MeasureTheory.Measure.prod ↑μ ↑ν
theorem
MeasureTheory.FiniteMeasure.prod_apply
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
(s : Set (α × β))
(s_mble : MeasurableSet s)
:
(fun (s : Set (α × β)) => ENNReal.toNNReal (↑↑↑(MeasureTheory.FiniteMeasure.prod μ ν) s)) s = ENNReal.toNNReal (∫⁻ (x : α), ↑↑↑ν (Prod.mk x ⁻¹' s) ∂↑μ)
theorem
MeasureTheory.FiniteMeasure.prod_apply_symm
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
(s : Set (α × β))
(s_mble : MeasurableSet s)
:
(fun (s : Set (α × β)) => ENNReal.toNNReal (↑↑↑(MeasureTheory.FiniteMeasure.prod μ ν) s)) s = ENNReal.toNNReal (∫⁻ (y : β), ↑↑↑μ ((fun (x : α) => (x, y)) ⁻¹' s) ∂↑ν)
theorem
MeasureTheory.FiniteMeasure.prod_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
(s : Set α)
(t : Set β)
:
(fun (s : Set (α × β)) => ENNReal.toNNReal (↑↑↑(MeasureTheory.FiniteMeasure.prod μ ν) s)) (s ×ˢ t) = (fun (s : Set α) => ENNReal.toNNReal (↑↑↑μ s)) s * (fun (s : Set β) => ENNReal.toNNReal (↑↑↑ν s)) t
@[simp]
theorem
MeasureTheory.FiniteMeasure.mass_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
:
@[simp]
theorem
MeasureTheory.FiniteMeasure.zero_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(ν : MeasureTheory.FiniteMeasure β)
:
@[simp]
theorem
MeasureTheory.FiniteMeasure.prod_zero
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
:
@[simp]
theorem
MeasureTheory.FiniteMeasure.map_fst_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
:
MeasureTheory.FiniteMeasure.map (MeasureTheory.FiniteMeasure.prod μ ν) Prod.fst = (fun (s : Set β) => ENNReal.toNNReal (↑↑↑ν s)) Set.univ • μ
@[simp]
theorem
MeasureTheory.FiniteMeasure.map_snd_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
:
MeasureTheory.FiniteMeasure.map (MeasureTheory.FiniteMeasure.prod μ ν) Prod.snd = (fun (s : Set α) => ENNReal.toNNReal (↑↑↑μ s)) Set.univ • ν
theorem
MeasureTheory.FiniteMeasure.map_prod_map
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
{α' : Type u_3}
[MeasurableSpace α']
{β' : Type u_4}
[MeasurableSpace β']
{f : α → α'}
{g : β → β'}
(f_mble : Measurable f)
(g_mble : Measurable g)
:
theorem
MeasureTheory.FiniteMeasure.prod_swap
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.FiniteMeasure α)
(ν : MeasureTheory.FiniteMeasure β)
:
noncomputable def
MeasureTheory.ProbabilityMeasure.prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
:
The binary product of probability measures.
Equations
- MeasureTheory.ProbabilityMeasure.prod μ ν = { val := MeasureTheory.Measure.prod ↑μ ↑ν, property := (_ : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.prod ↑μ ↑ν)) }
Instances For
@[simp]
theorem
MeasureTheory.ProbabilityMeasure.toMeasure_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
:
theorem
MeasureTheory.ProbabilityMeasure.prod_apply
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
(s : Set (α × β))
(s_mble : MeasurableSet s)
:
(fun (s : Set (α × β)) => ENNReal.toNNReal (↑↑↑(MeasureTheory.ProbabilityMeasure.prod μ ν) s)) s = ENNReal.toNNReal (∫⁻ (x : α), ↑↑↑ν (Prod.mk x ⁻¹' s) ∂↑μ)
theorem
MeasureTheory.ProbabilityMeasure.prod_apply_symm
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
(s : Set (α × β))
(s_mble : MeasurableSet s)
:
(fun (s : Set (α × β)) => ENNReal.toNNReal (↑↑↑(MeasureTheory.ProbabilityMeasure.prod μ ν) s)) s = ENNReal.toNNReal (∫⁻ (y : β), ↑↑↑μ ((fun (x : α) => (x, y)) ⁻¹' s) ∂↑ν)
theorem
MeasureTheory.ProbabilityMeasure.prod_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
(s : Set α)
(t : Set β)
:
(fun (s : Set (α × β)) => ENNReal.toNNReal (↑↑↑(MeasureTheory.ProbabilityMeasure.prod μ ν) s)) (s ×ˢ t) = (fun (s : Set α) => ENNReal.toNNReal (↑↑↑μ s)) s * (fun (s : Set β) => ENNReal.toNNReal (↑↑↑ν s)) t
@[simp]
theorem
MeasureTheory.ProbabilityMeasure.map_fst_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
:
MeasureTheory.ProbabilityMeasure.map (MeasureTheory.ProbabilityMeasure.prod μ ν) (_ : AEMeasurable Prod.fst) = μ
The first marginal of a product probability measure is the first probability measure.
@[simp]
theorem
MeasureTheory.ProbabilityMeasure.map_snd_prod
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
:
MeasureTheory.ProbabilityMeasure.map (MeasureTheory.ProbabilityMeasure.prod μ ν) (_ : AEMeasurable Prod.snd) = ν
The second marginal of a product probability measure is the second probability measure.
theorem
MeasureTheory.ProbabilityMeasure.map_prod_map
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
{α' : Type u_3}
[MeasurableSpace α']
{β' : Type u_4}
[MeasurableSpace β']
{f : α → α'}
{g : β → β'}
(f_mble : Measurable f)
(g_mble : Measurable g)
:
theorem
MeasureTheory.ProbabilityMeasure.prod_swap
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_2}
[MeasurableSpace β]
(μ : MeasureTheory.ProbabilityMeasure α)
(ν : MeasureTheory.ProbabilityMeasure β)
: