10.7. The Mathlib correspondence🔗

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

def

HexSparsePolyTheory.denseEquiv.{u} {R : Type u} [CommRing R]
  [DecidableEq R] : Hex.SparsePoly R ≃+* Hex.DensePoly R
HexSparsePolyTheory.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

HexSparsePolyTheory.equiv.{u} {R : Type u} [CommRing R]
  [DecidableEq R] : Hex.SparsePoly R ≃+* Polynomial R
HexSparsePolyTheory.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

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

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

theorem

HexSparsePolyTheory.equiv_support.{u} {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) :
  (HexSparsePolyTheory.equiv s).support = s.support.toList.toFinset
HexSparsePolyTheory.equiv_support.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] (s : Hex.SparsePoly R) :
  (HexSparsePolyTheory.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

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

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

theorem

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

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

theorem

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

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

theorem

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

Exponent substitution corresponds to composition with X ^ k.

theorem

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

Argument scaling corresponds to composition with C a * X.