StoppedDirichlet #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The remaining exit time of a continuous process #
Let Q be the continuous-path process of a conservative Feller kernel semigroup, let U be an
open set, let tau be the first exit time from U, and let
w y = E_y[tau]
be the expected exit time from the starting point y. This file proves the identity that
governs the stopped process at a deterministic horizon t:
E_x[w(X_{t and tau})] + E_x[t and tau] = w x (lintegral_expectedExitTime_add),
for every starting point x of U. In words: the expected time still to be spent in U after
the stopped time is the total expected time minus the expected time already spent.
The proof uses no generator and no domain membership. It rests on three facts. Pathwise, the
exit time splits as the truncated exit time plus, on the survival event {t < tau}, the exit time
of the path shifted by t (exitTime_eq_exitTimeTrunc_add). The simple Markov property at the
deterministic time t, restricted to the survival event -- which belongs to the canonical
filtration at time t -- converts the shifted term into w(X_t)
(lintegral_indicator_survivalEvent_shift). Finally, on the complementary event the stopped
path sits on the frontier of U, where w vanishes because a path starting outside U leaves
immediately (ae_expectedExitTime_eval_exitTimeTrunc).
The same restricted Markov property in Bochner form (setIntegral_shift) is recorded here; it is
what the harmonic identities of the companion file consume.
Two shapes of the main identity are given: the additive one in ℝ≥0∞, which needs no finiteness,
and the subtractive and real-valued ones under a finite expected exit time from the starting
point.
The survival event: the paths that are still in U at time t.
Equations
- DivergenceFormProcess.StoppedDirichlet.survivalEvent U t = {omega : MarkovProcess.ContinuousPath alpha | ↑t < MarkovProcess.ContinuousPath.exitTime U omega}
Instances For
The position of a path at its exit time from U, read at the time (exitTime U).toNNReal.
Equations
- DivergenceFormProcess.StoppedDirichlet.exitPosition U omega = omega (MarkovProcess.ContinuousPath.exitTime U omega).toNNReal
Instances For
On the survival event the exit time truncated at t is t.
Off the survival event the exit time truncated at t is the exit time itself.
Off the survival event the stopped position is the exit position.
On the survival event, and at a finite exit time, shifting by t does not move the exit
position.
The pathwise splitting of the exit time at a deterministic horizon. The exit time is the truncated exit time plus, on the survival event, the exit time of the shifted path.
The exit position is a Borel function on path space.
The survival event belongs to the canonical filtration at its own time.
The survival event is a Borel set of path space.
The expected exit time from U of the continuous process started at y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The expected exit time is a Borel function of the starting point.
A process started outside U leaves U at once, so the expected exit time vanishes off
U.
Almost surely from a starting point of U, the expected exit time read at the stopped
position is the expected exit time read at time t on the survival event, and zero elsewhere:
off the survival event the stopped path sits on the frontier of U.
The expected stopped time never exceeds the horizon, hence is finite.
The restricted Markov property at a deterministic time, in extended nonnegative form. On
the survival event, which belongs to the canonical filtration at time t, the expectation of a
nonnegative observable of the shifted path is its expectation under the process restarted from
the position at time t.
The restricted Markov property at a deterministic time, in Bochner form. Over an event of
the canonical filtration at time t, the integral of a bounded observable of the shifted path is
the integral of its expectation under the process restarted from the position at time t.
The remaining exit time at a deterministic horizon. From a starting point of the open set
U, the expected exit time read at the stopped position, plus the expected stopped time, is the
expected exit time from the starting point.
Under a finite expected exit time, the expected exit time read at the stopped position is finite.
The remaining exit time, in real form. Under a finite expected exit time from the starting point, the real expected exit time read at the stopped position, plus the real expected stopped time, is the real expected exit time.
The real expected exit time read at the stopped position is integrable.