claimroutine

Almost-invariant vectors are near translation-invariant

Generator-almost-invariant vectors are within 10qδ10q\delta of translation-fixed vectors
first step toward the spectral gap
Claim·§6 Conditional averaging in the shared environment·inside lemUniform spectral gap for affine group actions

Statement (paper)

Let PtrP_{\rm tr} be the orthogonal projection onto the subspace of ρ\rho-vectors fixed by all translations ZH\mathbb Z^H, and let q=(H2)q=\binom H2. Then for every unitary representation ρ\rho of GHG_H and every vector ξ\xi, with δ=max⁡g∈S∥ρ(g)ξ−ξ∥\delta=\max_{g\in\mathcal S}\|\rho(g)\xi-\xi\|, one has ∥ξ−Ptrξ∥≤10qδ\|\xi-P_{\rm tr}\xi\|\le 10q\delta.

In plain English

For any unitary representation ρ\rho of GH=SLH(Z)⋉ZHG_H=\mathrm{SL}_H(\mathbb Z)\ltimes\mathbb Z^H and any vector ξ\xi moved by at most δ\delta by each generator in S\mathcal S, the distance from ξ\xi to the subspace of translation-fixed vectors is at most 10qδ10q\delta, where q=(H2)q=\binom H2.

Why it's here

This is the first step in showing that near-invariance under the generators forces near-invariance under the full group. It shows that a vector moved little by the generators is already close to the translation-fixed subspace, with a constant depending only on HH. The follow-up claim then combines this with a Kazhdan-type bound on the SLH(Z)\mathrm{SL}_H(\mathbb Z) part to reach the full invariant subspace.
Classified routine:
A quantitative form of relative property (T) for the pair (SLH(Z)⋉ZH,ZH)(\mathrm{SL}_H(\mathbb Z)\ltimes\mathbb Z^H,\mathbb Z^H), known from Kazhdan–Margulis and Burger's spectral argument (with quantitative versions by Shalom). Here it is restated with an explicit constant 10q10q, presumably via a standard generator-by-generator argument.

Uses

Nothing else in the paper

Used by

claimDistance to full invariant subspace bounded

Sources

PaperOpen
Section
§6 Conditional averaging in the shared environment
Page
—
Label
—
Line
sections/averaging.tex:42
Leannot aligned

Phase 2 aligns this node to a Lean declaration.