mathlib3 documentation

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) [measurable_space α] [measurable_space β] :

add_submonoid (α → measure_theory.measure β)

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

probability_theory.kernel.has_coe_to_fun

@[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 β} :

⇑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 α β)) :

⇑(κ + η) = ⇑κ + ⇑η

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

probability_theory.kernel.coe_add_hom α β = {to_fun := coe_fn probability_theory.kernel.has_coe_to_fun, map_zero' := _, map_add' := _}

@[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)

@[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

@[class]

structure probability_theory.is_finite_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ↥(probability_theory.kernel α β)) :

Prop

exists_univ_le : ∃ (C : ennreal), C < ⊤ ∧ ∀ (a : α), ⇑(⇑κ a) set.univ ≤ C

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 β} (κ : ↥(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).

Equations

probability_theory.is_finite_kernel.bound κ = probability_theory.is_finite_kernel.exists_univ_le.some

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 κ] :

probability_theory.is_finite_kernel.bound κ < ⊤

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 κ] :

probability_theory.is_finite_kernel.bound κ ≠ ⊤

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 β} :

probability_theory.is_finite_kernel 0

@[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 η] :

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

measure_theory.is_probability_measure (⇑κ 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 : α) :

measure_theory.is_finite_measure (⇑κ 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 κ] :

probability_theory.is_finite_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_iff {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : ↥(probability_theory.kernel α β)} :

κ = η ↔ ∀ (a : α), ⇑κ a = ⇑η a

theorem probability_theory.kernel.ext_iff' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : ↥(probability_theory.kernel α β)} :

κ = η ↔ ∀ (a : α) (s : set β), measurable_set s → ⇑(⇑κ a) s = ⇑(⇑η a) s

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

κ = η

theorem probability_theory.kernel.ext_fun_iff {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : ↥(probability_theory.kernel α β)} :

κ = η ↔ ∀ (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 α β)) :

measurable ⇑κ

@[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 α β)) :

↥(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) :

⇑(⇑(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 α β)) :

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.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

@[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 κ] :

probability_theory.is_s_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.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

probability_theory.kernel.seq κ = probability_theory.is_s_finite_kernel.tsum_finite.some

Instances for probability_theory.kernel.seq

probability_theory.kernel.is_finite_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.is_s_finite_kernel κ] :

probability_theory.kernel.sum (probability_theory.kernel.seq κ) = κ

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.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.is_s_finite_kernel κ] (n : ℕ) :

probability_theory.is_finite_kernel (probability_theory.kernel.seq κ 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.is_s_finite_kernel κ] [probability_theory.is_s_finite_kernel η] :

probability_theory.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.is_s_finite_kernel (κs i)) :

probability_theory.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.is_s_finite_kernel (κs n)) :

probability_theory.is_s_finite_kernel (probability_theory.kernel.sum κs)

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.is_s_finite_kernel (κs n)) :

probability_theory.is_s_finite_kernel (probability_theory.kernel.sum κs)

noncomputable def probability_theory.kernel.deterministic {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (f : α → β) (hf : measurable f) :

↥(probability_theory.kernel α β)

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

Equations

probability_theory.kernel.deterministic f hf = ⟨λ (a : α), measure_theory.measure.dirac (f a), _⟩

Instances for probability_theory.kernel.deterministic

probability_theory.kernel.is_markov_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 : α) :

⇑(probability_theory.kernel.deterministic f hf) a = measure_theory.measure.dirac (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 f 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) :

probability_theory.is_markov_kernel (probability_theory.kernel.deterministic f hf)

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 ∂⇑(probability_theory.kernel.deterministic g hg) a = 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) [measurable_singleton_class β] :

∫⁻ (x : β), f x ∂⇑(probability_theory.kernel.deterministic g hg) a = 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 ∂⇑(probability_theory.kernel.deterministic g hg) a = 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) [measurable_singleton_class β] (s : set β) [decidable (g a ∈ s)] :

∫⁻ (x : β) in s, f x ∂⇑(probability_theory.kernel.deterministic g hg) a = 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} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : β → E} {g : α → β} {a : α} (hg : measurable g) (hf : measure_theory.strongly_measurable f) :

∫ (x : β), f x ∂⇑(probability_theory.kernel.deterministic g hg) a = 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} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : β → E} {g : α → β} {a : α} (hg : measurable g) [measurable_singleton_class β] :

∫ (x : β), f x ∂⇑(probability_theory.kernel.deterministic g hg) a = 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} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : β → E} {g : α → β} {a : α} (hg : measurable g) (hf : measure_theory.strongly_measurable f) {s : set β} (hs : measurable_set s) [decidable (g a ∈ s)] :

∫ (x : β) in s, f x ∂⇑(probability_theory.kernel.deterministic g hg) a = 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} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : β → E} {g : α → β} {a : α} (hg : measurable g) [measurable_singleton_class β] (s : set β) [decidable (g a ∈ s)] :

∫ (x : β) in s, f x ∂⇑(probability_theory.kernel.deterministic g hg) a = ite (g a ∈ s) (f (g a)) 0

def probability_theory.kernel.const (α : Type u_1) {β : Type u_2} [measurable_space α] {mβ : measurable_space β} (μβ : measure_theory.measure β) :

↥(probability_theory.kernel α β)

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 μβ] :

probability_theory.is_finite_kernel (probability_theory.kernel.const α μβ)

@[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 μβ] :

probability_theory.is_markov_kernel (probability_theory.kernel.const α μβ)

@[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 ∂⇑(probability_theory.kernel.const α μ) a = ∫⁻ (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 ∂⇑(probability_theory.kernel.const α μ) a = ∫⁻ (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} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : β → E} {μ : measure_theory.measure β} {a : α} :

∫ (x : β), f x ∂⇑(probability_theory.kernel.const α μ) a = ∫ (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} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : β → E} {μ : measure_theory.measure β} {a : α} {s : set β} :

∫ (x : β) in s, f x ∂⇑(probability_theory.kernel.const α μ) a = ∫ (x : β) in s, f x ∂μ

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 β) :

↥(probability_theory.kernel α β)

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

Equations

probability_theory.kernel.of_fun_of_countable f = ⟨f, _⟩

@[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) :

↥(probability_theory.kernel α β)

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

⇑(⇑(probability_theory.kernel.restrict κ hs) a) t = ⇑(⇑κ a) (t ∩ s)

@[simp]

theorem probability_theory.kernel.restrict_univ {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : ↥(probability_theory.kernel α β)} :

probability_theory.kernel.restrict κ measurable_set.univ = κ

@[simp]

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

@[simp]

theorem probability_theory.kernel.set_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) (t : set β) :

∫⁻ (b : β) in t, f b ∂⇑(probability_theory.kernel.restrict κ hs) a = ∫⁻ (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 β} {κ : ↥(probability_theory.kernel α β)} {s : set β} {E : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : β → E} {a : α} (hs : measurable_set s) (t : set β) :

∫ (x : β) in t, f x ∂⇑(probability_theory.kernel.restrict κ hs) a = ∫ (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 β} (κ : ↥(probability_theory.kernel α β)) [probability_theory.is_finite_kernel κ] (hs : measurable_set s) :

probability_theory.is_finite_kernel (probability_theory.kernel.restrict κ hs)

@[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.is_s_finite_kernel κ] (hs : measurable_set s) :

probability_theory.is_s_finite_kernel (probability_theory.kernel.restrict κ hs)

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 : γ → β} (κ : ↥(probability_theory.kernel α β)) (hf : measurable_embedding f) :

↥(probability_theory.kernel α γ)

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

probability_theory.kernel.comap_right κ hf = ⟨λ (a : α), measure_theory.measure.comap f (⇑κ 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 : γ → β} (κ : ↥(probability_theory.kernel α β)) (hf : measurable_embedding f) (a : α) :

⇑(probability_theory.kernel.comap_right κ hf) a = measure_theory.measure.comap 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 : γ → β} (κ : ↥(probability_theory.kernel α β)) (hf : measurable_embedding f) (a : α) {t : set γ} (ht : measurable_set t) :

⇑(⇑(probability_theory.kernel.comap_right κ hf) 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 : γ → β} (κ : ↥(probability_theory.kernel α β)) (hf : measurable_embedding f) (hκ : ∀ (a : α), ⇑(⇑κ a) (set.range f) = 1) :

probability_theory.is_markov_kernel (probability_theory.kernel.comap_right κ hf)

@[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 : γ → β} (κ : ↥(probability_theory.kernel α β)) [probability_theory.is_finite_kernel κ] (hf : measurable_embedding f) :

probability_theory.is_finite_kernel (probability_theory.kernel.comap_right κ hf)

@[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 : γ → β} (κ : ↥(probability_theory.kernel α β)) [probability_theory.is_s_finite_kernel κ] (hf : measurable_embedding f) :

probability_theory.is_s_finite_kernel (probability_theory.kernel.comap_right κ hf)

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) (κ η : ↥(probability_theory.kernel α β)) :

↥(probability_theory.kernel α β)

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

Equations

probability_theory.kernel.piecewise hs κ η = ⟨λ (a : α), ite (a ∈ s) (⇑κ a) (⇑η a), _⟩

Instances for probability_theory.kernel.piecewise

theorem probability_theory.kernel.piecewise_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] (a : α) :

⇑(probability_theory.kernel.piecewise hs κ η) a = ite (a ∈ s) (⇑κ a) (⇑η a)

theorem probability_theory.kernel.piecewise_apply' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] (a : α) (t : set β) :

⇑(⇑(probability_theory.kernel.piecewise hs κ η) 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 β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] [probability_theory.is_markov_kernel κ] [probability_theory.is_markov_kernel η] :

probability_theory.is_markov_kernel (probability_theory.kernel.piecewise hs κ η)

@[protected, instance]

def probability_theory.kernel.is_finite_kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] [probability_theory.is_finite_kernel κ] [probability_theory.is_finite_kernel η] :

probability_theory.is_finite_kernel (probability_theory.kernel.piecewise hs κ η)

@[protected, instance]

def probability_theory.kernel.is_s_finite_kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] [probability_theory.is_s_finite_kernel κ] [probability_theory.is_s_finite_kernel η] :

probability_theory.is_s_finite_kernel (probability_theory.kernel.piecewise hs κ η)

theorem probability_theory.kernel.lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] (a : α) (g : β → ennreal) :

∫⁻ (b : β), g b ∂⇑(probability_theory.kernel.piecewise hs κ η) 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 β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] (a : α) (g : β → ennreal) (t : set β) :

∫⁻ (b : β) in t, g b ∂⇑(probability_theory.kernel.piecewise hs κ η) 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 β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] {E : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (a : α) (g : β → E) :

∫ (b : β), g b ∂⇑(probability_theory.kernel.piecewise hs κ η) 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 β} {κ η : ↥(probability_theory.kernel α β)} {s : set α} {hs : measurable_set s} [decidable_pred (λ (_x : α), _x ∈ s)] {E : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (a : α) (g : β → E) (t : set β) :

∫ (b : β) in t, g b ∂⇑(probability_theory.kernel.piecewise hs κ η) a = ite (a ∈ s) (∫ (b : β) in t, g b ∂⇑κ a) (∫ (b : β) in t, g b ∂⇑η a)