Kernels to countable types

In the algorithms of the paper, the indices of the particles, which take finitely many values, are drawn from probabilities which are measurable functions of the particle positions. Two kernels are defined here: the kernel kernelOfMassFn f from a measurable space α to a countable type β, with mass f a b at b, that is, with density f a with respect to the counting measure, and the kernel kernelOfSections κ on α × β, for a countable β, whose section at b is the kernel κ b.

For a measurable mass function, kernelOfMassFn f is a Markov kernel if the masses sum to one. The kernel kernelOfSections κ is s-finite (an instance) or Markov if its sections are.

noncomputable def CSMC.kernelOfMassFn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable β] (f : α → β → NNReal) : ProbabilityTheory.Kernel α β

The kernel from α to a countable type β with mass f a b at b, that is, with density f a with respect to the counting measure. It is the zero kernel if f is not measurable.

Equations

• CSMC.kernelOfMassFn f = (ProbabilityTheory.Kernel.const α MeasureTheory.Measure.count).withDensity fun (a : α) (b : β) => ↑(f a b)

instance CSMC.instIsSFiniteKernelKernelOfMassFn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable β] (f : α → β → NNReal) : ProbabilityTheory.IsSFiniteKernel (kernelOfMassFn f)

The kernel kernelOfMassFn f is s-finite.

def CSMC.kernelOfSections {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [Countable β] [MeasurableSingletonClass β] (κ : β → ProbabilityTheory.Kernel α γ) : ProbabilityTheory.Kernel (α × β) γ

The kernel on α × β, for a countable β, whose section at b is the kernel κ b: (a, b) ↦ κ b a.

Equations

• CSMC.kernelOfSections κ = { toFun := fun (ab : α × β) => (κ ab.2) ab.1, measurable' := ⋯ }

@[simp]

theorem CSMC.kernelOfSections_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [Countable β] [MeasurableSingletonClass β] (κ : β → ProbabilityTheory.Kernel α γ) (a : α) (b : β) : (kernelOfSections κ) (a, b) = (κ b) a

The section of kernelOfSections κ at (a, b) is κ b a.

theorem CSMC.kernelOfMassFn_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable β] [MeasurableSingletonClass β] {f : α → β → NNReal} (hf : ∀ (b : β), Measurable fun (a : α) => f a b) (a : α) (b : β) : ((kernelOfMassFn f) a) {b} = ↑(f a b)

If f a b is measurable in a for every b, then kernelOfMassFn f a {b} = f a b.

theorem CSMC.lintegral_kernelOfMassFn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable β] [MeasurableSingletonClass β] {f : α → β → NNReal} (hf : ∀ (b : β), Measurable fun (a : α) => f a b) (a : α) (g : β → ENNReal) : ∫⁻ (b : β), g b ∂(kernelOfMassFn f) a = ∑' (b : β), ↑(f a b) * g b

If f a b is measurable in a for every b, integrals with respect to kernelOfMassFn f a are sums weighted by f a.

theorem CSMC.isMarkovKernel_kernelOfMassFn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] {f : α → β → NNReal} (hf : ∀ (b : β), Measurable fun (a : α) => f a b) (h : ∀ (a : α), ∑ b : β, f a b = 1) : ProbabilityTheory.IsMarkovKernel (kernelOfMassFn f)

If f a b is measurable in a for every b and the masses f a b sum to one over the finite type β, then kernelOfMassFn f is a Markov kernel.

instance CSMC.isSFiniteKernel_kernelOfSections {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [Countable β] [MeasurableSingletonClass β] {κ : β → ProbabilityTheory.Kernel α γ} [∀ (b : β), ProbabilityTheory.IsSFiniteKernel (κ b)] : ProbabilityTheory.IsSFiniteKernel (kernelOfSections κ)

The kernel whose sections are s-finite kernels is s-finite.

theorem CSMC.isMarkovKernel_kernelOfSections {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [Countable β] [MeasurableSingletonClass β] {κ : β → ProbabilityTheory.Kernel α γ} (hκ : ∀ (b : β), ProbabilityTheory.IsMarkovKernel (κ b)) : ProbabilityTheory.IsMarkovKernel (kernelOfSections κ)

The kernel whose sections are Markov kernels is a Markov kernel.