Processes driven by independent uniform rounds

Many dynamics in this repository are given by a deterministic update step : S → R → S applied to a sequence of i.i.d. uniform rounds r : R, with expectations computed by expList. ofStep step is the corresponding finite Markov kernel, and iterate_ofStep identifies its iterates with the expList expectations, so results about kernels (for instance Dynamics.Kernel.nested_phases) apply to such round-based processes.

noncomputable def Dynamics.Kernel.ofStep {S : Type u_1} {R : Type u_2} [Fintype S] [Fintype R] [Nonempty R] (step : S → R → S) : Kernel S

The Markov kernel of one uniformly random round of step.

Equations

• Dynamics.Kernel.ofStep step s = (Dynamics.Distribution.uniform R).map (step s)

theorem Dynamics.Kernel.apply_ofStep {S : Type u_1} {R : Type u_2} [Fintype S] [Fintype R] [Nonempty R] (step : S → R → S) (f : S → ℝ) (s : S) : (ofStep step).apply f s = avg fun (r : R) => f (step s r)

theorem Dynamics.Kernel.prob_ofStep {S : Type u_1} {R : Type u_2} [Fintype S] [Fintype R] [Nonempty R] (step : S → R → S) (P : S → Prop) (s : S) : (ofStep step s).prob P = avg fun (r : R) => if P (step s r) then 1 else 0

theorem Dynamics.Kernel.iterate_ofStep {S : Type u_1} {R : Type u_2} [Fintype S] [Fintype R] [Nonempty R] (step : S → R → S) (T : ℕ) (f : S → ℝ) (s : S) : (ofStep step).iterate T f s = expList R T fun (l : List R) => f (List.foldl step s l)

Iterating the kernel is averaging over T i.i.d. uniform rounds.

theorem Dynamics.Kernel.event_ofStep {S : Type u_1} {R : Type u_2} [Fintype S] [Fintype R] [Nonempty R] (step : S → R → S) (P : S → Prop) (T : ℕ) (s : S) : (ofStep step).event P T s = expList R T fun (l : List R) => if P (List.foldl step s l) then 1 else 0

theorem Dynamics.expList_escape {S : Type u_1} {R : Type u_2} [Fintype R] [Nonempty R] (step : S → R → S) {p : ℝ} (hp : 0 ≤ p) (T : ℕ) (G : ℕ → Set S) (x : S) : x ∈ G 0 → (∀ t < T, ∀ y ∈ G t, (avg fun (r : R) => if step y r ∈ G (t + 1) then 0 else 1) ≤ p) → (expList R T fun (l : List R) => if List.foldl step x l ∈ G T then 0 else 1) ≤ ↑T * p

Escaping a moving target. If a round-based process starts in G 0 and, for every t < T, one round from any state of G t misses G (t + 1) with probability at most p, then after T rounds it lies outside G T with probability at most T p. This is the union bound over rounds used by lower bounds such as Theorem 4.2 of Becchetti et al. (SPAA 2014).