claimroutineinferred_dep

Distance to full invariant subspace bounded

Such vectors are within CHδC_H\delta of the GHG_H-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 PtrP_{\rm tr} be the projection onto the subspace fixed by all translations, PinvP_{\rm inv} the projection onto the full GHG_H-invariant subspace, and κH>0\kappa_H>0 the Kazhdan constant for the elementary generators. Then ∥Ptrξ−Pinvξ∥≤κH−1δ\|P_{\rm tr}\xi-P_{\rm inv}\xi\|\le\kappa_H^{-1}\delta and ∥ξ−Pinvξ∥≤CHδ\|\xi-P_{\rm inv}\xi\|\le C_H\delta with CH=10q+κH−1C_H=10q+\kappa_H^{-1}, so the same generating set controls the distance to the invariant vectors in every unitary representation, with a constant depending only on HH.

In plain English

If a vector ξ\xi is moved by at most δ\delta by each generator, then ∥Ptrξ−Pinvξ∥≤κH−1δ\|P_{\rm tr}\xi-P_{\rm inv}\xi\|\le\kappa_H^{-1}\delta and ∥ξ−Pinvξ∥≤CHδ\|\xi-P_{\rm inv}\xi\|\le C_H\delta with CH=10q+κH−1C_H=10q+\kappa_H^{-1}. Here PtrP_{\rm tr} projects onto translation-fixed vectors, PinvP_{\rm inv} onto GHG_H-invariant vectors, and κH\kappa_H 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 GHG_H-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 HH, which is what the next claim needs to get a spectral gap on finite transitive GHG_H-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.

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

  • info
    inferred_dep
    outline: "Distance to full invariant subspace bounded" rests on claim-lem-env-affine-1