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) ∂μ

@[simp]

theorem MeasureTheory.Measure.compProd_apply_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsMarkovKernel κ] : (μ.compProd κ) Set.univ = μ Set.univ

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)

@[simp]

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

The composition product of a measure and a constant kernel is the product between the two measures.

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 η

@[simp]

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

theorem MeasureTheory.Measure.compProd_smul_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} (a : ENNReal) [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] : (a • μ).compProd κ = a • μ.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 ()) μ

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 κ)

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 κ)

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 κ)

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 κ)

@[deprecated MeasureTheory.Measure.AbsolutelyContinuous.compProd_left]

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 κ)

Alias of MeasureTheory.Measure.AbsolutelyContinuous.compProd_left.

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 η)

@[deprecated MeasureTheory.Measure.AbsolutelyContinuous.compProd_right]

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 η)

Alias of MeasureTheory.Measure.AbsolutelyContinuous.compProd_right.

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 η)

@[deprecated MeasureTheory.Measure.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 η)

Alias of MeasureTheory.Measure.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 ν

theorem MeasureTheory.Measure.absolutelyContinuous_compProd_left_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [ProbabilityTheory.IsFiniteKernel κ] [∀ (a : α), NeZero (κ a)] : (μ.compProd κ).AbsolutelyContinuous (ν.compProd κ) ↔ μ.AbsolutelyContinuous ν

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

theorem MeasureTheory.Measure.MutuallySingular.compProd_of_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} (hμν : μ.MutuallySingular ν) (κ η : ProbabilityTheory.Kernel α β) : (μ.compProd κ).MutuallySingular (ν.compProd η)

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

theorem MeasureTheory.Measure.mutuallySingular_compProd_left_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [MeasureTheory.SigmaFinite ν] [ProbabilityTheory.IsSFiniteKernel κ] [hκ : ∀ (x : α), NeZero (κ x)] : (μ.compProd κ).MutuallySingular (ν.compProd κ) ↔ μ.MutuallySingular ν

theorem MeasureTheory.Measure.AbsolutelyContinuous.mutuallySingular_compProd_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) : (μ.compProd κ).MutuallySingular (ν.compProd η) ↔ (μ.compProd κ).MutuallySingular (μ.compProd η)

theorem MeasureTheory.Measure.mutuallySingular_compProd_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : (μ.compProd κ).MutuallySingular (ν.compProd η) ↔ ∀ (ξ : MeasureTheory.Measure α), MeasureTheory.SFinite ξ → ξ.AbsolutelyContinuous μ → ξ.AbsolutelyContinuous ν → (ξ.compProd κ).MutuallySingular (ξ.compProd η)

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

theorem MeasureTheory.Measure.absolutelyContinuous_compProd_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] [∀ (x : α), NeZero (κ x)] : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) ↔ μ.AbsolutelyContinuous ν ∧ (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)