Sensitivity and block sensitivity

The measures of Section 1.1 of bs_lambda.txt:

• sensCoords f x is the set of coordinates sensitive at x, and sensAt f x is s(f,x), its cardinality;
• sens f is s(f);
• bsAt f x is bs(f,x), the largest number of pairwise disjoint sensitive blocks at x;
• bs f is bs(f).

bsAt is defined as a supremum over ℕ of the set of cardinalities of admissible families; the set is bounded above, so le_bsAt_of_family gives the lower bounds we need. card_le_bs_of_blocks packages the usual way to apply it: from an indexed family of nonempty, pairwise disjoint sensitive blocks.

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

A missing Set lemma

Mathlib has the iSupIndep analogue (iSupIndep.injOn) but not the PairwiseDisjoint one; it belongs next to Set.injOn_iff_pairwise_ne in Mathlib/Data/Set/Pairwise/Basic.lean.

theorem Set.PairwiseDisjoint.injOn {ι : Type u_1} {α : Type u_2} [Lattice α] [OrderBot α] {f : ι → α} {s : Set ι} (h : s.PairwiseDisjoint f) (hne : ∀ i ∈ s, f i ≠ ⊥) : InjOn f s

A pairwise disjoint family of nonzero elements is injective on its index set.

def BSLambda.SensitiveCoord {V : Type u_1} [DecidableEq V] (f : Input V → Bool) (x : Input V) (v : V) : Prop

A coordinate v is sensitive for f at x when flipping it changes the value.

Equations

• BSLambda.SensitiveCoord f x v = (f (BSLambda.flipSet x {v}) ≠ f x)

@[instance_reducible]

instance BSLambda.instDecidableSensitiveCoord {V : Type u_1} [DecidableEq V] (f : Input V → Bool) (x : Input V) (v : V) : Decidable (SensitiveCoord f x v)

Equations

• BSLambda.instDecidableSensitiveCoord f x v = { decide := !decide (f (BSLambda.flipSet x {v}) = f x), reflects_decide := ⋯ }

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

The sensitive coordinates of f at x.

Equations

• BSLambda.sensCoords f x = {v : V | BSLambda.SensitiveCoord f x v}

theorem BSLambda.mem_sensCoords {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} {x : Input V} {v : V} : v ∈ sensCoords f x ↔ SensitiveCoord f x v

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

s(f,x): the number of sensitive coordinates at x.

Equations

• BSLambda.sensAt f x = (BSLambda.sensCoords f x).card

theorem BSLambda.sensAt_le_card {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} {x : Input V} {s : Finset V} (h : sensCoords f x ⊆ s) : sensAt f x ≤ s.card

Any Finset containing every sensitive coordinate at x bounds s(f,x).

theorem BSLambda.sensAt_eq_card_univ {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} {x : Input V} (h : ∀ (v : V), SensitiveCoord f x v) : sensAt f x = Fintype.card V

If every coordinate is sensitive at x then s(f,x) counts all coordinates.

def BSLambda.sens {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) : ℕ

s(f): the sensitivity of f.

Equations

• BSLambda.sens f = Finset.univ.sup (BSLambda.sensAt f)

theorem BSLambda.sensAt_le_sens {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x : Input V) : sensAt f x ≤ sens f

theorem BSLambda.sens_le {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) {n : ℕ} (h : ∀ (x : Input V), sensAt f x ≤ n) : sens f ≤ n

structure BSLambda.IsSensitiveBlock {V : Type u_1} [DecidableEq V] (f : Input V → Bool) (x : Input V) (A : Finset V) : Prop

A nonempty set A of coordinates is a sensitive block at x when f (x^A) ≠ f x.

• nonempty : A.Nonempty
• flips : f (flipSet x A) ≠ f x

theorem BSLambda.isSensitiveBlock_of_eq_true {V : Type u_1} [DecidableEq V] {f : Input V → Bool} {x : Input V} {A : Finset V} (hA : A.Nonempty) (hx : f x = false) (hflip : f (flipSet x A) = true) : IsSensitiveBlock f x A

The usual way to exhibit a sensitive block: a nonempty A that turns f from false to true.

structure BSLambda.IsBlockFamily {V : Type u_1} [DecidableEq V] (f : Input V → Bool) (x : Input V) (𝓑 : Finset (Finset V)) : Prop

A family of pairwise disjoint sensitive blocks at x.

• sensitive (A : Finset V) : A ∈ 𝓑 → IsSensitiveBlock f x A
• disjoint : (↑𝓑).PairwiseDisjoint id

def BSLambda.blockFamilyCards {V : Type u_1} [DecidableEq V] (f : Input V → Bool) (x : Input V) : Set ℕ

The set of cardinalities of admissible block families at x.

Equations

• BSLambda.blockFamilyCards f x = {n : ℕ | ∃ (𝓑 : Finset (Finset V)), BSLambda.IsBlockFamily f x 𝓑 ∧ 𝓑.card = n}

theorem BSLambda.blockFamilyCards_bddAbove {V : Type u_1} [DecidableEq V] [Finite V] (f : Input V → Bool) (x : Input V) : BddAbove (blockFamilyCards f x)

noncomputable def BSLambda.bsAt {V : Type u_1} [DecidableEq V] (f : Input V → Bool) (x : Input V) : ℕ

bs(f,x): the maximum number of pairwise disjoint sensitive blocks at x.

Equations

• BSLambda.bsAt f x = sSup (BSLambda.blockFamilyCards f x)

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

bs(f): the block sensitivity of f.

Equations

• BSLambda.bs f = Finset.univ.sup (BSLambda.bsAt f)

theorem BSLambda.le_bsAt_of_family {V : Type u_1} [DecidableEq V] [Finite V] {f : Input V → Bool} {x : Input V} {𝓑 : Finset (Finset V)} (h : IsBlockFamily f x 𝓑) : 𝓑.card ≤ bsAt f x

Exhibiting a family of pairwise disjoint sensitive blocks bounds bsAt from below.

theorem BSLambda.bsAt_le_bs {V : Type u_1} [Fintype V] [DecidableEq V] (f : Input V → Bool) (x : Input V) : bsAt f x ≤ bs f

theorem BSLambda.le_bs_of_family {V : Type u_1} [Fintype V] [DecidableEq V] {f : Input V → Bool} {x : Input V} {𝓑 : Finset (Finset V)} (h : IsBlockFamily f x 𝓑) : 𝓑.card ≤ bs f

The main lower-bound interface for block sensitivity.

theorem BSLambda.isBlockFamily_image {V : Type u_1} [DecidableEq V] {ι : Type u_2} {f : Input V → Bool} {x : Input V} {B : ι → Finset V} {s : Finset ι} (hsens : ∀ i ∈ s, IsSensitiveBlock f x (B i)) (hdisj : (↑s).PairwiseDisjoint B) : IsBlockFamily f x (Finset.image B s)

Sensitive blocks indexed by a Finset ι and pairwise disjoint on it form a block family.

theorem BSLambda.card_le_bs_of_blocks {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} {f : Input V → Bool} {x : Input V} {B : ι → Finset V} {s : Finset ι} (hsens : ∀ i ∈ s, IsSensitiveBlock f x (B i)) (hdisj : (↑s).PairwiseDisjoint B) : s.card ≤ bs f

An indexed family of pairwise disjoint sensitive blocks bounds bs from below. The blocks are automatically pairwise distinct, being nonempty and pairwise disjoint.