Definition Lyapunov function [efr-C3WA]

Let t: S \to A + S be a kernel. A function u: A + S \to \mathbb {R} is called a Lyapunov function for t if u(a) = 0 and E_{x' \sim t(x)} u(x') < u(x) for all x