LemmaStatement: AI-adaptedProof: AI-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Internal-edge mixing bound — Lemma 3.3

PDF p. 19: Lemma 3.3

Statement

Let $G = (V, E)$ be an $(n, d^{*}, α)$ -expander, and let $X \subseteq V$ . Then

$- α d^{*} ∣ X ∣ \leq e (X, X) - (d^{*} / n) ∣ X ∣^{2} \leq α d^{*} ∣ X ∣ .$

Here $e (X, X)$ counts ordered adjacency entries, so a non-loop edge internal to $X$ contributes twice and a loop in $X$ contributes once.

Statement references

Adjacency spectral expander — Definition 1.3

Oriented edge count between sets

Facts & Assumptions

[F1]

The expander has a nonempty finite vertex set of size $n$ , adjacency matrix $A$ , all-ones matrix $J$ , and centered adjacency matrix $Δ_{A} = A - (d^{*} / n) J$ satisfying $∥ Δ_{A} ∥ \leq α d^{*}$ (Adjacency spectral expander — Definition 1.3).

[F2]

The ordered count is $e (X, X) = \sum_{x \in X} \sum_{y \in X} A_{x y}$ , including diagonal entries (Oriented edge count between sets).

[F3]

The vertex inner product is $⟨ f, g ⟩ = \sum_{x \in V} \overline{f (x)} g (x)$ , with induced norm $∥ f ∥_{2}$ and matrix action by finite row sums (Finite vertex Hilbert space in the article convention). The operator norm is the supremum of $∥ H f ∥_{2} / ∥ f ∥_{2}$ over nonzero $f$ (Loewner order, Hermitian inner product, and operator norm).

[F4]

Cauchy–Schwarz gives $∣ ⟨ f, g ⟩ ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ ; the vertex-space convention transfers the cited linear-first version by conjugation (Cauchy–Schwarz: |⟨ u,v⟩|≤‖ u‖‖ v‖, with equality exactly for linearly dependent vectors, Finite vertex Hilbert space in the article convention).

Proof

Given: An $(n, d^{*}, α)$ -expander $G$ and $X \subseteq V$ .

Goal: Establish the two displayed inequalities.

Proof technique: direct.

1.1F1F2F3

Let $1_{X}$ be the indicator function, equal to $1$ on $X$ and $0$ outside it. The coordinate sums give $⟨ 1_{X}, A 1_{X} ⟩ = e (X, X)$ , $⟨ 1_{X}, J 1_{X} ⟩ = ∣ X ∣^{2}$ , and $∥ 1_{X} ∥_{2}^{2} = ∣ X ∣$ . Hence $⟨ 1_{X}, Δ_{A} 1_{X} ⟩ = e (X, X) - (d^{*} / n) ∣ X ∣^{2}$ .

2.1F1F3F4step 1.1∎

If $1_{X} = 0$ , then $∥ Δ_{A} 1_{X} ∥_{2} = 0$ ; otherwise the operator-norm definition gives $∥ Δ_{A} 1_{X} ∥_{2} \leq ∥ Δ_{A} ∥ ∥ 1_{X} ∥_{2}$ . Thus Cauchy–Schwarz and the expander bound yield $∣ ⟨ 1_{X}, Δ_{A} 1_{X} ⟩ ∣ \leq ∥ Δ_{A} ∥ ∥ 1_{X} ∥_{2}^{2} \leq α d^{*} ∣ X ∣$ . The quantity in step 1.1 is real, so the absolute-value inequality is exactly the two claimed bounds.

Source notes

The statement and indicator-vector method are attributed to Expander graphs are globally synchronizing, Lemma 3.3. The proof above derives the bound from the stated mathematical suppliers.

Depends on

Used by · 3

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Expander graphs are globally synchronizing · PDF p. 19, Lemma 3.3 and proof