# mathlib3documentation

probability.kernel.basic

# Markov Kernels #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A kernel from a measurable space α to another measurable space β is a measurable map α → measure β, where the measurable space instance on measure β is the one defined in measure_theory.measure.measurable_space. That is, a kernel κ verifies that for all measurable sets s of β, a ↦ κ a s is measurable.

## Main definitions #

Classes of kernels:

• probability_theory.kernel α β: kernels from α to β, defined as the add_submonoid of the measurable functions in α → measure β.
• probability_theory.is_markov_kernel κ: a kernel from α to β is said to be a Markov kernel if for all a : α, k a is a probability measure.
• probability_theory.is_finite_kernel κ: a kernel from α to β is said to be finite if there exists C : ℝ≥0∞ such that C < ∞ and for all a : α, κ a univ ≤ C. This implies in particular that all measures in the image of κ are finite, but is stronger since it requires an uniform bound. This stronger condition is necessary to ensure that the composition of two finite kernels is finite.
• probability_theory.is_s_finite_kernel κ: a kernel is called s-finite if it is a countable sum of finite kernels.

Particular kernels:

• probability_theory.kernel.deterministic (f : α → β) (hf : measurable f): kernel a ↦ measure.dirac (f a).
• probability_theory.kernel.const α (μβ : measure β): constant kernel a ↦ μβ.
• probability_theory.kernel.restrict κ (hs : measurable_set s): kernel for which the image of a : α is (κ a).restrict s. Integral: ∫⁻ b, f b ∂(kernel.restrict κ hs a) = ∫⁻ b in s, f b ∂(κ a)

## Main statements #

• probability_theory.kernel.ext_fun: if ∫⁻ b, f b ∂(κ a) = ∫⁻ b, f b ∂(η a) for all measurable functions f and all a, then the two kernels κ and η are equal.
def probability_theory.kernel (α : Type u_1) (β : Type u_2)  :

A kernel from a measurable space α to another measurable space β is a measurable function κ : α → measure β. The measurable space structure on measure β is given by measure_theory.measure.measurable_space. A map κ : α → measure β is measurable iff ∀ s : set β, measurable_set s → measurable (λ a, κ a s).

Equations
Instances for ↥probability_theory.kernel
@[protected, instance]
def probability_theory.kernel.has_coe_to_fun {α : Type u_1} {β : Type u_2}  :
(λ (_x : ,
Equations
@[simp]
theorem probability_theory.kernel.coe_fn_zero {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} :
0 = 0
@[simp]
theorem probability_theory.kernel.coe_fn_add {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ η : ) :
+ η) = κ + η
def probability_theory.kernel.coe_add_hom (α : Type u_1) (β : Type u_2)  :

Coercion to a function as an additive monoid homomorphism.

Equations
@[simp]
theorem probability_theory.kernel.zero_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (a : α) :
0 a = 0
@[simp]
theorem probability_theory.kernel.coe_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} (I : finset ι) (κ : ι ) :
(I.sum (λ (i : ι), κ i)) = I.sum (λ (i : ι), (κ i))
theorem probability_theory.kernel.finset_sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} (I : finset ι) (κ : ι ) (a : α) :
(I.sum (λ (i : ι), κ i)) a = I.sum (λ (i : ι), (κ i) a)
theorem probability_theory.kernel.finset_sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} (I : finset ι) (κ : ι ) (a : α) (s : set β) :
((I.sum (λ (i : ι), κ i)) a) s = I.sum (λ (i : ι), ((κ i) a) s)
@[class]
structure probability_theory.is_markov_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) :
Prop
• is_probability_measure : (a : α),

A kernel is a Markov kernel if every measure in its image is a probability measure.

Instances of this typeclass
@[class]
structure probability_theory.is_finite_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) :
Prop

A kernel is finite if every measure in its image is finite, with a uniform bound.

Instances of this typeclass
noncomputable def probability_theory.is_finite_kernel.bound {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : )  :

A constant C : ℝ≥0∞ such that C < ∞ (is_finite_kernel.bound_lt_top κ) and for all a : α and s : set β, κ a s ≤ C (measure_le_bound κ a s).

Equations
theorem probability_theory.is_finite_kernel.bound_lt_top {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : )  :
theorem probability_theory.is_finite_kernel.bound_ne_top {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : )  :
theorem probability_theory.kernel.measure_le_bound {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) (a : α) (s : set β) :
@[protected, instance]
def probability_theory.is_finite_kernel_zero (α : Type u_1) (β : Type u_2) {mα : measurable_space α} {mβ : measurable_space β} :
@[protected, instance]
def probability_theory.is_finite_kernel.add {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ η : )  :
@[protected, instance]
def probability_theory.is_markov_kernel.is_probability_measure' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } (a : α) :
@[protected, instance]
def probability_theory.is_finite_kernel.is_finite_measure {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } (a : α) :
@[protected, instance]
def probability_theory.is_markov_kernel.is_finite_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : }  :
@[ext]
theorem probability_theory.kernel.ext {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } (h : (a : α), κ a = η a) :
κ = η
theorem probability_theory.kernel.ext_iff {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } :
κ = η (a : α), κ a = η a
theorem probability_theory.kernel.ext_iff' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } :
κ = η (a : α) (s : set β), (κ a) s = (η a) s
theorem probability_theory.kernel.ext_fun {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } (h : (a : α) (f : β ennreal), ∫⁻ (b : β), f b κ a = ∫⁻ (b : β), f b η a) :
κ = η
theorem probability_theory.kernel.ext_fun_iff {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } :
κ = η (a : α) (f : β ennreal), ∫⁻ (b : β), f b κ a = ∫⁻ (b : β), f b η a
@[protected]
theorem probability_theory.kernel.measurable {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) :
@[protected]
theorem probability_theory.kernel.measurable_coe {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) {s : set β} (hs : measurable_set s) :
measurable (λ (a : α), (κ a) s)
@[protected]
noncomputable def probability_theory.kernel.sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] (κ : ι ) :

Sum of an indexed family of kernels.

Equations
theorem probability_theory.kernel.sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] (κ : ι ) (a : α) :
= measure_theory.measure.sum (λ (n : ι), (κ n) a)
theorem probability_theory.kernel.sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] (κ : ι ) (a : α) {s : set β} (hs : measurable_set s) :
s = ∑' (n : ι), ((κ n) a) s
@[simp]
theorem probability_theory.kernel.sum_zero {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] :
probability_theory.kernel.sum (λ (i : ι), 0) = 0
theorem probability_theory.kernel.sum_comm {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] (κ : ι ι ) :
@[simp]
theorem probability_theory.kernel.sum_fintype {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [fintype ι] (κ : ι ) :
= finset.univ.sum (λ (i : ι), κ i)
theorem probability_theory.kernel.sum_add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] (κ η : ι ) :
probability_theory.kernel.sum (λ (n : ι), κ n + η n) =
@[class]
structure probability_theory.is_s_finite_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) :
Prop

A kernel is s-finite if it can be written as the sum of countably many finite kernels.

Instances of this typeclass
@[protected, instance]
noncomputable def probability_theory.kernel.seq {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : )  :

A sequence of finite kernels such that κ = kernel.sum (seq κ). See is_finite_kernel_seq and kernel_sum_seq.

Equations
Instances for probability_theory.kernel.seq
theorem probability_theory.kernel.kernel_sum_seq {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : )  :
theorem probability_theory.kernel.measure_sum_seq {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) (a : α) :
@[protected, instance]
def probability_theory.kernel.is_finite_kernel_seq {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) (n : ) :
@[protected, instance]
def probability_theory.kernel.is_s_finite_kernel.add {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ η : )  :
theorem probability_theory.kernel.is_s_finite_kernel.finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {κs : ι } (I : finset ι) (h : (i : ι), i I ) :
theorem probability_theory.kernel.is_s_finite_kernel_sum_of_denumerable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [denumerable ι] {κs : ι } (hκs : (n : ι), ) :
theorem probability_theory.kernel.is_s_finite_kernel_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] {κs : ι } (hκs : (n : ι), ) :
noncomputable def probability_theory.kernel.deterministic {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (f : α β) (hf : measurable f) :

Kernel which to a associates the dirac measure at f a. This is a Markov kernel.

Equations
• = λ (a : α), , _⟩
Instances for probability_theory.kernel.deterministic
theorem probability_theory.kernel.deterministic_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α β} (hf : measurable f) (a : α) :
theorem probability_theory.kernel.deterministic_apply' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α β} (hf : measurable f) (a : α) {s : set β} (hs : measurable_set s) :
a) s = s.indicator (λ (_x : β), 1) (f a)
@[protected, instance]
def probability_theory.kernel.is_markov_kernel_deterministic {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α β} (hf : measurable f) :
theorem probability_theory.kernel.lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : β ennreal} {g : α β} {a : α} (hg : measurable g) (hf : measurable f) :
∫⁻ (x : β), f x = f (g a)
@[simp]
theorem probability_theory.kernel.lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : β ennreal} {g : α β} {a : α} (hg : measurable g)  :
∫⁻ (x : β), f x = f (g a)
theorem probability_theory.kernel.set_lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : β ennreal} {g : α β} {a : α} (hg : measurable g) (hf : measurable f) {s : set β} (hs : measurable_set s) [decidable (g a s)] :
∫⁻ (x : β) in s, f x = ite (g a s) (f (g a)) 0
@[simp]
theorem probability_theory.kernel.set_lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : β ennreal} {g : α β} {a : α} (hg : measurable g) (s : set β) [decidable (g a s)] :
∫⁻ (x : β) in s, f x = ite (g a s) (f (g a)) 0
theorem probability_theory.kernel.integral_deterministic' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {E : Type u_3} [ E] {f : β E} {g : α β} {a : α} (hg : measurable g)  :
(x : β), f x = f (g a)
@[simp]
theorem probability_theory.kernel.integral_deterministic {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {E : Type u_3} [ E] {f : β E} {g : α β} {a : α} (hg : measurable g)  :
(x : β), f x = f (g a)
theorem probability_theory.kernel.set_integral_deterministic' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {E : Type u_3} [ E] {f : β E} {g : α β} {a : α} (hg : measurable g) {s : set β} (hs : measurable_set s) [decidable (g a s)] :
(x : β) in s, f x = ite (g a s) (f (g a)) 0
@[simp]
theorem probability_theory.kernel.set_integral_deterministic {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {E : Type u_3} [ E] {f : β E} {g : α β} {a : α} (hg : measurable g) (s : set β) [decidable (g a s)] :
(x : β) in s, f x = ite (g a s) (f (g a)) 0
def probability_theory.kernel.const (α : Type u_1) {β : Type u_2} {mβ : measurable_space β} (μβ : measure_theory.measure β) :

Constant kernel, which always returns the same measure.

Equations
• = λ (_x : α), μβ, _⟩
Instances for probability_theory.kernel.const
theorem probability_theory.kernel.const_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (μβ : measure_theory.measure β) (a : α) :
a = μβ
@[protected, instance]
@[protected, instance]
@[simp]
theorem probability_theory.kernel.lintegral_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : β ennreal} {μ : measure_theory.measure β} {a : α} :
∫⁻ (x : β), f x = ∫⁻ (x : β), f x μ
@[simp]
theorem probability_theory.kernel.set_lintegral_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : β ennreal} {μ : measure_theory.measure β} {a : α} {s : set β} :
∫⁻ (x : β) in s, f x = ∫⁻ (x : β) in s, f x μ
@[simp]
theorem probability_theory.kernel.integral_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {E : Type u_3} [ E] {f : β E} {μ : measure_theory.measure β} {a : α} :
(x : β), f x = (x : β), f x μ
@[simp]
theorem probability_theory.kernel.set_integral_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {E : Type u_3} [ E] {f : β E} {μ : measure_theory.measure β} {a : α} {s : set β} :
(x : β) in s, f x = (x : β) in s, f x μ
def probability_theory.kernel.of_fun_of_countable {α : Type u_1} {β : Type u_2} {mβ : measurable_space β} [countable α] (f : α ) :

In a countable space with measurable singletons, every function α → measure β defines a kernel.

Equations
@[protected]
noncomputable def probability_theory.kernel.restrict {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s : set β} (κ : ) (hs : measurable_set s) :

Kernel given by the restriction of the measures in the image of a kernel to a set.

Equations
Instances for probability_theory.kernel.restrict
theorem probability_theory.kernel.restrict_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s : set β} (κ : ) (hs : measurable_set s) (a : α) :
= (κ a).restrict s
theorem probability_theory.kernel.restrict_apply' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s t : set β} (κ : ) (hs : measurable_set s) (a : α) (ht : measurable_set t) :
a) t = (κ a) (t s)
@[simp]
theorem probability_theory.kernel.restrict_univ {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } :
@[simp]
theorem probability_theory.kernel.lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s : set β} (κ : ) (hs : measurable_set s) (a : α) (f : β ennreal) :
∫⁻ (b : β), f b = ∫⁻ (b : β) in s, f b κ a
@[simp]
theorem probability_theory.kernel.set_lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s : set β} (κ : ) (hs : measurable_set s) (a : α) (f : β ennreal) (t : set β) :
∫⁻ (b : β) in t, f b = ∫⁻ (b : β) in t s, f b κ a
@[simp]
theorem probability_theory.kernel.set_integral_restrict {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : } {s : set β} {E : Type u_3} [ E] {f : β E} {a : α} (hs : measurable_set s) (t : set β) :
(x : β) in t, f x = (x : β) in t s, f x κ a
@[protected, instance]
def probability_theory.kernel.is_finite_kernel.restrict {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s : set β} (κ : ) (hs : measurable_set s) :
@[protected, instance]
def probability_theory.kernel.is_s_finite_kernel.restrict {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s : set β} (κ : ) (hs : measurable_set s) :
noncomputable def probability_theory.kernel.comap_right {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} {f : γ β} (κ : ) (hf : measurable_embedding f) :

Kernel with value (κ a).comap f, for a measurable embedding f. That is, for a measurable set t : set β, comap_right κ hf a t = κ a (f '' t).

Equations
• = λ (a : α), , _⟩
Instances for probability_theory.kernel.comap_right
theorem probability_theory.kernel.comap_right_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} {f : γ β} (κ : ) (hf : measurable_embedding f) (a : α) :
=
theorem probability_theory.kernel.comap_right_apply' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} {f : γ β} (κ : ) (hf : measurable_embedding f) (a : α) {t : set γ} (ht : measurable_set t) :
a) t = (κ a) (f '' t)
theorem probability_theory.kernel.is_markov_kernel.comap_right {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} {f : γ β} (κ : ) (hf : measurable_embedding f) (hκ : (a : α), (κ a) (set.range f) = 1) :
@[protected, instance]
def probability_theory.kernel.is_finite_kernel.comap_right {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} {f : γ β} (κ : ) (hf : measurable_embedding f) :
@[protected, instance]
def probability_theory.kernel.is_s_finite_kernel.comap_right {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {γ : Type u_4} {mγ : measurable_space γ} {f : γ β} (κ : ) (hf : measurable_embedding f) :
def probability_theory.kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s : set α} [decidable_pred (λ (_x : α), _x s)] (hs : measurable_set s) (κ η : ) :

piecewise hs κ η is the kernel equal to κ on the measurable set s and to η on its complement.

Equations
Instances for probability_theory.kernel.piecewise
theorem probability_theory.kernel.piecewise_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)] (a : α) :
a = ite (a s) (κ a) (η a)
theorem probability_theory.kernel.piecewise_apply' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)] (a : α) (t : set β) :
( a) t = ite (a s) ((κ a) t) ((η a) t)
@[protected, instance]
def probability_theory.kernel.is_markov_kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)]  :
@[protected, instance]
def probability_theory.kernel.is_finite_kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)]  :
@[protected, instance]
def probability_theory.kernel.is_s_finite_kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)]  :
theorem probability_theory.kernel.lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)] (a : α) (g : β ennreal) :
∫⁻ (b : β), g b a = ite (a s) (∫⁻ (b : β), g b κ a) (∫⁻ (b : β), g b η a)
theorem probability_theory.kernel.set_lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)] (a : α) (g : β ennreal) (t : set β) :
∫⁻ (b : β) in t, g b a = ite (a s) (∫⁻ (b : β) in t, g b κ a) (∫⁻ (b : β) in t, g b η a)
theorem probability_theory.kernel.integral_piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)] {E : Type u_3} [ E] (a : α) (g : β E) :
(b : β), g b a = ite (a s) ( (b : β), g b κ a) ( (b : β), g b η a)
theorem probability_theory.kernel.set_integral_piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : } {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x s)] {E : Type u_3} [ E] (a : α) (g : β E) (t : set β) :
(b : β) in t, g b a = ite (a s) ( (b : β) in t, g b κ a) ( (b : β) in t, g b η a)