Proposition 1.1 — the time-reversed process keeps in equilibrium
ProvedKellyStochasticNetworks.reversed_process_ratesLet be a stationary Markov process on a finite state space with transition rates and a strictly positive equilibrium distribution , so that satisfies the equilibrium equations for . Proposition 1.1 of Kelly and Yudovina states that the reversed process is again a stationary Markov process, with the same equilibrium distribution and with transition rates
The two algebraic assertions that content amounts to, and which Exercise 1.4 asks the reader to check, are formalized here:
- the reversed rates have the same total rate out of every state,
so a jump of the reversed process occurs at the same rate as a jump of the original; 2. satisfies the equilibrium equations for , so is again an equilibrium distribution for the reversed process.
Together these say that is a legitimate rate matrix with the same holding-time parameters as , and that reversing a stationary process does not disturb its equilibrium distribution.
Formalization Note The state space is taken finite so that every sum appearing is a finite sum; the positivity of is what makes the quotient defining meaningful.
import Mathlib import Definitions.Def_KellyStochasticNetworks_Balance
namespace KellyStochasticNetworks
theorem reversed_process_rates {S : Type*} [Fintype S] (π : S → ℝ) (q : S → S → ℝ)
(hπ : ∀ j, 0 < π j) (h : FullBalance π q) :
(∀ j : S, (∑' k : S, reversedRates π q j k) = ∑' k : S, q j k) ∧
FullBalance π (reversedRates π q) := by sorry
end KellyStochasticNetworksConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.