claimroutineinferred_dep

Expander mixing bound from small bias

Claim·§6.1 Initial tests that exclude small violation sets·inside lemSparse parity checks force large supports

Statement (paper)

For sets

U

of left vertices and

V

of right vertices of the graph

G

, let

e_G(U,V)

count the edges between them, including multiplicity. Then

e_G(U,V)\le \frac{d_G|U||V|}{q_G}+\varepsilon d_G\sqrt{|U||V|}

In plain English

For any set

U

of left vertices and any set

V

of right vertices of

G

, the number of edges between them (with multiplicity) is at most

\frac{d_G|U||V|}{q_G}+\varepsilon d_G\sqrt{|U||V|}

Why it's here

Since the shifts from the small-bias claim make every nonzero Fourier coefficient at most

\varepsilon d_G

, the graph's nontrivial eigenvalues are small, which gives this expander mixing inequality. It bounds how many edges a small vertex set can have inside its neighborhood, and the Tanner-code weight bound then uses this to show nonzero words must have large weight.

Classified routine:

Direct application of the expander mixing lemma (Alon–Chung 1988) to the Cayley-type bipartite graph, whose nontrivial eigenvalues are bounded by the small-bias Fourier bound from the previous claim.

Uses

claimSmall-bias shifts exist and can be found

Used by

claimTanner code nonzero words have large weight

Sources

PaperOpen

Section: §6.1 Initial tests that exclude small violation sets
Page: —
Label: —
Line: main_full_version.tex:3336

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Expander mixing bound from small bias" rests on claim-lem-sparse-checks-2