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

@[instance_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

@[instance_reducible]

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

@[instance_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)

theorem CompPoly.CMlPolynomial.map_monomialBasis {R : Type u_1} {n : ℕ} [CommSemiring R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (x : Vector R n) : Vector.map (⇑f) (monomialBasis x) = monomialBasis (Vector.map (⇑f) x)

Mapping each monomial-basis value by a ring homomorphism equals evaluating the monomial basis at the mapped point.

@[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

@[inline, specialize #[]]

def CompPoly.CMlPolynomial.evalHornerStep {R : Type u_1} [CommSemiring R] {n : ℕ} (coeffs : Vector R (2 ^ (n + 1))) (x0 : R) : Vector R (2 ^ n)

One Horner reduction step, eliminating the next little-endian variable.

@[inline, specialize #[]]

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

Evaluate dense multilinear coefficients by eliminating one variable at a time.

@[inline, specialize #[]]

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

Evaluate a CMlPolynomial at a point using a multilinear Horner method.

@[inline, specialize #[]]

def CompPoly.CMlPolynomial.eval₂Horner {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

Evaluate a CMlPolynomial using a ring homomorphism and multilinear Horner method.

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

theorem CompPoly.CMlPolynomial.map_eval {R : Type u_1} {n : ℕ} [CommSemiring R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (p : CMlPolynomial R n) (x : Vector R n) : f (p.eval x) = (map f p).eval (Vector.map (⇑f) x)

Mapping a coefficient-form evaluation by a ring homomorphism equals evaluating the mapped coefficients at the mapped point.

def CompPoly.CMlPolynomial.evalWithProducts {R : Type u_1} {n : ℕ} [CommSemiring R] {W : Type u_3} [AddZero W] (product : R → R → W) (reduce : W →+ R) (p : CMlPolynomial R n) (x : Vector R n) : R

Evaluate monomial coefficients by accumulating their products with the monomial-basis values in W, starting at zero, then reducing once to a value in R.

theorem CompPoly.CMlPolynomial.evalWithProducts_eq_eval {R : Type u_1} {n : ℕ} [CommSemiring R] {W : Type u_3} [AddZero W] (product : R → R → W) (reduce : W →+ R) (hproduct : ∀ (a b : R), reduce (product a b) = a * b) (p : CMlPolynomial R n) (x : Vector R n) : evalWithProducts product reduce p x = p.eval x

Product accumulation followed by additive reduction agrees with coefficient evaluation when reducing each product gives the ordinary product of its two factors.

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

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

Horner evaluation agrees with the dot-product evaluator.

theorem CompPoly.CMlPolynomial.eval₂_horner_eq_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) : p.eval₂Horner f x = p.eval₂ f x

Horner evaluation through a ring homomorphism agrees with the dot-product evaluator.

@[instance_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

@[instance_reducible]

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

@[instance_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

@[inline, specialize #[]]

def CompPoly.CMlPolynomialEval.evalMleStep {R : Type u_1} [CommRing R] {n : ℕ} (values : Vector R (2 ^ (n + 1))) (x0 : R) : Vector R (2 ^ n)

One multilinear-extension interpolation step, eliminating the next little-endian variable.

@[inline, specialize #[]]

def CompPoly.CMlPolynomialEval.evalMleLayer {R : Type u_1} [CommRing R] {n : ℕ} (values : CMlPolynomialEval R (n + 1)) (x0 : R) : CMlPolynomialEval R n

Public multilinear-extension interpolation layer.

@[simp]

theorem CompPoly.CMlPolynomialEval.evalMleLayer_get {R : Type u_1} [CommRing R] {n : ℕ} (values : CMlPolynomialEval R (n + 1)) (x0 : R) (j : Fin (2 ^ n)) : Vector.get (values.evalMleLayer x0) j = (1 - x0) * Vector.get values ⟨2 * ↑j, ⋯⟩ + x0 * Vector.get values ⟨2 * ↑j + 1, ⋯⟩

The j-th entry after one MLE layer is the affine interpolation of its input pair.

@[inline, specialize #[]]

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

Evaluate hypercube values by recursively interpolating the multilinear extension.

@[inline, specialize #[]]

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

Evaluate a CMlPolynomialEval by recursive multilinear-extension interpolation.

@[simp]

theorem CompPoly.CMlPolynomialEval.evalMle_zero {R : Type u_1} [CommRing R] (p : CMlPolynomialEval R 0) (x : Vector R 0) : p.evalMle x = Vector.get p ⟨0, CMlPolynomial.evalHornerCoeffs._proof_3⟩

Evaluating a zero-variable hypercube table returns its only value.

@[simp]

theorem CompPoly.CMlPolynomialEval.evalMle_succ {R : Type u_1} [CommRing R] {n : ℕ} (p : CMlPolynomialEval R (n + 1)) (x : Vector R (n + 1)) : p.evalMle x = (p.evalMleLayer x.head).evalMle x.tail

Recursive MLE evaluation first folds the head variable, then evaluates the tail.

@[inline, specialize #[]]

def CompPoly.CMlPolynomialEval.eval₂Mle {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 through a ring homomorphism using multilinear-extension interpolation.

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

theorem CompPoly.CMlPolynomialEval.eval_smul {R : Type u_1} {n : ℕ} [CommRing R] (a : R) (p : CMlPolynomialEval R n) (x : Vector R n) : (a • p).eval x = a * p.eval x

Evaluation commutes with scalar multiplication of a hypercube table.

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

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

Multilinear-extension interpolation agrees with the dot-product evaluator.

theorem CompPoly.CMlPolynomialEval.eqTilde_eq_prod {R : Type u_1} {n : ℕ} [CommRing R] (w x : Vector R n) : eqTilde w x = ∏ i : Fin n, (w[i] * x[i] + (1 - w[i]) * (1 - x[i]))

The multilinear equality kernel is the product of its coordinatewise affine factors.

theorem CompPoly.CMlPolynomialEval.eqTilde_append {R : Type u_1} {n : ℕ} [CommRing R] {m : ℕ} (w₁ x₁ : Vector R n) (w₂ x₂ : Vector R m) : eqTilde (w₁ ++ w₂) (x₁ ++ x₂) = eqTilde w₁ x₁ * eqTilde w₂ x₂

The equality kernel factors across appended coordinate blocks.

theorem CompPoly.CMlPolynomialEval.eval₂_mle_eq_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) : p.eval₂Mle f x = p.eval₂ f x

Multilinear-extension interpolation through a ring homomorphism agrees with the dot-product evaluator.

@[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.