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 (α × β).
Notation #
μ ⊗ₘ κ = μ.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
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_of_not_sfinite
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
(κ : ProbabilityTheory.Kernel α β)
(h : ¬SFinite μ)
:
@[simp]
theorem
MeasureTheory.Measure.compProd_of_not_isSFiniteKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
(κ : ProbabilityTheory.Kernel α β)
(h : ¬ProbabilityTheory.IsSFiniteKernel κ)
:
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
MeasureTheory.Measure.compProd_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(h : ⇑κ =ᶠ[ae μ] ⇑η)
:
@[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 α)
:
theorem
MeasureTheory.Measure.compProd_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel κ]
:
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 : α)
:
theorem
MeasureTheory.Measure.compProd_id
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[SFinite μ]
:
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 ν]
:
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 η]
:
theorem
MeasureTheory.Measure.compProd_sum_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{ι : Type u_3}
[Countable ι]
{μ : ι → Measure α}
[∀ (i : ι), SFinite (μ i)]
:
theorem
MeasureTheory.Measure.compProd_sum_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{ι : Type u_3}
[Countable ι]
{κ : ι → ProbabilityTheory.Kernel α β}
[h : ∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (κ i)]
:
@[simp]
theorem
MeasureTheory.Measure.fst_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : Measure α)
[SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
:
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)
:
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.snd_dirac_unit_compProd_const
{β : Type u_2}
{mβ : MeasurableSpace β}
(μ : Measure β)
[SFinite μ]
:
instance
MeasureTheory.Measure.instSFiniteProdCompProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
:
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 κ)
instance
MeasureTheory.Measure.instIsZeroOrProbabilityMeasureProdCompProdOfIsZeroOrMarkovKernel
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[IsZeroOrProbabilityMeasure μ]
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
:
@[simp]
theorem
MeasureTheory.Measure.compProd_assoc
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{γ : Type u_3}
{mγ : MeasurableSpace γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
:
Measure.compProd is associative. We have to insert MeasurableEquiv.prodAssoc
because the products of types α × β × γ and (α × β) × γ are different.
@[simp]
theorem
MeasureTheory.Measure.compProd_assoc'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ : ProbabilityTheory.Kernel α β}
{γ : Type u_3}
{mγ : MeasurableSpace γ}
{η : ProbabilityTheory.Kernel (α × β) γ}
:
Measure.compProd is associative. We have to insert MeasurableEquiv.prodAssoc
because the products of types α × β × γ and (α × β) × γ are different.
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 κ)
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 η)
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 η)
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 η))
:
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_left_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ : ProbabilityTheory.Kernel α β}
[SFinite μ]
[SFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
:
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 ν)
:
∀ᵐ (x : α) ∂ξ, (κ x).MutuallySingular (η x)
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)]
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.mutuallySingular_compProd_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SigmaFinite μ]
[SigmaFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
:
theorem
MeasureTheory.Measure.mutuallySingular_compProd_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[SigmaFinite μ]
[SigmaFinite ν]
:
(μ.compProd κ).MutuallySingular (ν.compProd η) ↔ ∀ (ξ : Measure α),
SFinite ξ → ξ.AbsolutelyContinuous μ → ξ.AbsolutelyContinuous ν → (ξ.compProd κ).MutuallySingular (ξ.compProd η)
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)]
:
(μ.compProd κ).AbsolutelyContinuous (ν.compProd η) ↔ μ.AbsolutelyContinuous ν ∧ (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)