The sensitivity graph and lambda(f)

adj f is the adjacency matrix (over ℝ) of the sensitivity graph G_f: vertices are all inputs, and x ~ y when x and y are Hamming neighbours with f x ≠ f y.

lam f is defined as the largest eigenvalue of adj f, matching the definition lambda(f) = largest eigenvalue of A_f of Section 1.2 of bs_lambda.txt.

The L2 operator norm on matrices is a scoped instance; we open scoped Matrix.Norms.L2Operator throughout the spectral development.

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

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

The adjacency matrix A_f of the sensitivity graph G_f.

Equations

• BSLambda.adj f = Matrix.of fun (x y : BSLambda.Input V) => if hammingDist x y = 1 ∧ f x ≠ f y then 1 else 0

theorem BSLambda.adj_apply {V : Type u_1} [Fintype V] (f : Input V → Bool) (x y : Input V) : adj f x y = if hammingDist x y = 1 ∧ f x ≠ f y then 1 else 0

theorem BSLambda.adj_nonneg {V : Type u_1} [Fintype V] (f : Input V → Bool) (x y : Input V) : 0 ≤ adj f x y

The sensitivity adjacency matrix has nonnegative entries.

theorem BSLambda.adj_apply_eq_one_iff {V : Type u_1} [Fintype V] {f : Input V → Bool} {x y : Input V} : adj f x y = 1 ↔ hammingDist x y = 1 ∧ f x ≠ f y

theorem BSLambda.adj_eq_zero_of_apply_eq {V : Type u_1} [Fintype V] (f : Input V → Bool) {x y : Input V} (h : f x = f y) : adj f x y = 0

Two inputs on the same side of f are never adjacent in the sensitivity graph.

theorem BSLambda.apply_ne_of_adj_ne_zero {V : Type u_1} [Fintype V] (f : Input V → Bool) {x y : Input V} (h : adj f x y ≠ 0) : f x ≠ f y

Adjacent inputs take different f-values.

theorem BSLambda.adj_comm {V : Type u_1} [Fintype V] (f : Input V → Bool) (x y : Input V) : adj f x y = adj f y x

The adjacency matrix of the sensitivity graph is symmetric.

theorem BSLambda.transpose_adj {V : Type u_1} [Fintype V] (f : Input V → Bool) : (adj f).transpose = adj f

theorem BSLambda.isHermitian_adj {V : Type u_1} [Fintype V] (f : Input V → Bool) : (adj f).IsHermitian

def BSLambda.nbrs {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x : Input V) : Finset (Input V)

The neighbours of x in the sensitivity graph.

Equations

• BSLambda.nbrs f x = {y : BSLambda.Input V | hammingDist x y = 1 ∧ f x ≠ f y}

theorem BSLambda.mem_nbrs {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} {x y : Input V} : y ∈ nbrs f x ↔ hammingDist x y = 1 ∧ f x ≠ f y

y is a neighbour of x exactly when they are Hamming neighbours separated by f.

theorem BSLambda.nbrs_eq_image {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x : Input V) : nbrs f x = Finset.image (fun (v : V) => flipSet x {v}) (sensCoords f x)

The neighbours of x are exactly the one-coordinate flips at sensitive coordinates.

@[simp]

theorem BSLambda.card_nbrs {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x : Input V) : (nbrs f x).card = sensAt f x

The degree of x in G_f is s(f,x).

theorem BSLambda.adj_apply_eq_ite_mem_nbrs {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x y : Input V) : adj f x y = if y ∈ nbrs f x then 1 else 0

adj f x y is the indicator of y being a neighbour of x in G_f.

@[simp]

theorem BSLambda.sum_adj_row {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x : Input V) : ∑ y : Input V, adj f x y = ↑(sensAt f x)

Every row of adj f sums to the sensitivity at that point.

theorem BSLambda.sum_adj_col {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (y : Input V) : ∑ x : Input V, adj f x y = ↑(sensAt f y)

Column sums of the sensitivity adjacency matrix: it is symmetric (adj_comm), so they agree with the row sums of sum_adj_row.

theorem BSLambda.trace_adj {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : (adj f).trace = 0

The trace of the sensitivity adjacency matrix vanishes: no input is its own neighbour.

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

lambda(f): the largest eigenvalue of the sensitivity-graph adjacency matrix.

Equations

• BSLambda.lam f = ⨆ (i : BSLambda.Input V), ⋯.eigenvalues i

theorem BSLambda.lam_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : 0 ≤ lam f

lambda(f) ≥ 0: the eigenvalues of adj f sum to trace (adj f) = 0, so at least one of them, hence their supremum, is nonnegative (Section 11.1 of bs_lambda.txt).

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

lambda(f) is at most the L2 operator norm of the adjacency matrix (Section 11.1).