HitExitChaining #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Chaining a hit with the subsequent exit #
This module builds one restart step from two successive events: first hit a member of a
countable family of closed sets, then exit the corresponding open enlargement. Entrance into a
closed set D is represented by the exit time from the open complement Dᶜ. This closedness is
essential: entrance times of general open sets need not be stopping times for the raw canonical
filtration, and a continuous path first entering an open set need only land in its closure.
Accordingly, the union of the small sets is assumed closed and the enlarged sets V' i are
open; each individual V i need only be measurable, the intended use being closed sets with
V i ⊆ V' i. Closedness of the union is deliberately a separate hypothesis; it does not follow
for an arbitrary infinite family. At a finite hitting time the path lies in the selected V i
itself, not merely its closure. Reaching a cemetery point outside an enlargement counts as an
exit.
Public declarations:
ContinuousPath.hitTime;ContinuousPath.familyIndex;ContinuousPath.hitExitTime;ContinuousPath.measurable_familyIndex;ContinuousPath.familyIndex_mem_of_mem_iUnion;ContinuousPath.coordinate_hitTime_mem;ContinuousPath.isStoppingTime_hitExitTime;ContinuousPath.visited_before_iterated_subset;ContinuousPath.iteratedStoppingTime_hitExit_le_exitTime_of_visits;IsConservative.lintegral_exp_neg_exitTime_le_rho_pow_hitExit_of_cover;IsConservative.lintegral_exp_neg_exitTime_le_rho_pow_hitExit.
The first entrance time into D, represented as the exit time from its complement.
Equations
Instances For
The least member of a countable family containing a, with value zero off the union.
Equations
- Algsuperdiff.Process.ContinuousPath.familyIndex V a = if h : ∃ (i : ℕ), a ∈ V i then Nat.find h else 0
Instances For
First hit the closed family, then exit the open enlargement selected at the hitting state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The least-index selector of a measurable countable family is measurable.
A point in the union belongs to the family member selected by familyIndex.
At a finite entrance time into a closed set, the path lies in that set.
The composite hit-then-exit rule is a stopping time when the hit sets are measurable with a closed union and each enlargement is open.
The hit sets visited before the first k composite cycles fit in a finite set of at most
k * K indices when each selected enlargement meets at most K hit sets.
If a path visits more distinct hit sets than N overlap blocks can contain before
leaving U, then its first N hit-then-exit cycles finish before that exit.
A one-step discounted exit bound on every hitting set controls the composite hit-then-exit rule from every starting point.
The general exit-time chaining estimate specialized to the composite hit-then-exit rule.
The geometric comparison with the terminal exit time is supplied directly, guarded by
exitTime U omega < ⊤: paths that never leave U are unconstrained.
Composite hit-then-exit chaining bound. If each selected enlargement meets at most K
hit sets and almost every path visits at least D explicitly listed hit sets strictly before
leaving U, then N * K < D turns the one-cycle estimate into a rho ^ N terminal-exit
estimate.
The visits premise is guarded by exitTime U omega < ⊤, so it asks nothing of paths that never
leave U. Because almost every path starts at x, a starting point outside U leaves at time
0; no visit time is then strictly earlier, the guarded premise forces D = 0, and hcount
fails. The conclusion is therefore vacuous unless x ∈ U.