Corollary 10.8 -- the resistance triangle inequality
ProvedMarkovMixing.resistance_trianglemarkov-chainsmixing-timesprobability
Let be a network on a finite vertex set: a symmetric nonnegative conductance function with total conductance at every vertex, whose associated walk is irreducible. For distinct vertices, the effective resistance is defined through the voltage and the current as .
The theorem (Corollary 10.8 of Levin–Peres–Wilmer) asserts that effective resistance satisfies the triangle inequality: for pairwise distinct vertices ,
Together with symmetry and positivity this makes a genuine metric on the vertices of a connected network — the resistance metric. In the book it is a direct consequence of the commute time identity, which converts the claim into the sub-additivity of round-trip times through the intermediate vertex .
Preamble
import Definitions.Def_mm_network
Formal statement
namespace MarkovMixing
/-- **Corollary 10.8** (LPW): effective resistance satisfies the triangle
inequality `R(a↔c) ≤ R(a↔b) + R(b↔c)`. -/
theorem resistance_triangle {V : Type*} [Fintype V] [DecidableEq V]
(c : V → V → ℝ) (hc : IsConductance c)
(hpos : ∀ x : V, 0 < vertexConductance c x)
(hirr : Irreducible (networkWalk c)) (a b z : V)
(hab : a ≠ b) (hbz : b ≠ z) (haz : a ≠ z) :
effectiveResistance c a z ≤
effectiveResistance c a b + effectiveResistance c b 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 10.3, Corollary 10.8, Eq. (10.10), p. 131