mathlib documentation

probability.kernel.basic

Markov Kernels #

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:

Particular kernels:

Main statements #

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
@[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 β} (κ η : (probability_theory.kernel α β)) :
+ η) = κ + η
@[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 ι) (κ : ι (probability_theory.kernel α β)) :
(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 ι) (κ : ι (probability_theory.kernel α β)) (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 ι) (κ : ι (probability_theory.kernel α β)) (a : α) (s : set β) :
((I.sum (λ (i : ι), κ i)) a) s = I.sum (λ (i : ι), ((κ i) a) s)

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
@[protected, instance]
@[ext]
theorem probability_theory.kernel.ext {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : (probability_theory.kernel α β)} (h : (a : α), κ a = η a) :
κ = η
theorem probability_theory.kernel.ext_fun {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : (probability_theory.kernel α β)} (h : (a : α) (f : β ennreal), measurable f ∫⁻ (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 β} (κ : (probability_theory.kernel α β)) :
@[protected]
theorem probability_theory.kernel.measurable_coe {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) {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 ι] (κ : ι (probability_theory.kernel α β)) :

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 ι] (κ : ι (probability_theory.kernel α β)) (a : α) :
theorem probability_theory.kernel.sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] (κ : ι (probability_theory.kernel α β)) (a : α) {s : set β} (hs : measurable_set s) :
((probability_theory.kernel.sum κ) a) 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 ι] (κ : ι ι (probability_theory.kernel α β)) :
@[simp]
theorem probability_theory.kernel.sum_fintype {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [fintype ι] (κ : ι (probability_theory.kernel α β)) :

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.is_s_finite_kernel.finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {κs : ι (probability_theory.kernel α β)} (I : finset ι) (h : (i : ι), i I probability_theory.kernel.is_s_finite_kernel (κs i)) :
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
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 : α) {s : set β} (hs : measurable_set s) :
((probability_theory.kernel.deterministic hf) a) s = s.indicator (λ (_x : β), 1) (f a)

Constant kernel, which always returns the same measure.

Equations
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 : α) :

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 β} (κ : (probability_theory.kernel α β)) (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 β} (κ : (probability_theory.kernel α β)) (hs : measurable_set s) (a : α) :
theorem probability_theory.kernel.restrict_apply' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s t : set β} (κ : (probability_theory.kernel α β)) (hs : measurable_set s) (a : α) (ht : measurable_set t) :
theorem probability_theory.kernel.lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {s : set β} (κ : (probability_theory.kernel α β)) (hs : measurable_set s) (a : α) (f : β ennreal) :
∫⁻ (b : β), f b (probability_theory.kernel.restrict κ hs) a = ∫⁻ (b : β) in s, f b κ a
theorem probability_theory.kernel.measurable_prod_mk_mem_of_finite {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) {t : set × β)} (ht : measurable_set t) (hκs : (a : α), measure_theory.is_finite_measure (κ a)) :
measurable (λ (a : α), (κ a) {b : β | (a, b) t})

This is an auxiliary lemma for measurable_prod_mk_mem.

theorem probability_theory.kernel.measurable_prod_mk_mem {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) [probability_theory.kernel.is_s_finite_kernel κ] {t : set × β)} (ht : measurable_set t) :
measurable (λ (a : α), (κ a) {b : β | (a, b) t})
theorem probability_theory.kernel.measurable_lintegral_indicator_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) [probability_theory.kernel.is_s_finite_kernel κ] {t : set × β)} (ht : measurable_set t) (c : ennreal) :
measurable (λ (a : α), ∫⁻ (b : β), t.indicator (function.const × β) c) (a, b) κ a)
theorem probability_theory.kernel.measurable_lintegral {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) [probability_theory.kernel.is_s_finite_kernel κ] {f : α β ennreal} (hf : measurable (function.uncurry f)) :
measurable (λ (a : α), ∫⁻ (b : β), f a b κ a)

For an s-finite kernel κ and a function f : α → β → ℝ≥0∞ which is measurable when seen as a map from α × β (hypothesis measurable (function.uncurry f)), the integral a ↦ ∫⁻ b, f a b ∂(κ a) is measurable.

theorem probability_theory.kernel.measurable_lintegral' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) [probability_theory.kernel.is_s_finite_kernel κ] {f : β ennreal} (hf : measurable f) :
measurable (λ (a : α), ∫⁻ (b : β), f b κ a)
theorem probability_theory.kernel.measurable_set_lintegral {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) [probability_theory.kernel.is_s_finite_kernel κ] {f : α β ennreal} (hf : measurable (function.uncurry f)) {s : set β} (hs : measurable_set s) :
measurable (λ (a : α), ∫⁻ (b : β) in s, f a b κ a)
theorem probability_theory.kernel.measurable_set_lintegral' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) [probability_theory.kernel.is_s_finite_kernel κ] {f : β ennreal} (hf : measurable f) {s : set β} (hs : measurable_set s) :
measurable (λ (a : α), ∫⁻ (b : β) in s, f b κ a)

Kernel with image a).with_density (f a) if function.uncurry f is measurable, and with image 0 otherwise. If function.uncurry f is measurable, it satisfies ∫⁻ b, g b ∂(with_density κ f hf a) = ∫⁻ b, f a b * g b ∂(κ a).

Equations
Instances for probability_theory.kernel.with_density

If a kernel κ is finite and a function f : α → β → ℝ≥0∞ is bounded, then with_density κ f is finite.

Auxiliary lemma for is_s_finite_kernel_with_density. If a kernel κ is finite, then with_density κ f is s-finite.

For a s-finite kernel κ and a function f : α → β → ℝ≥0∞ which is everywhere finite, with_density κ f is s-finite.

@[protected, instance]

For a s-finite kernel κ and a function f : α → β → ℝ≥0, with_density κ f is s-finite.