claimroutineinferred_dep

Spectral gap on finite transitive actions

Lazy walk has Dirichlet form ≥ ∥f∥2/(4mCH2)\|f\|^2/(4mC_H^2) off constants
gives the spectral gap on finite transitive sets
Claim·§6 Conditional averaging in the shared environment·inside lemUniform spectral gap for affine group actions

Statement (paper)

Let ρ\rho be the permutation representation of a finite transitive GHG_H-set with the uniform probability measure, let m=∣S∣m=|\mathcal S|, and let KH=12I+12m∑g∈Sρ(g)K_H=\frac12I+\frac1{2m}\sum_{g\in\mathcal S}\rho(g). Then KHK_H is self-adjoint with spectrum in [0,1][0,1], its invariant functions are exactly the constants, and every ff orthogonal to constants satisfies ⟨f,(I−KH)f⟩≥14mCH2∥f∥22\langle f,(I-K_H)f\rangle\ge\frac1{4mC_H^2}\|f\|_2^2, so KHK_H has a spectral gap bounded below by 14mCH2\frac1{4mC_H^2}, depending only on HH.

In plain English

For the permutation representation of any finite transitive GHG_H-set, the lazy walk operator KH=12I+12m∑g∈Sρ(g)K_H=\frac12I+\frac1{2m}\sum_{g\in\mathcal S}\rho(g) is self-adjoint with spectrum in [0,1][0,1], fixes only constants, and satisfies ⟨f,(I−KH)f⟩≥14mCH2∥f∥22\langle f,(I-K_H)f\rangle\ge\frac1{4mC_H^2}\|f\|_2^2 for all ff orthogonal to constants.

Why it's here

This is the step that converts the representation-theoretic bound on distance to the invariant subspace into a spectral gap for the walk, which is what the lemma asserts. For ff orthogonal to constants, transitivity makes the invariant vectors exactly the constants, so the previous claim's bound ∥f−Pinvf∥≤CHδ\|f-P_{\rm inv}f\|\le C_H\delta forces some generator to move ff by a definite fraction of ∥f∥\|f\|. That lower-bounds the Dirichlet form ⟨f,(I−KH)f⟩\langle f,(I-K_H)f\rangle by a constant depending only on HH, uniformly over all finite transitive GHG_H-sets.
Classified routine:
Standard conversion of an almost-invariant-vector (Kazhdan-type) bound into a spectral gap for the lazy Cayley/Schreier walk via the Dirichlet form identity; follows directly from the preceding claim and transitivity.

Uses

claimDistance to full invariant subspace bounded

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Spectral gap on finite transitive actions" rests on claim-lem-env-affine-2