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

• μ.prod ν = ⟨(↑μ).prod ↑ν, ⋯⟩

@[simp]

theorem MeasureTheory.FiniteMeasure.toMeasure_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) : ↑(μ.prod ν) = (↑μ).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 (α × β)) => (↑↑↑(μ.prod ν) s).toNNReal) s = (∫⁻ (x : α), ↑↑↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal

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 (α × β)) => (↑↑↑(μ.prod ν) s).toNNReal) s = (∫⁻ (y : β), ↑↑↑μ ((fun (x : α) => (x, y)) ⁻¹' s) ∂↑ν).toNNReal

theorem MeasureTheory.FiniteMeasure.prod_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) (s : Set α) (t : Set β) : (fun (s : Set (α × β)) => (↑↑↑(μ.prod ν) s).toNNReal) (s ×ˢ t) = (fun (s : Set α) => (↑↑↑μ s).toNNReal) s * (fun (s : Set β) => (↑↑↑ν s).toNNReal) t

@[simp]

theorem MeasureTheory.FiniteMeasure.mass_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) : (μ.prod ν).mass = μ.mass * ν.mass

@[simp]

theorem MeasureTheory.FiniteMeasure.zero_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (ν : MeasureTheory.FiniteMeasure β) : MeasureTheory.FiniteMeasure.prod 0 ν = 0

@[simp]

theorem MeasureTheory.FiniteMeasure.prod_zero {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) : μ.prod 0 = 0

@[simp]

theorem MeasureTheory.FiniteMeasure.map_fst_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) : (μ.prod ν).map Prod.fst = (fun (s : Set β) => (↑↑↑ν s).toNNReal) Set.univ • μ

@[simp]

theorem MeasureTheory.FiniteMeasure.map_snd_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) : (μ.prod ν).map Prod.snd = (fun (s : Set α) => (↑↑↑μ s).toNNReal) 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) : (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g)

theorem MeasureTheory.FiniteMeasure.prod_swap {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) : (μ.prod ν).map Prod.swap = ν.prod μ

noncomputable def MeasureTheory.ProbabilityMeasure.prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) : MeasureTheory.ProbabilityMeasure (α × β)

The binary product of probability measures.

Equations

• μ.prod ν = ⟨(↑μ).prod ↑ν, ⋯⟩

@[simp]

theorem MeasureTheory.ProbabilityMeasure.toMeasure_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) : ↑(μ.prod ν) = (↑μ).prod ↑ν

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 (α × β)) => (↑↑↑(μ.prod ν) s).toNNReal) s = (∫⁻ (x : α), ↑↑↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal

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 (α × β)) => (↑↑↑(μ.prod ν) s).toNNReal) s = (∫⁻ (y : β), ↑↑↑μ ((fun (x : α) => (x, y)) ⁻¹' s) ∂↑ν).toNNReal

theorem MeasureTheory.ProbabilityMeasure.prod_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) (s : Set α) (t : Set β) : (fun (s : Set (α × β)) => (↑↑↑(μ.prod ν) s).toNNReal) (s ×ˢ t) = (fun (s : Set α) => (↑↑↑μ s).toNNReal) s * (fun (s : Set β) => (↑↑↑ν s).toNNReal) t

@[simp]

theorem MeasureTheory.ProbabilityMeasure.map_fst_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) : (μ.prod ν).map ⋯ = μ

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 β) : (μ.prod ν).map ⋯ = ν

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) : (μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯

theorem MeasureTheory.ProbabilityMeasure.prod_swap {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) : (μ.prod ν).map ⋯ = ν.prod μ