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
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
@[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 α)
:
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)
:
↑↑(MeasureTheory.Measure.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)
:
↑↑(MeasureTheory.Measure.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.kernel α β)}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(h : ⇑κ =ᶠ[MeasureTheory.Measure.ae μ] ⇑η)
:
theorem
MeasureTheory.Measure.ae_compProd_of_ae_ae
{α : 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})
(h : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b))
:
∀ᵐ (x : α × β) ∂MeasureTheory.Measure.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 : α × β) ∂MeasureTheory.Measure.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 : α × β) ∂MeasureTheory.Measure.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.Measure α)
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
:
theorem
MeasureTheory.Measure.compProd_add_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
[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)
:
∫⁻ (x : α × β), f x ∂MeasureTheory.Measure.compProd μ κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ
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 ∂MeasureTheory.Measure.compProd μ κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ
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 (MeasureTheory.Measure.compProd μ κ))
:
MeasureTheory.Integrable f (MeasureTheory.Measure.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 (MeasureTheory.Measure.compProd μ κ))
:
∫ (x : α × β), f x ∂MeasureTheory.Measure.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) (MeasureTheory.Measure.compProd μ κ))
:
∫ (x : α × β) in s ×ˢ t, f x ∂MeasureTheory.Measure.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) (MeasureTheory.Measure.compProd μ κ))
:
∫ (x : α × β) in s ×ˢ t, f x ∂MeasureTheory.Measure.compProd μ κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ
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.compProd (MeasureTheory.Measure.dirac a) κ) s = ↑↑(κ a) (Prod.mk a ⁻¹' 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 β}
(μ : MeasureTheory.Measure β)
[MeasureTheory.IsFiniteMeasure μ]
:
@[simp]
theorem
MeasureTheory.Measure.snd_dirac_unit_compProd_const
{β : Type u_2}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure β)
[MeasureTheory.IsFiniteMeasure μ]
:
instance
MeasureTheory.Measure.instSFiniteProdInstMeasurableSpaceCompProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ↥(ProbabilityTheory.kernel α β)}
:
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.instIsFiniteMeasureProdInstMeasurableSpaceCompProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ↥(ProbabilityTheory.kernel α β)}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.instIsProbabilityMeasureProdInstMeasurableSpaceCompProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ↥(ProbabilityTheory.kernel α β)}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
:
Equations
- ⋯ = ⋯