Lemma 9.6 -- the Green's function and effective resistance

Proved

MarkovMixing.green_resistance

by Shuze Chen · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

Let $c$ be a network on a finite vertex set: a symmetric nonnegative conductance function with total conductance $c(x)=\sum_yc(x,y)>0$ at every vertex, carrying the walk $P(x,y)=c(x,y)/c(x)$ , assumed irreducible. Fix distinct vertices $a\ne z$ . The Green's function of the walk stopped at $z$ is the expected number of visits to a vertex before first hitting $z$ :

G_{\tau_z}(a,x)=\mathbb E_a\bigl[\#\{t<\tau_z: X_t=x\}\bigr],

the walk starting at $a$ and $\tau_z$ being the hitting time of $z$ . The effective resistance $R(a\leftrightarrow z)$ is defined through the voltage: with $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$ (the harmonic function with boundary values $W(a)=1$ , $W(z)=0$ ), the current flowing out of $a$ is $\|I\|=\sum_yc(a,y)\bigl[W(a)-W(y)\bigr]$ , and $R(a\leftrightarrow z)=\|I\|^{-1}$ .

The theorem (Lemma 9.6 of Levin–Peres–Wilmer) asserts:

G_{\tau_z}(a,a)\;=\;c(a)\,R(a\leftrightarrow z).

The expected number of returns to the starting point before reaching $z$ is exactly the vertex conductance times the effective resistance — the identity through which escape probabilities and resistances translate into each other.

Preamble

import Definitions.Def_mm_network

Formal statement

namespace MarkovMixing

/-- **Lemma 9.6** (LPW): the Green's function of the network walk stopped at
`τ_z` satisfies `G_{τ_z}(a,a) = c(a) R(a ↔ z)`. -/
theorem green_resistance {V : Type*} [Fintype V] [DecidableEq V]
    (c : V → V → ℝ) (hc : IsConductance c)
    (hpos : ∀ x : V, 0 < vertexConductance c x)
    (hirr : Irreducible (networkWalk c)) (a z : V) (haz : a ≠ z) :
    greenFn (networkWalk c) a z a =
      vertexConductance c a * effectiveResistance c a z := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 9.4, Lemma 9.6, Eq. (9.18), p. 120

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: green_resistance

Let $V$ be a finite type with decidable equality, and let $c : V \times V \to \mathbb{R}$ satisfy the bundle's conductance predicate — $c(x,y) \ge 0$ and $c(x,y) = c(y,x)$ for all $x, y \in V$ (self-loops allowed) — together with the hypothesis that every vertex conductance is strictly positive: $c(x) := \sum_{y \in V} c(x,y) > 0$ for all $x$ . Let $P_c$ be the associated walk matrix, $P_c(x,y) = c(x,y)/c(x)$ (all denominators positive here), and assume $P_c$ is irreducible in the bundle's sense: for all $x, y \in V$ there exists $t \in \mathbb{N}$ (including possibly $t = 0$ , where $P_c^0$ is the identity) with $(P_c^t)(x,y) > 0$ . Fix two vertices $a, z \in V$ with $a \ne z$ (so $V$ has at least two elements). The theorem asserts the single real-number identity

G_z(a, a) = c(a) \cdot \mathcal{R}(a, z),

where the two sides unfold as follows.

The left side $G_z(a,a)$ is the bundle's greenFn of $P_c$ at $(a, z, a)$ : Lean's tsum over $t \in \mathbb{N}$ — the limit if the series is summable, and $0$ by convention if not — of the quantity

\sum_{\omega : \{0,\dots,t\} \to V} \mathbf{1}\big[\omega_0 = a,\ \omega_i \ne z \text{ for all } 0 \le i \le t,\ \omega_t = a\big] \prod_{i=0}^{t-1} P_c(\omega_i, \omega_{i+1}),

i.e. the total $P_c$ -weight of length- $t$ walks that start at $a$ , end at $a$ , and never visit $z$ at any time (the $t = 0$ term equals $1$ since $a \ne z$ ). Informally this is the expected number of visits to $a$ (counting time $0$ ) strictly before the walk from $a$ first hits $z$ , but the formal object is exactly the tsum just described.

The right side is the product of $c(a) = \sum_{y} c(a,y)$ with the bundle's effectiveResistance, which is the real inverse $\big(I(a,z)\big)^{-1}$ — equal to $0$ , not $+\infty$ , if $I(a,z) = 0$ — of the "current strength"

I(a,z) = \sum_{y \in V} c(a,y)\,\big(v(a) - v(y)\big).

Here $v(x)$ is the bundle's voltage: the tsum over $t \in \mathbb{N}$ (again $0$ if not summable) of the total $P_c$ -weight of paths $\omega : \{0,\dots,t\} \to V$ with $\omega_0 = x$ , $\omega_t = a$ , $\omega_i \ne a$ for all $i < t$ , and $\omega_i \ne z$ for all $0 \le i \le t$ — that is, walks from $x$ that hit $a$ for the first time at their final step while never visiting $z$ . In particular $v(a) = 1$ (only the length- $0$ path contributes, since $a \ne z$ ) and $v(z) = 0$ .

The claim is exactly this equality of two real numbers, for every $c$ , $a$ , $z$ satisfying the stated hypotheses; no claim of positivity, finiteness beyond the tsum conventions, or any inequality is made.

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph