Finite transition kernels and expectations at finite times

@[reducible, inline]

abbrev Dynamics.Kernel (α : Type u_1) [Fintype α] : Type u_1

A stochastic transition matrix, with its row normalization built in.

Equations

• Dynamics.Kernel α = (α → Dynamics.Distribution α)

noncomputable def Dynamics.Kernel.apply {α : Type u_1} [Fintype α] (K : Kernel α) (f : α → ℝ) (a : α) : ℝ

The transition operator on real observables.

Equations

• K.apply f a = (K a).expect f

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

Expected observable after n steps, starting at a.

Equations

• K.iterate 0 x✝ = x✝
• K.iterate n.succ x✝ = K.apply (K.iterate n x✝)

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem Dynamics.Kernel.iterate_add_time {α : Type u_1} [Fintype α] (K : Kernel α) (m n : ℕ) (f : α → ℝ) : K.iterate (m + n) f = K.iterate m (K.iterate n f)

theorem Dynamics.Kernel.iterate_invariant {α : Type u_1} [Fintype α] (K : Kernel α) {f : α → ℝ} (h : K.apply f = f) (n : ℕ) : K.iterate n f = f

A harmonic observable has constant expectation at every finite time.

noncomputable def Dynamics.Kernel.event {α : Type u_1} [Fintype α] (K : Kernel α) (s : α → Prop) (n : ℕ) (a : α) : ℝ

Probability of occupying an event at a finite time.

Equations

• K.event s n a = K.iterate n (fun (b : α) => if s b then 1 else 0) a

theorem Dynamics.Kernel.event_nonneg {α : Type u_1} [Fintype α] (K : Kernel α) (s : α → Prop) (n : ℕ) (a : α) : 0 ≤ K.event s n a

theorem Dynamics.Kernel.event_le_one {α : Type u_1} [Fintype α] (K : Kernel α) (s : α → Prop) (n : ℕ) (a : α) : K.event s n a ≤ 1

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

event computed with any decidability instance for the event.

def Dynamics.Kernel.Stationary {α : Type u_1} [Fintype α] (K : Kernel α) (p : Distribution α) : Prop

Stationarity of a distribution for a finite transition kernel.

Equations

• K.Stationary p = ∀ (b : α), ∑ a : α, p.weight a * (K a).weight b = p.weight b

theorem Dynamics.Kernel.stationary_expect {α : Type u_1} [Fintype α] (K : Kernel α) (p : Distribution α) (h : K.Stationary p) (f : α → ℝ) : p.expect (K.apply f) = p.expect f