Helpers for the drift theorems

Pointwise facts about a nonnegative potential Ψ and its survival indicator 1_{Ψ > 0}, and the two inductions on 𝔼[Ψ_t] behind Dynamics.Kernel.drift_absorption_seq and Dynamics.Kernel.multiplicative_drift_seq (Lemmas 2.2 and 2.4 of Berenbrink, Giakkoupis, Kermarrec, Mallmann-Trenn, ICALP 2016).

The paper handles the drift c / Ψ with Jensen's inequality, 𝔼[1_{Ψ > 0} / Ψ] ≥ P(Ψ > 0)² / 𝔼[Ψ]. We linearize instead: 1 / y ≥ 2 λ - λ² y for y > 0 and every λ (from (1 - λ y)² ≥ 0), so the drift hypothesis gives the pointwise bound K Ψ ≤ (1 + c λ²) Ψ - 2 c λ 1_{Ψ > 0} (apply_le_lin), which only needs monotonicity and linearity of iterateSeq. Jensen's bound is the optimum λ = P(Ψ > 0) / 𝔼[Ψ]; the proof uses the fixed λ = q / Ψ(x₀), with q the survival probability at the final time.

theorem Dynamics.Kernel.ind_eq_zero_eq {α : Type u_1} (Ψ : α → ℝ) (hΨ : ∀ (x : α), 0 ≤ Ψ x) : (fun (x : α) => if Ψ x = 0 then 1 else 0) = fun (x : α) => 1 - if 0 < Ψ x then 1 else 0

The indicator of Ψ = 0 is one minus the indicator of Ψ > 0 when Ψ ≥ 0.

theorem Dynamics.Kernel.ind_pos_le_div {α : Type u_1} (Ψ : α → ℝ) {Ψmin : ℝ} (hΨ : ∀ (x : α), 0 ≤ Ψ x) (hmin : 0 < Ψmin) (hgap : ∀ (x : α), 0 < Ψ x → Ψmin ≤ Ψ x) (x : α) : (if 0 < Ψ x then 1 else 0) ≤ Ψmin⁻¹ * Ψ x

Markov's inequality for the survival indicator: 1_{Ψ > 0} ≤ Ψ / Ψmin when every positive value of Ψ ≥ 0 is at least Ψmin > 0.

theorem Dynamics.Kernel.exists_pos_mul_ind_le {α : Type u_1} [Fintype α] (Ψ : α → ℝ) (hΨ : ∀ (x : α), 0 ≤ Ψ x) : ∃ (m : ℝ), 0 < m ∧ ∀ (x : α), (m * if 0 < Ψ x then 1 else 0) ≤ Ψ x

On a finite type the positive values of a nonnegative Ψ are bounded below by some m > 0, i.e. m · 1_{Ψ > 0} ≤ Ψ.

theorem Dynamics.Kernel.apply_ind_pos_le {α : Type u_1} [Fintype α] (K : Kernel α) (Ψ : α → ℝ) (hΨ : ∀ (x : α), 0 ≤ Ψ x) (habs : ∀ (x : α), Ψ x = 0 → K.apply Ψ x = 0) (x : α) : K.apply (fun (y : α) => if 0 < Ψ y then 1 else 0) x ≤ if 0 < Ψ x then 1 else 0

A kernel that keeps a nonnegative Ψ at zero from the zeros of Ψ does not increase the indicator of Ψ > 0.

theorem Dynamics.Kernel.iterateSeq_ind_pos_antitone {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (Ψ : α → ℝ) (hΨ : ∀ (x : α), 0 ≤ Ψ x) (T : ℕ) (habs : ∀ t < T, ∀ (x : α), Ψ x = 0 → (K t).apply Ψ x = 0) (x₀ : α) {t : ℕ} (ht : t ≤ T) : iterateSeq K T (fun (x : α) => if 0 < Ψ x then 1 else 0) x₀ ≤ iterateSeq K t (fun (x : α) => if 0 < Ψ x then 1 else 0) x₀

Survival is antitone up to time T when the zeros of Ψ are absorbing: P_T(Ψ > 0) ≤ P_t(Ψ > 0) for t ≤ T.

theorem Dynamics.Kernel.apply_le_lin {α : Type u_1} [Fintype α] (K : Kernel α) (Ψ : α → ℝ) (c lam : ℝ) (hc : 0 ≤ c) (hΨ : ∀ (x : α), 0 ≤ Ψ x) (hdrift : ∀ (x : α), 0 < Ψ x → K.apply Ψ x ≤ Ψ x - c / Ψ x) (habs : ∀ (x : α), Ψ x = 0 → K.apply Ψ x = 0) (x : α) : K.apply Ψ x ≤ (1 + c * lam ^ 2) * Ψ x + -(2 * c * lam) * if 0 < Ψ x then 1 else 0

Linearized drift. The drift c / Ψ, bounded with 1 / Ψ ≥ 2 λ - λ² Ψ: pointwise, K Ψ ≤ (1 + c λ²) Ψ - 2 c λ 1_{Ψ > 0}, for every λ.

theorem Dynamics.Kernel.iterateSeq_le_sub_of_drift {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (Ψ : α → ℝ) (c : ℕ → ℝ) (T : ℕ) (hΨ : ∀ (x : α), 0 ≤ Ψ x) (hc : ∀ t < T, 0 ≤ c t) (hdrift : ∀ t < T, ∀ (x : α), 0 < Ψ x → (K t).apply Ψ x ≤ Ψ x - c t / Ψ x) (habs : ∀ t < T, ∀ (x : α), Ψ x = 0 → (K t).apply Ψ x = 0) (x₀ : α) {lam q : ℝ} (hlam : 0 ≤ lam) (hq : 0 ≤ q) (hid : lam ^ 2 * Ψ x₀ = lam * q) (hsurv : ∀ t < T, q ≤ iterateSeq K t (fun (x : α) => if 0 < Ψ x then 1 else 0) x₀) (t : ℕ) : t ≤ T → iterateSeq K t Ψ x₀ ≤ Ψ x₀ - lam * q * ∑ s ∈ Finset.range t, c s

Iterated linearized drift. Let lam, q ≥ 0 with lam² Ψ(x₀) = lam q, and let the survival probability stay at least q before time T. Then for t ≤ T, 𝔼[Ψ_t] ≤ Ψ(x₀) - lam q ∑_{s < t} c s: each step lowers 𝔼[Ψ] by at least c_t lam q.

theorem Dynamics.Kernel.iterateSeq_le_prod_of_drift {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (Ψ : α → ℝ) (δ : ℕ → ℝ) (T : ℕ) (hδ : ∀ t < T, 0 ≤ 1 - δ t) (hdrift : ∀ t < T, ∀ (x : α), (K t).apply Ψ x ≤ (1 - δ t) * Ψ x) (x₀ : α) (t : ℕ) : t ≤ T → iterateSeq K t Ψ x₀ ≤ (∏ s ∈ Finset.range t, (1 - δ s)) * Ψ x₀

Iterated multiplicative drift. If K t Ψ ≤ (1 - δ t) Ψ with 1 - δ t ≥ 0 for every step t < T, then 𝔼[Ψ_t] ≤ ∏_{s < t} (1 - δ s) Ψ(x₀) for t ≤ T.