# Markov Kernels #

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

## Main definitions #

Classes of kernels:

• ProbabilityTheory.kernel α β: kernels from α to β, defined as the AddSubmonoid of the measurable functions in α → Measure β.
• ProbabilityTheory.IsMarkovKernel κ: a kernel from α to β is said to be a Markov kernel if for all a : α, k a is a probability measure.
• ProbabilityTheory.IsFiniteKernel κ: 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 a uniform bound. This stronger condition is necessary to ensure that the composition of two finite kernels is finite.
• ProbabilityTheory.IsSFiniteKernel κ: a kernel is called s-finite if it is a countable sum of finite kernels.

Particular kernels:

• ProbabilityTheory.kernel.deterministic (f : α → β) (hf : Measurable f): kernel a ↦ Measure.dirac (f a).
• ProbabilityTheory.kernel.const α (μβ : measure β): constant kernel a ↦ μβ.
• ProbabilityTheory.kernel.restrict κ (hs : MeasurableSet 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 #

• ProbabilityTheory.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.
noncomputable def ProbabilityTheory.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 MeasureTheory.Measure β is given by MeasureTheory.Measure.instMeasurableSpace. A map κ : α → MeasureTheory.Measure β is measurable iff ∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s).

Equations
• = { carrier := Measurable, add_mem' := , zero_mem' := }
Instances For
Equations
• ProbabilityTheory.instFunLikeSubtypeForallMeasureMemAddSubmonoidKernel = { coe := Subtype.val, coe_injective' := }
instance ProbabilityTheory.kernel.instCovariantAddLE {α : Type u_1} {β : Type u_2} [] [] :
CovariantClass (()) (()) (fun (x x_1 : ()) => x + x_1) fun (x x_1 : ()) => x x_1
Equations
• =
noncomputable instance ProbabilityTheory.kernel.instOrderBot {α : Type u_1} {β : Type u_2} [] [] :
Equations
• ProbabilityTheory.kernel.instOrderBot =
@[simp]
theorem ProbabilityTheory.kernel.coeFn_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } :
0 = 0
@[simp]
theorem ProbabilityTheory.kernel.coeFn_add {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (η : ()) :
(κ + η) = κ + η
def ProbabilityTheory.kernel.coeAddHom (α : Type u_4) (β : Type u_5) [] [] :
() →+

Coercion to a function as an additive monoid homomorphism.

Equations
• = ().subtype
Instances For
@[simp]
theorem ProbabilityTheory.kernel.zero_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (a : α) :
0 a = 0
@[simp]
theorem ProbabilityTheory.kernel.coe_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } (I : ) (κ : ι()) :
(I.sum fun (i : ι) => κ i) = I.sum fun (i : ι) => (κ i)
theorem ProbabilityTheory.kernel.finset_sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } (I : ) (κ : ι()) (a : α) :
(I.sum fun (i : ι) => κ i) a = I.sum fun (i : ι) => (κ i) a
theorem ProbabilityTheory.kernel.finset_sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } (I : ) (κ : ι()) (a : α) (s : Set β) :
((I.sum fun (i : ι) => κ i) a) s = I.sum fun (i : ι) => ((κ i) a) s
class ProbabilityTheory.IsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :

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

• isProbabilityMeasure : ∀ (a : α),
Instances
theorem ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} [self : ] (a : α) :
class ProbabilityTheory.IsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :

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

• exists_univ_le : C < , ∀ (a : α), (κ a) Set.univ C
Instances
theorem ProbabilityTheory.IsFiniteKernel.exists_univ_le {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} [self : ] :
C < , ∀ (a : α), (κ a) Set.univ C
noncomputable def ProbabilityTheory.IsFiniteKernel.bound {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :

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

Porting note (#11215): TODO: does it make sense to -- make ProbabilityTheory.IsFiniteKernel.bound the least possible bound? -- Should it be an NNReal number?

Equations
• = .choose
Instances For
theorem ProbabilityTheory.IsFiniteKernel.bound_lt_top {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
theorem ProbabilityTheory.IsFiniteKernel.bound_ne_top {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
theorem ProbabilityTheory.kernel.measure_le_bound {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (a : α) (s : Set β) :
instance ProbabilityTheory.isFiniteKernel_zero (α : Type u_4) (β : Type u_5) {mα : } {mβ : } :
Equations
• =
instance ProbabilityTheory.IsFiniteKernel.add {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (η : ()) :
Equations
• =
theorem ProbabilityTheory.isFiniteKernel_of_le {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} [hν : ] (hκν : κ ν) :
instance ProbabilityTheory.IsMarkovKernel.is_probability_measure' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} (a : α) :
Equations
• =
instance ProbabilityTheory.IsFiniteKernel.isFiniteMeasure {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} (a : α) :
Equations
• =
@[instance 100]
instance ProbabilityTheory.IsMarkovKernel.isFiniteKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} :
Equations
• =
theorem ProbabilityTheory.kernel.ext {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} (h : ∀ (a : α), κ a = η a) :
κ = η
theorem ProbabilityTheory.kernel.ext_iff {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} :
κ = η ∀ (a : α), κ a = η a
theorem ProbabilityTheory.kernel.ext_iff' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} :
κ = η ∀ (a : α) (s : Set β), (κ a) s = (η a) s
theorem ProbabilityTheory.kernel.ext_fun {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} (h : ∀ (a : α) (f : βENNReal), ∫⁻ (b : β), f bκ a = ∫⁻ (b : β), f bη a) :
κ = η
theorem ProbabilityTheory.kernel.ext_fun_iff {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} :
κ = η ∀ (a : α) (f : βENNReal), ∫⁻ (b : β), f bκ a = ∫⁻ (b : β), f bη a
theorem ProbabilityTheory.kernel.measurable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
theorem ProbabilityTheory.kernel.measurable_coe {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) {s : Set β} (hs : ) :
Measurable fun (a : α) => (κ a) s
theorem ProbabilityTheory.kernel.IsFiniteKernel.integrable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μ : ) (κ : ()) {s : Set β} (hs : ) :
MeasureTheory.Integrable (fun (x : α) => ((κ x) s).toReal) μ
theorem ProbabilityTheory.kernel.IsMarkovKernel.integrable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μ : ) (κ : ()) {s : Set β} (hs : ) :
MeasureTheory.Integrable (fun (x : α) => ((κ x) s).toReal) μ
noncomputable def ProbabilityTheory.kernel.sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (κ : ι()) :
()

Sum of an indexed family of kernels.

Equations
Instances For
theorem ProbabilityTheory.kernel.sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (κ : ι()) (a : α) :
= MeasureTheory.Measure.sum fun (n : ι) => (κ n) a
theorem ProbabilityTheory.kernel.sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (κ : ι()) (a : α) {s : Set β} (hs : ) :
() s = ∑' (n : ι), ((κ n) a) s
@[simp]
theorem ProbabilityTheory.kernel.sum_zero {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] :
(ProbabilityTheory.kernel.sum fun (x : ι) => 0) = 0
theorem ProbabilityTheory.kernel.sum_comm {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (κ : ιι()) :
(ProbabilityTheory.kernel.sum fun (n : ι) => ) = ProbabilityTheory.kernel.sum fun (m : ι) => ProbabilityTheory.kernel.sum fun (n : ι) => κ n m
@[simp]
theorem ProbabilityTheory.kernel.sum_fintype {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (κ : ι()) :
= Finset.univ.sum fun (i : ι) => κ i
theorem ProbabilityTheory.kernel.sum_add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (κ : ι()) (η : ι()) :
(ProbabilityTheory.kernel.sum fun (n : ι) => κ n + η n) =
class ProbabilityTheory.IsSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :

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

• tsum_finite : ∃ (κs : ()), (∀ (n : ), )
Instances
theorem ProbabilityTheory.IsSFiniteKernel.tsum_finite {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} [self : ] :
∃ (κs : ()), (∀ (n : ), )
@[instance 100]
instance ProbabilityTheory.kernel.IsFiniteKernel.isSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} :
Equations
• =
noncomputable def ProbabilityTheory.kernel.seq {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
()

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

Equations
• = .choose
Instances For
theorem ProbabilityTheory.kernel.kernel_sum_seq {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
theorem ProbabilityTheory.kernel.measure_sum_seq {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (a : α) :
(MeasureTheory.Measure.sum fun (n : ) => a) = κ a
instance ProbabilityTheory.kernel.isFiniteKernel_seq {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (n : ) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.sFinite {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} (a : α) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.add {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (η : ()) :
Equations
• =
theorem ProbabilityTheory.kernel.IsSFiniteKernel.finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } {κs : ι()} (I : ) (h : iI, ) :
ProbabilityTheory.IsSFiniteKernel (I.sum fun (i : ι) => κs i)
theorem ProbabilityTheory.kernel.isSFiniteKernel_sum_of_denumerable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] {κs : ι()} (hκs : ∀ (n : ι), ) :
theorem ProbabilityTheory.kernel.isSFiniteKernel_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] {κs : ι()} (hκs : ∀ (n : ι), ) :
noncomputable def ProbabilityTheory.kernel.deterministic {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (f : αβ) (hf : ) :
()

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

Equations
• = fun (a : α) => ,
Instances For
theorem ProbabilityTheory.kernel.deterministic_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβ} (hf : ) (a : α) :
theorem ProbabilityTheory.kernel.deterministic_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβ} (hf : ) (a : α) {s : Set β} (hs : ) :
() s = s.indicator (fun (x : β) => 1) (f a)
instance ProbabilityTheory.kernel.isMarkovKernel_deterministic {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβ} (hf : ) :
Equations
• =
theorem ProbabilityTheory.kernel.lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : βENNReal} {g : αβ} {a : α} (hg : ) (hf : ) :
∫⁻ (x : β), f x = f (g a)
@[simp]
theorem ProbabilityTheory.kernel.lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : βENNReal} {g : αβ} {a : α} (hg : ) :
∫⁻ (x : β), f x = f (g a)
theorem ProbabilityTheory.kernel.set_lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : βENNReal} {g : αβ} {a : α} (hg : ) (hf : ) {s : Set β} (hs : ) [Decidable (g a s)] :
∫⁻ (x : β) in s, f x = if g a s then f (g a) else 0
@[simp]
theorem ProbabilityTheory.kernel.set_lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : βENNReal} {g : αβ} {a : α} (hg : ) (s : Set β) [Decidable (g a s)] :
∫⁻ (x : β) in s, f x = if g a s then f (g a) else 0
theorem ProbabilityTheory.kernel.integral_deterministic' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] [] {f : βE} {g : αβ} {a : α} (hg : ) (hf : ) :
∫ (x : β), f x = f (g a)
@[simp]
theorem ProbabilityTheory.kernel.integral_deterministic {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] [] {f : βE} {g : αβ} {a : α} (hg : ) :
∫ (x : β), f x = f (g a)
theorem ProbabilityTheory.kernel.setIntegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] [] {f : βE} {g : αβ} {a : α} (hg : ) (hf : ) {s : Set β} (hs : ) [Decidable (g a s)] :
∫ (x : β) in s, f x = if g a s then f (g a) else 0
@[deprecated ProbabilityTheory.kernel.setIntegral_deterministic']
theorem ProbabilityTheory.kernel.set_integral_deterministic' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] [] {f : βE} {g : αβ} {a : α} (hg : ) (hf : ) {s : Set β} (hs : ) [Decidable (g a s)] :
∫ (x : β) in s, f x = if g a s then f (g a) else 0

Alias of ProbabilityTheory.kernel.setIntegral_deterministic'.

@[simp]
theorem ProbabilityTheory.kernel.setIntegral_deterministic {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] [] {f : βE} {g : αβ} {a : α} (hg : ) (s : Set β) [Decidable (g a s)] :
∫ (x : β) in s, f x = if g a s then f (g a) else 0
@[deprecated ProbabilityTheory.kernel.setIntegral_deterministic]
theorem ProbabilityTheory.kernel.set_integral_deterministic {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] [] {f : βE} {g : αβ} {a : α} (hg : ) (s : Set β) [Decidable (g a s)] :
∫ (x : β) in s, f x = if g a s then f (g a) else 0

Alias of ProbabilityTheory.kernel.setIntegral_deterministic.

def ProbabilityTheory.kernel.const (α : Type u_4) {β : Type u_5} [] :
{x : } →

Constant kernel, which always returns the same measure.

Equations
• = fun (x : α) => μβ,
Instances For
@[simp]
theorem ProbabilityTheory.kernel.const_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μβ : ) (a : α) :
a = μβ
@[simp]
theorem ProbabilityTheory.kernel.const_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } :
theorem ProbabilityTheory.kernel.const_add {α : Type u_1} {mα : } (β : Type u_4) [] (μ : ) (ν : ) :
theorem ProbabilityTheory.kernel.sum_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (μ : ) :
(ProbabilityTheory.kernel.sum fun (n : ι) => ) =
instance ProbabilityTheory.kernel.isFiniteKernel_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μβ : } :
Equations
• =
instance ProbabilityTheory.kernel.isSFiniteKernel_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μβ : } :
Equations
• =
instance ProbabilityTheory.kernel.isMarkovKernel_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μβ : } [hμβ : ] :
Equations
• =
@[simp]
theorem ProbabilityTheory.kernel.lintegral_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : βENNReal} {μ : } {a : α} :
∫⁻ (x : β), f x = ∫⁻ (x : β), f xμ
@[simp]
theorem ProbabilityTheory.kernel.set_lintegral_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : βENNReal} {μ : } {a : α} {s : Set β} :
∫⁻ (x : β) in s, f x = ∫⁻ (x : β) in s, f xμ
@[simp]
theorem ProbabilityTheory.kernel.integral_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] {f : βE} {μ : } {a : α} :
∫ (x : β), f x = ∫ (x : β), f xμ
@[simp]
theorem ProbabilityTheory.kernel.setIntegral_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] {f : βE} {μ : } {a : α} {s : Set β} :
∫ (x : β) in s, f x = ∫ (x : β) in s, f xμ
@[deprecated ProbabilityTheory.kernel.setIntegral_const]
theorem ProbabilityTheory.kernel.set_integral_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {E : Type u_4} [] {f : βE} {μ : } {a : α} {s : Set β} :
∫ (x : β) in s, f x = ∫ (x : β) in s, f xμ

Alias of ProbabilityTheory.kernel.setIntegral_const.

def ProbabilityTheory.kernel.ofFunOfCountable {α : Type u_1} {β : Type u_2} [] :
{x : } → [inst : ] → [inst : ] → ()()

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

Equations
Instances For
noncomputable def ProbabilityTheory.kernel.restrict {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {s : Set β} (κ : ()) (hs : ) :
()

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

Equations
• = fun (a : α) => (κ a).restrict s,
Instances For
theorem ProbabilityTheory.kernel.restrict_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {s : Set β} (κ : ()) (hs : ) (a : α) :
= (κ a).restrict s
theorem ProbabilityTheory.kernel.restrict_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {s : Set β} {t : Set β} (κ : ()) (hs : ) (a : α) (ht : ) :
() t = (κ a) (t s)
@[simp]
theorem ProbabilityTheory.kernel.restrict_univ {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} :
@[simp]
theorem ProbabilityTheory.kernel.lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {s : Set β} (κ : ()) (hs : ) (a : α) (f : βENNReal) :
∫⁻ (b : β), f b = ∫⁻ (b : β) in s, f bκ a
@[simp]
theorem ProbabilityTheory.kernel.set_lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {s : Set β} (κ : ()) (hs : ) (a : α) (f : βENNReal) (t : Set β) :
∫⁻ (b : β) in t, f b = ∫⁻ (b : β) in t s, f bκ a
@[simp]
theorem ProbabilityTheory.kernel.setIntegral_restrict {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {s : Set β} {E : Type u_4} [] {f : βE} {a : α} (hs : ) (t : Set β) :
∫ (x : β) in t, f x = ∫ (x : β) in t s, f xκ a
@[deprecated ProbabilityTheory.kernel.setIntegral_restrict]
theorem ProbabilityTheory.kernel.set_integral_restrict {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {s : Set β} {E : Type u_4} [] {f : βE} {a : α} (hs : ) (t : Set β) :
∫ (x : β) in t, f x = ∫ (x : β) in t s, f xκ a

Alias of ProbabilityTheory.kernel.setIntegral_restrict.

instance ProbabilityTheory.kernel.IsFiniteKernel.restrict {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {s : Set β} (κ : ()) (hs : ) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.restrict {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {s : Set β} (κ : ()) (hs : ) :
Equations
• =
noncomputable def ProbabilityTheory.kernel.comapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : γβ} (κ : ()) (hf : ) :
()

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

Equations
• = fun (a : α) => ,
Instances For
theorem ProbabilityTheory.kernel.comapRight_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : γβ} (κ : ()) (hf : ) (a : α) :
=
theorem ProbabilityTheory.kernel.comapRight_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : γβ} (κ : ()) (hf : ) (a : α) {t : Set γ} (ht : ) :
() t = (κ a) (f '' t)
@[simp]
theorem ProbabilityTheory.kernel.comapRight_id {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
theorem ProbabilityTheory.kernel.IsMarkovKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : γβ} (κ : ()) (hf : ) (hκ : ∀ (a : α), (κ a) () = 1) :
instance ProbabilityTheory.kernel.IsFiniteKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : γβ} (κ : ()) (hf : ) :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {γ : Type u_4} {mγ : } {f : γβ} (κ : ()) (hf : ) :
Equations
• =
def ProbabilityTheory.kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {s : Set α} [DecidablePred fun (x : α) => x s] (hs : ) (κ : ()) (η : ()) :
()

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

Equations
• = fun (a : α) => if a s then κ a else η a,
Instances For
theorem ProbabilityTheory.kernel.piecewise_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] (a : α) :
() a = if a s then κ a else η a
theorem ProbabilityTheory.kernel.piecewise_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] (a : α) (t : Set β) :
(() a) t = if a s then (κ a) t else (η a) t
instance ProbabilityTheory.kernel.IsMarkovKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] :
Equations
• =
instance ProbabilityTheory.kernel.IsFiniteKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] :
Equations
• =
instance ProbabilityTheory.kernel.IsSFiniteKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] :
Equations
• =
theorem ProbabilityTheory.kernel.lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] (a : α) (g : βENNReal) :
∫⁻ (b : β), g b() a = if a s then ∫⁻ (b : β), g bκ a else ∫⁻ (b : β), g bη a
theorem ProbabilityTheory.kernel.set_lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] (a : α) (g : βENNReal) (t : Set β) :
∫⁻ (b : β) in t, g b() a = if a s then ∫⁻ (b : β) in t, g bκ a else ∫⁻ (b : β) in t, g bη a
theorem ProbabilityTheory.kernel.integral_piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] {E : Type u_4} [] (a : α) (g : βE) :
∫ (b : β), g b() a = if a s then ∫ (b : β), g bκ a else ∫ (b : β), g bη a
theorem ProbabilityTheory.kernel.setIntegral_piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] {E : Type u_4} [] (a : α) (g : βE) (t : Set β) :
∫ (b : β) in t, g b() a = if a s then ∫ (b : β) in t, g bκ a else ∫ (b : β) in t, g bη a
@[deprecated ProbabilityTheory.kernel.setIntegral_piecewise]
theorem ProbabilityTheory.kernel.set_integral_piecewise {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {η : ()} {s : Set α} {hs : } [DecidablePred fun (x : α) => x s] {E : Type u_4} [] (a : α) (g : βE) (t : Set β) :
∫ (b : β) in t, g b() a = if a s then ∫ (b : β) in t, g bκ a else ∫ (b : β) in t, g bη a

Alias of ProbabilityTheory.kernel.setIntegral_piecewise.