lambda (f ∘ g) = lambda f * lambda g

Write an input of comp f g as a W-indexed family of blocks, blk x w : Input V, and let topBits g x : Input W be the string of block values w ↦ g (blk x w), so that comp f g x = f (topBits g x).

Two inputs of comp f g are adjacent in the sensitivity graph exactly when they differ in one coordinate (w, v), that flip is sensitive for g inside the block w, and the resulting flip of the w-th top bit is sensitive for f; this is BSLambda.adj_comp_flip, and summing it over the coordinates gives the master identity BSLambda.adj_comp_mulVec_apply

(A_{f∘g} *ᵥ ψ) x = ∑ w, A_f (topBits g x) ((topBits g x)^w) * (A_g *ᵥ ψ^{x,w}) (blk x w)

where ψ^{x,w} z = ψ (setBlk x w z) is the restriction of ψ to the w-th block through x.

Upper bound. Group the inputs into the fibres of topBits g (BSLambda.sum_sq_fibres). On the fibre over b the identity above expresses A_{f∘g} ψ as a sum of at most deg_f(b) terms, each of which is a copy of A_g acting inside one block and the identity elsewhere, so each has norm at most lambda(g) times the norm of ψ on the fibre over b^w (BSLambda.sum_sq_block_le). Minkowski's inequality bounds the fibre (BSLambda.sum_sq_fibre_adj_comp_mulVec_le), and the operator bound for A_f applied to the vector of fibre norms BSLambda.fibreNorm then gives ‖A_{f∘g}‖ ≤ lambda(f) * lambda(g).

Lower bound. If A_g u = lambda(g) u and A_f v = lambda(f) v, then φ x = v (topBits g x) * ∏ w, u (blk x w) satisfies A_{f∘g} φ = lambda(f) lambda(g) φ exactly. It is nonzero because the support of an eigenvector for a nonzero eigenvalue of a bipartite graph meets both sides.

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

Minkowski's inequality

The lemma below mentions nothing from this development. Mathlib has the two-summand Minkowski inequality Real.Lp_add_le and the abstract triangle inequality norm_sum_le, but not the coordinate form for a finite family of vectors at p = 2; the proof is the standard reduction to norm_sum_le in EuclideanSpace ℝ X. It is stated in the root namespace because it is Mathlib-shaped, not BSLambda-shaped.

theorem sum_sq_sum_le_sq_sum {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (F : Y → X → ℝ) (t : Y → ℝ) (ht0 : ∀ (y : Y), 0 ≤ t y) (ht : ∀ (y : Y), ∑ x : X, F y x ^ 2 ≤ t y ^ 2) : ∑ x : X, (∑ y : Y, F y x) ^ 2 ≤ (∑ y : Y, t y) ^ 2

Minkowski's inequality for a finite family of vectors, in sum-of-squares form: if the ℓ²-norm of each F y is at most t y, then the ℓ²-norm of ∑ y, F y is at most ∑ y, t y.

Blocks of a composed input

An input of comp f g is a W-indexed family of V-blocks. Passing to that view is Function.curry, and overwriting one block is Function.update read through it, so the rewriting API below is Mathlib's Function.update API transported along blk_setBlk.

def BSLambda.blk {W : Type u_1} {V : Type u_2} (x : Input (W × V)) : W → Input V

The w-th block of an input of comp f g, i.e. x viewed as a W-indexed family.

Equations

• BSLambda.blk x = Function.curry x

def BSLambda.topBits {W : Type u_1} {V : Type u_2} (g : Input V → Bool) (x : Input (W × V)) : Input W

The string of block values w ↦ g (blk x w), which comp f g feeds into f.

Equations

• BSLambda.topBits g x w = g (BSLambda.blk x w)

theorem BSLambda.comp_apply_topBits {W : Type u_1} {V : Type u_2} (f : Input W → Bool) (g : Input V → Bool) (x : Input (W × V)) : comp f g x = f (topBits g x)

comp f g is f applied to the top bits.

theorem BSLambda.blk_injective {W : Type u_1} {V : Type u_2} : Function.Injective blk

An input is determined by its blocks.

def BSLambda.setBlk {W : Type u_1} {V : Type u_2} [DecidableEq W] (x : Input (W × V)) (w : W) (z : Input V) : Input (W × V)

setBlk x w z replaces the w-th block of x by z.

Equations

• BSLambda.setBlk x w z = Function.uncurry (Function.update (BSLambda.blk x) w z)

@[simp]

theorem BSLambda.blk_setBlk {W : Type u_1} {V : Type u_2} [DecidableEq W] (x : Input (W × V)) (w : W) (z : Input V) : blk (setBlk x w z) = Function.update (blk x) w z

The blocks of setBlk x w z are the blocks of x with the w-th one updated. Every other setBlk lemma below is this together with Mathlib's Function.update API.

@[simp]

theorem BSLambda.setBlk_blk_self {W : Type u_1} {V : Type u_2} [DecidableEq W] (x : Input (W × V)) (w : W) : setBlk x w (blk x w) = x

Writing back the block that is already there does nothing.

@[simp]

theorem BSLambda.setBlk_setBlk {W : Type u_1} {V : Type u_2} [DecidableEq W] (x : Input (W × V)) (w : W) (z z' : Input V) : setBlk (setBlk x w z) w z' = setBlk x w z'

Only the last value written to the w-th block survives.

theorem BSLambda.prod_blk_setBlk {W : Type u_1} {V : Type u_2} [DecidableEq W] {M : Type u_3} [Fintype W] [CommMonoid M] (u : Input V → M) (x : Input (W × V)) (w : W) (z : Input V) : ∏ w' : W, u (blk (setBlk x w z) w') = u z * ∏ w' ∈ Finset.univ.erase w, u (blk x w')

Overwriting the w-th block changes exactly one factor of a product over the blocks.

theorem BSLambda.flipSet_prod_singleton {W : Type u_1} {V : Type u_2} [DecidableEq W] [DecidableEq V] (x : Input (W × V)) (w : W) (v : V) : flipSet x {(w, v)} = setBlk x w (flipSet (blk x w) {v})

Flipping the coordinate (w, v) flips the coordinate v inside the w-th block.

theorem BSLambda.topBits_setBlk_apply_self {W : Type u_1} {V : Type u_2} [DecidableEq W] (g : Input V → Bool) (x : Input (W × V)) (w : W) (z : Input V) : topBits g (setBlk x w z) w = g z

The w-th top bit of setBlk x w z is the value of g on the new block.

theorem BSLambda.topBits_setBlk_apply_of_ne {W : Type u_1} {V : Type u_2} [DecidableEq W] (g : Input V → Bool) (x : Input (W × V)) (w : W) (z : Input V) {w' : W} (h : w' ≠ w) : topBits g (setBlk x w z) w' = topBits g x w'

Away from w, the top bits of setBlk x w z are those of x.

theorem BSLambda.topBits_setBlk_of_eq {W : Type u_1} {V : Type u_2} [DecidableEq W] (g : Input V → Bool) (x : Input (W × V)) (w : W) (z : Input V) (h : g z = g (blk x w)) : topBits g (setBlk x w z) = topBits g x

Rewriting the w-th block without changing its g-value leaves the top bits alone.

theorem BSLambda.topBits_setBlk_of_ne {W : Type u_1} {V : Type u_2} [DecidableEq W] (g : Input V → Bool) (x : Input (W × V)) (w : W) (z : Input V) (h : g z ≠ g (blk x w)) : topBits g (setBlk x w z) = flipSet (topBits g x) {w}

Rewriting the w-th block so as to change its g-value flips the w-th top bit.

theorem BSLambda.topBits_setBlk_ne {W : Type u_1} {V : Type u_2} [DecidableEq W] (g : Input V → Bool) (x : Input (W × V)) (w : W) {c : Input W} {w' : W} (hw' : w' ≠ w) (h : topBits g x w' ≠ c w') (z : Input V) : topBits g (setBlk x w z) ≠ c

If the top bits of x disagree with c at some coordinate other than w, then no rewriting of the w-th block lands in the fibre of topBits g over c.

theorem BSLambda.topBits_setBlk_eq_iff {W : Type u_1} {V : Type u_2} [DecidableEq W] (g : Input V → Bool) (x : Input (W × V)) (w : W) {c : Input W} (hc : ∀ (w' : W), w' ≠ w → topBits g x w' = c w') (z : Input V) : topBits g (setBlk x w z) = c ↔ g z = c w

If the top bits of x already agree with c away from w, then setBlk x w z lies in the fibre of topBits g over c exactly when g z is the w-th bit of c.

The adjacency matrix of a composition

theorem BSLambda.adj_comp_flip {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) (x : Input (W × V)) (w : W) (v : V) : adj (comp f g) x (flipSet x {(w, v)}) = adj f (topBits g x) (flipSet (topBits g x) {w}) * adj g (blk x w) (flipSet (blk x w) {v})

An edge of the sensitivity graph of comp f g is a g-sensitive flip inside one block whose effect on the top bits is an f-sensitive flip.

theorem BSLambda.adj_comp_mulVec_apply {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) (ψ : Input (W × V) → ℝ) (x : Input (W × V)) : (adj (comp f g)).mulVec ψ x = ∑ w : W, adj f (topBits g x) (flipSet (topBits g x) {w}) * (adj g).mulVec (fun (z : Input V) => ψ (setBlk x w z)) (blk x w)

Master identity. A_{f∘g} acts on a vector by applying A_g inside each block and weighting the blocks by the entries of A_f at the top bits.

The upper bound

theorem BSLambda.sum_sq_fibres {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (g : Input V → Bool) (F : Input (W × V) → ℝ) : ∑ b : Input W, ∑ x : Input (W × V), (if topBits g x = b then F x else 0) ^ 2 = ∑ x : Input (W × V), F x ^ 2

The fibres of topBits g partition the inputs, so the squares of the fibrewise truncations of F sum to ∑ x, F x ^ 2.

noncomputable def BSLambda.fibreNorm {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (g : Input V → Bool) (ψ : Input (W × V) → ℝ) (b : Input W) : ℝ

The ℓ²-norm of ψ on the fibre of topBits g over b.

Equations

• BSLambda.fibreNorm g ψ b = √(∑ x : BSLambda.Input (W × V), (if BSLambda.topBits g x = b then ψ x else 0) ^ 2)

theorem BSLambda.fibreNorm_nonneg {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (g : Input V → Bool) (ψ : Input (W × V) → ℝ) (b : Input W) : 0 ≤ fibreNorm g ψ b

Fibre norms are nonnegative.

theorem BSLambda.sq_fibreNorm {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (g : Input V → Bool) (ψ : Input (W × V) → ℝ) (b : Input W) : fibreNorm g ψ b ^ 2 = ∑ x : Input (W × V), (if topBits g x = b then ψ x else 0) ^ 2

The defining property of the fibre norm, with the square root cleared.

theorem BSLambda.sum_sq_fibreNorm {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (g : Input V → Bool) (ψ : Input (W × V) → ℝ) : ∑ b : Input W, fibreNorm g ψ b ^ 2 = ∑ x : Input (W × V), ψ x ^ 2

The fibre norms of ψ recombine into its ℓ²-norm.

def BSLambda.blockEquiv {W : Type u_1} {V : Type u_2} [DecidableEq W] (w : W) : Input V × { x : Input (W × V) // blk x w = zeroInput V } ≃ Input (W × V)

Splitting an input of comp f g into its w-th block and everything else.

Equations

• One or more equations did not get rendered due to their size.

theorem BSLambda.sum_setBlk {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (w : W) (F : Input (W × V) → ℝ) : ∑ y : { x : Input (W × V) // blk x w = zeroInput V }, ∑ a : Input V, F (setBlk (↑y) w a) = ∑ x : Input (W × V), F x

Every input decomposes as a value for the w-th block together with an input whose w-th block is zero, so a sum over all inputs splits accordingly.

theorem BSLambda.sum_sq_block_le {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (g : Input V → Bool) (ψ : Input (W × V) → ℝ) (b : Input W) (w : W) : ∑ x : Input (W × V), (if topBits g x = b then (adj g).mulVec (fun (z : Input V) => ψ (setBlk x w z)) (blk x w) else 0) ^ 2 ≤ lam g ^ 2 * fibreNorm g ψ (flipSet b {w}) ^ 2

Applying A_g inside the block w and the identity elsewhere is an operator of norm at most lambda(g) from the fibre of topBits g over b^w to the fibre over b.

theorem BSLambda.sum_sq_fibre_summand_le {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) (ψ : Input (W × V) → ℝ) (b : Input W) (w : W) : ∑ x : Input (W × V), (if topBits g x = b then adj f b (flipSet b {w}) * (adj g).mulVec (fun (z : Input V) => ψ (setBlk x w z)) (blk x w) else 0) ^ 2 ≤ (adj f b (flipSet b {w}) * (lam g * fibreNorm g ψ (flipSet b {w}))) ^ 2

The w-th summand of the master identity, restricted to the fibre of topBits g over b. This is sum_sq_block_le with the constant A_f b b^w pulled out of the sum.

theorem BSLambda.sum_sq_fibre_adj_comp_mulVec_le {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) (ψ : Input (W × V) → ℝ) (b : Input W) : ∑ x : Input (W × V), (if topBits g x = b then (adj (comp f g)).mulVec ψ x else 0) ^ 2 ≤ lam g ^ 2 * (adj f).mulVec (fibreNorm g ψ) b ^ 2

The fibrewise bound. On the fibre of topBits g over b, the master identity writes A_{f∘g} ψ as a sum of #W vectors whose norms sum_sq_fibre_summand_le controls; Minkowski's inequality then bounds the fibre by lambda(g) times the value at b of A_f applied to the vector of fibre norms of ψ.

theorem BSLambda.sum_sq_adj_comp_mulVec_le {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) (ψ : Input (W × V) → ℝ) : ∑ x : Input (W × V), (adj (comp f g)).mulVec ψ x ^ 2 ≤ (lam f * lam g) ^ 2 * ∑ x : Input (W × V), ψ x ^ 2

The operator bound for A_{f∘g}, in sum-of-squares form.

theorem BSLambda.lam_comp_le {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) : lam (comp f g) ≤ lam f * lam g

Submultiplicativity of lambda.

The lower bound

theorem BSLambda.exists_apply_eq_and_ne_zero {V : Type u_2} [Fintype V] [DecidableEq V] (g : Input V → Bool) {μ : ℝ} (hμ : μ ≠ 0) {u : Input V → ℝ} (hu : u ≠ 0) (hev : (adj g).mulVec u = μ • u) (β : Bool) : ∃ (a : Input V), g a = β ∧ u a ≠ 0

The support of an eigenvector for a nonzero eigenvalue meets both sides of the bipartition.

theorem BSLambda.adj_mulVec_block_prod {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (g : Input V → Bool) {u : Input V → ℝ} (v : Input W → ℝ) (hu : (adj g).mulVec u = lam g • u) (x : Input (W × V)) (w : W) : (adj g).mulVec (fun (z : Input V) => v (topBits g (setBlk x w z)) * ∏ w' : W, u (blk (setBlk x w z) w')) (blk x w) = lam g * v (flipSet (topBits g x) {w}) * ∏ w' : W, u (blk x w')

The block step of the product eigenvector computation. Applying A_g inside the w-th block to x ↦ v (topBits g x) * ∏ w, u (blk x w) multiplies it by lambda(g) and flips the w-th top bit: only blocks z adjacent to blk x w contribute, and for those the top bits change exactly at w.

theorem BSLambda.adj_comp_mulVec_prod {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) {u : Input V → ℝ} {v : Input W → ℝ} (hu : (adj g).mulVec u = lam g • u) (hv : (adj f).mulVec v = lam f • v) : ((adj (comp f g)).mulVec fun (x : Input (W × V)) => v (topBits g x) * ∏ w : W, u (blk x w)) = (lam f * lam g) • fun (x : Input (W × V)) => v (topBits g x) * ∏ w : W, u (blk x w)

The product eigenvector: if u and v are eigenvectors of A_g and A_f then x ↦ v (topBits g x) * ∏ w, u (blk x w) is an eigenvector of A_{f∘g}.

theorem BSLambda.prod_eigenvector_ne_zero {W : Type u_1} {V : Type u_2} [Fintype W] (g : Input V → Bool) {u : Input V → ℝ} {v : Input W → ℝ} (hboth : ∀ (β : Bool), ∃ (a : Input V), g a = β ∧ u a ≠ 0) (hv : v ≠ 0) : (fun (x : Input (W × V)) => v (topBits g x) * ∏ w : W, u (blk x w)) ≠ 0

The product eigenvector is nonzero.

theorem BSLambda.le_lam_comp {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) : lam f * lam g ≤ lam (comp f g)

Supermultiplicativity of lambda.

theorem BSLambda.lam_comp {W : Type u_1} {V : Type u_2} [Fintype W] [DecidableEq W] [Fintype V] [DecidableEq V] (f : Input W → Bool) (g : Input V → Bool) : lam (comp f g) = lam f * lam g

The composition theorem (Section 14 of bs_lambda.txt, imported there from ABKRT): lambda is multiplicative under block composition.

Self-composition

theorem BSLambda.lam_iterFun_zero {V : Type u_2} [Fintype V] [DecidableEq V] (f : Input V → Bool) : lam (iterFun f 0) = 1

The one-bit identity function has lambda = 1.

theorem BSLambda.lam_iterFun_eq {V : Type u_2} [Fintype V] [DecidableEq V] (f : Input V → Bool) (m : ℕ) : lam (iterFun f m) = lam f ^ m

lambda(F_m) = lambda(f)^m for the m-fold self-composition (Section 14).