# mathlib3documentation

probability.kernel.composition

# 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 of `is_markov_kernel`, `is_finite_kernel`, `is_s_finite_kernel` and operation is one of `comp_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 × β) γ)) (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`.

Equations
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 × β) γ)) (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 × β) γ)) (a : α) (f : set × γ)) (hf_meas : (i : ), measurable_set (f i)) (hf_disj : pairwise (disjoint on f)) :
( (i : ), f i) = ∑' (i : ), (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 × β) γ)) (a : α) (hs : measurable_set s) :
= ∑' (n : ),
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 × β) γ)) (a : α) (s : set × γ)) :
= ∑' (n : ),
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 × β) γ)) (a : α) (hs : measurable_set 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 × β) γ)) (hs : measurable_set s) :
measurable (λ (a : α),

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 × β) γ)) (hs : measurable_set s) :
measurable (λ (a : α),
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 × β) γ))  :
× γ))

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
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 × β) γ)) (a : α) (hs : measurable_set s) :
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 × β) γ)) (a : α) (hs : measurable_set s) :
a) s = ∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) s} κ a
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 × β) γ)) (a : α) (s : set × γ)) :
∫⁻ (b : β), (η (a, b)) {c : γ | (b, c) s} κ a a) s

### `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 × β) γ)} (a : α) (h2s : a) s ) :
∀ᵐ (b : β) κ a, (η (a, b)) (prod.mk b ⁻¹' 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 × β) γ)} (a : α) (hs : measurable_set s) :
a) s = 0 (λ (b : β), (η (a, b)) (prod.mk b ⁻¹' s)) =ᵐ[κ a] 0
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 × β) γ)} {a : α} (h : a) s = 0) :
(λ (b : β), (η (a, b)) (prod.mk b ⁻¹' s)) =ᵐ[κ a] 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 × β) γ)} {a : α} {p : β × γ Prop} (h : ∀ᵐ (bc : β × γ) , p bc) :
∀ᵐ (b : β) κ a, ∀ᵐ (c : γ) η (a, b), p (b, c)
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 × β) γ)} {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 × β) γ)} {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 × β) γ)} {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 × β) γ)) (a : α) {f : β } (hf : measurable ) :
∫⁻ (bc : β × γ), f bc.fst bc.snd = ∫⁻ (b : β), ∫⁻ (c : γ), f b c η (a, b) κ a

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 × β) γ)) (a : α) {f : β × γ ennreal} (hf : measurable f) :
∫⁻ (bc : β × γ), f bc = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) η (a, b) κ a

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 × β) γ)) (a : α) {f : β × γ ennreal} (hf : a)) :
∫⁻ (z : β × γ), f z = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) η (a, x) κ 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 × β) γ)) (a : α) {f : β × γ ennreal} (hf : measurable f) {s : set β} {t : set γ} (hs : measurable_set s) (ht : measurable_set t) :
∫⁻ (z : β × γ) in s ×ˢ t, f z = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) η (a, x) κ a
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 × β) γ)) (a : α) {f : β × γ ennreal} (hf : measurable f) {s : set β} (hs : measurable_set s) :
∫⁻ (z : β × γ) in , f z = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) η (a, x) κ a
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 × β) γ)) (a : α) {f : β × γ ennreal} (hf : measurable f) {t : set γ} (ht : measurable_set t) :
∫⁻ (z : β × γ) in , f z = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) η (a, x) κ a
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 × β) γ)) (a : α) (hs : measurable_set s) :
a) s = ∑' (n m : ),
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 × β) γ))  :
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 × β) γ))  :
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 × β) γ))  :
@[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 × β) γ))  :
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 × β) γ)) (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 × β) γ))  :
@[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 × β) γ))  :

### 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 γ} (κ : ) (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
• = λ (a : α), (κ 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 : β γ} (κ : ) (hf : measurable f) (a : α) :
hf) a = (κ 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 : β γ} (κ : ) (hf : measurable f) (a : α) {s : set γ} (hs : measurable_set s) :
( hf) a) s = (κ a) (f ⁻¹' 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 : β γ} (κ : ) (hf : measurable f) (a : α) {g' : γ ennreal} (hg : measurable g') :
∫⁻ (b : γ), g' b hf) a = ∫⁻ (a : β), g' (f a) κ a
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 : β γ} (κ : ) (hf : measurable f) :
@[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 : β γ} (κ : ) (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 : β γ} (κ : ) (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 : β γ} (κ : ) (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 γ} (κ : ) (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
• = λ (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 : γ α} (κ : ) (hg : measurable g) (c : γ) :
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 : γ α} (κ : ) (hg : measurable g) (c : γ) (s : set β) :
( hg) c) s = (κ (g c)) s
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 : γ α} (κ : ) (hg : measurable g) (c : γ) (g' : β ennreal) :
∫⁻ (b : β), g' b hg) c = ∫⁻ (b : β), g' b κ (g c)
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 : γ α} (κ : ) (hg : measurable g) :
@[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 : γ α} (κ : ) (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 : γ α} (κ : ) (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 : γ α} (κ : ) (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) (κ : ) :

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 γ} (κ : ) (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 γ} (κ : ) (ca : γ × α) (s : set β) :
ca) s = (κ ca.snd) s
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 γ} (κ : ) (ca : γ × α) (g : β ennreal) :
∫⁻ (b : β), g b = ∫⁻ (b : β), g b κ ca.snd
@[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 γ} (κ : )  :
@[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 γ} (κ : )  :
@[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 γ} (κ : )  :
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 × β) γ)) :

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 : β × α) :
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 γ) :
= (κ a.swap) s
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) :
∫⁻ (c : γ), g c = ∫⁻ (c : γ), g c κ a.swap
@[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 × β) γ))  :
@[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 × β) γ))  :
@[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 × β) γ))  :
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 γ} (κ : × γ))) :
× β))

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 γ} (κ : × γ))) (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 γ} (κ : × γ))) (a : α) {s : set × β)} (hs : measurable_set s) :
= (κ a) {p : β × γ | p.swap 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 γ} (κ : × γ))) (a : α) {g : γ × β ennreal} (hg : measurable g) :
∫⁻ (c : γ × β), g c = ∫⁻ (bc : β × γ), g bc.swap κ a
@[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 γ} (κ : × γ)))  :
@[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 γ} (κ : × γ)))  :
@[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 γ} (κ : × γ)))  :
noncomputable def probability_theory.kernel.fst {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} (κ : × γ))) :

Define a `kernel α β` from a `kernel α (β × γ)` by taking the map of the first projection.

Equations
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 γ} (κ : × γ))) (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 γ} (κ : × γ))) (a : α) {s : set β} (hs : measurable_set s) :
s = (κ a) {p : β × γ | p.fst 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 γ} (κ : × γ))) (a : α) {g : β ennreal} (hg : measurable g) :
∫⁻ (c : β), g c = ∫⁻ (bc : β × γ), g bc.fst κ a
@[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 γ} (κ : × γ)))  :
@[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 γ} (κ : × γ)))  :
@[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 γ} (κ : × γ)))  :
noncomputable def probability_theory.kernel.snd {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} (κ : × γ))) :

Define a `kernel α γ` from a `kernel α (β × γ)` by taking the map of the second projection.

Equations
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 γ} (κ : × γ))) (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 γ} (κ : × γ))) (a : α) {s : set γ} (hs : measurable_set s) :
s = (κ a) {p : β × γ | p.snd 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 γ} (κ : × γ))) (a : α) {g : γ ennreal} (hg : measurable g) :
∫⁻ (c : γ), g c = ∫⁻ (bc : β × γ), g bc.snd κ a
@[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 γ} (κ : × γ)))  :
@[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 γ} (κ : × γ)))  :
@[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 γ} (κ : × γ)))  :

### 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 γ} (η : ) (κ : ) :

Composition of two s-finite kernels.

Equations
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 γ} (η : ) (κ : ) (a : α) :
= (κ a).bind η
theorem probability_theory.kernel.comp_apply' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} (η : ) (κ : ) (a : α) {s : set γ} (hs : measurable_set s) :
a) s = ∫⁻ (b : β), (η b) s κ a
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 γ} (η : ) (κ : )  :
theorem probability_theory.kernel.lintegral_comp {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} (η : ) (κ : ) (a : α) {g : γ ennreal} (hg : measurable g) :
∫⁻ (c : γ), g c = ∫⁻ (b : β), ∫⁻ (c : γ), g c η b κ a
@[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 γ} (η : ) (κ : )  :
@[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 γ} (η : ) (κ : )  :
@[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 γ} (η : ) (κ : )  :
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 δ} (ξ : ) (η : ) (κ : ) :

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) (κ : ) :
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 : γ α} (κ : ) (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 γ} (κ : ) (η : )  :
× γ))

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 γ} (κ : ) (η : ) (a : α) {s : set × γ)} (hs : measurable_set s) :
a) s = ∫⁻ (b : β), (η a) {c : γ | (b, c) s} κ a
theorem probability_theory.kernel.lintegral_prod {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} (κ : ) (η : ) (a : α) {g : β × γ ennreal} (hg : measurable g) :
∫⁻ (c : β × γ), g c = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) η a κ a
@[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 γ} (κ : ) (η : )  :
@[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 γ} (κ : ) (η : )  :
@[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 γ} (κ : ) (η : )  :