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 aMeasure (α × β).
Notations #
μ ⊗ₘ κ = μ.compProd κ
noncomputable def
MeasureTheory.Measure.compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
(κ : ProbabilityTheory.Kernel α β)
:
The composition-product of a measure and a kernel.
Equations
- μ.compProd κ = ((ProbabilityTheory.Kernel.const Unit μ).compProd (ProbabilityTheory.Kernel.prodMkLeft Unit κ)) ()
Instances For
The composition-product of a measure and a kernel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.Measure.compProd_of_not_sfinite
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
(κ : ProbabilityTheory.Kernel α β)
(h : ¬SFinite μ)
:
μ.compProd κ = 0
theorem
MeasureTheory.Measure.compProd_of_not_isSFiniteKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : 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 α β)
:
@[simp]
theorem
MeasureTheory.Measure.compProd_zero_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
:
μ.compProd 0 = 0
theorem
MeasureTheory.Measure.compProd_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{s : Set (α × β)}
(hs : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.Measure.compProd_apply_univ
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsMarkovKernel κ]
:
theorem
MeasureTheory.Measure.compProd_apply_prod
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{s : Set α}
{t : Set β}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{γ : Type u_3}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
(a : α)
:
(κ.compProd η) a = (κ a).compProd (η.sectR a)
theorem
MeasureTheory.Measure.compProd_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(h : ⇑κ =ᶠ[ae μ] ⇑η)
:
μ.compProd κ = μ.compProd η
theorem
MeasureTheory.Measure.ae_compProd_of_ae_ae
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{p : α × β → Prop}
(hp : MeasurableSet {x : α × β | p x})
(h : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b))
:
theorem
MeasureTheory.Measure.ae_ae_of_ae_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{p : α × β → Prop}
(h : ∀ᵐ (x : α × β) ∂μ.compProd κ, p x)
:
theorem
MeasureTheory.Measure.ae_compProd_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{p : α × β → Prop}
(hp : MeasurableSet {x : α × β | p x})
:
@[simp]
theorem
MeasureTheory.Measure.compProd_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{ν : Measure β}
[SFinite μ]
[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 β}
(μ ν : Measure α)
[SFinite μ]
[SFinite ν]
(κ : ProbabilityTheory.Kernel α β)
:
theorem
MeasureTheory.Measure.compProd_add_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
(κ η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
@[simp]
theorem
MeasureTheory.Measure.fst_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
[SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
:
(μ.compProd κ).fst = μ
theorem
MeasureTheory.Measure.compProd_smul_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
(a : ENNReal)
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
:
theorem
MeasureTheory.Measure.lintegral_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α × β → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.Measure.setLIntegral_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α × β → ENNReal}
(hf : Measurable f)
{s : Set α}
(hs : MeasurableSet s)
{t : Set β}
(ht : MeasurableSet t)
:
@[deprecated MeasureTheory.Measure.setLIntegral_compProd (since := "2024-06-29")]
theorem
MeasureTheory.Measure.set_lintegral_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α × β → ENNReal}
(hf : Measurable f)
{s : Set α}
(hs : MeasurableSet s)
{t : Set β}
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.integrable_compProd_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{E : Type u_3}
[NormedAddCommGroup E]
{f : α × β → E}
(hf : AEStronglyMeasurable f (μ.compProd κ))
:
Integrable f (μ.compProd κ) ↔ (∀ᵐ (x : α) ∂μ, Integrable (fun (y : β) => f (x, y)) (κ x)) ∧ Integrable (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
theorem
MeasureTheory.Measure.integral_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α × β → E}
(hf : Integrable f (μ.compProd κ))
:
theorem
MeasureTheory.Measure.setIntegral_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set α}
(hs : MeasurableSet s)
{t : Set β}
(ht : MeasurableSet t)
{f : α × β → E}
(hf : IntegrableOn f (s ×ˢ t) (μ.compProd κ))
:
@[deprecated MeasureTheory.Measure.setIntegral_compProd (since := "2024-04-17")]
theorem
MeasureTheory.Measure.set_integral_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{s : Set α}
(hs : MeasurableSet s)
{t : Set β}
(ht : MeasurableSet t)
{f : α × β → E}
(hf : IntegrableOn f (s ×ˢ t) (μ.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)
:
theorem
MeasureTheory.Measure.dirac_unit_compProd
{β : Type u_2}
{mβ : MeasurableSpace β}
(κ : ProbabilityTheory.Kernel Unit β)
[ProbabilityTheory.IsSFiniteKernel κ]
:
theorem
MeasureTheory.Measure.dirac_unit_compProd_const
{β : Type u_2}
{mβ : MeasurableSpace β}
(μ : Measure β)
[IsFiniteMeasure μ]
:
theorem
MeasureTheory.Measure.snd_dirac_unit_compProd_const
{β : Type u_2}
{mβ : MeasurableSpace β}
(μ : Measure β)
[IsFiniteMeasure μ]
:
((dirac ()).compProd (ProbabilityTheory.Kernel.const Unit μ)).snd = μ
instance
MeasureTheory.Measure.instSFiniteProdCompProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
:
SFinite (μ.compProd κ)
instance
MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
IsFiniteMeasure (μ.compProd κ)
instance
MeasureTheory.Measure.instIsProbabilityMeasureProdCompProdOfIsMarkovKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
:
IsProbabilityMeasure (μ.compProd κ)
theorem
MeasureTheory.Measure.AbsolutelyContinuous.compProd_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
[SFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
(κ : ProbabilityTheory.Kernel α β)
:
(μ.compProd κ).AbsolutelyContinuous (ν.compProd κ)
@[deprecated MeasureTheory.Measure.AbsolutelyContinuous.compProd_left (since := "2024-12-11")]
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
[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 β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel η]
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
(μ.compProd κ).AbsolutelyContinuous (μ.compProd η)
@[deprecated MeasureTheory.Measure.AbsolutelyContinuous.compProd_right (since := "2024-12-11")]
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[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 β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SFinite ν]
[ProbabilityTheory.IsSFiniteKernel η]
(hμν : μ.AbsolutelyContinuous ν)
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
(μ.compProd κ).AbsolutelyContinuous (ν.compProd η)
@[deprecated MeasureTheory.Measure.AbsolutelyContinuous.compProd (since := "2024-12-11")]
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[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 β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[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 β}
{μ ν : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[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 β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[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 β}
{μ ν : 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 β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
{ξ : Measure α}
[SFinite μ]
[SFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(h : (μ.compProd κ).MutuallySingular (ν.compProd η))
(hμ : ξ.AbsolutelyContinuous μ)
(hν : ξ.AbsolutelyContinuous ν)
:
theorem
MeasureTheory.Measure.mutuallySingular_compProd_left_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[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 β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SigmaFinite μ]
[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 β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SigmaFinite μ]
[SigmaFinite ν]
:
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_of_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SigmaFinite μ]
[SigmaFinite ν]
(hκη : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
:
(μ.compProd κ).AbsolutelyContinuous (μ.compProd η)
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SigmaFinite μ]
[SigmaFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
[∀ (x : α), NeZero (κ x)]
: