Expectations of finite weighted trajectories

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

Expected functional of the history and endpoint of n transitions. The history contains the initial state and the following n - 1 states; the endpoint is supplied separately, so the definition also handles zero steps.

Equations

• K.trajectory 0 x✝¹ x✝ = x✝ [] x✝¹
• K.trajectory n.succ x✝¹ x✝ = (K x✝¹).expect fun (b : α) => K.trajectory n b fun (l : List α) (c : α) => x✝ (x✝¹ :: l) c

theorem Dynamics.Kernel.trajectory_endpoint {α : Type u_1} [Fintype α] (K : Kernel α) (n : ℕ) (a : α) (f : α → ℝ) : (K.trajectory n a fun (x : List α) (b : α) => f b) = K.iterate n f a

Endpoint observables agree with transition-operator iteration.