Products of finite measures and probability measures

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

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

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

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

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

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 ⋯ = μ

@[simp]

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

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

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

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