StoppedPositionStream

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The stopped position of the stream process

Fix one realization of the stream field, an open subset U of the one-point compactification of the live space, a deterministic horizon t, and a starting point x of U. Write theta for the exit time from U truncated at t. Almost every continuous path of the stream process started at x satisfies

  eta theta ∈ closure U ,

that is, at the moment it either leaves U or reaches the horizon the path is in the closure of U: inside U if the horizon comes first, on the frontier if the exit comes first.

The statement is the one already available for the continuous-path process of an abstract conservative Feller semigroup (ae_eval_exitTimeTrunc_mem_closure), read at the process the model produces. The reading is definitional: the stream process is the continuous-path process of the compactified kernel semigroup of the split-skew analytic resolvent, and the Kolmogorov regularity that statement asks for is the corresponding field of the shift-dependent exhaustion-tail input's regularity datum.

Main results

• ae_eval_exitTimeTrunc_mem_closure_streamProcess — the stopped position lies in the closure of the domain, almost surely.
• ae_eval_exitTimeTrunc_mem_closure_streamProcess_cubeSetAt — the same at the image of a triadic cube, from any starting point of the cube.

References

• ABK26, the stopped displacement bounds of Section 5.4.

2. The stopped position lies in the closure

theorem Algsuperdiff.Section5.Provider.ae_eval_exitTimeTrunc_mem_closure_streamProcess {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) {U : Set (OnePoint (HCPolySupport.Vec d))} (hU : IsOpen U) (t : NNReal) {x : OnePoint (HCPolySupport.Vec d)} (hx : x ∈ U) : ∀ᵐ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) ∂(Field.streamProcess M omega) x, eta (MarkovProcess.ContinuousPath.exitTimeTrunc U t eta) ∈ closure U

The stopped position of the stream process lies in the closure of the domain. Almost every path of the stream process started at a point of the open set U is, at the time at which it either leaves U or reaches the horizon t, in the closure of U.

The two ingredients are the path-level statement, that a continuous path started inside U is in the closure of U at the truncated exit time, and the fact that the process started at x starts at x almost surely; the latter is where the Kolmogorov regularity of the compactified kernel semigroup enters.

3. The stopped position on a triadic cube

theorem Algsuperdiff.Section5.Provider.ae_eval_exitTimeTrunc_mem_closure_streamProcess_cubeSetAt {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) (t : NNReal) {z : HCPolySupport.Vec d} (hz : z ∈ Support.cubeSetAt y n) : ∀ᵐ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) ∂(Field.streamProcess M omega) ↑z, eta (MarkovProcess.ContinuousPath.exitTimeTrunc (OnePoint.some '' Support.cubeSetAt y n) t eta) ∈ closure (OnePoint.some '' Support.cubeSetAt y n)

The stopped position of the stream process on a triadic cube. From any live starting point of the cube, the position at the exit time from the image of the cube truncated at the horizon lies almost surely in the closure of that image.

theorem Algsuperdiff.Section5.Provider.ae_eval_exitTimeTrunc_mem_closure_streamProcess_cubeSetAt_self {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (y : HCPolySupport.Vec d) (n : ℤ) (t : NNReal) : ∀ᵐ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) ∂(Field.streamProcess M omega) ↑y, eta (MarkovProcess.ContinuousPath.exitTimeTrunc (OnePoint.some '' Support.cubeSetAt y n) t eta) ∈ closure (OnePoint.some '' Support.cubeSetAt y n)

The stopped position of the stream process on a triadic cube, from its centre.