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:
kernel α β
: kernels fromα
toβ
, defined as theadd_submonoid
of the measurable functions inα → measure β
.is_markov_kernel κ
: a kernel fromα
toβ
is said to be a Markov kernel if for alla : α
,k a
is a probability measure.is_finite_kernel κ
: a kernel fromα
toβ
is said to be finite if there existsC : ℝ≥0∞
such thatC < ∞
and for alla : α
,κ 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.is_s_finite_kernel κ
: a kernel is called s-finite if it is a countable sum of finite kernels.
Particular kernels:
deterministic {f : α → β} (hf : measurable f)
: kernela ↦ measure.dirac (f a)
.const α (μβ : measure β)
: constant kernela ↦ μβ
.kernel.restrict κ (hs : measurable_set s)
: kernel for which the image ofa : α
is(κ a).restrict s
. Integral:∫⁻ b, f b ∂(kernel.restrict κ hs a) = ∫⁻ b in s, f b ∂(κ a)
kernel.with_density κ (f : α → β → ℝ≥0∞)
: kernela ↦ (κ a).with_density (f a)
. It is defined ifκ
is s-finite. Iff
is finite everywhere, then this is also an s-finite kernel. The class of s-finite kernels is the smallest class of kernels that contains finite kernels and which is stable bywith_density
. Integral:∫⁻ b, g b ∂(with_density κ f a) = ∫⁻ b, f a b * g b ∂(κ a)
Main statements #
-
ext_fun
: if∫⁻ b, f b ∂(κ a) = ∫⁻ b, f b ∂(η a)
for all measurable functionsf
and alla
, then the two kernelsκ
andη
are equal. -
measurable_lintegral
: the functiona ↦ ∫⁻ b, f a b ∂(κ a)
is measurable, for an s-finite kernelκ : kernel α β
and a functionf : α → β → ℝ≥0∞
such thatfunction.uncurry f
is measurable.
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
- probability_theory.kernel α β = {carrier := measurable measure_theory.measure.measurable_space, add_mem' := _, zero_mem' := _}
Instances for ↥probability_theory.kernel
Equations
- probability_theory.kernel.has_coe_to_fun = {coe := λ (κ : ↥(probability_theory.kernel α β)), κ.val}
Coercion to a function as an additive monoid homomorphism.
Equations
- is_probability_measure : ∀ (a : α), measure_theory.is_probability_measure (⇑κ a)
A kernel is a Markov kernel if every measure in its image is a probability measure.
Instances of this typeclass
- probability_theory.kernel.is_markov_kernel_deterministic
- probability_theory.kernel.is_markov_kernel_const
- probability_theory.kernel.is_markov_kernel.comp_prod
- probability_theory.kernel.is_markov_kernel.map
- probability_theory.kernel.is_markov_kernel.comap
- probability_theory.kernel.is_markov_kernel.prod_mk_left
- probability_theory.kernel.is_markov_kernel.swap_left
- probability_theory.kernel.is_markov_kernel.swap_right
- probability_theory.kernel.is_markov_kernel.fst
- probability_theory.kernel.is_markov_kernel.snd
- probability_theory.kernel.is_markov_kernel.comp
- probability_theory.kernel.is_markov_kernel.prod
A kernel is finite if every measure in its image is finite, with a uniform bound.
Instances of this typeclass
- probability_theory.is_markov_kernel.is_finite_kernel
- probability_theory.is_finite_kernel_zero
- probability_theory.is_finite_kernel.add
- probability_theory.kernel.is_finite_kernel_seq
- probability_theory.kernel.is_finite_kernel_const
- probability_theory.kernel.is_finite_kernel.restrict
- probability_theory.kernel.is_finite_kernel.comp_prod
- probability_theory.kernel.is_finite_kernel.map
- probability_theory.kernel.is_finite_kernel.comap
- probability_theory.kernel.is_finite_kernel.prod_mk_left
- probability_theory.kernel.is_finite_kernel.swap_left
- probability_theory.kernel.is_finite_kernel.swap_right
- probability_theory.kernel.is_finite_kernel.fst
- probability_theory.kernel.is_finite_kernel.snd
- probability_theory.kernel.is_finite_kernel.comp
- probability_theory.kernel.is_finite_kernel.prod
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
).
Sum of an indexed family of kernels.
Equations
- probability_theory.kernel.sum κ = ⟨λ (a : α), measure_theory.measure.sum (λ (n : ι), ⇑(κ n) a), _⟩
- tsum_finite : ∃ (κs : ℕ → ↥(probability_theory.kernel α β)), (∀ (n : ℕ), probability_theory.is_finite_kernel (κs n)) ∧ κ = probability_theory.kernel.sum κs
A kernel is s-finite if it can be written as the sum of countably many finite kernels.
Instances of this typeclass
- probability_theory.kernel.is_finite_kernel.is_s_finite_kernel
- probability_theory.kernel.is_s_finite_kernel.add
- probability_theory.kernel.is_s_finite_kernel.restrict
- probability_theory.kernel.with_density.is_s_finite_kernel
- probability_theory.kernel.is_s_finite_kernel.comp_prod
- probability_theory.kernel.is_s_finite_kernel.map
- probability_theory.kernel.is_s_finite_kernel.comap
- probability_theory.kernel.is_s_finite_kernel.prod_mk_left
- probability_theory.kernel.is_s_finite_kernel.swap_left
- probability_theory.kernel.is_s_finite_kernel.swap_right
- probability_theory.kernel.is_s_finite_kernel.fst
- probability_theory.kernel.is_s_finite_kernel.snd
- probability_theory.kernel.is_s_finite_kernel.comp
- probability_theory.kernel.is_s_finite_kernel.prod
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
Kernel which to a
associates the dirac measure at f a
. This is a Markov kernel.
Equations
- probability_theory.kernel.deterministic hf = ⟨λ (a : α), measure_theory.measure.dirac (f a), _⟩
Instances for probability_theory.kernel.deterministic
Constant kernel, which always returns the same measure.
Equations
- probability_theory.kernel.const α μβ = ⟨λ (_x : α), μβ, _⟩
Instances for probability_theory.kernel.const
In a countable space with measurable singletons, every function α → measure β
defines a
kernel.
Equations
Kernel given by the restriction of the measures in the image of a kernel to a set.
Equations
- probability_theory.kernel.restrict κ hs = ⟨λ (a : α), (⇑κ a).restrict s, _⟩
Instances for probability_theory.kernel.restrict
This is an auxiliary lemma for measurable_prod_mk_mem
.
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.
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
- probability_theory.kernel.with_density κ f = dite (measurable (function.uncurry f)) (λ (hf : measurable (function.uncurry f)), ⟨λ (a : α), (⇑κ a).with_density (f a), _⟩) (λ (hf : ¬measurable (function.uncurry f)), 0)
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.
For a s-finite kernel κ
and a function f : α → β → ℝ≥0
, with_density κ f
is s-finite.