Lemma 9.6 -- the Green's function and effective resistance
ProvedMarkovMixing.green_resistanceLet be a network on a finite vertex set: a symmetric nonnegative conductance function with total conductance at every vertex, carrying the walk , assumed irreducible. Fix distinct vertices . The Green's function of the walk stopped at is the expected number of visits to a vertex before first hitting :
the walk starting at and being the hitting time of . The effective resistance is defined through the voltage: with (the harmonic function with boundary values , ), the current flowing out of is , and .
The theorem (Lemma 9.6 of Levin–Peres–Wilmer) asserts:
The expected number of returns to the starting point before reaching is exactly the vertex conductance times the effective resistance — the identity through which escape probabilities and resistances translate into each other.
import Definitions.Def_mm_network
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