Multilinear Polynomials

This file defines computable representations of multilinear polynomials.

The first representation is by their coefficients, and the second representation is by their evaluations over the Boolean hypercube {0,1}^n. Both representations are defined as Vectors of length 2^n, where n is the number of variables. We will define operations on these representations, and prove equivalence between them, and with the standard Mathlib definition of multilinear polynomials, which is the type R⦃≤ 1⦄[X Fin n] (notation for MvPolynomial.restrictDegree (Fin n) R 1).

TODOs

• The abstract zeta formula for monoToLagrange
• A naive O(4^n) zeta spec monoToLagrangeSpec mirroring lagrangeToMonoSpec, plus equivalence monoToLagrange = monoToLagrangeSpec

@[reducible]

def CompPoly.CMlPolynomial (R : Type u_1) (n : ℕ) : Type u_1

CMlPolynomial n R is the type of multilinear polynomials in n variables over a ring R. It is represented by its monomial coefficients as a Vector of length 2^n. The indexing is little-endian (i.e. the least significant bit is the first bit).

def CompPoly.CMlPolynomial.mk {R : Type u_1} (n : ℕ) (v : Vector R (2 ^ n)) : CMlPolynomial R n

@[reducible]

def CompPoly.CMlPolynomialEval (R : Type u_1) (n : ℕ) : Type u_1

CMlPolynomialEval n R is the type of multilinear polynomials in n variables over a ring R. It is represented by its evaluations over the Boolean hypercube {0,1}^n, i.e. Lagrange basis coefficients. The indexing is little-endian (i.e. the least significant bit is the first bit).

def CompPoly.CMlPolynomialEval.mk {R : Type u_1} (n : ℕ) (v : Vector R (2 ^ n)) : CMlPolynomialEval R n

@[implicit_reducible]

instance CompPoly.CMlPolynomial.inhabited {R : Type u_1} {n : ℕ} [Inhabited R] : Inhabited (CMlPolynomial R n)

@[inline]

def CompPoly.CMlPolynomial.ofArray {R : Type u_1} [Zero R] (coeffs : Array R) (n : ℕ) : CMlPolynomial R n

Conform a list of coefficients to a CMlPolynomial with a given number of variables. May either pad with zeros or truncate.

@[inline]

def CompPoly.CMlPolynomial.zero {R : Type u_1} {n : ℕ} [Zero R] : CMlPolynomial R n

theorem CompPoly.CMlPolynomial.zero_def {R : Type u_1} {n : ℕ} [Zero R] : zero = Vector.replicate (2 ^ n) 0

@[inline]

def CompPoly.CMlPolynomial.add {R : Type u_1} {n : ℕ} [Add R] (p q : CMlPolynomial R n) : CMlPolynomial R n

Add two CMlPolynomials

@[inline]

def CompPoly.CMlPolynomial.neg {R : Type u_1} {n : ℕ} [Neg R] (p : CMlPolynomial R n) : CMlPolynomial R n

Negation of a CMlPolynomial

@[inline]

def CompPoly.CMlPolynomial.smul {R : Type u_1} {n : ℕ} [Mul R] (r : R) (p : CMlPolynomial R n) : CMlPolynomial R n

Scalar multiplication of a CMlPolynomial

@[inline]

def CompPoly.CMlPolynomial.nsmul {R : Type u_1} {n : ℕ} [SMul ℕ R] (m : ℕ) (p : CMlPolynomial R n) : CMlPolynomial R n

Scalar multiplication of a CMlPolynomial by a natural number

@[inline]

def CompPoly.CMlPolynomial.zsmul {R : Type u_1} {n : ℕ} [SMul ℤ R] (m : ℤ) (p : CMlPolynomial R n) : CMlPolynomial R n

Scalar multiplication of a CMlPolynomial by an integer

@[implicit_reducible]

instance CompPoly.CMlPolynomial.instAddCommMonoid {R : Type u_1} {n : ℕ} [AddCommMonoid R] : AddCommMonoid (CMlPolynomial R n)

@[implicit_reducible]

instance CompPoly.CMlPolynomial.instModule {R : Type u_1} {n : ℕ} [Semiring R] : Module R (CMlPolynomial R n)

def CompPoly.CMlPolynomial.monomialBasis {R : Type u_1} {n : ℕ} [CommSemiring R] (w : Vector R n) : Vector R (2 ^ n)

@[simp]

theorem CompPoly.CMlPolynomial.monomialBasis_zero {R : Type u_1} [CommSemiring R] {w : Vector R 0} : monomialBasis w = #v[1]

theorem CompPoly.CMlPolynomial.monomialBasis_getElem {R : Type u_1} {n : ℕ} [CommSemiring R] {w : Vector R n} (i : Fin (2 ^ n)) : (monomialBasis w)[i] = ∏ j : Fin n, if { toFin := i }.getLsb j = true then w[j] else 1

The i-th element of monomialBasis w is the product of w[j] if the j-th bit of i is 1, and 1 if the j-th bit of i is 0.

def CompPoly.CMlPolynomial.map {n : ℕ} {R : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] (f : R →+* S) (p : CMlPolynomial R n) : CMlPolynomial S n

def CompPoly.CMlPolynomial.eval {R : Type u_1} {n : ℕ} [CommSemiring R] (p : CMlPolynomial R n) (x : Vector R n) : R

Evaluate a CMlPolynomial at a point

def CompPoly.CMlPolynomial.eval₂ {R : Type u_1} {n : ℕ} [CommSemiring R] {S : Type u_2} [CommSemiring S] (p : CMlPolynomial R n) (f : R →+* S) (x : Vector S n) : S

@[implicit_reducible]

instance CompPoly.CMlPolynomialEval.inhabited {R : Type u_1} {n : ℕ} [Inhabited R] : Inhabited (CMlPolynomialEval R n)

@[inline]

def CompPoly.CMlPolynomialEval.ofArray {R : Type u_1} [Zero R] (coeffs : Array R) (n : ℕ) : CMlPolynomialEval R n

Conform a list of coefficients to a CMlPolynomialEval with a given number of variables. May either pad with zeros or truncate.

@[inline]

def CompPoly.CMlPolynomialEval.zero {R : Type u_1} {n : ℕ} [Zero R] : CMlPolynomialEval R n

theorem CompPoly.CMlPolynomialEval.zero_def {R : Type u_1} {n : ℕ} [Zero R] : zero = Vector.replicate (2 ^ n) 0

@[inline]

def CompPoly.CMlPolynomialEval.add {R : Type u_1} {n : ℕ} [Add R] (p q : CMlPolynomialEval R n) : CMlPolynomialEval R n

Add two CMlPolynomialEvals

@[inline]

def CompPoly.CMlPolynomialEval.neg {R : Type u_1} {n : ℕ} [Neg R] (p : CMlPolynomialEval R n) : CMlPolynomialEval R n

Negation of a CMlPolynomialEval

@[inline]

def CompPoly.CMlPolynomialEval.smul {R : Type u_1} {n : ℕ} [Mul R] (r : R) (p : CMlPolynomialEval R n) : CMlPolynomialEval R n

Scalar multiplication of a CMlPolynomialEval

@[inline]

def CompPoly.CMlPolynomialEval.nsmul {R : Type u_1} {n : ℕ} [SMul ℕ R] (m : ℕ) (p : CMlPolynomialEval R n) : CMlPolynomialEval R n

Scalar multiplication of a CMlPolynomialEval by a natural number

@[inline]

def CompPoly.CMlPolynomialEval.zsmul {R : Type u_1} {n : ℕ} [SMul ℤ R] (m : ℤ) (p : CMlPolynomialEval R n) : CMlPolynomialEval R n

Scalar multiplication of a CMlPolynomialEval by an integer

@[implicit_reducible]

instance CompPoly.CMlPolynomialEval.instAddCommMonoid {R : Type u_1} {n : ℕ} [AddCommMonoid R] : AddCommMonoid (CMlPolynomialEval R n)

@[implicit_reducible]

instance CompPoly.CMlPolynomialEval.instModule {R : Type u_1} {n : ℕ} [Semiring R] : Module R (CMlPolynomialEval R n)

def CompPoly.CMlPolynomialEval.lagrangeBasis {R : Type u_1} {n : ℕ} [CommRing R] (w : Vector R n) : Vector R (2 ^ n)

Lagrange (hypercube) basis at point w.

Returns the length-2^n vector v such that for any x ∈ {0,1}^n, letting i = ∑_{j=0}^{n-1} x_j · 2^j (little‑endian indexing), we have v[i] = ∏_{j < n} (x_j · w[j] + (1 - x_j) · (1 - w[j])). Equivalently, for i : Fin (2^n), v[i] = ∏_{j < n}, (if the j-th bit of i is 1 then w[j] else 1 - w[j]).

@[simp]

theorem CompPoly.CMlPolynomialEval.lagrangeBasis_zero {R : Type u_1} [CommRing R] {w : Vector R 0} : lagrangeBasis w = #v[1]

theorem CompPoly.CMlPolynomialEval.lagrangeBasis_getElem {R : Type u_1} {n : ℕ} [CommRing R] {w : Vector R n} (i : Fin (2 ^ n)) : (lagrangeBasis w)[i] = ∏ j : Fin n, if { toFin := i }.getLsb j = true then w[j] else 1 - w[j]

The i-th element of lagrangeBasis w is the product of w[j] if the j-th bit of i is 1, and 1 - w[j] if the j-th bit of i is 0.

def CompPoly.CMlPolynomialEval.map {n : ℕ} {R : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] (f : R →+* S) (p : CMlPolynomialEval R n) : CMlPolynomialEval S n

Map a ring homomorphism over a CMlPolynomialEval

def CompPoly.CMlPolynomialEval.eval {R : Type u_1} {n : ℕ} [CommRing R] (p : CMlPolynomialEval R n) (x : Vector R n) : R

Evaluate a CMlPolynomialEval at a point

def CompPoly.CMlPolynomialEval.eval₂ {R : Type u_1} {n : ℕ} [CommRing R] {S : Type u_2} [CommRing S] (p : CMlPolynomialEval R n) (f : R →+* S) (x : Vector S n) : S

Evaluate a CMlPolynomialEval at a point using a ring homomorphism

@[inline]

def CompPoly.CMlPolynomialEval.eqTilde {R : Type u_1} {n : ℕ} [CommRing R] (w x : Vector R n) : R

Evaluate the multilinear equality kernel eq̃(w, x).

@[inline]

def CompPoly.CMlPolynomial.monoToLagrangeLevel {R : Type u_2} [AddCommGroup R] {n : ℕ} (j : Fin n) : Vector R (2 ^ n) → Vector R (2 ^ n)

One level of the zeta‑transform (coefficient to evaluation).

Processes the j-th variable by folding the "partner" index (with bit j cleared) into every index that has bit j set. At output index i: $$ (\text{monoToLagrangeLevel}\ j\ v)[i] \ =\ \begin{cases} v[i] + v[i - 2^j] & \text{if bit } j \text{ of } i \text{ is } 1 \\ v[i] & \text{otherwise} \end{cases} $$

After applying every level 0, 1, …, n-1 the resulting entry at i is $\sum_{j \subseteq i} p[j]$ (bitwise subset), which is the hypercube evaluation at the Boolean point encoded by i. Cost per level: $O(2^n)$ additions, so the full transform is $O(n \cdot 2^n)$.

The stride is $2^j$, the distance between indices that differ only in bit j.

@[inline]

def CompPoly.CMlPolynomial.monoToLagrange {R : Type u_2} [AddCommGroup R] (n : ℕ) : CMlPolynomial R n → CMlPolynomialEval R n

Full zeta transform: coefficients → evaluations.

Applies monoToLagrangeLevel 0, 1, …, n-1 in that order via foldl. The resulting entry at each index i : Fin (2 ^ n) is $\sum_{j \subseteq i} p[j]$ (the classical zeta transform on the Boolean lattice).

Complexity: $O(n \cdot 2^n)$ additions — this is the butterfly form. Contrast with the naive monoToLagrangeSpec which is $O(4^n)$.

@[inline]

def CompPoly.CMlPolynomial.lagrangeToMonoLevel {R : Type u_2} [AddCommGroup R] {n : ℕ} (j : Fin n) : Vector R (2 ^ n) → Vector R (2 ^ n)

One level of the inverse zeta‑transform / Möbius transform (evaluation to coefficient).

Processes the j-th variable by subtracting the partner entry (bit j cleared) from every index that has bit j set. At output index i: $$ (\text{lagrangeToMonoLevel}\ j\ v)[i] \ =\ \begin{cases} v[i] - v[i - 2^j] & \text{if bit } j \text{ of } i \text{ is } 1 \\ v[i] & \text{otherwise} \end{cases} $$

Each level is the exact inverse of monoToLagrangeLevel j (see lagrangeToMonoLevel_monoToLagrangeLevel_id).

The stride is $2^j$.

@[inline]

def CompPoly.CMlPolynomial.lagrangeToMono {R : Type u_2} [AddCommGroup R] (n : ℕ) : Vector R (2 ^ n) → Vector R (2 ^ n)

Full inverse / Möbius transform: evaluations → coefficients.

Applies lagrangeToMonoLevel (n-1), (n-2), …, 0 via foldr. The resulting entry at each index i : Fin (2 ^ n) is the inclusion-exclusion sum $\sum_{j \subseteq i} (-1)^{\mathrm{popCount}(i) - \mathrm{popCount}(j)} \cdot p[j]$ — see lagrangeToMono_eq_lagrangeToMonoSpec.

Complexity: $O(n \cdot 2^n)$ additions/subtractions. Contrast with the naive lagrangeToMonoSpec which is $O(4^n)$.

def CompPoly.CMlPolynomial.lagrangeToMonoSpec {n : ℕ} {R : Type u_2} [AddCommGroup R] (p : CMlPolynomialEval R n) : CMlPolynomialEval R n

The $O(4^n)$ inclusion-exclusion specification for the Möbius transform.

For each output index i, this sums over all indices j that are bitwise subsets of i (i &&& j = j), with sign $(-1)^{\mathrm{popCount}(i) - \mathrm{popCount}(j)}$: $$ (\text{lagrangeToMonoSpec}\ p)[i] = \sum_{j \subseteq i} (-1)^{\mathrm{popCount}(i) - \mathrm{popCount}(j)} \cdot p[j]. $$

Provable equivalent to the fast lagrangeToMono — see lagrangeToMono_eq_lagrangeToMonoSpec.

def CompPoly.CMlPolynomial.monoToLagrangeSpec {n : ℕ} {R : Type u_2} [AddCommGroup R] (p : CMlPolynomial R n) : CMlPolynomialEval R n

The $O(4^n)$ specification for the zeta transform (the mirror of lagrangeToMonoSpec).

For each output index i, this sums p[j] over every index j that is a bitwise subset of i (i &&& j = j): $$ (\text{monoToLagrangeSpec}\ p)[i]\ =\ \sum_{j \subseteq i} p[j]. $$

Provable equivalent to the fast monoToLagrange — see monoToLagrange_eq_monoToLagrangeSpec.

def CompPoly.CMlPolynomial.forwardRange (n : ℕ) (r : Fin n) (l : Fin (↑r + 1)) : List (Fin n)

Generates a list of indices representing a range of bit positions [l, r] in increasing order. Used for optimized recursive transforms that operate on segments of variables. Returns a list containing l, l+1, ..., r. The result is used to fold over dimensions in monoToLagrangeSegment and lagrangeToMonoSegment.

theorem CompPoly.CMlPolynomial.forwardRange_length (n : ℕ) (r : Fin n) (l : Fin (↑r + 1)) : (forwardRange n r l).length = ↑r - ↑l + 1

theorem CompPoly.CMlPolynomial.forwardRange_eq_of_r_eq (n : ℕ) (r1 r2 : Fin n) (h_r_eq : r1 = r2) (l : Fin (↑r1 + 1)) : forwardRange n r1 l = forwardRange n r2 ⟨↑l, ⋯⟩

theorem CompPoly.CMlPolynomial.forwardRange_getElem (n : ℕ) (r : Fin n) (l : Fin (↑r + 1)) (k : Fin (↑r - ↑l + 1)) : (forwardRange n r l).get ⟨↑k, ⋯⟩ = ⟨↑l + ↑k, ⋯⟩

theorem CompPoly.CMlPolynomial.forwardRange_succ_right_ne_empty (n : ℕ) (r : Fin (n - 1)) (l : Fin (↑r + 1)) : forwardRange n ⟨↑r + 1, ⋯⟩ ⟨↑l, ⋯⟩ ≠ []

theorem CompPoly.CMlPolynomial.forwardRange_pred_le_ne_empty (n : ℕ) (r : Fin n) (l : Fin (↑r + 1)) (h_l_gt_0 : ↑l > 0) : forwardRange n r ⟨↑l - 1, ⋯⟩ ≠ []

theorem CompPoly.CMlPolynomial.forwardRange_dropLast (n : ℕ) (r : Fin (n - 1)) (l : Fin (↑r + 1)) : (forwardRange n ⟨↑r + 1, ⋯⟩ ⟨↑l, ⋯⟩).dropLast = forwardRange n ⟨↑r, ⋯⟩ ⟨↑l, ⋯⟩

theorem CompPoly.CMlPolynomial.forwardRange_tail (n : ℕ) (r : Fin n) (l : Fin (↑r + 1)) (h_l_gt_0 : ↑l > 0) : (forwardRange n r ⟨↑l - 1, ⋯⟩).tail = forwardRange n r l

theorem CompPoly.CMlPolynomial.forwardRange_0_eq_finRange (n : ℕ) [NeZero n] : forwardRange n ⟨n - 1, ⋯⟩ 0 = List.finRange n

def CompPoly.CMlPolynomial.monoToLagrangeSegment {R : Type u_2} [AddCommGroup R] (n : ℕ) (r : Fin n) (l : Fin (↑r + 1)) : Vector R (2 ^ n) → Vector R (2 ^ n)

Performs the zeta-transform (coefficient to evaluation) on a segment of dimensions from l to r. Iteratively applies monoToLagrangeLevel for each dimension in the range. 0 ≤ l ≤ r < n.

def CompPoly.CMlPolynomial.lagrangeToMonoSegment {R : Type u_2} [AddCommGroup R] (n : ℕ) (r : Fin n) (l : Fin (↑r + 1)) : Vector R (2 ^ n) → Vector R (2 ^ n)

Performs the inverse zeta-transform (evaluation to coefficient) on a segment of dimensions

from l to r.

Iteratively applies lagrangeToMonoLevel for each dimension in the range (in reverse order).

0 ≤ l ≤ r < n.

theorem CompPoly.CMlPolynomial.monoToLagrange_eq_monoToLagrangeSegment {R : Type u_2} [AddCommGroup R] (n : ℕ) [NeZero n] (v : Vector R (2 ^ n)) : have h_n_ne_zero := ⋯; monoToLagrange n v = monoToLagrangeSegment n ⟨n - 1, ⋯⟩ ⟨0, ⋯⟩ v

theorem CompPoly.CMlPolynomial.lagrangeToMono_eq_lagrangeToMonoSegment {R : Type u_2} [AddCommGroup R] (n : ℕ) [NeZero n] (v : Vector R (2 ^ n)) : have h_n_ne_zero := ⋯; lagrangeToMono n v = lagrangeToMonoSegment n ⟨n - 1, ⋯⟩ ⟨0, ⋯⟩ v

theorem CompPoly.CMlPolynomial.testBit_of_sub_two_pow_of_bit_1 {n i : ℕ} (h_testBit_eq_1 : n.testBit i = true) : (n - 2 ^ i).testBit i = false

theorem CompPoly.CMlPolynomial.lagrangeToMonoLevel_monoToLagrangeLevel_id {n : ℕ} {R : Type u_2} [AddCommGroup R] (v : Vector R (2 ^ n)) (i : Fin n) : lagrangeToMonoLevel i (monoToLagrangeLevel i v) = v

theorem CompPoly.CMlPolynomial.monoToLagrangeLevel_lagrangeToMonoLevel_id {n : ℕ} {R : Type u_2} [AddCommGroup R] (v : Vector R (2 ^ n)) (i : Fin n) : monoToLagrangeLevel i (lagrangeToMonoLevel i v) = v

theorem CompPoly.CMlPolynomial.mobius_apply_zeta_apply_eq_id {R : Type u_2} [AddCommGroup R] (n : ℕ) [NeZero n] (r : Fin n) (l : Fin (↑r + 1)) (v : Vector R (2 ^ n)) : lagrangeToMonoSegment n r l (monoToLagrangeSegment n r l v) = v

theorem CompPoly.CMlPolynomial.zeta_apply_mobius_apply_eq_id {R : Type u_2} [AddCommGroup R] (n : ℕ) (r : Fin n) (l : Fin (↑r + 1)) (v : Vector R (2 ^ n)) : monoToLagrangeSegment n r l (lagrangeToMonoSegment n r l v) = v

def CompPoly.CMlPolynomial.equivMonomialLagrangeRepr {n : ℕ} {R : Type u_2} [AddCommGroup R] : CMlPolynomial R n ≃ CMlPolynomialEval R n

The equivalence between the monomial basis representation (CMlPolynomial) and the Lagrange basis representation (CMlPolynomialEval) of a multilinear polynomial. The forward map is monoToLagrange (zeta transform) and the inverse is lagrangeToMono (inverse zeta transform/Mobius transform).

#eval Tests

This section contains tests to verify the functionality of multilinear polynomial operations.