# 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)`: kernel `a ↦ Measure.dirac (f a)`.
- `ProbabilityTheory.Kernel.id`: the identity kernel, deterministic kernel for the identity function.
- `ProbabilityTheory.Kernel.copy α`: the deterministic kernel that maps `x : α` to the Dirac measure at `(x, x) : α × α`.
- `ProbabilityTheory.Kernel.discard α`: the Markov kernel to the type `Unit`.
- `ProbabilityTheory.Kernel.swap α β`: the deterministic kernel that maps `(x, y)` to the Dirac measure at `(y, x)`.
- `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 ∂(κ.restrict hs a) = ∫⁻ b in s, f b ∂(κ a)`
- `ProbabilityTheory.Kernel.comapRight`: 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)`
- `ProbabilityTheory.Kernel.piecewise (hs : MeasurableSet s) κ η`: the kernel equal to `κ` on the measurable set `s` and to `η` on its complement.

## Main statements #

source
noncomputable def ProbabilityTheory.Kernel.deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) (hf : Measurable f) :
Kernel α β

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

source
theorem ProbabilityTheory.Kernel.deterministic_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) (a : α) :
(deterministic f hf) a = MeasureTheory.Measure.dirac (f a)
source
theorem ProbabilityTheory.Kernel.deterministic_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) (a : α) {s : Set β} (hs : MeasurableSet s) :
((deterministic f hf) a) s = s.indicator (fun (x : β) => 1) (f a)
source
theorem ProbabilityTheory.Kernel.deterministic_congr {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f g : α → β} {hf : Measurable f} (h : f = g) :
deterministic f hf = deterministic g ⋯

Because of the measurability field in `Kernel.deterministic`, `rw [h]` will not rewrite `deterministic f hf` to `deterministic g ⋯`. Instead one can do `rw [deterministic_congr h]`.

source
instance ProbabilityTheory.Kernel.isMarkovKernel_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) :
IsMarkovKernel (deterministic f hf)
source
theorem ProbabilityTheory.Kernel.lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α} (hg : Measurable g) (hf : Measurable f) :
∫⁻ (x : β), f x ∂(deterministic g hg) a = f (g a)
source
@[simp]
theorem ProbabilityTheory.Kernel.lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] :
∫⁻ (x : β), f x ∂(deterministic g hg) a = f (g a)
source
theorem ProbabilityTheory.Kernel.setLIntegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α} (hg : Measurable g) (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) [Decidable (g a ∈ s)] :
∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0
source
@[simp]
theorem ProbabilityTheory.Kernel.setLIntegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] (s : Set β) [Decidable (g a ∈ s)] :
∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0
source
noncomputable def ProbabilityTheory.Kernel.id {α : Type u_1} {mα : MeasurableSpace α} :
Kernel α α

The identity kernel, that maps `x : α` to the Dirac measure at `x`.

Equations

- ProbabilityTheory.Kernel.id = ProbabilityTheory.Kernel.deterministic id ⋯

Instances For

source
instance ProbabilityTheory.Kernel.instIsMarkovKernelId {α : Type u_1} {mα : MeasurableSpace α} :
IsMarkovKernel Kernel.id
source
theorem ProbabilityTheory.Kernel.id_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) :
Kernel.id a = MeasureTheory.Measure.dirac a
source
theorem ProbabilityTheory.Kernel.lintegral_id' {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal} (hf : Measurable f) (a : α) :
∫⁻ (a : α), f a ∂Kernel.id a = f a
source
theorem ProbabilityTheory.Kernel.lintegral_id {α : Type u_1} {mα : MeasurableSpace α} [MeasurableSingletonClass α] {f : α → ENNReal} (a : α) :
∫⁻ (a : α), f a ∂Kernel.id a = f a
source
noncomputable def ProbabilityTheory.Kernel.copy (α : Type u_4) [MeasurableSpace α] :
Kernel α (α × α)

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

source
instance ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy {α : Type u_1} {mα : MeasurableSpace α} :
IsMarkovKernel (copy α)
source
theorem ProbabilityTheory.Kernel.copy_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) :
(copy α) a = MeasureTheory.Measure.dirac (a, a)
source
noncomputable def ProbabilityTheory.Kernel.discard (α : Type u_4) [MeasurableSpace α] :
Kernel α Unit

The Markov kernel to the `Unit` type.

Equations

- ProbabilityTheory.Kernel.discard α = ProbabilityTheory.Kernel.deterministic (fun (x : α) => ()) ⋯

Instances For

source
instance ProbabilityTheory.Kernel.instIsMarkovKernelUnitDiscard {α : Type u_1} {mα : MeasurableSpace α} :
IsMarkovKernel (discard α)
source
@[simp]
theorem ProbabilityTheory.Kernel.discard_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) :
(discard α) a = MeasureTheory.Measure.dirac ()
source
noncomputable def ProbabilityTheory.Kernel.swap (α : Type u_4) (β : Type u_5) [MeasurableSpace α] [MeasurableSpace β] :
Kernel (α × β) (β × α)

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

source
instance ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
IsMarkovKernel (swap α β)
source
theorem ProbabilityTheory.Kernel.swap_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (ab : α × β) :
(swap α β) ab = MeasureTheory.Measure.dirac ab.swap

See `swap_apply'` for a fully applied version of this lemma.

source
theorem ProbabilityTheory.Kernel.swap_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (ab : α × β) {s : Set (β × α)} (hs : MeasurableSet s) :
((swap α β) ab) s = s.indicator 1 ab.swap

See `swap_apply` for a partially applied version of this lemma.

source
def ProbabilityTheory.Kernel.const (α : Type u_4) {β : Type u_5} [MeasurableSpace α] {x✝ : MeasurableSpace β} (μβ : MeasureTheory.Measure β) :
Kernel α β

Constant kernel, which always returns the same measure.

Equations

- ProbabilityTheory.Kernel.const α μβ = { toFun := fun (x : α) => μβ, measurable' := ⋯ }

Instances For

source
@[simp]
theorem ProbabilityTheory.Kernel.const_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μβ : MeasureTheory.Measure β) (a : α) :
(const α μβ) a = μβ
source
@[simp]
theorem ProbabilityTheory.Kernel.const_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
const α 0 = 0
source
theorem ProbabilityTheory.Kernel.const_add {α : Type u_1} {mα : MeasurableSpace α} (β : Type u_4) [MeasurableSpace β] (μ ν : MeasureTheory.Measure α) :
const β (μ + ν) = const β μ + const β ν
source
theorem ProbabilityTheory.Kernel.sum_const {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (μ : ι → MeasureTheory.Measure β) :
(Kernel.sum fun (n : ι) => const α (μ n)) = const α (MeasureTheory.Measure.sum μ)
source
instance ProbabilityTheory.Kernel.const.instIsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure μβ] :
IsFiniteKernel (const α μβ)
source
instance ProbabilityTheory.Kernel.const.instIsSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [MeasureTheory.SFinite μβ] :
IsSFiniteKernel (const α μβ)
source
instance ProbabilityTheory.Kernel.const.instIsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [hμβ : MeasureTheory.IsProbabilityMeasure μβ] :
IsMarkovKernel (const α μβ)
source
instance ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [hμβ : MeasureTheory.IsZeroOrProbabilityMeasure μβ] :
IsZeroOrMarkovKernel (const α μβ)
source
theorem ProbabilityTheory.Kernel.isSFiniteKernel_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α] {μβ : MeasureTheory.Measure β} :
IsSFiniteKernel (const α μβ) ↔ MeasureTheory.SFinite μβ
source
instance ProbabilityTheory.Kernel.instNonemptySubtypeIsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty β] :
Nonempty { κ : Kernel α β // IsMarkovKernel κ }
source
@[simp]
theorem ProbabilityTheory.Kernel.lintegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {μ : MeasureTheory.Measure β} {a : α} :
∫⁻ (x : β), f x ∂(const α μ) a = ∫⁻ (x : β), f x ∂μ
source
@[simp]
theorem ProbabilityTheory.Kernel.setLIntegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {μ : MeasureTheory.Measure β} {a : α} {s : Set β} :
∫⁻ (x : β) in s, f x ∂(const α μ) a = ∫⁻ (x : β) in s, f x ∂μ
source
theorem ProbabilityTheory.Kernel.discard_eq_const {α : Type u_1} {mα : MeasurableSpace α} :
discard α = const α (MeasureTheory.Measure.dirac ())
source
def ProbabilityTheory.Kernel.ofFunOfCountable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {x✝ : MeasurableSpace β} [Countable α] [MeasurableSingletonClass α] (f : α → MeasureTheory.Measure β) :
Kernel α β

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

Equations

- ProbabilityTheory.Kernel.ofFunOfCountable f = { toFun := f, measurable' := ⋯ }

Instances For

source
noncomputable def ProbabilityTheory.Kernel.restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : Kernel α β) (hs : MeasurableSet s) :
Kernel α β

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

source
theorem ProbabilityTheory.Kernel.restrict_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : Kernel α β) (hs : MeasurableSet s) (a : α) :
(κ.restrict hs) a = (κ a).restrict s
source
theorem ProbabilityTheory.Kernel.restrict_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s t : Set β} (κ : Kernel α β) (hs : MeasurableSet s) (a : α) (ht : MeasurableSet t) :
((κ.restrict hs) a) t = (κ a) (t ∩ s)
source
@[simp]
theorem ProbabilityTheory.Kernel.restrict_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} :
κ.restrict ⋯ = κ
source
@[simp]
theorem ProbabilityTheory.Kernel.lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : Kernel α β) (hs : MeasurableSet s) (a : α) (f : β → ENNReal) :
∫⁻ (b : β), f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in s, f b ∂κ a
source
@[simp]
theorem ProbabilityTheory.Kernel.setLIntegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : Kernel α β) (hs : MeasurableSet s) (a : α) (f : β → ENNReal) (t : Set β) :
∫⁻ (b : β) in t, f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in t ∩ s, f b ∂κ a
source
instance ProbabilityTheory.Kernel.IsFiniteKernel.restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : Kernel α β) [IsFiniteKernel κ] (hs : MeasurableSet s) :
IsFiniteKernel (κ.restrict hs)
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : Kernel α β) [IsSFiniteKernel κ] (hs : MeasurableSet s) :
IsSFiniteKernel (κ.restrict hs)
source
noncomputable def ProbabilityTheory.Kernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : Kernel α β) (hf : MeasurableEmbedding f) :
Kernel α γ

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

source
theorem ProbabilityTheory.Kernel.comapRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : Kernel α β) (hf : MeasurableEmbedding f) (a : α) :
(κ.comapRight hf) a = MeasureTheory.Measure.comap f (κ a)
source
theorem ProbabilityTheory.Kernel.comapRight_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : Kernel α β) (hf : MeasurableEmbedding f) (a : α) {t : Set γ} (ht : MeasurableSet t) :
((κ.comapRight hf) a) t = (κ a) (f '' t)
source
@[simp]
theorem ProbabilityTheory.Kernel.comapRight_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) :
κ.comapRight ⋯ = κ
source
theorem ProbabilityTheory.Kernel.IsMarkovKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : Kernel α β) (hf : MeasurableEmbedding f) (hκ : ∀ (a : α), (κ a) (Set.range f) = 1) :
IsMarkovKernel (κ.comapRight hf)
source
instance ProbabilityTheory.Kernel.IsFiniteKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : Kernel α β) [IsFiniteKernel κ] (hf : MeasurableEmbedding f) :
IsFiniteKernel (κ.comapRight hf)
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : Kernel α β) [IsSFiniteKernel κ] (hf : MeasurableEmbedding f) :
IsSFiniteKernel (κ.comapRight hf)
source
def ProbabilityTheory.Kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) (κ η : Kernel α β) :
Kernel α β

`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

source
theorem ProbabilityTheory.Kernel.piecewise_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) :
(piecewise hs κ η) a = if a ∈ s then κ a else η a
source
theorem ProbabilityTheory.Kernel.piecewise_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) (t : Set β) :
((piecewise hs κ η) a) t = if a ∈ s then (κ a) t else (η a) t
source
instance ProbabilityTheory.Kernel.IsMarkovKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] [IsMarkovKernel κ] [IsMarkovKernel η] :
IsMarkovKernel (Kernel.piecewise hs κ η)
source
instance ProbabilityTheory.Kernel.IsFiniteKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] [IsFiniteKernel κ] [IsFiniteKernel η] :
IsFiniteKernel (Kernel.piecewise hs κ η)
source
instance ProbabilityTheory.Kernel.IsSFiniteKernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
IsSFiniteKernel (piecewise hs κ η)
source
theorem ProbabilityTheory.Kernel.lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) (g : β → ENNReal) :
∫⁻ (b : β), g b ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a
source
theorem ProbabilityTheory.Kernel.setLIntegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x ∈ s] (a : α) (g : β → ENNReal) (t : Set β) :
∫⁻ (b : β) in t, g b ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a
source
theorem ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} {μ : MeasureTheory.Measure α} (h : ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)) (h' : μ ≠ 0) :
∃ (η : Kernel α β), ⇑κ =ᵐ[μ] ⇑η ∧ IsMarkovKernel η
source
def ProbabilityTheory.Kernel.boolKernel {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) :
Kernel Bool α

The kernel from `Bool` that sends `false` to `μ` and `true` to `ν`.

Equations

- ProbabilityTheory.Kernel.boolKernel μ ν = { toFun := fun (b : Bool) => if b = true then ν else μ, measurable' := ⋯ }

Instances For

source
theorem ProbabilityTheory.Kernel.boolKernel_false {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} :
(boolKernel μ ν) false = μ
source
theorem ProbabilityTheory.Kernel.boolKernel_true {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} :
(boolKernel μ ν) true = ν
source
@[simp]
theorem ProbabilityTheory.Kernel.boolKernel_apply {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (b : Bool) :
(boolKernel μ ν) b = if b = true then ν else μ
source
instance ProbabilityTheory.Kernel.instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] :
IsFiniteKernel (boolKernel μ ν)
source
instance ProbabilityTheory.Kernel.instIsMarkovKernelBoolBoolKernelOfIsProbabilityMeasure {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] :
IsMarkovKernel (boolKernel μ ν)
source
instance ProbabilityTheory.Kernel.instIsSFiniteKernelBoolBoolKernelOfSFinite {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] :
IsSFiniteKernel (boolKernel μ ν)
source
theorem ProbabilityTheory.Kernel.eq_boolKernel {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel Bool α) :
κ = boolKernel (κ false) (κ true)