Boundary incidence and the positive-side Gram matrix

Section 11.1 of bs_lambda.txt splits the vertex set of the sensitivity graph G_f into the positive inputs S = f⁻¹(1) and the negative inputs T = f⁻¹(0). The graph is bipartite between S and T, with biadjacency matrix M (BSLambda.biadj), so that in the vertex order S, T

A_f = [ 0    M   ]
      [ Mᵀ   0   ]

and lambda(f)^2 = rho(K) for the positive-side Gram matrix K = M Mᵀ (BSLambda.gram).

We prove the inequality half of that identity, which is all the later sections need:

BSLambda.lam_sq_le_l2_opNorm_gram : lam f ^ 2 ≤ ‖gram f‖.

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

The two sides and the biadjacency matrix

@[reducible, inline]

abbrev BSLambda.Ones {V : Type u_1} (f : Input V → Bool) : Type u_1

The inputs on which f is 1: the positive side S = f⁻¹(1) (Section 11.1 of bs_lambda.txt).

Equations

• BSLambda.Ones f = { x : BSLambda.Input V // f x = true }

@[reducible, inline]

abbrev BSLambda.Zeros {V : Type u_1} (f : Input V → Bool) : Type u_1

The inputs on which f is 0: the negative side T = f⁻¹(0) (Section 11.1 of bs_lambda.txt).

Equations

• BSLambda.Zeros f = { x : BSLambda.Input V // f x = false }

noncomputable def BSLambda.biadj {V : Type u_1} [Fintype V] (f : Input V → Bool) : Matrix (Ones f) (Zeros f) ℝ

The biadjacency matrix M of the sensitivity graph, rows indexed by S, columns by T (Section 11.1).

Equations

• BSLambda.biadj f = Matrix.of fun (x : BSLambda.Ones f) (z : BSLambda.Zeros f) => if hammingDist ↑x ↑z = 1 then 1 else 0

noncomputable def BSLambda.gram {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : Matrix (Ones f) (Ones f) ℝ

The positive-side Gram matrix K = M Mᵀ (Section 11.1).

Equations

• BSLambda.gram f = BSLambda.biadj f * (BSLambda.biadj f).transpose

theorem BSLambda.biadj_apply {V : Type u_1} [Fintype V] (f : Input V → Bool) (x : Ones f) (z : Zeros f) : biadj f x z = if hammingDist ↑x ↑z = 1 then 1 else 0

Entries of the biadjacency matrix of Section 11.1.

theorem BSLambda.biadj_nonneg {V : Type u_1} [Fintype V] (f : Input V → Bool) (x : Ones f) (z : Zeros f) : 0 ≤ biadj f x z

The biadjacency matrix of Section 11.1 has nonnegative entries.

theorem BSLambda.biadj_eq_adj {V : Type u_1} [Fintype V] (f : Input V → Bool) (x : Ones f) (z : Zeros f) : biadj f x z = adj f ↑x ↑z

The biadjacency matrix is the restriction of the adjacency matrix to S × T: the condition f x ≠ f z of BSLambda.adj is automatic there (Section 11.1).

theorem BSLambda.sum_ones_add_sum_zeros {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (g : Input V → ℝ) : ∑ x : Ones f, g ↑x + ∑ z : Zeros f, g ↑z = ∑ y : Input V, g y

Splitting a sum over all inputs into its positive and its negative part (Section 11.1).

The positive-side Gram matrix

theorem BSLambda.gram_apply {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x y : Ones f) : gram f x y = ↑{z : Zeros f | hammingDist ↑x ↑z = 1 ∧ hammingDist ↑y ↑z = 1}.card

Counting form of the Gram entries. For x, y ∈ S, the entry K_{x,y} counts the negative inputs adjacent to both x and y (Section 11.1 of bs_lambda.txt).

theorem BSLambda.gram_ne_zero_iff {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} {x y : Ones f} : gram f x y ≠ 0 ↔ ∃ (z : Zeros f), hammingDist ↑x ↑z = 1 ∧ hammingDist ↑y ↑z = 1

A Gram entry is nonzero exactly when the two positive inputs have a common negative Hamming neighbour: gram_apply with the cardinality turned into an existential (Section 11.1).

theorem BSLambda.gram_comm {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} (x y : Ones f) : gram f x y = gram f y x

The Gram matrix of Section 11.1 is symmetric, entrywise.

theorem BSLambda.gram_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x y : Ones f) : 0 ≤ gram f x y

The Gram matrix of Section 11.1 has nonnegative entries.

theorem BSLambda.gram_diag {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x : Ones f) : gram f x x = ↑(sensAt f ↑x)

On the diagonal, K_{x,x} = s(f,x) (Section 11.1 of bs_lambda.txt).

theorem BSLambda.gram_isHermitian {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : (gram f).IsHermitian

The Gram matrix K = M Mᵀ of Section 11.1 is symmetric.

The block decomposition of the adjacency matrix

theorem BSLambda.mulVec_adj_ones {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (v : Input V → ℝ) (x : Ones f) : (adj f).mulVec v ↑x = (biadj f).mulVec (fun (z : Zeros f) => v ↑z) x

The Ones f rows of the block decomposition of A_f: at a positive input, A_f *ᵥ v sees only the negative coordinates of v, and there it is governed by M (Section 11.1).

theorem BSLambda.mulVec_adj_zeros {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (v : Input V → ℝ) (z : Zeros f) : (adj f).mulVec v ↑z = (biadj f).transpose.mulVec (fun (x : Ones f) => v ↑x) z

The Zeros f rows of the block decomposition of A_f: at a negative input, A_f *ᵥ v sees only the positive coordinates of v, and there it is governed by Mᵀ (Section 11.1).

theorem BSLambda.l2_opNorm_adj_le {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : ‖adj f‖ ≤ ‖biadj f‖

The L2 operator norm of A_f is bounded by that of its off-diagonal block M (Section 11.1 of bs_lambda.txt).

theorem BSLambda.l2_opNorm_gram {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : ‖gram f‖ = ‖biadj f‖ * ‖biadj f‖

The norm of the Gram matrix K = M Mᵀ is the square of the norm of M (Section 11.1).

theorem BSLambda.lam_sq_le_l2_opNorm_gram {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : lam f ^ 2 ≤ ‖gram f‖

lambda(f)^2 <= ‖K‖, where K = M Mᵀ is the positive-side Gram matrix (Section 11.1 of bs_lambda.txt).