Composition-Product of a measure and a kernel

This operation, denoted by ⊗ₘ, takes μ : Measure α and κ : Kernel α β and creates μ ⊗ₘ κ : Measure (α × β). The integral of a function against μ ⊗ₘ κ is ∫⁻ x, f x ∂(μ ⊗ₘ κ) = ∫⁻ a, ∫⁻ b, f (a, b) ∂(κ a) ∂μ.

μ ⊗ₘ κ is defined as ((Kernel.const Unit μ) ⊗ₖ (Kernel.prodMkLeft Unit κ)) ().

Main definitions

• Measure.compProd: from μ : Measure α and κ : Kernel α β, get a Measure (α × β).

Notations

• μ ⊗ₘ κ = μ.compProd κ

noncomputable def MeasureTheory.Measure.compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α β) : MeasureTheory.Measure (α × β)

The composition-product of a measure and a kernel.

Equations

• μ.compProd κ = ((ProbabilityTheory.Kernel.const Unit μ).compProd (ProbabilityTheory.Kernel.prodMkLeft Unit κ)) ()

def ProbabilityTheory.«term_⊗ₘ_» : Lean.TrailingParserDescr

The composition-product of a measure and a kernel.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.compProd_of_not_sfinite {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α β) (h : ¬MeasureTheory.SFinite μ) : μ.compProd κ = 0

theorem MeasureTheory.Measure.compProd_of_not_isSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α β) (h : ¬ProbabilityTheory.IsSFiniteKernel κ) : μ.compProd κ = 0

@[simp]

theorem MeasureTheory.Measure.compProd_zero_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) : MeasureTheory.Measure.compProd 0 κ = 0

@[simp]

theorem MeasureTheory.Measure.compProd_zero_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) : μ.compProd 0 = 0

theorem MeasureTheory.Measure.compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {s : Set (α × β)} (hs : MeasurableSet s) : (μ.compProd κ) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ

theorem MeasureTheory.Measure.compProd_apply_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) : (μ.compProd κ) (s ×ˢ t) = ∫⁻ (a : α) in s, (κ a) t ∂μ

theorem MeasureTheory.Measure.compProd_congr {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ η : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] (h : ⇑κ =ᵐ[μ] ⇑η) : μ.compProd κ = μ.compProd η

theorem MeasureTheory.Measure.ae_compProd_of_ae_ae {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {p : α × β → Prop} (hp : MeasurableSet {x : α × β | p x}) (h : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)) : ∀ᵐ (x : α × β) ∂μ.compProd κ, p x

theorem MeasureTheory.Measure.ae_ae_of_ae_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {p : α × β → Prop} (h : ∀ᵐ (x : α × β) ∂μ.compProd κ, p x) : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)

theorem MeasureTheory.Measure.ae_compProd_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {p : α × β → Prop} (hp : MeasurableSet {x : α × β | p x}) : (∀ᵐ (x : α × β) ∂μ.compProd κ, p x) ↔ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)

theorem MeasureTheory.Measure.compProd_add_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (κ : ProbabilityTheory.Kernel α β) : (μ + ν).compProd κ = μ.compProd κ + ν.compProd κ

theorem MeasureTheory.Measure.compProd_add_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) (κ η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] : μ.compProd (κ + η) = μ.compProd κ + μ.compProd η

theorem MeasureTheory.Measure.lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {f : α × β → ENNReal} (hf : Measurable f) : ∫⁻ (x : α × β), f x ∂μ.compProd κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ

theorem MeasureTheory.Measure.setLIntegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {f : α × β → ENNReal} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ.compProd κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ

@[deprecated MeasureTheory.Measure.setLIntegral_compProd]

theorem MeasureTheory.Measure.set_lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {f : α × β → ENNReal} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ.compProd κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ

Alias of MeasureTheory.Measure.setLIntegral_compProd.

theorem MeasureTheory.Measure.integrable_compProd_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {E : Type u_3} [NormedAddCommGroup E] {f : α × β → E} (hf : MeasureTheory.AEStronglyMeasurable f (μ.compProd κ)) : MeasureTheory.Integrable f (μ.compProd κ) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (y : β) => f (x, y)) (κ x)) ∧ MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ

theorem MeasureTheory.Measure.integral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α × β → E} (hf : MeasureTheory.Integrable f (μ.compProd κ)) : ∫ (x : α × β), f x ∂μ.compProd κ = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ

theorem MeasureTheory.Measure.setIntegral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) {f : α × β → E} (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.compProd κ)) : ∫ (x : α × β) in s ×ˢ t, f x ∂μ.compProd κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

@[deprecated MeasureTheory.Measure.setIntegral_compProd]

theorem MeasureTheory.Measure.set_integral_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) {f : α × β → E} (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.compProd κ)) : ∫ (x : α × β) in s ×ˢ t, f x ∂μ.compProd κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Alias of MeasureTheory.Measure.setIntegral_compProd.

theorem MeasureTheory.Measure.dirac_compProd_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [MeasurableSingletonClass α] {a : α} [ProbabilityTheory.IsSFiniteKernel κ] {s : Set (α × β)} (hs : MeasurableSet s) : ((MeasureTheory.Measure.dirac a).compProd κ) s = (κ a) (Prod.mk a ⁻¹' s)

theorem MeasureTheory.Measure.dirac_unit_compProd {β : Type u_2} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel Unit β) [ProbabilityTheory.IsSFiniteKernel κ] : (MeasureTheory.Measure.dirac ()).compProd κ = MeasureTheory.Measure.map (Prod.mk ()) (κ ())

theorem MeasureTheory.Measure.dirac_unit_compProd_const {β : Type u_2} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure μ] : (MeasureTheory.Measure.dirac ()).compProd (ProbabilityTheory.Kernel.const Unit μ) = MeasureTheory.Measure.map (Prod.mk ()) μ

@[simp]

theorem MeasureTheory.Measure.snd_dirac_unit_compProd_const {β : Type u_2} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure μ] : ((MeasureTheory.Measure.dirac ()).compProd (ProbabilityTheory.Kernel.const Unit μ)).snd = μ

instance MeasureTheory.Measure.instSFiniteProdCompProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} : MeasureTheory.SFinite (μ.compProd κ)

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] : MeasureTheory.IsFiniteMeasure (μ.compProd κ)

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.instIsProbabilityMeasureProdCompProdOfIsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.IsProbabilityMeasure (μ.compProd κ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.Measure.absolutelyContinuous_compProd_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SFinite ν] (hμν : μ.AbsolutelyContinuous ν) (κ : ProbabilityTheory.Kernel α β) : (μ.compProd κ).AbsolutelyContinuous (ν.compProd κ)

theorem MeasureTheory.Measure.absolutelyContinuous_compProd_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel η] (hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)

theorem MeasureTheory.Measure.absolutelyContinuous_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite ν] [ProbabilityTheory.IsSFiniteKernel η] (hμν : μ.AbsolutelyContinuous ν) (hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η)

theorem MeasureTheory.Measure.absolutelyContinuous_of_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] [h_zero : ∀ (a : α), NeZero (κ a)] (h : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η)) : μ.AbsolutelyContinuous ν