6.7. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexSparsePolyMathlib identifies the sparse representation with Mathlib's Polynomial R, composing a ring equivalence with the dense representation and HexPolyMathlib's equivalence.

def

HexSparsePolyMathlib.denseEquiv.{u} {R : Type u} [CommRing R]
  [DecidableEq R] : Hex.SparsePoly R ≃+* Hex.DensePoly R
HexSparsePolyMathlib.denseEquiv.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] :
  Hex.SparsePoly R ≃+* Hex.DensePoly R

The executable sparse representation is ring-equivalent to the executable dense representation, by the core library's conversions.

def

HexSparsePolyMathlib.equiv.{u} {R : Type u} [CommRing R]
  [DecidableEq R] : Hex.SparsePoly R ≃+* Polynomial R
HexSparsePolyMathlib.equiv.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] :
  Hex.SparsePoly R ≃+* Polynomial R

The executable sparse representation is ring-equivalent to Mathlib polynomials.

The identification is exact, coefficient by coefficient, and the stored exponents are exactly Mathlib's support, which is the sense in which the representation is sparse.

theorem

HexSparsePolyMathlib.coeff_equiv.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) (e : ℕ) :
  (HexSparsePolyMathlib.equiv s).coeff e = s.coeff e
HexSparsePolyMathlib.coeff_equiv.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R)
  (e : ℕ) :
  (HexSparsePolyMathlib.equiv s).coeff e =
    s.coeff e

equiv preserves coefficients; the identification is exact, coefficient by coefficient.

theorem

HexSparsePolyMathlib.equiv_support.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) :
  (HexSparsePolyMathlib.equiv s).support = s.support.toList.toFinset
HexSparsePolyMathlib.equiv_support.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) :
  (HexSparsePolyMathlib.equiv s).support =
    s.support.toList.toFinset

The stored exponents of the canonical representation are exactly Mathlib's support: the headline sense in which the representation is sparse.

One correspondence lemma per public operation transports evaluation, differentiation, composition, exponent substitution, and argument scaling, alongside the constructor and observer images.

theorem

HexSparsePolyMathlib.equiv_eval.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) (x : R) :
  Polynomial.eval x (HexSparsePolyMathlib.equiv s) = s.eval x
HexSparsePolyMathlib.equiv_eval.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R)
  (x : R) :
  Polynomial.eval x
      (HexSparsePolyMathlib.equiv s) =
    s.eval x

Evaluation corresponds: Mathlib evaluation of the image is the executable gap-Horner evaluation.

theorem

HexSparsePolyMathlib.equiv_derivative.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) :
  Polynomial.derivative (HexSparsePolyMathlib.equiv s) =
    HexSparsePolyMathlib.equiv s.derivative
HexSparsePolyMathlib.equiv_derivative.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) :
  Polynomial.derivative
      (HexSparsePolyMathlib.equiv s) =
    HexSparsePolyMathlib.equiv
      s.derivative

Differentiation corresponds: Mathlib's derivative of the image is the image of the executable derivative.

theorem

HexSparsePolyMathlib.equiv_compose.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (s t : Hex.SparsePoly R) :
  (HexSparsePolyMathlib.equiv s).comp (HexSparsePolyMathlib.equiv t) =
    HexSparsePolyMathlib.equiv (s.compose t)
HexSparsePolyMathlib.equiv_compose.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R]
  (s t : Hex.SparsePoly R) :
  (HexSparsePolyMathlib.equiv s).comp
      (HexSparsePolyMathlib.equiv t) =
    HexSparsePolyMathlib.equiv
      (s.compose t)

Composition corresponds: Mathlib's comp of the images is the image of the executable composition.

theorem

HexSparsePolyMathlib.equiv_substPow.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) (k : ℕ) :
  (HexSparsePolyMathlib.equiv s).comp (Polynomial.X ^ k) =
    HexSparsePolyMathlib.equiv (s.substPow k)
HexSparsePolyMathlib.equiv_substPow.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R)
  (k : ℕ) :
  (HexSparsePolyMathlib.equiv s).comp
      (Polynomial.X ^ k) =
    HexSparsePolyMathlib.equiv
      (s.substPow k)

Exponent substitution corresponds to composition with X ^ k.

theorem

HexSparsePolyMathlib.equiv_substScale.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) (a : R) :
  (HexSparsePolyMathlib.equiv s).comp (Polynomial.C a * Polynomial.X) =
    HexSparsePolyMathlib.equiv (s.substScale a)
HexSparsePolyMathlib.equiv_substScale.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R)
  (a : R) :
  (HexSparsePolyMathlib.equiv s).comp
      (Polynomial.C a * Polynomial.X) =
    HexSparsePolyMathlib.equiv
      (s.substScale a)

Argument scaling corresponds to composition with C a * X.