Multilinear Representation and Degree

Every Boolean function f : (Fin n → Bool) → Bool has a unique multilinear polynomial representation over ℤ. This file defines the Möbius coefficients of that representation and the multilinear degree of f.

Main definitions

• LeanPoolSensitivity.indicator — the indicator assignment of a finite set of coordinates.
• LeanPoolSensitivity.boolToInt — the integer encoding of a Boolean value.
• LeanPoolSensitivity.BoolFun.moebius — the Möbius coefficient c_S(f) = ∑_{T ⊆ S} (-1)^{|S|-|T|} f(1_T).
• LeanPoolSensitivity.BoolFun.degree — the multilinear degree of f.

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

The Boolean assignment that is true on coordinates in S and false elsewhere.

Equations

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

@[simp]

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

@[simp]

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

def LeanPoolSensitivity.boolToInt (b : Bool) : ℤ

Integer encoding of a Boolean value: true ↦ 1 and false ↦ 0.

Equations

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

@[simp]

theorem LeanPoolSensitivity.boolToInt_true : boolToInt true = 1

@[simp]

theorem LeanPoolSensitivity.boolToInt_false : boolToInt false = 0

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

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

Equations

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

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

The multilinear degree of f: the maximum cardinality of S for which the Möbius coefficient c_S(f) is nonzero.

Equations

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

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

The multilinear degree of f is at most n.

theorem LeanPoolSensitivity.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 multilinear degree is positive, there exists a "witness" set S of cardinality equal to the degree at which the Möbius coefficient is nonzero.