The tanh contraction lemma

Proved

MarkovMixing.ising_tanh_lemma

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

markov-chainsmixing-timesprobability

Fix an inverse temperature $\beta>0$ and consider the function

g(x)\;=\;\tanh\bigl(\beta(x+1)\bigr)-\tanh\bigl(\beta(x-1)\bigr),

which measures how much the conditional probability of a $+$ spin under the Ising Glauber dynamics moves when the neighbourhood field increases from $x-1$ to $x+1$ (the heat-bath update at a site with neighbouring spin sum $S$ chooses $+$ with probability $(1+\tanh(\beta S))/2$ ).

The theorem (Lemma 15.2 of Levin–Peres–Wilmer) asserts four elementary properties:

$g$ is even: $g(-x)=g(x)$ for every real $x$ ;
$g$ is non-increasing on $[0,\infty)$ : $0\le x\le y$ implies $g(y)\le g(x)$ ;
$g(x)\le 2\tanh\beta$ for every real $x$ — the value at $x=0$ is the global maximum;
over odd integers the sharper bound holds: $g(k)\le\tanh(2\beta)$ for every odd $k\in\mathbb Z$ — the value at $k=\pm1$ is the maximum among odd integers.

These four inequalities are the entire analytic content of the high-temperature theorem: in the one-site coupling of two adjacent configurations, the probability that the updated site disagrees is controlled by $g$ evaluated at the neighbouring spin sum, which for a graph with all degrees even is an odd integer — whence the two conditions $\Delta\tanh\beta<1$ and $(\Delta/2)\tanh(2\beta)<1$ of the goal theorem.

Preamble

import Definitions.Def_mm_ising

Formal statement

namespace MarkovMixing

/-- **Lemma 15.2** (LPW): the function
`ϕ(x) = tanh(β(x+1)) − tanh(β(x−1))` is even, is decreasing on `[0,∞)`,
is bounded by `ϕ(0) = 2 tanh β`, and on odd integers is bounded by
`ϕ(1) = tanh 2β`. -/
theorem ising_tanh_lemma (β : ℝ) (hβ : 0 < β) :
    (∀ x : ℝ, Real.tanh (β * (-x + 1)) - Real.tanh (β * (-x - 1)) =
      Real.tanh (β * (x + 1)) - Real.tanh (β * (x - 1))) ∧
    (∀ x y : ℝ, 0 ≤ x → x ≤ y →
      Real.tanh (β * (y + 1)) - Real.tanh (β * (y - 1)) ≤
        Real.tanh (β * (x + 1)) - Real.tanh (β * (x - 1))) ∧
    (∀ x : ℝ, Real.tanh (β * (x + 1)) - Real.tanh (β * (x - 1)) ≤
      2 * Real.tanh β) ∧
    ∀ k : ℤ, Odd k →
      Real.tanh (β * (k + 1)) - Real.tanh (β * (k - 1)) ≤
        Real.tanh (2 * β) := 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 15.1, Lemma 15.2, Eqs. (15.3)-(15.4), p. 202

Read-back

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

Read-back: ising_tanh_lemma

Fix a real number $\beta$ with the single hypothesis $\beta > 0$ . Writing $g(x) = \tanh(\beta(x+1)) - \tanh(\beta(x-1))$ (the hyperbolic tangent is the standard real $\tanh$ ), the theorem asserts the conjunction of four claims:

Evenness. For every real $x$ ,

\tanh(\beta(-x+1)) - \tanh(\beta(-x-1)) \;=\; \tanh(\beta(x+1)) - \tanh(\beta(x-1)),

i.e. $g(-x) = g(x)$ .

Monotone decrease on $[0,\infty)$ . For all reals $x, y$ with $0 \le x$ and $x \le y$ ,

\tanh(\beta(y+1)) - \tanh(\beta(y-1)) \;\le\; \tanh(\beta(x+1)) - \tanh(\beta(x-1)),

i.e. $g(y) \le g(x)$ — a non-strict inequality, so $g$ is (weakly) decreasing on the nonnegative reals.

Global bound. For every real $x$ (of either sign),

\tanh(\beta(x+1)) - \tanh(\beta(x-1)) \;\le\; 2\tanh\beta,

i.e. $g(x) \le 2\tanh\beta$ . (Only an upper bound; no lower bound is asserted.)

Bound at odd integers. For every integer $k$ that is odd (odd in $\mathbb{Z}$ , so $k$ ranges over $\dots,-3,-1,1,3,\dots$ , negatives included), with $k$ coerced to a real number,

\tanh(\beta(k+1)) - \tanh(\beta(k-1)) \;\le\; \tanh(2\beta),

i.e. $g(k) \le \tanh(2\beta)$ at every odd integer.

All four parts are stated for the same fixed $\beta > 0$ ; no other hypotheses appear, and no claim is made for $\beta \le 0$ . The inequalities in parts 2–4 are all non-strict ( $\le$ ), and parts 3 and 4 have different right-hand sides ( $2\tanh\beta$ for all reals versus $\tanh(2\beta)$ for odd integers).

Human review

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

View graph