Products of finite measures and probability measures

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

The binary product of finite measures.

Equations

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

@[simp]

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

theorem MeasureTheory.FiniteMeasure.prod_apply {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : FiniteMeasure α) (ν : FiniteMeasure β) (s : Set (α × β)) (s_mble : MeasurableSet s) : (μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal

theorem MeasureTheory.FiniteMeasure.prod_apply_symm {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : FiniteMeasure α) (ν : FiniteMeasure β) (s : Set (α × β)) (s_mble : MeasurableSet s) : (μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun (x : α) => (x, y)) ⁻¹' s) ∂↑ν).toNNReal

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

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

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

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

@[simp]

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

@[simp]

theorem MeasureTheory.FiniteMeasure.map_snd_prod {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : FiniteMeasure α) (ν : FiniteMeasure β) : (μ.prod ν).map Prod.snd = μ Set.univ • ν

theorem MeasureTheory.FiniteMeasure.map_prod_map {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : FiniteMeasure α) (ν : 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_apply_null {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : FiniteMeasure α) (ν : FiniteMeasure β) {s : Set (α × β)} (hs : MeasurableSet s) : (μ.prod ν) s = 0 ↔ (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae ↑μ] 0

theorem MeasureTheory.FiniteMeasure.measure_ae_null_of_prod_null {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : FiniteMeasure α) (ν : FiniteMeasure β) {s : Set (α × β)} (h : (μ.prod ν) s = 0) : (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae ↑μ] 0

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

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

The binary product of probability measures.

Equations

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

@[simp]

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

theorem MeasureTheory.ProbabilityMeasure.prod_apply {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : ProbabilityMeasure α) (ν : ProbabilityMeasure β) (s : Set (α × β)) (s_mble : MeasurableSet s) : (μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal

theorem MeasureTheory.ProbabilityMeasure.prod_apply_symm {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : ProbabilityMeasure α) (ν : ProbabilityMeasure β) (s : Set (α × β)) (s_mble : MeasurableSet s) : (μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun (x : α) => (x, y)) ⁻¹' s) ∂↑ν).toNNReal

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

@[simp]

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

@[simp]

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

theorem MeasureTheory.ProbabilityMeasure.map_prodMap {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : ProbabilityMeasure α) (ν : 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_apply_null {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : ProbabilityMeasure α) (ν : ProbabilityMeasure β) {s : Set (α × β)} (hs : MeasurableSet s) : (μ.prod ν) s = 0 ↔ (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae ↑μ] 0

theorem MeasureTheory.ProbabilityMeasure.measure_ae_null_of_prod_null {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (μ : ProbabilityMeasure α) (ν : ProbabilityMeasure β) {s : Set (α × β)} (h : (μ.prod ν) s = 0) : (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae ↑μ] 0

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