claimroutineinferred_dep
Distance to full invariant subspace bounded
Such vectors are within of the -invariant subspace by Kazhdan
upgrades closeness to full invariance
Claim·§6 Conditional averaging in the shared environment·inside lemUniform spectral gap for affine group actions
Statement (paper)
Let be the projection onto the subspace fixed by all translations, the projection onto the full -invariant subspace, and the Kazhdan constant for the elementary generators. Then and with , so the same generating set controls the distance to the invariant vectors in every unitary representation, with a constant depending only on .
In plain English
If a vector is moved by at most by each generator, then and with . Here projects onto translation-fixed vectors, onto -invariant vectors, and is the Kazhdan constant of the elementary generators.
Why it's here
This upgrades the previous claim, which gives closeness to translation-fixed vectors, to closeness to fully -invariant vectors by applying the Kazhdan property to the translation-invariant part. The bound holds in every unitary representation with a constant depending only on , which is what the next claim needs to get a spectral gap on finite transitive -sets.
Classified routine:
Direct consequence of the previous claim plus the standard Kazhdan property (T) inequality for SL_H(Z), H≥3 (Kazhdan 1967; Bekka–de la Harpe–Valette), applied to the translation-invariant subrepresentation, followed by the triangle inequality.
Uses
Used by
Sources
PaperOpen
- Section
- §6 Conditional averaging in the shared environment
- Page
- —
- Label
—- Line
sections/averaging.tex:74
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infoinferred_depoutline: "Distance to full invariant subspace bounded" rests on claim-lem-env-affine-1