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_submonoidof the measurable functions inα → measure β.is_markov_kernel κ: a kernel fromαtoβis said to be a Markov kernel if for alla : α,k ais 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. Iffis 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 functionsfand 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 fis measurable.
def
probability_theory.kernel
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
[measurable_space β] :
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
@[protected, instance]
def
probability_theory.kernel.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β] :
has_coe_to_fun ↥(probability_theory.kernel α β) (λ (_x : ↥(probability_theory.kernel α β)), α → measure_theory.measure β)
Equations
- probability_theory.kernel.has_coe_to_fun = {coe := λ (κ : ↥(probability_theory.kernel α β)), κ.val}
@[simp]
theorem
probability_theory.kernel.coe_fn_zero
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β} :
@[simp]
theorem
probability_theory.kernel.coe_fn_add
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ η : ↥(probability_theory.kernel α β)) :
def
probability_theory.kernel.coe_add_hom
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
[measurable_space β] :
↥(probability_theory.kernel α β) →+ α → measure_theory.measure β
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 : α) :
@[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 α β)) :
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 : α) :
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 β) :
@[class]
structure
probability_theory.is_markov_kernel
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β)) :
Prop
- 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
@[class]
structure
probability_theory.is_finite_kernel
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β)) :
Prop
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
noncomputable
def
probability_theory.is_finite_kernel.bound
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[h : probability_theory.is_finite_kernel κ] :
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).
theorem
probability_theory.is_finite_kernel.bound_lt_top
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[h : probability_theory.is_finite_kernel κ] :
theorem
probability_theory.is_finite_kernel.bound_ne_top
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[h : probability_theory.is_finite_kernel κ] :
theorem
probability_theory.kernel.measure_le_bound
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[h : probability_theory.is_finite_kernel κ]
(a : α)
(s : set β) :
⇑(⇑κ a) s ≤ probability_theory.is_finite_kernel.bound κ
@[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 β}
(κ η : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
[probability_theory.is_finite_kernel η] :
@[protected, instance]
def
probability_theory.is_markov_kernel.is_probability_measure'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{κ : ↥(probability_theory.kernel α β)}
[h : probability_theory.is_markov_kernel κ]
(a : α) :
@[protected, instance]
def
probability_theory.is_finite_kernel.is_finite_measure
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{κ : ↥(probability_theory.kernel α β)}
[h : probability_theory.is_finite_kernel κ]
(a : α) :
@[protected, instance]
def
probability_theory.is_markov_kernel.is_finite_kernel
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{κ : ↥(probability_theory.kernel α β)}
[h : probability_theory.is_markov_kernel κ] :
@[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
- probability_theory.kernel.sum κ = ⟨λ (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 ι]
(κ : ι → ↥(probability_theory.kernel α β))
(a : α) :
⇑(probability_theory.kernel.sum κ) 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 ι]
(κ : ι → ↥(probability_theory.kernel α β))
(a : α)
{s : set β}
(hs : measurable_set 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 α β)) :
probability_theory.kernel.sum (λ (n : ι), probability_theory.kernel.sum (κ n)) = probability_theory.kernel.sum (λ (m : ι), probability_theory.kernel.sum (λ (n : ι), κ n m))
@[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 α β)) :
probability_theory.kernel.sum κ = 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 α β)) :
probability_theory.kernel.sum (λ (n : ι), κ n + η n) = probability_theory.kernel.sum κ + probability_theory.kernel.sum η
@[class]
structure
probability_theory.kernel.is_s_finite_kernel
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β)) :
Prop
- 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
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.is_s_finite_kernel
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{κ : ↥(probability_theory.kernel α β)}
[h : probability_theory.is_finite_kernel κ] :
noncomputable
def
probability_theory.kernel.seq
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[h : probability_theory.kernel.is_s_finite_kernel κ] :
ℕ → ↥(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.kernel_sum_seq
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[h : probability_theory.kernel.is_s_finite_kernel κ] :
theorem
probability_theory.kernel.measure_sum_seq
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[h : probability_theory.kernel.is_s_finite_kernel κ]
(a : α) :
measure_theory.measure.sum (λ (n : ℕ), ⇑(probability_theory.kernel.seq κ n) a) = ⇑κ a
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel_seq
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[h : probability_theory.kernel.is_s_finite_kernel κ]
(n : ℕ) :
@[protected, instance]
def
probability_theory.kernel.is_s_finite_kernel.add
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ η : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
[probability_theory.kernel.is_s_finite_kernel η] :
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)) :
probability_theory.kernel.is_s_finite_kernel (I.sum (λ (i : ι), κs 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 : ι → ↥(probability_theory.kernel α β)}
(hκs : ∀ (n : ι), probability_theory.kernel.is_s_finite_kernel (κ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 : ι → ↥(probability_theory.kernel α β)}
(hκs : ∀ (n : ι), probability_theory.kernel.is_s_finite_kernel (κ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
- probability_theory.kernel.deterministic hf = ⟨λ (a : α), measure_theory.measure.dirac (f 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) :
⇑(⇑(probability_theory.kernel.deterministic hf) 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) :
def
probability_theory.kernel.const
(α : Type u_1)
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(μβ : measure_theory.measure β) :
Constant kernel, which always returns the same measure.
Equations
- probability_theory.kernel.const α μβ = ⟨λ (_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 : α) :
⇑(probability_theory.kernel.const α μβ) a = μβ
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel_const
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{μβ : measure_theory.measure β}
[hμβ : measure_theory.is_finite_measure μβ] :
@[protected, instance]
def
probability_theory.kernel.is_markov_kernel_const
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{μβ : measure_theory.measure β}
[hμβ : measure_theory.is_probability_measure μβ] :
def
probability_theory.kernel.of_fun_of_countable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
[countable α]
[measurable_singleton_class α]
(f : α → measure_theory.measure β) :
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
- probability_theory.kernel.restrict κ hs = ⟨λ (a : α), (⇑κ a).restrict s, _⟩
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 : α) :
⇑(probability_theory.kernel.restrict κ hs) 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 β}
(κ : ↥(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) :
@[protected, instance]
def
probability_theory.kernel.is_finite_kernel.restrict
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{s : set β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
(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 β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(hs : measurable_set s) :
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) :
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) :
noncomputable
def
probability_theory.kernel.with_density
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(f : α → β → ennreal) :
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
theorem
probability_theory.kernel.with_density_of_not_measurable
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{f : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(hf : ¬measurable (function.uncurry f)) :
@[protected]
theorem
probability_theory.kernel.with_density_apply
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{f : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(hf : measurable (function.uncurry f))
(a : α) :
⇑(probability_theory.kernel.with_density κ f) a = (⇑κ a).with_density (f a)
theorem
probability_theory.kernel.with_density_apply'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{f : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(hf : measurable (function.uncurry f))
(a : α)
{s : set β}
(hs : measurable_set s) :
theorem
probability_theory.kernel.lintegral_with_density
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{f : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(hf : measurable (function.uncurry f))
(a : α)
{g : β → ennreal}
(hg : measurable g) :
theorem
probability_theory.kernel.with_density_add_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ η : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
[probability_theory.kernel.is_s_finite_kernel η]
(f : α → β → ennreal) :
theorem
probability_theory.kernel.with_density_kernel_sum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : measurable_space α}
{mβ : measurable_space β}
[countable ι]
(κ : ι → ↥(probability_theory.kernel α β))
(hκ : ∀ (i : ι), probability_theory.kernel.is_s_finite_kernel (κ i))
(f : α → β → ennreal) :
theorem
probability_theory.kernel.with_density_tsum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : measurable_space α}
{mβ : measurable_space β}
[countable ι]
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
{f : ι → α → β → ennreal}
(hf : ∀ (i : ι), measurable (function.uncurry (f i))) :
probability_theory.kernel.with_density κ (∑' (n : ι), f n) = probability_theory.kernel.sum (λ (n : ι), probability_theory.kernel.with_density κ (f n))
theorem
probability_theory.kernel.is_finite_kernel_with_density_of_bounded
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{f : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
{B : ennreal}
(hB_top : B ≠ ⊤)
(hf_B : ∀ (a : α) (b : β), f a b ≤ B) :
If a kernel κ is finite and a function f : α → β → ℝ≥0∞ is bounded, then with_density κ f
is finite.
theorem
probability_theory.kernel.is_s_finite_kernel_with_density_of_is_finite_kernel
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{f : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
(hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤) :
Auxiliary lemma for is_s_finite_kernel_with_density.
If a kernel κ is finite, then with_density κ f is s-finite.
theorem
probability_theory.kernel.is_s_finite_kernel.with_density
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
{f : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤) :
For a s-finite kernel κ and a function f : α → β → ℝ≥0∞ which is everywhere finite,
with_density κ f is s-finite.
@[protected, instance]
def
probability_theory.kernel.with_density.is_s_finite_kernel
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(f : α → β → nnreal) :
probability_theory.kernel.is_s_finite_kernel (probability_theory.kernel.with_density κ (λ (a : α) (b : β), ↑(f a b)))
For a s-finite kernel κ and a function f : α → β → ℝ≥0, with_density κ f is s-finite.