Product and composition of kernels #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define
- the composition-product
κ ⊗ₖ ηof two s-finite kernelsκ : kernel α βandη : kernel (α × β) γ, a kernel fromαtoβ × γ. - the map and comap of a kernel along a measurable function.
- the composition
η ∘ₖ κof kernelsκ : kernel α βandη : kernel β γ, kernel fromαtoγ. - the product
κ ×ₖ ηof 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 #
Kernels built from other kernels:
comp_prod (κ : kernel α β) (η : kernel (α × β) γ) : kernel α (β × γ): composition-product of 2 s-finite kernels. We define a notationκ ⊗ₖ η = comp_prod κ η.∫⁻ bc, f bc ∂((κ ⊗ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)map (κ : kernel α β) (f : β → γ) (hf : measurable f) : kernel α γ∫⁻ c, g c ∂(map κ f hf a) = ∫⁻ b, g (f b) ∂(κ a)comap (κ : kernel α β) (f : γ → α) (hf : measurable f) : kernel γ β∫⁻ b, g b ∂(comap κ f hf c) = ∫⁻ b, g b ∂(κ (f c))comp (η : kernel β γ) (κ : kernel α β) : kernel α γ: composition of 2 kernels. We define a notationη ∘ₖ κ = comp η κ.∫⁻ c, g c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, g c ∂(η b) ∂(κ a)prod (κ : kernel α β) (η : kernel α γ) : kernel α (β × γ): product of 2 s-finite kernels.∫⁻ bc, f bc ∂((κ ×ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η a) ∂(κ a)
Main statements #
lintegral_comp_prod,lintegral_map,lintegral_comap,lintegral_comp,lintegral_prod: Lebesgue integral of a function against a composition-product/map/comap/composition/product of kernels.- Instances of the form
<class>.<operation>where class is one ofis_markov_kernel,is_finite_kernel,is_s_finite_kerneland operation is one ofcomp_prod,map,comap,comp,prod. These instances state that the three classes are stable by the various operations.
Notations #
κ ⊗ₖ η = probability_theory.kernel.comp_prod κ ηη ∘ₖ κ = probability_theory.kernel.comp η κκ ×ₖ η = probability_theory.kernel.prod κ η
Composition-Product of kernels #
We define a kernel composition-product
comp_prod : kernel α β → kernel (α × β) γ → kernel α (β × γ).
noncomputable
def
probability_theory.kernel.comp_prod_fun
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(η : ↥(probability_theory.kernel (α × β) γ))
(a : α)
(s : set (β × γ)) :
Auxiliary function for the definition of the composition-product of two kernels.
For all a : α, comp_prod_fun κ η a is a countably additive function with value zero on the empty
set, and the composition-product of kernels is defined in kernel.comp_prod through
measure.of_measurable.
theorem
probability_theory.kernel.comp_prod_fun_empty
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(η : ↥(probability_theory.kernel (α × β) γ))
(a : α) :
theorem
probability_theory.kernel.comp_prod_fun_Union
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
(f : ℕ → set (β × γ))
(hf_meas : ∀ (i : ℕ), measurable_set (f i))
(hf_disj : pairwise (disjoint on f)) :
probability_theory.kernel.comp_prod_fun κ η a (⋃ (i : ℕ), f i) = ∑' (i : ℕ), probability_theory.kernel.comp_prod_fun κ η a (f i)
theorem
probability_theory.kernel.comp_prod_fun_tsum_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
(κ : ↥(probability_theory.kernel α β))
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
(hs : measurable_set s) :
probability_theory.kernel.comp_prod_fun κ η a s = ∑' (n : ℕ), probability_theory.kernel.comp_prod_fun κ (probability_theory.kernel.seq η n) a s
theorem
probability_theory.kernel.comp_prod_fun_tsum_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel κ]
(a : α)
(s : set (β × γ)) :
probability_theory.kernel.comp_prod_fun κ η a s = ∑' (n : ℕ), probability_theory.kernel.comp_prod_fun (probability_theory.kernel.seq κ n) η a s
theorem
probability_theory.kernel.comp_prod_fun_eq_tsum
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
(hs : measurable_set s) :
probability_theory.kernel.comp_prod_fun κ η a s = ∑' (n m : ℕ), probability_theory.kernel.comp_prod_fun (probability_theory.kernel.seq κ n) (probability_theory.kernel.seq η m) a s
theorem
probability_theory.kernel.measurable_comp_prod_fun_of_finite
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_finite_kernel η]
(hs : measurable_set s) :
measurable (λ (a : α), probability_theory.kernel.comp_prod_fun κ η a s)
Auxiliary lemma for measurable_comp_prod_fun.
theorem
probability_theory.kernel.measurable_comp_prod_fun
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(hs : measurable_set s) :
measurable (λ (a : α), probability_theory.kernel.comp_prod_fun κ η a s)
noncomputable
def
probability_theory.kernel.comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η] :
↥(probability_theory.kernel α (β × γ))
Composition-Product of kernels. It verifies
∫⁻ bc, f bc ∂(comp_prod κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
(see lintegral_comp_prod).
Equations
- probability_theory.kernel.comp_prod κ η = ⟨λ (a : α), measure_theory.measure.of_measurable (λ (s : set (β × γ)) (hs : measurable_set s), probability_theory.kernel.comp_prod_fun κ η a s) _ _, _⟩
Instances for probability_theory.kernel.comp_prod
theorem
probability_theory.kernel.comp_prod_apply_eq_comp_prod_fun
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
(hs : measurable_set s) :
⇑(⇑(probability_theory.kernel.comp_prod κ η) a) s = probability_theory.kernel.comp_prod_fun κ η a s
theorem
probability_theory.kernel.comp_prod_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
(hs : measurable_set s) :
theorem
probability_theory.kernel.le_comp_prod_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
(s : set (β × γ)) :
ae filter of the composition-product #
theorem
probability_theory.kernel.ae_kernel_lt_top
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
{κ : ↥(probability_theory.kernel α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
(a : α)
(h2s : ⇑(⇑(probability_theory.kernel.comp_prod κ η) a) s ≠ ⊤) :
theorem
probability_theory.kernel.comp_prod_null
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
{κ : ↥(probability_theory.kernel α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
(a : α)
(hs : measurable_set s) :
theorem
probability_theory.kernel.ae_null_of_comp_prod_null
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
{κ : ↥(probability_theory.kernel α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
{a : α}
(h : ⇑(⇑(probability_theory.kernel.comp_prod κ η) a) s = 0) :
theorem
probability_theory.kernel.ae_ae_of_ae_comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{κ : ↥(probability_theory.kernel α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
{a : α}
{p : β × γ → Prop}
(h : ∀ᵐ (bc : β × γ) ∂⇑(probability_theory.kernel.comp_prod κ η) a, p bc) :
theorem
probability_theory.kernel.comp_prod_restrict
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{κ : ↥(probability_theory.kernel α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
{s : set β}
{t : set γ}
(hs : measurable_set s)
(ht : measurable_set t) :
theorem
probability_theory.kernel.comp_prod_restrict_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{κ : ↥(probability_theory.kernel α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
{s : set β}
(hs : measurable_set s) :
theorem
probability_theory.kernel.comp_prod_restrict_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{κ : ↥(probability_theory.kernel α β)}
[probability_theory.is_s_finite_kernel κ]
{η : ↥(probability_theory.kernel (α × β) γ)}
[probability_theory.is_s_finite_kernel η]
{t : set γ}
(ht : measurable_set t) :
Lebesgue integral #
theorem
probability_theory.kernel.lintegral_comp_prod'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
{f : β → γ → ennreal}
(hf : measurable (function.uncurry f)) :
Lebesgue integral against the composition-product of two kernels.
theorem
probability_theory.kernel.lintegral_comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
{f : β × γ → ennreal}
(hf : measurable f) :
Lebesgue integral against the composition-product of two kernels.
theorem
probability_theory.kernel.lintegral_comp_prod₀
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
{f : β × γ → ennreal}
(hf : ae_measurable f (⇑(probability_theory.kernel.comp_prod κ η) a)) :
Lebesgue integral against the composition-product of two kernels.
theorem
probability_theory.kernel.set_lintegral_comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
{f : β × γ → ennreal}
(hf : measurable f)
{s : set β}
{t : set γ}
(hs : measurable_set s)
(ht : measurable_set t) :
theorem
probability_theory.kernel.set_lintegral_comp_prod_univ_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
{f : β × γ → ennreal}
(hf : measurable f)
{s : set β}
(hs : measurable_set s) :
theorem
probability_theory.kernel.set_lintegral_comp_prod_univ_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
{f : β × γ → ennreal}
(hf : measurable f)
{t : set γ}
(ht : measurable_set t) :
theorem
probability_theory.kernel.comp_prod_eq_tsum_comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{s : set (β × γ)}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
(hs : measurable_set s) :
⇑(⇑(probability_theory.kernel.comp_prod κ η) a) s = ∑' (n m : ℕ), ⇑(⇑(probability_theory.kernel.comp_prod (probability_theory.kernel.seq κ n) (probability_theory.kernel.seq η m)) a) s
theorem
probability_theory.kernel.comp_prod_eq_sum_comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η] :
theorem
probability_theory.kernel.comp_prod_eq_sum_comp_prod_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η] :
theorem
probability_theory.kernel.comp_prod_eq_sum_comp_prod_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η] :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_markov_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_markov_kernel η] :
theorem
probability_theory.kernel.comp_prod_apply_univ_le
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_finite_kernel η]
(a : α) :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_finite_kernel η] :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel η] :
map, comap #
noncomputable
def
probability_theory.kernel.map
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(f : β → γ)
(hf : measurable f) :
The pushforward of a kernel along a measurable function.
We include measurability in the assumptions instead of using junk values
to make sure that typeclass inference can infer that the map of a Markov kernel
is again a Markov kernel.
Equations
- probability_theory.kernel.map κ f hf = ⟨λ (a : α), measure_theory.measure.map f (⇑κ a), _⟩
Instances for probability_theory.kernel.map
theorem
probability_theory.kernel.map_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{f : β → γ}
(κ : ↥(probability_theory.kernel α β))
(hf : measurable f)
(a : α) :
⇑(probability_theory.kernel.map κ f hf) a = measure_theory.measure.map f (⇑κ a)
theorem
probability_theory.kernel.map_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{f : β → γ}
(κ : ↥(probability_theory.kernel α β))
(hf : measurable f)
(a : α)
{s : set γ}
(hs : measurable_set s) :
theorem
probability_theory.kernel.lintegral_map
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{f : β → γ}
(κ : ↥(probability_theory.kernel α β))
(hf : measurable f)
(a : α)
{g' : γ → ennreal}
(hg : measurable g') :
theorem
probability_theory.kernel.sum_map_seq
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{f : β → γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(hf : measurable f) :
probability_theory.kernel.sum (λ (n : ℕ), probability_theory.kernel.map (probability_theory.kernel.seq κ n) f hf) = probability_theory.kernel.map κ f hf
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.map
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{f : β → γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_markov_kernel κ]
(hf : measurable f) :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.map
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{f : β → γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
(hf : measurable f) :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.map
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{f : β → γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(hf : measurable f) :
def
probability_theory.kernel.comap
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(g : γ → α)
(hg : measurable g) :
Pullback of a kernel, such that for each set s comap κ g hg c s = κ (g c) s.
We include measurability in the assumptions instead of using junk values
to make sure that typeclass inference can infer that the comap of a Markov kernel
is again a Markov kernel.
Equations
- probability_theory.kernel.comap κ g hg = ⟨λ (a : γ), ⇑κ (g a), _⟩
Instances for probability_theory.kernel.comap
theorem
probability_theory.kernel.comap_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{g : γ → α}
(κ : ↥(probability_theory.kernel α β))
(hg : measurable g)
(c : γ) :
⇑(probability_theory.kernel.comap κ g hg) c = ⇑κ (g c)
theorem
probability_theory.kernel.comap_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{g : γ → α}
(κ : ↥(probability_theory.kernel α β))
(hg : measurable g)
(c : γ)
(s : set β) :
theorem
probability_theory.kernel.lintegral_comap
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{g : γ → α}
(κ : ↥(probability_theory.kernel α β))
(hg : measurable g)
(c : γ)
(g' : β → ennreal) :
theorem
probability_theory.kernel.sum_comap_seq
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{g : γ → α}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(hg : measurable g) :
probability_theory.kernel.sum (λ (n : ℕ), probability_theory.kernel.comap (probability_theory.kernel.seq κ n) g hg) = probability_theory.kernel.comap κ g hg
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.comap
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{g : γ → α}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_markov_kernel κ]
(hg : measurable g) :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.comap
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{g : γ → α}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
(hg : measurable g) :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.comap
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{g : γ → α}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(hg : measurable g) :
def
probability_theory.kernel.prod_mk_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(γ : Type u_3)
[measurable_space γ]
(κ : ↥(probability_theory.kernel α β)) :
↥(probability_theory.kernel (γ × α) β)
Define a kernel (γ × α) β from a kernel α β by taking the comap of the projection.
Equations
Instances for probability_theory.kernel.prod_mk_left
theorem
probability_theory.kernel.prod_mk_left_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(ca : γ × α) :
⇑(probability_theory.kernel.prod_mk_left γ κ) ca = ⇑κ ca.snd
theorem
probability_theory.kernel.prod_mk_left_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(ca : γ × α)
(s : set β) :
theorem
probability_theory.kernel.lintegral_prod_mk_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
(ca : γ × α)
(g : β → ennreal) :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.prod_mk_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_markov_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.prod_mk_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.prod_mk_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ] :
def
probability_theory.kernel.swap_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel (α × β) γ)) :
↥(probability_theory.kernel (β × α) γ)
Define a kernel (β × α) γ from a kernel (α × β) γ by taking the comap of prod.swap.
Equations
Instances for probability_theory.kernel.swap_left
theorem
probability_theory.kernel.swap_left_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel (α × β) γ))
(a : β × α) :
⇑(probability_theory.kernel.swap_left κ) a = ⇑κ a.swap
theorem
probability_theory.kernel.swap_left_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel (α × β) γ))
(a : β × α)
(s : set γ) :
theorem
probability_theory.kernel.lintegral_swap_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel (α × β) γ))
(a : β × α)
(g : γ → ennreal) :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.swap_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_markov_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.swap_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_finite_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.swap_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel (α × β) γ))
[probability_theory.is_s_finite_kernel κ] :
noncomputable
def
probability_theory.kernel.swap_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ))) :
↥(probability_theory.kernel α (γ × β))
Define a kernel α (γ × β) from a kernel α (β × γ) by taking the map of prod.swap.
Equations
Instances for probability_theory.kernel.swap_right
theorem
probability_theory.kernel.swap_right_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α) :
theorem
probability_theory.kernel.swap_right_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α)
{s : set (γ × β)}
(hs : measurable_set s) :
theorem
probability_theory.kernel.lintegral_swap_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α)
{g : γ × β → ennreal}
(hg : measurable g) :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.swap_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_markov_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.swap_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_finite_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.swap_right
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_s_finite_kernel κ] :
noncomputable
def
probability_theory.kernel.fst
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ))) :
Define a kernel α β from a kernel α (β × γ) by taking the map of the first projection.
Instances for probability_theory.kernel.fst
theorem
probability_theory.kernel.fst_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α) :
theorem
probability_theory.kernel.fst_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α)
{s : set β}
(hs : measurable_set s) :
theorem
probability_theory.kernel.lintegral_fst
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α)
{g : β → ennreal}
(hg : measurable g) :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.fst
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_markov_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.fst
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_finite_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.fst
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_s_finite_kernel κ] :
noncomputable
def
probability_theory.kernel.snd
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ))) :
Define a kernel α γ from a kernel α (β × γ) by taking the map of the second projection.
Instances for probability_theory.kernel.snd
theorem
probability_theory.kernel.snd_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α) :
theorem
probability_theory.kernel.snd_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α)
{s : set γ}
(hs : measurable_set s) :
theorem
probability_theory.kernel.lintegral_snd
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
(a : α)
{g : γ → ennreal}
(hg : measurable g) :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.snd
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_markov_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.snd
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_finite_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.snd
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α (β × γ)))
[probability_theory.is_s_finite_kernel κ] :
Composition of two kernels #
noncomputable
def
probability_theory.kernel.comp
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
(κ : ↥(probability_theory.kernel α β)) :
Composition of two s-finite kernels.
Instances for probability_theory.kernel.comp
theorem
probability_theory.kernel.comp_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
(κ : ↥(probability_theory.kernel α β))
(a : α) :
theorem
probability_theory.kernel.comp_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
(κ : ↥(probability_theory.kernel α β))
(a : α)
{s : set γ}
(hs : measurable_set s) :
theorem
probability_theory.kernel.comp_eq_snd_comp_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
[probability_theory.is_s_finite_kernel η]
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ] :
theorem
probability_theory.kernel.lintegral_comp
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
(κ : ↥(probability_theory.kernel α β))
(a : α)
{g : γ → ennreal}
(hg : measurable g) :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.comp
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
[probability_theory.is_markov_kernel η]
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_markov_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.comp
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
[probability_theory.is_finite_kernel η]
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ] :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.comp
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
[probability_theory.is_s_finite_kernel η]
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ] :
theorem
probability_theory.kernel.comp_assoc
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{δ : Type u_3}
{mδ : measurable_space δ}
(ξ : ↥(probability_theory.kernel γ δ))
[probability_theory.is_s_finite_kernel ξ]
(η : ↥(probability_theory.kernel β γ))
(κ : ↥(probability_theory.kernel α β)) :
Composition of kernels is associative.
theorem
probability_theory.kernel.deterministic_comp_eq_map
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{f : β → γ}
(hf : measurable f)
(κ : ↥(probability_theory.kernel α β)) :
theorem
probability_theory.kernel.comp_deterministic_eq_comap
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
{g : γ → α}
(κ : ↥(probability_theory.kernel α β))
(hg : measurable g) :
Product of two kernels #
noncomputable
def
probability_theory.kernel.prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel α γ))
[probability_theory.is_s_finite_kernel η] :
↥(probability_theory.kernel α (β × γ))
Product of two s-finite kernels.
Equations
Instances for probability_theory.kernel.prod
theorem
probability_theory.kernel.prod_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel α γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
{s : set (β × γ)}
(hs : measurable_set s) :
theorem
probability_theory.kernel.lintegral_prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel α γ))
[probability_theory.is_s_finite_kernel η]
(a : α)
{g : β × γ → ennreal}
(hg : measurable g) :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel.prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_markov_kernel κ]
(η : ↥(probability_theory.kernel α γ))
[probability_theory.is_markov_kernel η] :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
(η : ↥(probability_theory.kernel α γ))
[probability_theory.is_finite_kernel η] :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.prod
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{γ : Type u_4}
{mγ : measurable_space γ}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(η : ↥(probability_theory.kernel α γ))
[probability_theory.is_s_finite_kernel η] :