Measurability and fresh-start identities for real-walk exits

This file proves that restart exit times are measurable, determined by finite prefixes, and strictly increasing before their absorbing sentinel. It also expresses the next exit after a deterministic time in terms of the shifted walk.

theorem BGW.Probability.RealWalk.measurable_nextExit (M : ℕ) (r : ℝ) (a : ℕ) : Measurable fun (ω : ℕ → ℝ) => nextExit M r ω a

nextExit M r · a is measurable (the codomain ℕ carries the discrete σ-algebra).

theorem BGW.Probability.RealWalk.measurable_exitTimes (M : ℕ) (r : ℝ) (j : ℕ) : Measurable fun (ω : ℕ → ℝ) => exitTimes M r ω j

Every restart exit time is measurable.

theorem BGW.Probability.RealWalk.measurable_exitCount (M : ℕ) (r : ℝ) : Measurable fun (ω : ℕ → ℝ) => exitCount M r ω

The finite count of actual exits is measurable.

theorem BGW.Probability.RealWalk.measurableSet_closeExit (M : ℕ) (r : ℝ) (l : ℕ) : MeasurableSet {ω : ℕ → ℝ | closeExit M r l ω}

The existence of a close successive pair of actual exits is measurable.

theorem BGW.Probability.RealWalk.exitTimes_lt_succ {M : ℕ} {r : ℝ} {ω : ℕ → ℝ} {j : ℕ} (h : exitTimes M r ω j ≤ M) : exitTimes M r ω j < exitTimes M r ω (j + 1)

Exit times are strictly increasing as long as they are actual exits (≤ M).

theorem BGW.Probability.RealWalk.exitTimes_eq_sentinel {M : ℕ} {r : ℝ} {ω : ℕ → ℝ} {j : ℕ} (h : M < exitTimes M r ω j) {i : ℕ} (hi : 1 ≤ i) : exitTimes M r ω (j + i) = M + 1

Once the sentinel M + 1 (or anything > M) is reached, all later exit times are sentinel.

theorem BGW.Probability.RealWalk.exitCount_le (M : ℕ) (r : ℝ) (ω : ℕ → ℝ) : exitCount M r ω ≤ M

The number of actual exits is at most M.

theorem BGW.Probability.RealWalk.nextExit_eq_of_prefix_eq {M : ℕ} {r : ℝ} {ω ω' : ℕ → ℝ} {a k : ℕ} (hk : k ≤ M) (hω : ∀ i < k, ω i = ω' i) (h : nextExit M r ω a = k) : nextExit M r ω' a = k

The exit event {nextExit a = k}, k ≤ M, depends only on the coordinates < k.

theorem BGW.Probability.RealWalk.exists_prefixSet_exitTimes (M : ℕ) (r : ℝ) (j k : ℕ) (hk : k ≤ M) : ∃ (A : Set (Fin k → ℝ)), MeasurableSet A ∧ {ω : ℕ → ℝ | exitTimes M r ω j = k} = prefixVec k ⁻¹' A

Prefix-determination of the j-th exit time at an actual exit.

theorem BGW.Probability.RealWalk.exitTimes_succ_eq_shift {M : ℕ} {r : ℝ} {ω : ℕ → ℝ} {j k : ℕ} (hk : k ≤ M) (h : exitTimes M r ω j = k) : exitTimes M r ω (j + 1) = k + nextExit (M - k) r (shift k ω) 0

The next exit after an actual j-th exit is computed by the shifted walk.