Multilinear Representation and Degree

Every Boolean function has a unique multilinear polynomial representation over ℤ. We define the Möbius coefficients and the degree.

Main definitions

• BoolFun.moebius — the Möbius coefficient c_S of f
• BoolFun.degree — the multilinear degree

def Sensitivity.indicator {n : ℕ} (S : Finset (Fin n)) : Fin n → Bool

Indicator assignment: x_i = true iff i ∈ S.

Equations

• Sensitivity.indicator S i = decide (i ∈ S)

@[simp]

theorem Sensitivity.indicator_mem {n : ℕ} {S : Finset (Fin n)} {i : Fin n} : indicator S i = true ↔ i ∈ S

@[simp]

theorem Sensitivity.indicator_not_mem {n : ℕ} {S : Finset (Fin n)} {i : Fin n} : indicator S i = false ↔ i ∉ S

def Sensitivity.boolToInt (b : Bool) : ℤ

The integer encoding of a Bool: true ↦ 1, false ↦ 0.

Equations

• Sensitivity.boolToInt b = if b = true then 1 else 0

@[simp]

theorem Sensitivity.boolToInt_true : boolToInt true = 1

@[simp]

theorem Sensitivity.boolToInt_false : boolToInt false = 0

def Sensitivity.BoolFun.moebius {n : ℕ} (f : BoolFun n) (S : Finset (Fin n)) : ℤ

The Möbius coefficient of f at S: coefficient of ∏{i∈S} x_i in the unique multilinear polynomial representing f. Computed by inclusion-exclusion: c_S = ∑{T⊆S} (-1)^{|S|-|T|} f(1_T).

Equations

• f.moebius S = ∑ T ∈ S.powerset, (-1) ^ (S.card - T.card) * Sensitivity.boolToInt (f (Sensitivity.indicator T))

noncomputable def Sensitivity.BoolFun.degree {n : ℕ} (f : BoolFun n) : ℕ

The multilinear degree of f: maximum |S| over S with nonzero Möbius coefficient.

Equations

• f.degree = {S : Finset (Fin n) | f.moebius S ≠ 0}.sup Finset.card

theorem Sensitivity.BoolFun.degree_le {n : ℕ} (f : BoolFun n) : f.degree ≤ n

The degree is at most n.

theorem Sensitivity.BoolFun.exists_degree_witness {n : ℕ} (f : BoolFun n) (hd : 0 < f.degree) : ∃ (S : Finset (Fin n)), S.card = f.degree ∧ f.moebius S ≠ 0

If the degree is d > 0, there exists a set S of size d with nonzero coefficient.