Power-moment decay bounds the Rayleigh quotient of a symmetric operator

Proved

MarkovChainCLT.quadratic_le_of_symmetric_power_decay_unit

by Zehao Jin · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

functional-analysisrayleigh-quotientself-adjointspectral-gap

Let $T$ be a bounded symmetric operator on a real inner-product space, and let $x$ be a unit vector. Suppose $t\ge0$ , $C\ge0$ , and every power moment of $x$ obeys

|\langle T^n x,x\rangle|\le Ct^n \qquad(n\ge0).

Then the one-step Rayleigh form is bounded by the same rate:

|\langle Tx,x\rangle|\le t.

This is an elementary spectral-radius principle for a single vector. Symmetry yields a moment-doubling inequality, and iteration along powers of two forces any larger one-step Rayleigh quotient to contradict the assumed exponential moment bound.

Preamble

import Mathlib.Analysis.InnerProductSpace.Rayleigh
import Mathlib.Analysis.SpecificLimits.Basic

open Filter Function
open scoped NNReal Topology

Formal statement

theorem MarkovChainCLT.quadratic_le_of_symmetric_power_decay_unit
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (T : E →L[ℝ] E) (hT : (T : E →ₗ[ℝ] E).IsSymmetric)
    (x : E) (hx : ‖x‖ = 1)
    (t C : ℝ) (ht : 0 ≤ t) (hC : 0 ≤ C)
    (hdecay : ∀ n : ℕ, |inner ℝ ((T ^ n) x) x| ≤ C * t ^ n) :
    |inner ℝ (T x) x| ≤ t := by sorry

Source

G. O. Roberts and J. S. Rosenthal, Geometric Ergodicity and Hybrid Markov Chains, Electronic Communications in Probability 2 (1997), Theorem 2 and proof, pp. 7-9, https://www.probability.ca/jeff/ftpdir/hybrid.pdf. This is the single-vector moment-growth core of the self-adjoint spectral argument.

View graph