Markov kernels, bundled fibrewise

IsMarkovKernel κ says exactly that every fibre of κ : Kernel β Ω is a probability measure. Consumers that want a random probability measure — a β → ProbabilityMeasure Ω, the shape predicates like MixedIIDWith and ConditionallyIIDWith take as their witness — must pair each fibre with that instance by hand. Kernel.probabilityMeasure does it once.

The bundling is canonical: there is no choice to make, and correspondingly no probability-measure lemma here, since the type already carries it.

Main results

• Kernel.probabilityMeasure — the bundled kernel;
• Kernel.probabilityMeasure_toMeasure — its underlying measure is the kernel's fibre, and the abstraction boundary for importing modules;
• Kernel.measurable_probabilityMeasure — measurability into ProbabilityMeasure Ω.
• samplingKernel — the tautological Markov kernel from a probability measure to itself.

Stated for an arbitrary Markov kernel rather than for any particular construction. The regular conditional distribution ProbabilityTheory.condDistrib is one instance; conditioning on a sub-σ-algebra is that instance with the conditioning map id, which is how the de Finetti directing measures arise.

def TauCeti.Probability.Kernel.probabilityMeasure {β : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [mβ : MeasurableSpace β] (κ : ProbabilityTheory.Kernel β Ω) [ProbabilityTheory.IsMarkovKernel κ] (b : β) : MeasureTheory.ProbabilityMeasure Ω

A Markov kernel with each fibre bundled as a ProbabilityMeasure.

Note this lives in TauCeti.Probability.Kernel, not Mathlib's ProbabilityTheory.Kernel, so it is spelled Kernel.probabilityMeasure κ rather than by dot notation on κ.

Equations

• TauCeti.Probability.Kernel.probabilityMeasure κ b = ⟨κ b, ⋯⟩

@[simp]

theorem TauCeti.Probability.Kernel.probabilityMeasure_toMeasure {β : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [mβ : MeasurableSpace β] (κ : ProbabilityTheory.Kernel β Ω) [ProbabilityTheory.IsMarkovKernel κ] (b : β) : ↑(probabilityMeasure κ b) = κ b

The underlying measure of a bundled fibre is the kernel's fibre.

This is the abstraction boundary: importing modules should reason through this lemma rather than unfold Kernel.probabilityMeasure, which is why the definition is not @[expose].

theorem TauCeti.Probability.Kernel.measurable_probabilityMeasure {β : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [mβ : MeasurableSpace β] (κ : ProbabilityTheory.Kernel β Ω) [ProbabilityTheory.IsMarkovKernel κ] : Measurable (probabilityMeasure κ)

The bundled kernel is measurable into ProbabilityMeasure Ω.

def TauCeti.Probability.samplingKernel (α : Type u_4) [MeasurableSpace α] : ProbabilityTheory.Kernel (MeasureTheory.ProbabilityMeasure α) α

The tautological Markov kernel. It sends each bundled probability measure to its underlying measure on α, so the fibre at P is P itself.

Equations

• TauCeti.Probability.samplingKernel α = { toFun := fun (P : MeasureTheory.ProbabilityMeasure α) => ↑P, measurable' := ⋯ }

@[simp]

theorem TauCeti.Probability.samplingKernel_apply {α : Type u_3} [MeasurableSpace α] (P : MeasureTheory.ProbabilityMeasure α) : (samplingKernel α) P = ↑P

instance TauCeti.Probability.instIsMarkovKernelProbabilityMeasureSamplingKernel {α : Type u_3} [MeasurableSpace α] : ProbabilityTheory.IsMarkovKernel (samplingKernel α)