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

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.

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)

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)

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

instance ProbabilityTheory.Kernel.isMarkovKernel_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) : IsMarkovKernel (deterministic f hf)

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)

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

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

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

noncomputable def ProbabilityTheory.Kernel.id {α : Type u_1} {mα : MeasurableSpace α} : Kernel α α

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

instance ProbabilityTheory.Kernel.instIsMarkovKernelId {α : Type u_1} {mα : MeasurableSpace α} : IsMarkovKernel Kernel.id

theorem ProbabilityTheory.Kernel.id_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) : Kernel.id a = MeasureTheory.Measure.dirac a

theorem ProbabilityTheory.Kernel.lintegral_id' {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal} (hf : Measurable f) (a : α) : ∫⁻ (a : α), f a ∂Kernel.id a = f a

theorem ProbabilityTheory.Kernel.lintegral_id {α : Type u_1} {mα : MeasurableSpace α} [MeasurableSingletonClass α] {f : α → ENNReal} (a : α) : ∫⁻ (a : α), f a ∂Kernel.id a = f a

noncomputable def ProbabilityTheory.Kernel.copy (α : Type u_4) [MeasurableSpace α] : Kernel α (α × α)

The deterministic kernel that maps x : α to the Dirac measure at (x, x) : α × α.

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy {α : Type u_1} {mα : MeasurableSpace α} : IsMarkovKernel (copy α)

theorem ProbabilityTheory.Kernel.copy_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) : (copy α) a = MeasureTheory.Measure.dirac (a, a)

noncomputable def ProbabilityTheory.Kernel.discard (α : Type u_4) [MeasurableSpace α] : Kernel α Unit

The Markov kernel to the Unit type.

instance ProbabilityTheory.Kernel.instIsMarkovKernelUnitDiscard {α : Type u_1} {mα : MeasurableSpace α} : IsMarkovKernel (discard α)

@[simp]

theorem ProbabilityTheory.Kernel.discard_apply {α : Type u_1} {mα : MeasurableSpace α} (a : α) : (discard α) a = MeasureTheory.Measure.dirac ()

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

instance ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : IsMarkovKernel (swap α β)

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.

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.

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

Constant kernel, which always returns the same measure.

@[simp]

theorem ProbabilityTheory.Kernel.const_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μβ : MeasureTheory.Measure β) (a : α) : (const α μβ) a = μβ

@[simp]

theorem ProbabilityTheory.Kernel.const_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : const α 0 = 0

theorem ProbabilityTheory.Kernel.const_add {α : Type u_1} {mα : MeasurableSpace α} (β : Type u_4) [MeasurableSpace β] (μ ν : MeasureTheory.Measure α) : const β (μ + ν) = const β μ + const β ν

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

instance ProbabilityTheory.Kernel.const.instIsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure μβ] : IsFiniteKernel (const α μβ)

instance ProbabilityTheory.Kernel.const.instIsSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [MeasureTheory.SFinite μβ] : IsSFiniteKernel (const α μβ)

instance ProbabilityTheory.Kernel.const.instIsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [hμβ : MeasureTheory.IsProbabilityMeasure μβ] : IsMarkovKernel (const α μβ)

instance ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β} [hμβ : MeasureTheory.IsZeroOrProbabilityMeasure μβ] : IsZeroOrMarkovKernel (const α μβ)

theorem ProbabilityTheory.Kernel.isSFiniteKernel_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α] {μβ : MeasureTheory.Measure β} : IsSFiniteKernel (const α μβ) ↔ MeasureTheory.SFinite μβ

instance ProbabilityTheory.Kernel.instNonemptySubtypeIsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty β] : Nonempty { κ : Kernel α β // IsMarkovKernel κ }

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

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

theorem ProbabilityTheory.Kernel.discard_eq_const {α : Type u_1} {mα : MeasurableSpace α} : discard α = const α (MeasureTheory.Measure.dirac ())

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.

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.

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

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)

@[simp]

theorem ProbabilityTheory.Kernel.restrict_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} : κ.restrict ⋯ = κ

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

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

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)

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)

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

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)

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)

@[simp]

theorem ProbabilityTheory.Kernel.comapRight_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : κ.comapRight ⋯ = κ

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)

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)

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)

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.

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

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

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 κ η)

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 κ η)

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 κ η)

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

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

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 η