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).

This function performs the transformation for the j-th variable (corresponding to the j-th bit). It iterates over all indices i in the boolean hypercube. If the j-th bit of i is 1, it adds the value at the corresponding index with the j-th bit 0 (i - stride) to the current value. This effectively computes the partial sum along the j-th dimension, which corresponds to evaluating the polynomial at $X_j = 1$ given its values at $X_j = 0$ (coefficients) and difference.

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

@[inline]

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

Full transform: coefficients → evaluations.

@[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 (evaluation to coefficient).

This function performs the inverse transformation for the j-th variable. It iterates over all indices i. If the j-th bit of i is 1, it subtracts the value at the corresponding index with the j-th bit 0 (i - stride) from the current value. This recovers the coefficient for the term involving $X_j$ from the evaluations.

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 transform: evaluations → coefficients.

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

The $ O(4^n) $ computable version of the Mobius Transform, serving as the spec.

For each output index $ i $, this sums over all indices $ j $ that are bitwise subsets of $ i $, with sign determined by the parity of the Hamming-weight difference.

Fast ↔ Spec equivalence for the Möbius transform

We prove lagrangeToMono = lagrangeToMonoSpec by introducing an indexed family of "partial Möbius sums" mobiusPartial k that interpolates between the identity (at k = n) and the full spec (at k = 0). Each step of the fast transform lagrangeToMonoLevel (k - 1) decrements the parameter by exactly one. Combined with the base case we obtain the result by descending induction on k.

theorem CompPoly.CMlPolynomial.lagrangeToMono_eq_lagrangeToMonoSpec {R : Type u_3} [AddCommGroup R] {n : ℕ} (p : Vector R (2 ^ n)) : lagrangeToMono n p = lagrangeToMonoSpec p

The fast Möbius transform lagrangeToMono is pointwise equal to the inclusion-exclusion specification lagrangeToMonoSpec. Combines the fold lemma with the k = 0 base case.

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.