Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 1.1 — the time-reversed process keeps π\piπ in equilibrium

Proved
KellyStochasticNetworks.reversed_process_rates

by naimengye · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chainreversibilitystochastic-networks

Let (X(t),t∈R)(X(t), t \in \mathbb{R})(X(t),t∈R) be a stationary Markov process on a finite state space SSS with transition rates qqq and a strictly positive equilibrium distribution π\piπ, so that π\piπ satisfies the equilibrium equations for qqq. Proposition 1.1 of Kelly and Yudovina states that the reversed process Y(t)=X(−t)Y(t) = X(-t)Y(t)=X(−t) is again a stationary Markov process, with the same equilibrium distribution π\piπ and with transition rates

q′(j,k)=π(k) q(k,j)π(j).q'(j,k) = \frac{\pi(k)\,q(k,j)}{\pi(j)}.q′(j,k)=π(j)π(k)q(k,j)​.

The two algebraic assertions that content amounts to, and which Exercise 1.4 asks the reader to check, are formalized here:

  1. the reversed rates have the same total rate out of every state,
∑k∈Sq′(j,k)=∑k∈Sq(j,k)for all j∈S,\sum_{k \in S} q'(j,k) = \sum_{k \in S} q(j,k) \qquad \text{for all } j \in S,k∈S∑​q′(j,k)=k∈S∑​q(j,k)for all j∈S,

so a jump of the reversed process occurs at the same rate as a jump of the original; 2. π\piπ satisfies the equilibrium equations for q′q'q′, so π\piπ is again an equilibrium distribution for the reversed process.

Together these say that q′q'q′ is a legitimate rate matrix with the same holding-time parameters as qqq, 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 π\piπ is what makes the quotient defining q′q'q′ meaningful.

Preamble
import Mathlib
import Definitions.Def_KellyStochasticNetworks_Balance
Formal statement
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 KellyStochasticNetworks
Source
Kelly & Yudovina, Stochastic Networks, CUP 2014, pp. 16-17 (PDF pp. 24-25), Proposition 1.1 and Exercise 1.4: 'Check that the distribution (pi(j), j in S) and the transition rates (q'(j,k), j,k in S) found in Proposition 1.1 satisfy the equilibrium equations.' sha256 ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a
Human review
  • Endorsed by Shuze Chen · Sep 25, 2026

    Confirmed by the moderator at approval.

  • Endorsed by naimengye · Sep 25, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me