Theorem 9.12 -- Rayleigh's monotonicity law

Proved

MarkovMixing.rayleigh_monotonicity

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

markov-chainsmixing-timesprobability

Let $c$ and $c'$ be two networks on the same finite vertex set — symmetric nonnegative conductance functions, each with strictly positive total conductance $c(x)=\sum_yc(x,y)$ at every vertex and an irreducible associated walk $P(x,y)=c(x,y)/c(x)$ . For distinct vertices $a\ne z$ , the effective resistance $R_c(a\leftrightarrow z)$ is defined through the voltage $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$ and the current $\|I\|=\sum_yc(a,y)[W(a)-W(y)]$ as $R_c(a\leftrightarrow z)=\|I\|^{-1}$ .

The theorem (Rayleigh's Monotonicity Law, Theorem 9.12 of Levin–Peres–Wilmer) asserts: if $c'(x,y)\le c(x,y)$ on every edge — resistances are only increased — then

R_c(a\leftrightarrow z)\;\le\;R_{c'}(a\leftrightarrow z).

Decreasing conductances can only increase effective resistance. Deceptively simple, this is one of the most-used facts of the theory: it lets one bound resistances in a complicated network by deleting edges (setting conductances to zero) or by comparison with a tractable subnetwork, and through the commute-time identity it transfers to monotonicity statements for hitting times.

Preamble

import Definitions.Def_mm_network

Formal statement

namespace MarkovMixing

/-- **Theorem 9.12, Rayleigh's Monotonicity Law** (LPW): decreasing
conductances (increasing resistances) can only increase the effective
resistance: if `c' ≤ c` edgewise, then `R_c(a↔z) ≤ R_{c'}(a↔z)`. -/
theorem rayleigh_monotonicity {V : Type*} [Fintype V] [DecidableEq V]
    (c c' : V → V → ℝ) (hc : IsConductance c) (hc' : IsConductance c')
    (hpos : ∀ x : V, 0 < vertexConductance c x)
    (hpos' : ∀ x : V, 0 < vertexConductance c' x)
    (hirr : Irreducible (networkWalk c)) (hirr' : Irreducible (networkWalk c'))
    (hle : ∀ x y : V, c' x y ≤ c x y) (a z : V) (haz : a ≠ z) :
    effectiveResistance c a z ≤ 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, Theorem 9.12, p. 123

Read-back

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

Let $V$ be a finite type with decidable equality, and let $c, c' : V \times V \to \mathbb{R}$ be two functions each satisfying nonnegativity and symmetry — $c(x,y) \ge 0$ , $c(x,y) = c(y,x)$ , and likewise for $c'$ (self-loop values $c(x,x)$ are permitted). Write $c(x) = \sum_{y \in V} c(x,y)$ and $c'(x) = \sum_{y \in V} c'(x,y)$ for the vertex conductances, and assume both are strictly positive at every vertex: $c(x) > 0$ and $c'(x) > 0$ for all $x \in V$ . Let $P$ and $P'$ be the transition matrices $P(x,y) = c(x,y)/c(x)$ and $P'(x,y) = c'(x,y)/c'(x)$ , and assume each is irreducible in the sense that for every pair $x, y \in V$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (respectively $(P'^t)(x,y) > 0$ ; since $P^0$ is the identity, the case $x = y$ is automatic). Assume the pointwise comparison $c'(x,y) \le c(x,y)$ for all $x, y \in V$ , and fix two vertices $a \ne z$ . For a conductance function $b$ , the effective resistance $\mathcal{R}_b(a,z)$ is defined as follows: the voltage $v_b(x)$ is the probability that the Markov chain with transition matrix $b(x,y)/b(x)$ started at $x$ reaches $a$ strictly before $z$ — concretely $v_b(x) = \sum_{t=0}^{\infty} \sum_{\omega} \prod_{i=0}^{t-1} \frac{b(\omega_i,\omega_{i+1})}{b(\omega_i)}$ , summed over paths $\omega : \{0,\dots,t\} \to V$ with $\omega_0 = x$ , $\omega_t = a$ , $\omega_i \ne a$ for $i < t$ , and $\omega_i \ne z$ for all $i \le t$ (so $v_b(a) = 1$ , $v_b(z) = 0$ ) — the current strength is $I_b = \sum_{y \in V} b(a,y)\,\bigl(v_b(a) - v_b(y)\bigr)$ , and $\mathcal{R}_b(a,z) = I_b^{-1}$ , with the Lean convention that the reciprocal of $0$ is $0$ (so if the current strength for either network were $0$ , the corresponding effective resistance would be the junk value $0$ ). Under all of these hypotheses, the theorem asserts the single inequality

\mathcal{R}_c(a,z) \le \mathcal{R}_{c'}(a,z),

i.e. the effective resistance between $a$ and $z$ computed from the larger conductance function $c$ is less than or equal to the effective resistance computed from the smaller conductance function $c'$ (non-strict inequality, for this one fixed pair of vertices).

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