Kernels between countable spaces

The kernel ofFunOfCountable f that a function out of a countable type defines has row f a at a. Every measure on a countable type is s-finite, and every kernel out of a countable type with measurable singletons is a countable sum of the kernels concentrated at one point, so every kernel between two countable types is s-finite. The pushforward of a kernel into a countable type gives a point the mass of the fibre over it. [UPSTREAM] candidate for Mathlib/Probability/Kernel/Basic.lean.

theorem ProbabilityTheory.Kernel.ofFunOfCountable_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (f : α → MeasureTheory.Measure β) (a : α) : (ofFunOfCountable f) a = f a

theorem ProbabilityTheory.Kernel.sum_piecewise_singleton_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (κ : Kernel α β) : (Kernel.sum fun (a : α) => piecewise ⋯ (const α (κ a)) 0) = κ

A kernel out of a countable type is the sum over points a of the kernel that is κ a at a and 0 elsewhere.

instance ProbabilityTheory.Kernel.instIsSFiniteKernelOfMeasurableSingletonClassOfCountable_linglib {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Countable β] (κ : Kernel α β) : IsSFiniteKernel κ

theorem ProbabilityTheory.Kernel.map_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {γ : Type u_3} [MeasurableSpace γ] [MeasurableSingletonClass γ] [Countable β] [MeasurableSingletonClass β] (κ : Kernel α β) (f : β → γ) (a : α) (c : γ) : ((κ.map f) a) {c} = (κ a) (f ⁻¹' {c})

On a countable space the mass a pushforward gives a point is the mass of the fibre over it.

theorem ProbabilityTheory.Kernel.map_apply_singleton_ne_zero_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {γ : Type u_3} [MeasurableSpace γ] [MeasurableSingletonClass γ] [Countable β] [MeasurableSingletonClass β] (κ : Kernel α β) (f : β → γ) (a : α) (c : γ) : ((κ.map f) a) {c} ≠ 0 ↔ ∃ (b : β), f b = c ∧ (κ a) {b} ≠ 0

On a countable space a pushforward gives a point mass exactly when the kernel gives mass to a point of the fibre over it.