The Spectral Lemma

Section 11.3 of bs_lambda.txt: lambda(f)^2 ≤ c + 2 √((c-1) A B) for a certificate family.

Write G = gram F.ind for the positive-side Gram matrix of a certificate family. Section 11.2 (in BSLambda/Spectral/GramClass.lean) shows that every off-diagonal entry of G is 0 or 1, and that a nonzero entry G x y is oriented: exactly one of x, y lies at distance one from the other's certificate.

Splitting G accordingly as G = D + R + Rᵀ, where D is the diagonal and R keeps only the oriented entries, we get

• ‖D‖ ≤ c because every diagonal entry is a sensitivity, bounded by the codimension;
• every row of R has at most A (c-1) nonzero entries — at most A certificates lie at distance one from x, and for each the partner y is a single flip of the projection π_{C_j}(x) at one of the c coordinates fixed by C_i, minus the flip that returns x itself;
• every column of R has at most B nonzero entries — at most B certificates lie at distance at most two from y, and each determines x = π_{C_i}(y).

The Schur test (BSLambda/Spectral/SchurTest.lean) then gives ‖R‖ ≤ √(A(c-1)·B), and lam f ^ 2 ≤ ‖G‖ ≤ ‖D‖ + 2‖R‖.

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

theorem Finset.sum_le_card_filter_ne_zero {α : Type u_1} (s : Finset α) {f : α → ℝ} (hf : ∀ a ∈ s, f a ≤ 1) : ∑ a ∈ s, f a ≤ ↑{a ∈ s | f a ≠ 0}.card

A finite sum of reals that are each at most one is at most the number of nonzero terms. This is a general Finset fact, stated here because Mathlib does not have it.

The splitting G = D + R + Rᵀ

noncomputable def BSLambda.CertFamily.diagMat {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : Matrix (Ones F.ind) (Ones F.ind) ℝ

The diagonal part D of the Gram matrix (Section 11.3).

Equations

• F.diagMat = Matrix.diagonal (BSLambda.gram F.ind).diag

noncomputable def BSLambda.CertFamily.offMat {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : Matrix (Ones F.ind) (Ones F.ind) ℝ

The oriented off-diagonal part R of the Gram matrix: the entry G x y is kept only when x lies at distance one from y's certificate (Section 11.3).

Equations

• F.offMat = Matrix.of fun (x y : BSLambda.Ones F.ind) => if F.owner x ≠ F.owner y ∧ (F.P (F.owner y)).dist ↑x = 1 then BSLambda.gram F.ind x y else 0

noncomputable def BSLambda.CertFamily.offBound {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : ℝ

The Schur-test bound √(A (c-1) B) on the oriented part (Section 11.3).

Equations

• F.offBound = √(↑(F.A * (F.c - 1)) * ↑F.B)

theorem BSLambda.CertFamily.diagMat_apply {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x y : Ones F.ind) : F.diagMat x y = if x = y then gram F.ind x x else 0

The defining formula for an entry of the diagonal part (Section 11.3).

theorem BSLambda.CertFamily.offMat_apply {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x y : Ones F.ind) : F.offMat x y = if F.owner x ≠ F.owner y ∧ (F.P (F.owner y)).dist ↑x = 1 then gram F.ind x y else 0

The defining formula for an entry of the oriented part (Section 11.3).

theorem BSLambda.CertFamily.offMat_nonneg {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x y : Ones F.ind) : 0 ≤ F.offMat x y

The entries of R are Gram entries or zero, hence nonnegative — one of the two hypotheses of the Schur test (Section 11.3).

theorem BSLambda.CertFamily.offMat_diag {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x : Ones F.ind) : F.offMat x x = 0

The diagonal of R vanishes, since a point owns itself: this is what makes D in the splitting G = D + R + Rᵀ carry the whole diagonal (Section 11.3).

theorem BSLambda.CertFamily.offMat_le_one {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x y : Ones F.ind) : F.offMat x y ≤ 1

The entries of R are at most one, by gram_le_one; this is what turns the row and column counts of Section 11.3 into bounds on the row and column sums.

theorem BSLambda.CertFamily.gram_eq_add {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : gram F.ind = F.diagMat + F.offMat + F.offMat.transpose

The splitting G = D + R + Rᵀ of the Gram matrix (Section 11.3).

Counting the nonzero entries of R

theorem BSLambda.CertFamily.offMat_ne_zero_iff {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} : F.offMat x y ≠ 0 ↔ F.owner x ≠ F.owner y ∧ (F.P (F.owner y)).dist ↑x = 1 ∧ gram F.ind x y ≠ 0

Reading off the three conditions hidden behind a nonzero entry of the oriented part (Section 11.3).

theorem BSLambda.CertFamily.card_offMat_row_slice_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x : Ones F.ind} {j : ι} (hj : j ≠ F.owner x) (hd : (F.P j).dist ↑x = 1) : {y : Ones F.ind | F.offMat x y ≠ 0 ∧ F.owner y = j}.card ≤ F.c - 1

For a fixed second owner j, at most c - 1 inputs y give a nonzero oriented entry in the row of x: each such y is a single flip of π_{C_j}(x) at a coordinate fixed by C_i, and the flip that returns x itself is excluded (Section 11.3, row bound).

theorem BSLambda.CertFamily.card_offMat_row_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x : Ones F.ind) : {y : Ones F.ind | F.offMat x y ≠ 0}.card ≤ F.A * (F.c - 1)

Every row of the oriented part has at most A (c - 1) nonzero entries: the row splits into at most A slices, one per certificate at distance one from x, and card_offMat_row_slice_le bounds each slice (Section 11.3, row bound).

theorem BSLambda.CertFamily.card_offMat_col_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (y : Ones F.ind) : {x : Ones F.ind | F.offMat x y ≠ 0}.card ≤ F.B

Every column of the oriented part has at most B nonzero entries: every row index x of the column of y has a distinct owner, at distance two from y, and listTwo bounds the number of those (Section 11.3, column bound).

The Schur test and the Spectral Lemma

theorem BSLambda.CertFamily.offMat_row_sum_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x : Ones F.ind) : ∑ y : Ones F.ind, F.offMat x y ≤ ↑(F.A * (F.c - 1))

Every row sum of the oriented part is at most A (c - 1): the entries are at most one, so the sum is at most the count of card_offMat_row_le (Section 11.3).

theorem BSLambda.CertFamily.offMat_col_sum_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (y : Ones F.ind) : ∑ x : Ones F.ind, F.offMat x y ≤ ↑F.B

Every column sum of the oriented part is at most B: the entries are at most one, so the sum is at most the count of card_offMat_col_le (Section 11.3).

theorem BSLambda.CertFamily.l2_opNorm_diagMat_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : ‖F.diagMat‖ ≤ ↑F.c

The diagonal part has operator norm at most the codimension c: the L2 operator norm of a diagonal matrix is the supremum norm of its diagonal, and gram_diag_le bounds every Gram diagonal entry by c (Section 11.3).

theorem BSLambda.CertFamily.l2_opNorm_offMat_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : ‖F.offMat‖ ≤ F.offBound

The Schur test applied to R, with the row bound A (c-1) and the column bound B (Section 11.3).

theorem BSLambda.CertFamily.l2_opNorm_offMat_transpose_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : ‖F.offMat.transpose‖ ≤ F.offBound

The transpose of R obeys the same bound, since transposition preserves the L2 operator norm (Section 11.3).

theorem BSLambda.CertFamily.l2_opNorm_gram_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : ‖gram F.ind‖ ≤ ↑F.c + 2 * F.offBound

The triangle inequality on the splitting G = D + R + Rᵀ (Section 11.3).

theorem BSLambda.CertFamily.lam_sq_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : lam F.ind ^ 2 ≤ ↑F.c + 2 * F.offBound

The Spectral Lemma (Section 11.3): lambda(f)^2 ≤ c + 2 √(A (c-1) B). Combining lam_sq_le_l2_opNorm_gram with the norm bound on G.

theorem BSLambda.CertFamily.lam_sq_le_sqrt {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (hc : 1 ≤ F.c) : lam F.ind ^ 2 ≤ ↑F.c + 2 * √((↑F.c - 1) * ↑F.A * ↑F.B)

The Spectral Lemma with offBound unfolded and the subtraction taken in ℝ rather than in ℕ, which is how Section 11.3 displays it. Nothing downstream needs this form — lam_sq_le is the one the development uses — but it is the statement free of a truncated subtraction.