Cemetery extensions of sub-Markov kernel semigroups

This file shows that conservative cemetery extension preserves the identity kernel and composition of sub-Markov kernels. Consequently, applying the extension at every time turns any sub-Markov kernel semigroup into a conservative semigroup on the cemetery state space.

theorem MarkovProcess.Kernel.cemeteryExtension_id {α : Type u_1} [MeasurableSpace α] : cemeteryExtension ProbabilityTheory.Kernel.id = ProbabilityTheory.Kernel.id

Conservative cemetery extension preserves the identity kernel.

theorem MarkovProcess.Kernel.cemeteryExtension_comp_alive_image {α : Type u_1} [MeasurableSpace α] (η κ : ProbabilityTheory.Kernel α α) (x : α) {s : Set α} (hs : MeasurableSet s) : ((cemeteryExtension (η.comp κ)) (Cemetery.alive x)) (Cemetery.alive '' s) = (((cemeteryExtension η).comp (cemeteryExtension κ)) (Cemetery.alive x)) (Cemetery.alive '' s)

On live measurable sets, cemetery extension preserves kernel composition.

theorem MarkovProcess.Kernel.cemeteryExtension_comp {α : Type u_1} [MeasurableSpace α] (η κ : ProbabilityTheory.Kernel α α) (hη : IsSubMarkovKernel η) (hκ : IsSubMarkovKernel κ) : cemeteryExtension (η.comp κ) = (cemeteryExtension η).comp (cemeteryExtension κ)

Conservative cemetery extension preserves composition of sub-Markov kernels.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.cemeterySemigroup {α : Type u_1} [MeasurableSpace α] (P : SubMarkovKernelSemigroup α) : SubMarkovKernelSemigroup (Cemetery α)

The conservative cemetery extension of a sub-Markov kernel semigroup.

Equations

• P.cemeterySemigroup = { kernel := fun (t : NNReal) => MarkovProcess.Kernel.cemeteryExtension (P.kernel t), measurable_kernel := ⋯, kernel_zero := ⋯, kernel_add := ⋯, isSubMarkovKernel := ⋯ }

@[simp]

theorem MarkovProcess.SubMarkovKernelSemigroup.cemeterySemigroup_apply {α : Type u_1} [MeasurableSpace α] (P : SubMarkovKernelSemigroup α) (t : NNReal) : P.cemeterySemigroup.kernel t = Kernel.cemeteryExtension (P.kernel t)

theorem MarkovProcess.SubMarkovKernelSemigroup.isConservative_cemeterySemigroup {α : Type u_1} [MeasurableSpace α] (P : SubMarkovKernelSemigroup α) : P.cemeterySemigroup.IsConservative

The cemetery extension semigroup is conservative.

theorem MarkovProcess.SubMarkovKernelSemigroup.cemeterySemigroup_absorbing {α : Type u_1} [MeasurableSpace α] (P : SubMarkovKernelSemigroup α) (t : NNReal) : (P.cemeterySemigroup.kernel t) Cemetery.delta = MeasureTheory.Measure.dirac Cemetery.delta

The cemetery state is absorbing at every time in the extension semigroup.