Basic kernels #
This file contains basic results about kernels in general and definitions of some particular kernels.
Main definitions #
ProbabilityTheory.Kernel.deterministic (f : α → β) (hf : Measurable f)
: kernela ↦ Measure.dirac (f a)
.ProbabilityTheory.Kernel.id
: the identity kernel, deterministic kernel for the identity function.ProbabilityTheory.Kernel.copy α
: the deterministic kernel that mapsx : α
to the Dirac measure at(x, x) : α × α
.ProbabilityTheory.Kernel.discard α
: the Markov kernel to the typeUnit
.ProbabilityTheory.Kernel.swap α β
: the deterministic kernel that maps(x, y)
to the Dirac measure at(y, x)
.ProbabilityTheory.Kernel.const α (μβ : measure β)
: constant kernela ↦ μβ
.ProbabilityTheory.Kernel.restrict κ (hs : MeasurableSet s)
: kernel for which the image ofa : α
is(κ a).restrict s
. Integral:∫⁻ b, f b ∂(κ.restrict hs a) = ∫⁻ b in s, f b ∂(κ a)
ProbabilityTheory.Kernel.comapRight
: Kernel with value(κ a).comap f
, for a measurable embeddingf
. That is, for a measurable sett : Set β
,ProbabilityTheory.Kernel.comapRight κ hf a t = κ a (f '' t)
ProbabilityTheory.Kernel.piecewise (hs : MeasurableSet s) κ η
: the kernel equal toκ
on the measurable sets
and toη
on its complement.
Main statements #
Kernel which to a
associates the dirac measure at f a
. This is a Markov kernel.
Equations
- ProbabilityTheory.Kernel.deterministic f hf = { toFun := fun (a : α) => MeasureTheory.Measure.dirac (f a), measurable' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Alias of ProbabilityTheory.Kernel.setLIntegral_deterministic'
.
Alias of ProbabilityTheory.Kernel.setLIntegral_deterministic
.
The identity kernel, that maps x : α
to the Dirac measure at x
.
Equations
- ProbabilityTheory.Kernel.id = ProbabilityTheory.Kernel.deterministic id ⋯
Instances For
Equations
- ⋯ = ⋯
The deterministic kernel that maps x : α
to the Dirac measure at (x, x) : α × α
.
Equations
- ProbabilityTheory.Kernel.copy α = ProbabilityTheory.Kernel.deterministic (fun (x : α) => (x, x)) ⋯
Instances For
Equations
- ⋯ = ⋯
The Markov kernel to the Unit
type.
Equations
- ProbabilityTheory.Kernel.discard α = ProbabilityTheory.Kernel.deterministic (fun (x : α) => ()) ⋯
Instances For
Equations
- ⋯ = ⋯
The deterministic kernel that maps (x, y)
to the Dirac measure at (y, x)
.
Equations
- ProbabilityTheory.Kernel.swap α β = ProbabilityTheory.Kernel.deterministic Prod.swap ⋯
Instances For
Equations
- ⋯ = ⋯
See swap_apply'
for a fully applied version of this lemma.
See swap_apply
for a partially applied version of this lemma.
Constant kernel, which always returns the same measure.
Equations
- ProbabilityTheory.Kernel.const α μβ = { toFun := fun (x : α) => μβ, measurable' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
In a countable space with measurable singletons, every function α → MeasureTheory.Measure β
defines a kernel.
Equations
- ProbabilityTheory.Kernel.ofFunOfCountable f = { toFun := f, measurable' := ⋯ }
Instances For
Kernel given by the restriction of the measures in the image of a kernel to a set.
Equations
- κ.restrict hs = { toFun := fun (a : α) => (κ a).restrict s, measurable' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
- κ.comapRight hf = { toFun := fun (a : α) => MeasureTheory.Measure.comap f (κ a), measurable' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
ProbabilityTheory.Kernel.piecewise hs κ η
is the kernel equal to κ
on the measurable set s
and to η
on its complement.
Equations
- ProbabilityTheory.Kernel.piecewise hs κ η = { toFun := fun (a : α) => if a ∈ s then κ a else η a, measurable' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯