Multilinear extensions of functions on the cube

Every function g : (ι → Bool) → R on a finite cube is the restriction of a multilinear polynomial: the sum over the points a of the cube of g a times the indicator polynomial of a, the product of X i over the coordinates where a i is true and of 1 - X i over the others. Its total degree is at most the dimension.

Main definitions

• Cslib.BitString.indicatorPoly: the multilinear polynomial that is 1 at a point of the cube and 0 at every other point.
• Cslib.BitString.multilinearExtension: the multilinear extension of a function on the cube.

Main results

• Cslib.BitString.eval_multilinearExtension: the extension agrees with the function on the cube.
• Cslib.BitString.totalDegree_multilinearExtension_le: its total degree is at most the dimension.
• Cslib.BitString.rename_multilinearExtension: renaming the coordinates along an equivalence gives the multilinear extension of the function read through the equivalence.

References

• R. O'Donnell, Analysis of Boolean Functions, Section 1.2 for the indicator polynomials.

noncomputable def Cslib.BitString.indicatorPoly {ι : Type u_1} {R : Type u_3} [CommRing R] [Fintype ι] (a : ι → Bool) : MvPolynomial ι R

The indicator polynomial of a point a of the cube: the product of X i where a i is true and of 1 - X i where it is false.

noncomputable def Cslib.BitString.multilinearExtension {ι : Type u_1} {R : Type u_3} [CommRing R] [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → R) : MvPolynomial ι R

The multilinear extension of a function on the cube.

theorem Cslib.BitString.eval_indicatorPoly_apply {ι : Type u_1} {R : Type u_3} [CommRing R] [Fintype ι] (a : ι → Bool) (z : ι → R) : (MvPolynomial.eval z) (indicatorPoly a) = ∏ i : ι, if a i = true then z i else 1 - z i

The value of an indicator polynomial at any point.

theorem Cslib.BitString.eval_indicatorPoly {ι : Type u_1} {R : Type u_3} [CommRing R] [Fintype ι] (a x : ι → Bool) : (MvPolynomial.eval fun (i : ι) => bitVal R (x i)) (indicatorPoly a) = if a = x then 1 else 0

On the cube, the indicator polynomial of a is 1 at a and 0 elsewhere.

theorem Cslib.BitString.eval_multilinearExtension {ι : Type u_1} {R : Type u_3} [CommRing R] [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → R) (x : ι → Bool) : (MvPolynomial.eval fun (i : ι) => bitVal R (x i)) (multilinearExtension g) = g x

The multilinear extension agrees with the function on the cube.

theorem Cslib.BitString.totalDegree_indicatorPoly_le {ι : Type u_1} {R : Type u_3} [CommRing R] [Fintype ι] (a : ι → Bool) : (indicatorPoly a).totalDegree ≤ Fintype.card ι

An indicator polynomial has total degree at most the dimension.

theorem Cslib.BitString.totalDegree_multilinearExtension_le {ι : Type u_1} {R : Type u_3} [CommRing R] [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → R) : (multilinearExtension g).totalDegree ≤ Fintype.card ι

The multilinear extension has total degree at most the dimension.

theorem Cslib.BitString.rename_multilinearExtension {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [CommRing R] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (g : (ι → Bool) → R) : (MvPolynomial.rename ⇑e) (multilinearExtension g) = multilinearExtension fun (z : κ → Bool) => g (z ∘ ⇑e)

Renaming the coordinates along an equivalence e turns the multilinear extension of g into the multilinear extension of g read through e.