Proposition 9.1 -- existence and uniqueness of harmonic extensions

Proved

MarkovMixing.harmonic_extension

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

markov-chainsmixing-timesprobability

Let $P$ be an irreducible Markov chain on a finite state space $V$ . A function $h:V\to\mathbb R$ is harmonic at $x$ when it satisfies the mean-value property $h(x)=\sum_yP(x,y)\,h(y)$ . Fix a nonempty set of states $B$ and boundary data $f:B\to\mathbb R$ , write $\tau_B$ for the first time the chain visits $B$ , and let $\mathbb P_x\{X_{\tau_B}=y\}$ denote the probability that the chain started at $x$ first enters $B$ at the state $y$ . Define the harmonic extension of $f$ as its expected boundary value at the first visit,

h(x)=\mathbb E_x\bigl[f(X_{\tau_B})\bigr]=\sum_{y\in B}f(y)\,\mathbb P_x\{X_{\tau_B}=y\}.

The theorem (Proposition 9.1 of Levin–Peres–Wilmer) asserts:

$h$ agrees with $f$ on $B$ ;
$h$ is harmonic at every state outside $B$ ;
$h$ is the unique such function: any $g$ that agrees with $f$ on $B$ and is harmonic off $B$ equals $h$ everywhere.

This is the discrete Dirichlet problem: boundary data on $B$ extends in exactly one way to a function harmonic off $B$ , and the extension is probabilistic. Voltages in the electrical dictionary are exactly such extensions.

Preamble

import Definitions.Def_mm_network

Formal statement

namespace MarkovMixing

/-- **Proposition 9.1** (LPW): for an irreducible chain and a nonempty set
`B` of states with boundary data `f`, the function
`h(x) = E_x f(X_{τ_B}) = ∑_{y ∈ B} f(y) P_x{X_{τ_B} = y}` is the unique
extension of `f` that agrees with `f` on `B` and is harmonic off `B`. -/
theorem harmonic_extension {V : Type*} [Fintype V] [DecidableEq V]
    (P : Matrix V V ℝ) (hP : IsStochastic P) (hirr : Irreducible P)
    (B : Finset V) (hB : B.Nonempty) (f : V → ℝ) :
    (∀ x ∈ B, (∑ y ∈ B, f y * firstHitAtProb P x B y) = f x) ∧
    HarmonicOn P (fun x => ∑ y ∈ B, f y * firstHitAtProb P x B y)
      {x : V | x ∉ B} ∧
    ∀ g : V → ℝ, (∀ x ∈ B, g x = f x) → HarmonicOn P g {x : V | x ∉ B} →
      g = fun x => ∑ y ∈ B, f y * firstHitAtProb P x B y := 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.2, Proposition 9.1, p. 116

Read-back

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

Read-back: harmonic_extension

Let $V$ be a finite type with decidable equality, and let $P$ be a $V \times V$ real matrix assumed stochastic ( $P(x,y) \ge 0$ for all $x,y$ , and $\sum_{y \in V} P(x,y) = 1$ for every $x$ ) and irreducible in the bundle's sense: for all $x, y \in V$ there exists some $t \in \mathbb{N}$ (with $t = 0$ allowed, in which case $P^0$ is the identity matrix) such that the $(x,y)$ entry of $P^t$ is strictly positive. Let $B$ be a nonempty finite subset of $V$ (which forces $V$ nonempty), and let $f : V \to \mathbb{R}$ be a completely arbitrary function. Define the candidate extension $h : V \to \mathbb{R}$ by

h(x) = \sum_{y \in B} f(y)\, \mathbb{P}^{\mathrm{hit}}_B(x, y),

where $\mathbb{P}^{\mathrm{hit}}_B(x, y)$ (the bundle's firstHitAtProb) unfolds as follows: it is Lean's tsum over all $t \in \mathbb{N}$ — equal to the limit when the series is summable and defined as $0$ when it is not — of the total weight $\sum_\omega \prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1})$ over paths $\omega : \{0, \dots, t\} \to V$ satisfying $\omega_0 = x$ , $\omega_i \notin B$ for every index $i < t$ (the constraint covers the start but not the final index), and $\omega_t = y$ . Since here $y$ ranges over $B$ , for $x \notin B$ this is the summed weight over all lengths of walks that stay outside $B$ strictly before their final step and first enter $B$ at $y$ ; for $x \in B$ only the length- $0$ path can satisfy the constraints (any longer path violates $\omega_0 \notin B$ ), so $\mathbb{P}^{\mathrm{hit}}_B(x,y)$ is $1$ if $x = y$ and $0$ otherwise, making $h(x) = f(x)$ definitionally forced on $B$ . The theorem asserts, for every such $P$ , $B$ , $f$ , the conjunction of three claims:

Boundary agreement: for every $x \in B$ , $\sum_{y \in B} f(y)\, \mathbb{P}^{\mathrm{hit}}_B(x, y) = f(x)$ — i.e. $h = f$ on $B$ (by the degenerate-case analysis above this conjunct's content reduces to the length- $0$ path bookkeeping).
Harmonicity off $B$ : $h$ is harmonic on the complement of $B$ , meaning for every $x \in V$ with $x \notin B$ ,

h(x) = \sum_{y \in V} P(x,y)\, h(y),

the sum running over all of $V$ . (If $B = V$ this conjunct is vacuous.)

Uniqueness: for every function $g : V \to \mathbb{R}$ , if $g(x) = f(x)$ for all $x \in B$ and $g$ is harmonic on $\{x : x \notin B\}$ in the same sense ( $g(x) = \sum_{y} P(x,y) g(y)$ for every $x \notin B$ ), then $g$ equals $h$ as a function on all of $V$ , i.e. $g(x) = \sum_{y \in B} f(y)\, \mathbb{P}^{\mathrm{hit}}_B(x,y)$ for every $x \in V$ .

Note that $f$ is quantified over all real-valued functions on $V$ (its values off $B$ are irrelevant to $h$ but unconstrained), and no aperiodicity or reversibility is assumed.

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