‖A_f‖ = lambda(f)

Conjugating an eigenvector by the sign pattern x ↦ (-1)^{f x} turns an eigenvector for μ into an eigenvector for -μ (BSLambda.exists_neg_eigenvector), because every edge of the sensitivity graph flips the sign. Hence |μ| ≤ lambda(f) for every eigenvalue μ (BSLambda.abs_eigenvalues_adj_le_lam) and therefore ‖A_f‖ = lambda(f) (BSLambda.l2_opNorm_adj_eq_lam). This upgrades the inequality BSLambda.lam_le_l2_opNorm_adj of Section 11.1 of bs_lambda.txt to an equality, which is what the composition theorem of Section 14 needs.

The consequences used later are the operator bound BSLambda.sum_sq_adj_mulVec_le : ∑ x, (A_f *ᵥ v) x ^ 2 ≤ lambda(f)^2 * ∑ x, v x ^ 2 and the existence of a top eigenvector BSLambda.exists_top_eigenvector.

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

theorem BSLambda.le_lam_of_eigenvector {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) {μ : ℝ} {v : Input V → ℝ} (hv : v ≠ 0) (hev : (adj f).mulVec v = μ • v) : μ ≤ lam f

An eigenvalue of A_f is at most lambda(f).

def BSLambda.signPattern {V : Type u_1} (f : Input V → Bool) (x : Input V) : ℝ

The sign pattern (-1)^{f x}: it is 1 on f⁻¹(true) and -1 on f⁻¹(false).

Equations

• BSLambda.signPattern f x = if f x = true then 1 else -1

theorem BSLambda.exists_neg_eigenvector {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) {μ : ℝ} {v : Input V → ℝ} (hv : v ≠ 0) (hev : (adj f).mulVec v = μ • v) : ∃ (w : Input V → ℝ), w ≠ 0 ∧ (adj f).mulVec w = -μ • w

The sign flip x ↦ (-1)^{f x} conjugates an eigenvector for μ into one for -μ: every edge of the sensitivity graph joins inputs with different f-values.

theorem BSLambda.abs_eigenvalues_adj_le_lam {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (i : Input V) : |⋯.eigenvalues i| ≤ lam f

Every eigenvalue of A_f is at most lambda(f) in absolute value.

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

The L2 operator norm of the sensitivity adjacency matrix is at most lambda(f).

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

lambda(f) is the L2 operator norm of A_f. The sensitivity graph is bipartite, so its spectrum is symmetric about 0 and the largest eigenvalue is the spectral radius.

theorem BSLambda.sum_sq_adj_mulVec_le {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (v : Input V → ℝ) : ∑ x : Input V, (adj f).mulVec v x ^ 2 ≤ lam f ^ 2 * ∑ x : Input V, v x ^ 2

The operator bound defining lambda(f), in sum-of-squares form.

theorem BSLambda.sum_sq_adj_mulVec_side_le {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (v : Input V → ℝ) (β : Bool) : ∑ x : Input V, (if f x = β then (adj f).mulVec v x else 0) ^ 2 ≤ lam f ^ 2 * ∑ x : Input V, (if f x = β then 0 else v x) ^ 2

The operator bound restricted to one side of the bipartition: A_f *ᵥ v reads v only on the other side, so only the other side's coordinates appear on the right.

theorem BSLambda.exists_top_eigenvector {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : ∃ (u : Input V → ℝ), u ≠ 0 ∧ (adj f).mulVec u = lam f • u

The largest eigenvalue of A_f is attained by an eigenvector.

theorem BSLambda.adj_mulVec_apply {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (ν : Input V → ℝ) (x : Input V) : (adj f).mulVec ν x = ∑ i : V, adj f x (flipSet x {i}) * ν (flipSet x {i})

A_f *ᵥ v written as a sum over coordinate flips.

theorem BSLambda.lam_le_of_sensAt_le {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} {k : ℝ} (hk : 0 ≤ k) (hs : ∀ (x : Input V), ↑(sensAt f x) ≤ k) : lam f ≤ k

A bound on the sensitivity of f bounds lambda(f): the adjacency matrix has nonnegative entries and all its row sums are at most k.

theorem BSLambda.lam_eq_of_sensAt_eq {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} {k : ℝ} (hk : 0 ≤ k) (hs : ∀ (x : Input V), ↑(sensAt f x) = k) : lam f = k

A sensitivity graph all of whose vertices have degree k has lambda = k: the row sums give lam f ≤ k, and the all-ones vector is an eigenvector for k.