Hitting probabilities through the stopped chain

The chain K.stopped B follows K outside B and stays put once in B. It is in B at time n exactly when the original chain has visited B by time n, so the non-hitting probability 1 - K.hitProb B n a is the event ¬ B at time n of the stopped chain (one_sub_hitProb_eq_event_stopped). This turns hitting times into finite-time events, to which the drift theorems of Dynamics.Drift apply.

one_sub_hitProb_le_of_drift is the resulting geometric drift bound: a potential V ≥ 0 vanishing on B, at least Vmin > 0 off B, with 𝔼[V(X_{t+1}) | X_t = a] ≤ ρ V(a) off B, gives P_a(T_B > t) ≤ ρ^t V(a) / Vmin. It is multiplicative_drift (the argument of Lemma 2.4 of Berenbrink, Giakkoupis, Kermarrec, Mallmann-Trenn, ICALP 2016) for the stopped chain.

Recursion for hitProb

theorem Dynamics.Kernel.hitProb_of_mem {α : Type u_1} [Fintype α] (K : Kernel α) {B : α → Prop} {a : α} (h : B a) (n : ℕ) : K.hitProb B n a = 1

A chain started in B has hit B at time 0.

theorem Dynamics.Kernel.hitProb_zero_of_not_mem {α : Type u_1} [Fintype α] (K : Kernel α) {B : α → Prop} {a : α} (h : ¬B a) : K.hitProb B 0 a = 0

Outside B, the chain has not hit B at time 0.

theorem Dynamics.Kernel.hitProb_succ_of_not_mem {α : Type u_1} [Fintype α] (K : Kernel α) {B : α → Prop} {a : α} (h : ¬B a) (n : ℕ) : K.hitProb B (n + 1) a = (K a).expect (K.hitProb B n)

Outside B, hitting B within n + 1 steps means hitting it within n steps from the next state.

The stopped chain

noncomputable def Dynamics.Kernel.stopped {α : Type u_1} [Fintype α] (K : Kernel α) (B : α → Prop) : Kernel α

The chain K stopped on entering B: it moves with K outside B and stays put in B.

Equations

• K.stopped B a = if B a then Dynamics.Distribution.point a else K a

theorem Dynamics.Kernel.stopped_of_mem {α : Type u_1} [Fintype α] (K : Kernel α) {B : α → Prop} {a : α} (h : B a) : K.stopped B a = Distribution.point a

theorem Dynamics.Kernel.stopped_of_not_mem {α : Type u_1} [Fintype α] (K : Kernel α) {B : α → Prop} {a : α} (h : ¬B a) : K.stopped B a = K a

theorem Dynamics.Kernel.iterate_stopped_eq_one_sub_hitProb {α : Type u_1} [Fintype α] (K : Kernel α) (B : α → Prop) (f : α → ℝ) (hf0 : ∀ (b : α), B b → f b = 0) (hf1 : ∀ (b : α), ¬B b → f b = 1) (n : ℕ) (a : α) : (K.stopped B).iterate n f a = 1 - K.hitProb B n a

The stopped chain started at a is outside B at time n with probability 1 - K.hitProb B n a, for any observable f that is the indicator of the complement of B.

theorem Dynamics.Kernel.one_sub_hitProb_eq_event_stopped {α : Type u_1} [Fintype α] (K : Kernel α) (B : α → Prop) (n : ℕ) (a : α) : 1 - K.hitProb B n a = (K.stopped B).event (fun (b : α) => ¬B b) n a

The non-hitting probability P_a(T_B > n) is the probability that the stopped chain is outside B at time n.

theorem Dynamics.Kernel.one_sub_hitProb_le_of_drift {α : Type u_1} [Fintype α] (K : Kernel α) (B : α → Prop) (V : α → ℝ) {ρ Vmin : ℝ} (hV : ∀ (x : α), 0 ≤ V x) (hVB : ∀ (x : α), B x → V x = 0) (hmin : 0 < Vmin) (hgap : ∀ (x : α), ¬B x → Vmin ≤ V x) (hdrift : ∀ (x : α), ¬B x → K.apply V x ≤ ρ * V x) (t : ℕ) (a : α) : 1 - K.hitProb B t a ≤ ρ ^ t * V a / Vmin

Geometric drift bound for hitting times. Let V ≥ 0 vanish on B and be at least Vmin > 0 off B. If 𝔼[V(X_{t+1}) | X_t = x] ≤ ρ V(x) from every x ∉ B, then the chain started at a has not hit B within t steps with probability at most ρ^t V(a) / Vmin. This is multiplicative_drift for the stopped chain.