The killed semigroup on the domain

The killed kernels killedKernel P hP U hU t of Killed/Kernel.lean live on the whole state space and are the identity only on U at time zero. Restricting them to the carrier U (the subtype, with its Borel sigma-algebra) gives kernels killedKernelOn P hP U hU t : Kernel U U which do form a sub-Markov kernel semigroup, the killed semigroup killedSemigroup P hP U hU hFeller hK : SubMarkovKernelSemigroup U:

killedSemigroup t x B = Q x {ω | t < τ_U(ω) ∧ ω t ∈ B} for x ∈ U, B ⊆ U.

The passage to the subtype uses that the killed kernels put no mass outside U (killedKernel_apply_compl), so nothing is lost: (killedKernelOn t x).map Subtype.val = killedKernel t x (map_val_killedKernelOn). The Chapman--Kolmogorov law, joint measurability and the sub-Markov bound transfer from the carrier alpha.

No Feller property, strong continuity, or regularity of the killed semigroup is claimed, and its process is not identified with the cemetery-extended process on lifetime paths.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedKernel_apply_compl {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) (x : alpha) : ((killedKernel P hP U hU t) x) Uᶜ = 0

The killed kernels put no mass outside U: a path still inside U at time t is at a point of U at time t.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.ae_mem_killedKernel {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) (x : alpha) : ∀ᵐ (y : alpha) ∂(killedKernel P hP U hU t) x, y ∈ U

Almost every point under a killed kernel lies in U.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedKernelOn {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) : ProbabilityTheory.Kernel ↑U ↑U

The killed transition kernel at time t, on the carrier U.

Equations

• One or more equations did not get rendered due to their size.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedKernelOn_apply_eq {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) (x : ↑U) : (killedKernelOn P hP U hU t) x = MeasureTheory.Measure.comap Subtype.val ((killedKernel P hP U hU t) ↑x)

The killed kernel on U is the pullback of the killed kernel on alpha along the inclusion.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedKernelOn_apply {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) (x : ↑U) {B : Set ↑U} (hB : MeasurableSet B) : ((killedKernelOn P hP U hU t) x) B = ((killedKernel P hP U hU t) ↑x) (Subtype.val '' B)

The killed kernel on U evaluated on a measurable set of U.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedKernelOn_apply_eq_continuousProcess {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) (x : ↑U) {B : Set ↑U} (hB : MeasurableSet B) : ((killedKernelOn P hP U hU t) x) B = ((continuousProcess P hP) ↑x) (ContinuousPath.killedEvent U t (Subtype.val '' B))

The killed kernel on U, evaluated on a set, as a probability of the path event.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.map_val_killedKernelOn {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) (x : ↑U) : MeasureTheory.Measure.map Subtype.val ((killedKernelOn P hP U hU t) x) = (killedKernel P hP U hU t) ↑x

Pushing the killed kernel on U forward along the inclusion recovers the killed kernel on alpha.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedKernelOn_apply_univ {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) (x : ↑U) : ((killedKernelOn P hP U hU t) x) Set.univ = ((killedKernel P hP U hU t) ↑x) U

The total mass of the killed kernel on U is the survival probability.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.isSubMarkovKernel_killedKernelOn {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (t : NNReal) : IsSubMarkovKernel (killedKernelOn P hP U hU t)

The killed kernels on U are sub-Markov.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.measurable_killedKernelOn {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) : Measurable fun (q : NNReal × ↑U) => (killedKernelOn P hP U hU q.1) q.2

The killed kernels on U are jointly measurable in time and starting point.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedKernelOn_zero {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (hK : P.KolmogorovRegular hP) : killedKernelOn P hP U hU 0 = ProbabilityTheory.Kernel.id

At time zero the killed kernel on U is the identity kernel of U.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedKernelOn_add {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) [LocallyCompactSpace alpha] (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (s t : NNReal) : killedKernelOn P hP U hU (s + t) = (killedKernelOn P hP U hU t).comp (killedKernelOn P hP U hU s)

Chapman--Kolmogorov law for the killed kernels on U.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedSemigroup {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) [LocallyCompactSpace alpha] (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) : SubMarkovKernelSemigroup ↑U

The killed semigroup on the domain U: the process of P killed when it leaves U, as a sub-Markov kernel semigroup on the carrier U.

Equations

• One or more equations did not get rendered due to their size.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedSemigroup_apply {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) [LocallyCompactSpace alpha] (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (t : NNReal) : (killedSemigroup P hP U hU hFeller hK).kernel t = killedKernelOn P hP U hU t

The transition kernels of the killed semigroup are the killed kernels on U.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedSemigroup_apply_apply {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) [LocallyCompactSpace alpha] (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (t : NNReal) (x : ↑U) {B : Set ↑U} (hB : MeasurableSet B) : (((killedSemigroup P hP U hU hFeller hK).kernel t) x) B = ((continuousProcess P hP) ↑x) (ContinuousPath.killedEvent U t (Subtype.val '' B))

The killed semigroup evaluated on a set: the probability that the process started at x ∈ U is still in U at time t and sits in B at time t.