Equivalence between CMlPolynomial and multilinear polynomials in MvPolynomial

This file establishes the mathematical foundations for CMlPolynomial by proving:

1. Basis properties for the coefficient representation
2. Change-of-basis matrices between different representations
3. Equivalences with mathlib's MvPolynomial.restrictDegree: equivMvPolynomialDeg1
4. Arithmetic operation compatibilities

Equivalence with Mathlib MvPolynomial

• Note: maybe we have to add more restrictions on CMlPolynomial R n and CMlPolynomialEval R n so we can differentiate them?

noncomputable def CompPoly.CMlPolynomial.monomialOfNat {n : ℕ} (i : ℕ) : Fin n →₀ ℕ

Converts a natural number to a monomial with 0/1 exponents. Uses little‑endian bit encoding: bit 0 is the least significant bit. The exponent at variable j is Nat.getBit j i ∈ {0,1}.

theorem CompPoly.CMlPolynomial.eq_monomialOfNat_iff_eq_bitRepr {n : ℕ} (m : Fin n →₀ ℕ) (h_binary : ∀ (j : Fin n), m j ≤ 1) (i : Fin (2 ^ n)) : monomialOfNat ↑i = m ↔ i = Nat.binaryFinMapToNat (⇑m) h_binary

noncomputable def CompPoly.CMlPolynomial.toMvPolynomial {R : Type u_1} [CommSemiring R] {n : ℕ} (p : CMlPolynomial R n) : MvPolynomial (Fin n) R

Converts an CMlPolynomial to a mathlib multivariate polynomial. Sums over all indices i : Fin (2^n) with monomial exponents from monomialOfNat i and coefficients p[i].

theorem CompPoly.CMlPolynomial.toMvPolynomial_is_multilinear {R : Type u_1} [CommSemiring R] {n : ℕ} (p : CMlPolynomial R n) : p.toMvPolynomial ∈ MvPolynomial.restrictDegree (Fin n) R 1

theorem CompPoly.CMlPolynomial.coeff_of_toMvPolynomial_eq_coeff_of_CMlPolynomial {R : Type u_1} [CommSemiring R] {n : ℕ} (p : CMlPolynomial R n) (m : Fin n →₀ ℕ) : MvPolynomial.coeff m p.toMvPolynomial = if h_binary : ∀ (j : Fin n), m j ≤ 1 then let i_of_m := ↑(Nat.binaryFinMapToNat (⇑m) h_binary); p[i_of_m] else 0

noncomputable def CompPoly.CMlPolynomial.toMvPolynomialDeg1 {R : Type u_1} [CommSemiring R] {n : ℕ} (p : CMlPolynomial R n) : ↥(MvPolynomial.restrictDegree (Fin n) R 1)

Converts an CMlPolynomial to a mathlib restricted-degree multivariate polynomial. Wraps toMvPolynomial with a proof that the result is multilinear (i.e. individual degrees ≤ 1).

noncomputable def CompPoly.CMlPolynomial.ofMvPolynomialDeg1 {R : Type u_1} [CommSemiring R] {n : ℕ} (p : ↥(MvPolynomial.restrictDegree (Fin n) R 1)) : CMlPolynomial R n

Converts a mathlib restricted-degree multivariate polynomial to an CMlPolynomial. Extracts coefficients using monomialOfNat to map indices to monomials.

noncomputable def CompPoly.CMlPolynomial.equivMvPolynomialDeg1 {R : Type u_1} [CommSemiring R] {n : ℕ} : CMlPolynomial R n ≃ ↥(MvPolynomial.restrictDegree (Fin n) R 1)

Equivalence between CMlPolynomial and mathlib's restricted-degree multivariate polynomials. Establishes that both representations are isomorphic via coefficient extraction/insertion.

noncomputable def CompPoly.CMlPolynomial.linearEquivMvPolynomialDeg1 {R : Type u_1} [CommSemiring R] {n : ℕ} : CMlPolynomial R n ≃ₗ[R] ↥(MvPolynomial.restrictDegree (Fin n) R 1)

Linear equivalence between CMlPolynomial and MvPolynomial.restrictDegree

noncomputable def CompPoly.CMlPolynomialEval.toMvPolynomial {R : Type u_1} [CommSemiring R] {n : ℕ} [AddCommGroup R] (p : CMlPolynomialEval R n) : MvPolynomial (Fin n) R

Converts a hypercube-evaluation representation to a Mathlib multivariate polynomial by first recovering the monomial-basis representation.

noncomputable def CompPoly.CMlPolynomialEval.toMvPolynomialDeg1 {R : Type u_1} [CommSemiring R] {n : ℕ} [AddCommGroup R] (p : CMlPolynomialEval R n) : ↥(MvPolynomial.restrictDegree (Fin n) R 1)

Converts a hypercube-evaluation representation to a Mathlib restricted-degree multivariate polynomial.

noncomputable def CompPoly.CMlPolynomialEval.eqPolynomial {R : Type u_1} [CommSemiring R] {n : ℕ} [CommRing R] (w : Vector R n) : MvPolynomial (Fin n) R

The multilinear equality polynomial centered at w.

noncomputable def CompPoly.CMlPolynomialEval.eqPolynomialDeg1 {R : Type u_1} [CommSemiring R] {n : ℕ} [CommRing R] (w : Vector R n) : ↥(MvPolynomial.restrictDegree (Fin n) R 1)

The restricted-degree multilinear equality polynomial centered at w.