Geometric convergence from a uniform absorption block

theorem Dynamics.Kernel.geometric_blocks {α : Type u_1} [Fintype α] (K : Kernel α) (f : α → ℝ) (q : ℝ) (hq : 0 ≤ q) (m : ℕ) (hblock : ∀ (a : α), K.iterate m f a ≤ q * f a) (n : ℕ) (a : α) : K.iterate (n * m) f a ≤ q ^ n * f a

If a nonnegative survival observable contracts every m rounds, its expectation has a geometric bound at multiples of m.

theorem Dynamics.Kernel.geometric_blocks_tendsto {α : Type u_1} [Fintype α] (K : Kernel α) (f : α → ℝ) (hf : ∀ (a : α), 0 ≤ f a) (q : ℝ) (hq : 0 ≤ q) (hq1 : q < 1) (m : ℕ) (hblock : ∀ (a : α), K.iterate m f a ≤ q * f a) (a : α) : Filter.Tendsto (fun (n : ℕ) => K.iterate (n * m) f a) Filter.atTop (nhds 0)

The block bound tends to zero whenever the contraction factor is below one.

theorem Dynamics.Kernel.iterate_antitone {α : Type u_1} [Fintype α] (K : Kernel α) (f : α → ℝ) (h : ∀ (a : α), K.apply f a ≤ f a) (a : α) : Antitone fun (n : ℕ) => K.iterate n f a

An observable satisfying K f ≤ f has antitone finite-time expectations.

theorem Dynamics.Kernel.exists_uniform_block {α : Type u_1} [Fintype α] [Nonempty α] (K : Kernel α) (f : α → ℝ) (hf : ∀ (a : α), f a = 0 ∨ f a = 1) (hstep : ∀ (a : α), K.apply f a ≤ f a) (haccess : ∀ (a : α), ∃ (n : ℕ), K.iterate n f a < 1) : ∃ (m : ℕ), 0 < m ∧ ∃ (q : ℝ), 0 ≤ q ∧ q < 1 ∧ ∀ (a : α), K.iterate m f a ≤ q * f a

Finiteness turns state-dependent access into a uniform contraction block.

theorem Dynamics.Kernel.finite_absorption {α : Type u_1} [Fintype α] [Nonempty α] (K : Kernel α) (f : α → ℝ) (hf : ∀ (a : α), f a = 0 ∨ f a = 1) (hstep : ∀ (a : α), K.apply f a ≤ f a) (haccess : ∀ (a : α), ∃ (n : ℕ), K.iterate n f a < 1) (a : α) : Filter.Tendsto (fun (n : ℕ) => K.iterate n f a) Filter.atTop (nhds 0)

An accessible absorbing target in a finite chain has vanishing survival probability. f is its complement indicator; hstep expresses absorption and haccess access.