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 β}
(μ : 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 κ)) ()
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 β}
(μ : 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 α β)
:
@[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)
:
@[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)
:
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})
:
@[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 α β)
:
theorem
MeasureTheory.Measure.compProd_add_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
(κ η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
:
@[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 κ]
:
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)
:
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)
:
@[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)
:
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 κ))
:
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 κ))
:
@[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 κ))
:
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 κ)
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 ν