Stopped laws and exit distributions

For the continuous-path process Q of a conservative semigroup, this file packages as kernels the laws that the strong Markov property and the boundary value problems of a domain consume:

• stoppedLaw T hT : Kernel alpha (NNReal × alpha), the joint law of a finite stopping time and the position at that time, with its two marginals;
• exitLawTrunc U hU K : Kernel alpha alpha, the law of the position at the exit time of an open set U truncated at the horizon K; from a starting point in U it lives on the closure of U (exitLawTrunc_apply_compl_closure);
• exitLaw U hU : Kernel alpha alpha, the exit distribution (harmonic measure): the law of the position at the exit time on the event that the path leaves U; its total mass is the exit probability, and from a starting point in U it lives on the frontier of U (exitLaw_apply_compl_frontier).

The harmonic representation of Trajectory/HarmonicRepresentation.lean reads, in these terms, ∫ f d(exitLawTrunc U hU K x) = f x whenever L f = 0 on U (integral_exitLawTrunc_eq_of_generator_eq_zero).

theorem MarkovProcess.ContinuousPath.untopD_exitTimeTop_eq_toNNReal {alpha : Type u_1} [PseudoMetricSpace alpha] (U : Set alpha) (omega : ContinuousPath alpha) (h : exitTime U omega ≠ ⊤) : WithTop.untopD 0 (exitTimeTop U omega) = (exitTime U omega).toNNReal

The finite value of a finite exit time, read through untopD, is its toNNReal.

theorem MarkovProcess.ContinuousPath.measurableSet_exitTime_lt_top {alpha : Type u_1} [PseudoMetricSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] (U : Set alpha) (hU : IsOpen U) : MeasurableSet {omega : ContinuousPath alpha | exitTime U omega < ⊤}

The event that a path leaves the open set U is measurable.

theorem MarkovProcess.ContinuousPath.measurable_prodMk_stoppingTime {alpha : Type u_1} [PseudoMetricSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] (T : ContinuousPath alpha → NNReal) (hT : MeasureTheory.IsStoppingTime canonicalFiltration fun (omega : ContinuousPath alpha) => ↑(T omega)) : Measurable fun (omega : ContinuousPath alpha) => (T omega, omega (T omega))

The pair of a finite stopping time and the position at that time is measurable.

theorem MarkovProcess.ContinuousPath.measurable_eval_untopD_exitTimeTop {alpha : Type u_1} [PseudoMetricSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] (U : Set alpha) (hU : IsOpen U) : Measurable fun (omega : ContinuousPath alpha) => omega (WithTop.untopD 0 (exitTimeTop U omega))

The position at the exit time of an open set, on the event that the path leaves it, is measurable.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.IsConservative.stoppedLaw {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsConservative) (T : ContinuousPath alpha → NNReal) (hT : MeasureTheory.IsStoppingTime ContinuousPath.canonicalFiltration fun (omega : ContinuousPath alpha) => ↑(T omega)) : ProbabilityTheory.Kernel alpha (NNReal × alpha)

The stopped law: the joint law of a finite stopping time and the position at that time, as a kernel from the starting point.

Equations

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

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.stoppedLaw_apply {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsConservative) (T : ContinuousPath alpha → NNReal) (hT : MeasureTheory.IsStoppingTime ContinuousPath.canonicalFiltration fun (omega : ContinuousPath alpha) => ↑(T omega)) (x : alpha) : (hP.stoppedLaw T hT) x = MeasureTheory.Measure.map (fun (omega : ContinuousPath alpha) => (T omega, omega (T omega))) ((continuousProcess P hP) x)

instance MarkovProcess.SubMarkovKernelSemigroup.isMarkovKernel_stoppedLaw {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsConservative) (T : ContinuousPath alpha → NNReal) (hT : MeasureTheory.IsStoppingTime ContinuousPath.canonicalFiltration fun (omega : ContinuousPath alpha) => ↑(T omega)) : ProbabilityTheory.IsMarkovKernel (hP.stoppedLaw T hT)

The stopped law is a Markov kernel.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.stoppedLaw_map_fst {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsConservative) (T : ContinuousPath alpha → NNReal) (hT : MeasureTheory.IsStoppingTime ContinuousPath.canonicalFiltration fun (omega : ContinuousPath alpha) => ↑(T omega)) : (hP.stoppedLaw T hT).map Prod.fst = (continuousProcess P hP).map T

The first marginal of the stopped law is the law of the stopping time.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.stoppedLaw_map_snd {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsConservative) (T : ContinuousPath alpha → NNReal) (hT : MeasureTheory.IsStoppingTime ContinuousPath.canonicalFiltration fun (omega : ContinuousPath alpha) => ↑(T omega)) : (hP.stoppedLaw T hT).map Prod.snd = (continuousProcess P hP).map fun (omega : ContinuousPath alpha) => omega (T omega)

The second marginal of the stopped law is the law of the stopped position.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.IsConservative.exitLawTrunc {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) (K : NNReal) : ProbabilityTheory.Kernel alpha alpha

The law of the position at the exit time of U truncated at the horizon K.

Equations

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

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.exitLawTrunc_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) (K : NNReal) (x : alpha) : (hP.exitLawTrunc U hU K) x = MeasureTheory.Measure.map (fun (omega : ContinuousPath alpha) => omega (ContinuousPath.exitTimeTrunc U K omega)) ((continuousProcess P hP) x)

instance MarkovProcess.SubMarkovKernelSemigroup.isMarkovKernel_exitLawTrunc {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) (K : NNReal) : ProbabilityTheory.IsMarkovKernel (hP.exitLawTrunc U hU K)

The truncated exit law is a Markov kernel.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.integral_exitLawTrunc {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) (K : NNReal) (x : alpha) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : alpha → E) (hf : MeasureTheory.StronglyMeasurable f) : ∫ (y : alpha), f y ∂(hP.exitLawTrunc U hU K) x = ∫ (omega : ContinuousPath alpha), f (omega (ContinuousPath.exitTimeTrunc U K omega)) ∂(continuousProcess P hP) x

Integrals against the truncated exit law are expectations of the stopped position.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.exitLawTrunc_apply_compl_closure {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) (K : NNReal) {x : alpha} (hx : x ∈ U) : ((hP.exitLawTrunc U hU K) x) (closure U)ᶜ = 0

From a starting point in U, the truncated exit law lives on the closure of U.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.IsConservative.exitLaw {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) : ProbabilityTheory.Kernel alpha alpha

The exit distribution (harmonic measure) of U: the law of the position at the exit time, on the event that the path leaves U.

Equations

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

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.exitLaw_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) (x : alpha) {B : Set alpha} (hB : MeasurableSet B) : ((hP.exitLaw U hU) x) B = ((continuousProcess P hP) x) {omega : ContinuousPath alpha | ContinuousPath.exitTime U omega < ⊤ ∧ omega (WithTop.untopD 0 (ContinuousPath.exitTimeTop U omega)) ∈ B}

The exit distribution evaluated on a measurable set.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.exitLaw_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) (x : alpha) : ((hP.exitLaw U hU) x) Set.univ = ((continuousProcess P hP) x) {omega : ContinuousPath alpha | ContinuousPath.exitTime U omega < ⊤}

The total mass of the exit distribution is the probability of leaving U.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.exitLaw_apply_compl_frontier {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) {x : alpha} (hx : x ∈ U) : ((hP.exitLaw U hU) x) (frontier U)ᶜ = 0

From a starting point in U, the exit distribution lives on the frontier of U.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.integral_exitLawTrunc_eq_of_generator_eq_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) [LocallyCompactSpace alpha] (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (f : ↥hFeller.c0Semigroup.generatorDomain) (hLf : ∀ y ∈ U, (hFeller.c0Semigroup.generator f) y = 0) (K : NNReal) (x : alpha) : ∫ (y : alpha), ↑f y ∂(hP.exitLawTrunc U hU K) x = ↑f x

Harmonic representation in kernel form. If L f = 0 on U, then f x is the integral of f against the truncated exit law from x, for every horizon.