Time-dependent finite chains

A time-dependent chain moves from time t to time t + 1 with the kernel K t. This is the setting of the voter model on a dynamic graph sequence G₁, G₂, … in Berenbrink, Giakkoupis, Kermarrec, Mallmann-Trenn, Bounds on the voter model in dynamic networks (ICALP 2016), whose drift lemma (Lemma 2.2) lets the drift depend on the time through the conductance φ_t.

iterateSeq K n f a is the expected value of f after the steps K 0, …, K (n - 1), started at a. For a constant family it is Kernel.iterate (iterateSeq_const).

noncomputable def Dynamics.Kernel.iterateSeq {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) : ℕ → (α → ℝ) → α → ℝ

Expected value of f after n steps of the time-dependent chain that moves from time t to time t + 1 with the kernel K t, started at a. The last step K n is applied first to f.

Equations

• Dynamics.Kernel.iterateSeq K 0 x✝ = x✝
• Dynamics.Kernel.iterateSeq K n.succ x✝ = Dynamics.Kernel.iterateSeq K n ((K n).apply x✝)

theorem Dynamics.Kernel.iterateSeq_const {α : Type u_1} [Fintype α] (K : Kernel α) (n : ℕ) (f : α → ℝ) : iterateSeq (fun (x : ℕ) => K) n f = K.iterate n f

A constant family of kernels is a time-homogeneous chain.

@[simp]

theorem Dynamics.Kernel.iterateSeq_zero {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (f : α → ℝ) : iterateSeq K 0 f = f

Zero steps leave the observable unchanged.

theorem Dynamics.Kernel.iterateSeq_succ {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (n : ℕ) (f : α → ℝ) : iterateSeq K (n + 1) f = iterateSeq K n ((K n).apply f)

The last of n + 1 steps acts first on the observable.

Linearity and monotonicity

theorem Dynamics.Kernel.apply_add {α : Type u_1} [Fintype α] (K : Kernel α) (f g : α → ℝ) : (K.apply fun (a : α) => f a + g a) = fun (a : α) => K.apply f a + K.apply g a

One step is additive in the observable.

theorem Dynamics.Kernel.apply_mul {α : Type u_1} [Fintype α] (K : Kernel α) (c : ℝ) (f : α → ℝ) : (K.apply fun (a : α) => c * f a) = fun (a : α) => c * K.apply f a

One step commutes with scalar multiplication.

theorem Dynamics.Kernel.apply_const {α : Type u_1} [Fintype α] (K : Kernel α) (c : ℝ) : (K.apply fun (x : α) => c) = fun (x : α) => c

One step fixes constant observables.

theorem Dynamics.Kernel.iterateSeq_mono {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (n : ℕ) {f g : α → ℝ} (h : ∀ (a : α), f a ≤ g a) (a : α) : iterateSeq K n f a ≤ iterateSeq K n g a

Expectations are monotone in the observable.

theorem Dynamics.Kernel.iterateSeq_add {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (n : ℕ) (f g : α → ℝ) : (iterateSeq K n fun (a : α) => f a + g a) = fun (a : α) => iterateSeq K n f a + iterateSeq K n g a

Expectations are additive in the observable.

theorem Dynamics.Kernel.iterateSeq_mul {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (n : ℕ) (c : ℝ) (f : α → ℝ) : (iterateSeq K n fun (a : α) => c * f a) = fun (a : α) => c * iterateSeq K n f a

Expectations commute with scalar multiplication.

theorem Dynamics.Kernel.iterateSeq_const_fun {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (n : ℕ) (c : ℝ) : (iterateSeq K n fun (x : α) => c) = fun (x : α) => c

Constant observables keep their value.

theorem Dynamics.Kernel.iterateSeq_nonneg {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (n : ℕ) {f : α → ℝ} (h : ∀ (a : α), 0 ≤ f a) (a : α) : 0 ≤ iterateSeq K n f a

Nonnegative observables have nonnegative expectations.

theorem Dynamics.Kernel.iterateSeq_lin {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (n : ℕ) (u v : ℝ) (f g : α → ℝ) (a : α) : iterateSeq K n (fun (x : α) => u * f x + v * g x) a = u * iterateSeq K n f a + v * iterateSeq K n g a

iterateSeq of a linear combination of two observables.

theorem Dynamics.Kernel.iterateSeq_one_sub {α : Type u_1} [Fintype α] (K : ℕ → Kernel α) (n : ℕ) (f : α → ℝ) (a : α) : iterateSeq K n (fun (x : α) => 1 - f x) a = 1 - iterateSeq K n f a

Expectation of a complement: 𝔼[1 - f] = 1 - 𝔼[f].

theorem Dynamics.Kernel.event_eq_iterateSeq {α : Type u_1} [Fintype α] (K : Kernel α) (s : α → Prop) [DecidablePred s] (n : ℕ) (a : α) : K.event s n a = iterateSeq (fun (x : ℕ) => K) n (fun (b : α) => if s b then 1 else 0) a

Kernel.event (classical decidability) as an iterateSeq of a constant family, with any decidability instance.