Subcube Restriction

We define the restriction of a Boolean function to a subcube by fixing some coordinates to a base assignment, and prove that this operation can only decrease sensitivity and preserves Möbius coefficients on subsets of the "free" coordinates.

Main definitions

• LeanPoolSensitivity.embed — embed a free-coordinate assignment into a full input by reading the remaining coordinates from a base assignment.
• LeanPoolSensitivity.BoolFun.restrictTo — restrict f by fixing the coordinates outside free to base.

Main results

• LeanPoolSensitivity.BoolFun.restrictTo_sensitivity_le — restriction cannot increase sensitivity.
• LeanPoolSensitivity.BoolFun.exists_fullDegree_restriction — if f has positive degree d, there is a subcube of dimension d on which the restriction has full degree d.

def LeanPoolSensitivity.embed {n : ℕ} (free : Finset (Fin n)) (base x : Fin n → Bool) : Fin n → Bool

Embed an assignment of the "free" coordinates into the full hypercube by copying values from base on the non-free coordinates.

Equations

• LeanPoolSensitivity.embed free base x j = if j ∈ free then x j else base j

theorem LeanPoolSensitivity.embed_flipBit_free {n : ℕ} (free : Finset (Fin n)) (base x : Fin n → Bool) (i : Fin n) (hi : i ∈ free) : embed free base (flipBit x i) = flipBit (embed free base x) i

For a free coordinate i, embedding commutes with flipping bit i.

theorem LeanPoolSensitivity.embed_flipBit_nonfree {n : ℕ} (free : Finset (Fin n)) (base x : Fin n → Bool) (i : Fin n) (hi : i ∉ free) : embed free base (flipBit x i) = embed free base x

For a non-free coordinate i, embedding ignores flips at i.

theorem LeanPoolSensitivity.embed_indicator_subset {n : ℕ} (free S T : Finset (Fin n)) (hS : S ⊆ free) (hT : T ⊆ S) : embed free (fun (x : Fin n) => false) (indicator T) = indicator T

Embedding the indicator of T ⊆ S ⊆ free with base = false recovers the original indicator of T.

def LeanPoolSensitivity.BoolFun.restrictTo {n : ℕ} (f : BoolFun n) (free : Finset (Fin n)) (base : Fin n → Bool) : BoolFun n

Restriction of f to the subcube parametrised by the free coordinates free and the fixed assignment base on the remaining coordinates.

Equations

• f.restrictTo free base x = f (LeanPoolSensitivity.embed free base x)

theorem LeanPoolSensitivity.BoolFun.restrictTo_flipBit_nonfree {n : ℕ} (f : BoolFun n) (free : Finset (Fin n)) (base x : Fin n → Bool) (i : Fin n) (hi : i ∉ free) : f.restrictTo free base (flipBit x i) = f.restrictTo free base x

Flipping a coordinate outside free does not change the restriction.

theorem LeanPoolSensitivity.BoolFun.restrictTo_not_sensitiveAt_nonfree {n : ℕ} (f : BoolFun n) (free : Finset (Fin n)) (base x : Fin n → Bool) (i : Fin n) (hi : i ∉ free) : ¬(f.restrictTo free base).sensitiveAt x i

The restriction is never sensitive in a coordinate outside free.

theorem LeanPoolSensitivity.BoolFun.restrictTo_sensitivity_le {n : ℕ} (f : BoolFun n) (free : Finset (Fin n)) (base : Fin n → Bool) : (f.restrictTo free base).sensitivity ≤ f.sensitivity

Restriction cannot increase sensitivity.

theorem LeanPoolSensitivity.BoolFun.restrictTo_moebius_subset {n : ℕ} (f : BoolFun n) (free S : Finset (Fin n)) (hS : S ⊆ free) : (f.restrictTo free fun (x : Fin n) => false).moebius S = f.moebius S

Restricting with base = false preserves Möbius coefficients on subsets of the free coordinates.

theorem LeanPoolSensitivity.BoolFun.exists_fullDegree_restriction {n : ℕ} (f : BoolFun n) (hd : 0 < f.degree) : ∃ (S : Finset (Fin n)), S.card = f.degree ∧ f.moebius S ≠ 0 ∧ (f.restrictTo S fun (x : Fin n) => false).moebius S ≠ 0

Key lemma: if f has degree d ≥ 1, there is a subcube of dimension d on which the restriction has full degree d (its top Möbius coefficient is nonzero).