Subcube Restriction

We define "restriction" of a Boolean function by fixing some coordinates, and prove that this preserves relevant properties.

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

Embed an assignment into the "restricted" hypercube: keep values for coordinates in free, use base for the rest.

Equations

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

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

Restriction of f: fix coordinates outside free to base.

Equations

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

theorem Sensitivity.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

theorem Sensitivity.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

theorem Sensitivity.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 doesn't change the restriction.

theorem Sensitivity.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 not sensitive outside free.

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

Sensitivity of the restriction is at most the sensitivity of f.

theorem Sensitivity.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 gives back the indicator of T.

theorem Sensitivity.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

When we restrict with base = false, the Möbius coefficient at S ⊆ free is preserved.

theorem Sensitivity.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 exists S with |S| = d, f.moebius S ≠ 0, and the restriction preserves the coefficient.