Composition-product of kernels #
We define the composition-product κ ⊗ₖ η of two s-finite kernels κ : Kernel α β and
η : Kernel (α × β) γ, a kernel from α to β × γ.
A note on names:
The composition-product Kernel α β → Kernel (α × β) γ → Kernel α (β × γ) is named composition in
[Kal21] and product on the wikipedia article on transition kernels.
Most papers studying categories of kernels call composition the map we call composition. We adopt
that convention because it fits better with the use of the name comp elsewhere in mathlib.
Main definitions #
compProd (κ : Kernel α β) (η : Kernel (α × β) γ) : Kernel α (β × γ): composition-product of 2 s-finite kernels. We define a notationκ ⊗ₖ η = compProd κ η.∫⁻ bc, f bc ∂((κ ⊗ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
Main statements #
lintegral_compProd: Lebesgue integral of a function against a composition-product of kernels.- Instances stating that
IsMarkovKernel,IsZeroOrMarkovKernel,IsFiniteKernelandIsSFiniteKernelare stable by composition-product.
Notation #
κ ⊗ₖ η = ProbabilityTheory.Kernel.compProd κ η
Composition-Product of kernels #
We define a kernel composition-product
compProd : Kernel α β → Kernel (α × β) γ → Kernel α (β × γ).
theorem
ProbabilityTheory.Kernel.compProd_def
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
:
κ.compProd η = (((((swap γ β).comp (η.parallelComp Kernel.id)).comp (deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯)).comp
(Kernel.id.parallelComp (copy β))).comp
(Kernel.id.parallelComp κ)).comp
(copy α)
@[irreducible]
noncomputable def
ProbabilityTheory.Kernel.compProd
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
:
Composition-Product of kernels. For s-finite kernels, it satisfies
∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
(see ProbabilityTheory.Kernel.lintegral_compProd).
If either of the kernels is not s-finite, compProd is given the junk value 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Composition-Product of kernels. For s-finite kernels, it satisfies
∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
(see ProbabilityTheory.Kernel.lintegral_compProd).
If either of the kernels is not s-finite, compProd is given the junk value 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
(h : ¬IsSFiniteKernel κ)
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
(h : ¬IsSFiniteKernel η)
:
theorem
ProbabilityTheory.Kernel.compProd_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(hs : MeasurableSet s)
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
:
theorem
ProbabilityTheory.Kernel.le_compProd_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
(s : Set (β × γ))
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_apply_univ
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
[IsSFiniteKernel κ]
[IsMarkovKernel η]
{a : α}
:
theorem
ProbabilityTheory.Kernel.compProd_apply_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
{a : α}
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.compProd_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η η' : Kernel (α × β) γ}
[IsSFiniteKernel η]
[IsSFiniteKernel η']
(h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b))
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_zero_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel (α × β) γ)
:
@[simp]
theorem
ProbabilityTheory.Kernel.compProd_zero_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : Kernel α β)
(γ : Type u_4)
{mγ : MeasurableSpace γ}
:
theorem
ProbabilityTheory.Kernel.compProd_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.compProd_preimage_fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set β}
(hs : MeasurableSet s)
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsMarkovKernel η]
(x : α)
:
theorem
ProbabilityTheory.Kernel.compProd_deterministic_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasurableSingletonClass γ]
{f : α × β → γ}
(hf : Measurable f)
{s : Set (β × γ)}
(hs : MeasurableSet s)
(κ : Kernel α β)
[IsSFiniteKernel κ]
(x : α)
:
ae filter of the composition-product #
theorem
ProbabilityTheory.Kernel.ae_kernel_lt_top
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
(a : α)
(h2s : ((κ.compProd η) a) s ≠ ⊤)
:
theorem
ProbabilityTheory.Kernel.compProd_null
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.ae_null_of_compProd_null
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
(h : ((κ.compProd η) a) s = 0)
:
theorem
ProbabilityTheory.Kernel.ae_ae_of_ae_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
{p : β × γ → Prop}
(h : ∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc)
:
theorem
ProbabilityTheory.Kernel.ae_compProd_of_ae_ae
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{a : α}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
{p : β × γ → Prop}
(hp : MeasurableSet {x : β × γ | p x})
(h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c))
:
theorem
ProbabilityTheory.Kernel.ae_compProd_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{a : α}
{p : β × γ → Prop}
(hp : MeasurableSet {x : β × γ | p x})
:
theorem
ProbabilityTheory.Kernel.compProd_restrict
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.compProd_restrict_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{s : Set β}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.compProd_restrict_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{η : Kernel (α × β) γ}
[IsSFiniteKernel η]
{t : Set γ}
(ht : MeasurableSet t)
:
Lebesgue integral #
theorem
ProbabilityTheory.Kernel.lintegral_compProd'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β → γ → ENNReal}
(hf : Measurable (Function.uncurry f))
:
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.Kernel.lintegral_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
:
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.Kernel.lintegral_compProd₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : AEMeasurable f ((κ.compProd η) a))
:
Lebesgue integral against the composition-product of two kernels.
theorem
ProbabilityTheory.Kernel.setLIntegral_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
{s : Set β}
{t : Set γ}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
{f : β × γ → ENNReal}
(hf : Measurable f)
{t : Set γ}
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.compProd_eq_sum_compProd_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
:
theorem
ProbabilityTheory.Kernel.compProd_eq_sum_compProd_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.compProd_eq_sum_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.compProd_eq_tsum_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{s : Set (β × γ)}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
(a : α)
(hs : MeasurableSet s)
:
instance
ProbabilityTheory.Kernel.IsMarkovKernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsMarkovKernel κ]
(η : Kernel (α × β) γ)
[IsMarkovKernel η]
:
IsMarkovKernel (κ.compProd η)
instance
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsZeroOrMarkovKernel κ]
(η : Kernel (α × β) γ)
[IsZeroOrMarkovKernel η]
:
IsZeroOrMarkovKernel (κ.compProd η)
theorem
ProbabilityTheory.Kernel.compProd_apply_univ_le
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsFiniteKernel η]
(a : α)
:
instance
ProbabilityTheory.Kernel.IsFiniteKernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
[IsFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsFiniteKernel η]
:
IsFiniteKernel (κ.compProd η)
instance
ProbabilityTheory.Kernel.IsSFiniteKernel.compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
:
IsSFiniteKernel (κ.compProd η)
theorem
ProbabilityTheory.Kernel.compProd_assoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
{ξ : Kernel (α × β × γ) δ}
:
(κ.compProd (η.compProd (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯))).map ⇑MeasurableEquiv.prodAssoc.symm = (κ.compProd η).compProd ξ
Kernel.compProd is associative. We have to insert MeasurableEquiv.prodAssoc in two places
because the products of types α × β × γ and (α × β) × γ are different.
theorem
ProbabilityTheory.Kernel.compProd_add_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel μ]
[IsSFiniteKernel κ]
:
theorem
ProbabilityTheory.Kernel.compProd_add_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : Kernel α β)
(κ η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
:
theorem
ProbabilityTheory.Kernel.compProd_sum_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{ι : Type u_4}
[Countable ι]
{κ : ι → Kernel α β}
{η : Kernel (α × β) γ}
[∀ (i : ι), IsSFiniteKernel (κ i)]
:
theorem
ProbabilityTheory.Kernel.compProd_sum_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{ι : Type u_4}
[Countable ι]
{κ : Kernel α β}
{η : ι → Kernel (α × β) γ}
[∀ (i : ι), IsSFiniteKernel (η i)]
:
theorem
ProbabilityTheory.Kernel.comapRight_compProd_id_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{δ : Type u_4}
{mδ : MeasurableSpace δ}
(κ : Kernel α β)
[IsSFiniteKernel κ]
(η : Kernel (α × β) γ)
[IsSFiniteKernel η]
{f : δ → γ}
(hf : MeasurableEmbedding f)
:
theorem
ProbabilityTheory.Kernel.fst_compProd_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
(x : α)
{s : Set β}
(hs : MeasurableSet s)
:
If η is a Markov kernel, use instead fst_compProd to get (κ ⊗ₖ η).fst = κ.
@[simp]
theorem
ProbabilityTheory.Kernel.fst_compProd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : Kernel α β)
(η : Kernel (α × β) γ)
[IsSFiniteKernel κ]
[IsMarkovKernel η]
: