Finite-horizon optional stopping (roadmap FND-4)

Let K be a finite kernel, A and B two target events on which an observable φ takes constant values φA and φB, and suppose that φ is conserved in expectation from x₀: 𝔼[φ(X_T)] = φ(x₀) for every time T. Pointwise, φ - φB = (φA - φB) · 1_A + (φ - φB) · 1_{¬A ∧ ¬B}, so the conservation law determines the probability of A at time T up to the survival probability P(X_T ∉ A ∪ B) (event_error_of_invariant). When survival vanishes, the probability of A tends to (φ(x₀) − φB) / (φA − φB) (tendsto_event_of_invariant); if A is absorbing, this limit is the absorption probability, the supremum of the increasing finite-time probabilities (iSup_event_of_invariant).

This is the argument of Hassin–Peleg, Lemma 2.2 (Voter.whiteProbability_error), and of the fixation formulas of moran/ (Moran.fixation_eq_of_invariant). Since φ is constant on the absorbing targets, φ(X_T) and the stopped value φ(X_{τ ∧ T}) agree, so no stopping time or path space is needed.

theorem Dynamics.Kernel.eq_add_target_add_survival {α : Type u_1} (φ : α → ℝ) (A B : α → Prop) [DecidablePred A] [DecidablePred B] (φA φB : ℝ) (hA : ∀ (a : α), A a → φ a = φA) (hB : ∀ (a : α), B a → φ a = φB) (a : α) : φ a = φB + (((φA - φB) * if A a then 1 else 0) + (φ a - φB) * if ¬A a ∧ ¬B a then 1 else 0)

Pointwise decomposition behind optional stopping: φ - φB equals φA - φB on A, vanishes on B, and is unchanged off A ∪ B. No disjointness is needed: on A ∩ B, φA = φB.

theorem Dynamics.Kernel.iterate_eq_event_add {α : Type u_1} [Fintype α] (K : Kernel α) (φ : α → ℝ) (A B : α → Prop) [DecidablePred A] [DecidablePred B] (φA φB : ℝ) (hA : ∀ (a : α), A a → φ a = φA) (hB : ∀ (a : α), B a → φ a = φB) (T : ℕ) (x₀ : α) : K.iterate T φ x₀ = φB + ((φA - φB) * K.event A T x₀ + K.iterate T (fun (a : α) => (φ a - φB) * if ¬A a ∧ ¬B a then 1 else 0) x₀)

Optional-stopping identity at time T: the expectation of φ is φB, plus the contribution (φA - φB) P(X_T ∈ A) of A, plus the contribution of the survivors.

theorem Dynamics.Kernel.event_error_of_invariant {α : Type u_1} [Fintype α] (K : Kernel α) (φ : α → ℝ) (A B : α → Prop) (φA φB m M : ℝ) (hA : ∀ (a : α), A a → φ a = φA) (hB : ∀ (a : α), B a → φ a = φB) (hS : ∀ (a : α), ¬A a → ¬B a → m ≤ φ a - φB ∧ φ a - φB ≤ M) (x₀ : α) (T : ℕ) (hinv : K.iterate T φ x₀ = φ x₀) : m * K.event (fun (a : α) => ¬A a ∧ ¬B a) T x₀ ≤ φ x₀ - φB - (φA - φB) * K.event A T x₀ ∧ φ x₀ - φB - (φA - φB) * K.event A T x₀ ≤ M * K.event (fun (a : α) => ¬A a ∧ ¬B a) T x₀

Finite-horizon optional stopping (roadmap FND-4, finite-time form). Let φ equal φA on A and φB on B, satisfy m ≤ φ - φB ≤ M outside A ∪ B, and have expectation φ x₀ at time T from x₀. Then φ x₀ - φB - (φA - φB) P(X_T ∈ A) lies between m and M times the survival probability P(X_T ∉ A ∪ B).

theorem Dynamics.Kernel.tendsto_event_of_invariant {α : Type u_1} [Fintype α] (K : Kernel α) (φ : α → ℝ) (A B : α → Prop) (φA φB : ℝ) (hA : ∀ (a : α), A a → φ a = φA) (hB : ∀ (a : α), B a → φ a = φB) (hAB : φA ≠ φB) (x₀ : α) (hinv : ∀ (T : ℕ), K.iterate T φ x₀ = φ x₀) (hsurv : Filter.Tendsto (fun (T : ℕ) => K.event (fun (a : α) => ¬A a ∧ ¬B a) T x₀) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (T : ℕ) => K.event A T x₀) Filter.atTop (nhds ((φ x₀ - φB) / (φA - φB)))

Finite-horizon optional stopping (roadmap FND-4, limit form). If φ equals φA on A and φB ≠ φA on B, 𝔼[φ(X_T)] = φ(x₀) for every T, and the survival probability P(X_T ∉ A ∪ B) tends to 0, then P(X_T ∈ A) tends to (φ(x₀) − φB) / (φA − φB).

theorem Dynamics.Kernel.iSup_event_of_invariant {α : Type u_1} [Fintype α] (K : Kernel α) (φ : α → ℝ) (A B : α → Prop) (φA φB : ℝ) (hA : ∀ (a : α), A a → φ a = φA) (hB : ∀ (a : α), B a → φ a = φB) (hAB : φA ≠ φB) (hAabs : ∀ (a : α), A a → (K a).prob A = 1) (x₀ : α) (hinv : ∀ (T : ℕ), K.iterate T φ x₀ = φ x₀) (hsurv : Filter.Tendsto (fun (T : ℕ) => K.event (fun (a : α) => ¬A a ∧ ¬B a) T x₀) Filter.atTop (nhds 0)) : ⨆ (T : ℕ), K.event A T x₀ = (φ x₀ - φB) / (φA - φB)

Finite-horizon optional stopping (roadmap FND-4, absorption probability). Under the hypotheses of tendsto_event_of_invariant, if moreover A is absorbing, the absorption probability in A from x₀, i.e. the supremum of the finite-time probabilities P(X_T ∈ A), is (φ(x₀) − φB) / (φA − φB).