Expected exit counts and close-pair probabilities

The expected number of restart exits is controlled by splitting exits according to their gap from the previous exit. Far exits inject into time blocks. Close successive exits are charged to the preceding exit by finite-prefix determination and fresh-start independence.

theorem BGW.Probability.RealWalk.measure_closeExit_le (ν : MeasureTheory.ProbabilityMeasure ℝ) {M : ℕ} {r : ℝ} (hr : 0 < r) (l : ℕ) : (↑(iidLaw ν)).real {ω : ℕ → ℝ | closeExit M r l ω} ≤ (∫ (ω : ℕ → ℝ), ↑(exitCount M r ω) ∂↑(iidLaw ν)) * maxTail ν l r

Close pairs are bounded by the expected exit count times the fresh-start tail.

theorem BGW.Probability.RealWalk.integral_exitCount_le (ν : MeasureTheory.ProbabilityMeasure ℝ) {M L : ℕ} {r : ℝ} (hr : 0 < r) (hL : 1 ≤ L) (hsafe : maxTail ν L r ≤ 1 / 2) : ∫ (ω : ℕ → ℝ), ↑(exitCount M r ω) ∂↑(iidLaw ν) ≤ 2 * (↑M / ↑L + 1)

Expected number of exits under the safe-block hypothesis.

theorem BGW.Probability.RealWalk.measure_closeExit_le_of_safe (ν : MeasureTheory.ProbabilityMeasure ℝ) {M L : ℕ} {r : ℝ} (hr : 0 < r) (hL : 1 ≤ L) (hsafe : maxTail ν L r ≤ 1 / 2) (l : ℕ) : (↑(iidLaw ν)).real {ω : ℕ → ℝ | closeExit M r l ω} ≤ 2 * (↑M / ↑L + 1) * maxTail ν l r

Close-pair bound with the safe-block expected-count estimate.