Power decay on a dense subspace bounds a symmetric operator norm

Proved

MarkovChainCLT.opNorm_le_of_symmetric_power_decay_on_dense

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

dense-subspacefunctional-analysisself-adjointspectral-gap

Let $T$ be a bounded symmetric operator on a real inner-product space, and let $D$ be a dense linear subspace. Suppose $t\ge0$ and, for every $z\in D$ , there is a finite constant $C_z\ge0$ such that

|\langle T^n z,z\rangle|\le C_z t^n \qquad(n\ge0).

Then the operator norm is bounded by the same rate:

\|T\|\le t.

The constant may depend on the vector. The result upgrades vectorwise moment decay on a dense core to a uniform spectral bound by normalization, continuity of the quadratic form, and the Rayleigh-quotient characterization of the norm of a symmetric operator.

Preamble

import Theorems.Thm_MarkovChainCLT_quadratic_le_of_symmetric_power_decay_unit
import Mathlib.Analysis.InnerProductSpace.Rayleigh

open Filter Function Set
open scoped NNReal Topology

Formal statement

theorem MarkovChainCLT.opNorm_le_of_symmetric_power_decay_on_dense
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (T : E →L[ℝ] E) (hT : (T : E →ₗ[ℝ] E).IsSymmetric)
    (D : Submodule ℝ E) (hD : Dense (D : Set E))
    (t : ℝ) (ht : 0 ≤ t)
    (hdecay : ∀ z : D, ∃ C : ℝ, 0 ≤ C ∧
      ∀ n : ℕ, |inner ℝ ((T ^ n) (z : E)) (z : E)| ≤ C * t ^ n) :
    ‖T‖ ≤ 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 packages the dense-subspace-to-spectral-gap step for symmetric operators.

View graph