2.9. The Mathlib correspondence🔗

HexTruncatedSeriesTheory gives TSeries R n Mathlib's CommRing structure, built from the operations above, so Mathlib's lemmas apply to the same addition and multiplication that the programs use. It defines HexTruncatedSeriesTheory.ofPowerSeries, which keeps the first n coefficients of a Mathlib power series, as a surjective ring homomorphism:

def

HexTruncatedSeriesTheory.ofPowerSeriesHom.{u} {R : Type u} {n : ℕ}
  [CommRing R] : PowerSeries R →+* Hex.TSeries R n
HexTruncatedSeriesTheory.ofPowerSeriesHom.{u}
  {R : Type u} {n : ℕ} [CommRing R] :
  PowerSeries R →+* Hex.TSeries R n

Truncation from power series is a ring homomorphism.

theorem

HexTruncatedSeriesTheory.ker_ofPowerSeriesHom.{u} {R : Type u} {n : ℕ}
  [CommRing R] :
  RingHom.ker HexTruncatedSeriesTheory.ofPowerSeriesHom =
    Ideal.span {PowerSeries.X ^ n}
HexTruncatedSeriesTheory.ker_ofPowerSeriesHom.{u}
  {R : Type u} {n : ℕ} [CommRing R] :
  RingHom.ker
      HexTruncatedSeriesTheory.ofPowerSeriesHom =
    Ideal.span {PowerSeries.X ^ n}

The kernel of coefficient truncation is the principal ideal (X^n).

So TSeries R n is the quotient of the ring of power series by (Xⁿ):

def

HexTruncatedSeriesTheory.quotEquiv.{u} {R : Type u} {n : ℕ}
  [CommRing R] :
  PowerSeries R ⧸ Ideal.span {PowerSeries.X ^ n} ≃+* Hex.TSeries R n
HexTruncatedSeriesTheory.quotEquiv.{u}
  {R : Type u} {n : ℕ} [CommRing R] :
  PowerSeries R ⧸
      Ideal.span {PowerSeries.X ^ n} ≃+*
    Hex.TSeries R n

Fixed-precision series are power series modulo X^n.

Truncation commutes with inversion:

theorem

HexTruncatedSeriesTheory.ofPowerSeries_invOfUnit.{u} {R : Type u}
  {n : ℕ} [CommRing R] (f : PowerSeries R) (u : Rˣ)
  (hu : PowerSeries.constantCoeff f = ↑u) :
  HexTruncatedSeriesTheory.ofPowerSeries (f.invOfUnit u) =
    (HexTruncatedSeriesTheory.ofPowerSeries f).invOfUnit ↑u⁻¹
HexTruncatedSeriesTheory.ofPowerSeries_invOfUnit.{u}
  {R : Type u} {n : ℕ} [CommRing R]
  (f : PowerSeries R) (u : Rˣ)
  (hu :
    PowerSeries.constantCoeff f = ↑u) :
  HexTruncatedSeriesTheory.ofPowerSeries
      (f.invOfUnit u) =
    (HexTruncatedSeriesTheory.ofPowerSeries
          f).invOfUnit
      ↑u⁻¹

Truncation carries Mathlib's unit-certified inverse to executable Newton inversion.

This turns computations into proofs about Mathlib's power series. The theorem below determines the coefficient of x¹⁰ in the inverse of the finite product (1 - x)(1 - x²)⋯(1 - x¹⁰). The factors beyond it do not change that coefficient, so by Euler's identity it is p(10) = 42; the theorem itself does not mention partitions. The proof truncates at precision 11, moves the inverse and the product across the homomorphism, and lets decide +kernel run the Newton iteration:

open HexTruncatedSeriesTheory in
theorem partitions_ten :
    PowerSeries.coeff 10 (PowerSeries.invOfUnit
      (∏ j ∈ Finset.range 10,
        (1 - PowerSeries.X ^ (j + 1)) :
        PowerSeries ℤ) 1) = 42 := by⊢ (PowerSeries.coeff 10) ((∏ j ∈ Finset.range 10, (1 - PowerSeries.X ^ (j + 1))).invOfUnit 1) = 42
  rw [← coeff_ofPowerSeries (n := 11) _ 10 (by⊢ 10 < 11 decideAll goals completed! 🐙),
    ofPowerSeries_invOfUnit _ 1 (by⊢ PowerSeries.constantCoeff (∏ j ∈ Finset.range 10, (1 - PowerSeries.X ^ (j + 1))) = ↑1 simpAll goals completed! 🐙),
    ← ofPowerSeriesHom_apply,⊢ ((ofPowerSeriesHom (∏ j ∈ Finset.range 10, (1 - PowerSeries.X ^ (j + 1)))).invOfUnit ↑1⁻¹).coeff 10 = 42 map_prod⊢ ((∏ x ∈ Finset.range 10, ofPowerSeriesHom (1 - PowerSeries.X ^ (x + 1))).invOfUnit ↑1⁻¹).coeff 10 = 42]⊢ ((∏ x ∈ Finset.range 10, ofPowerSeriesHom (1 - PowerSeries.X ^ (x + 1))).invOfUnit ↑1⁻¹).coeff 10 = 42
  simp only [map_sub, map_one, map_pow,
    ofPowerSeriesHom_apply, ofPowerSeries_X]⊢ ((∏ x ∈ Finset.range 10, (1 - X ^ (x + 1))).invOfUnit ↑1⁻¹).coeff 10 = 42
  decide +kernelAll goals completed! 🐙

end HexTruncatedSeriesChapter

The companion proves the same kind of statement for the other operations that have a counterpart in Mathlib: substitution (HexTruncatedSeriesTheory.ofPowerSeries_subst), the compositional inverse (HexTruncatedSeriesTheory.ofPowerSeries_substInvOfIsUnit), the exponential (HexTruncatedSeriesTheory.ofPowerSeries_exp) and the logarithm (HexTruncatedSeriesTheory.ofPowerSeries_logOf), as well as powers, truncation and the derivative. Their hypotheses differ from Mathlib's in two places. Mathlib's substitution f.subst g needs only that the constant coefficient of g be nilpotent, while comp needs it to be 0, and the correspondence assumes the stronger hypothesis: over ℤ/4ℤ at precision 1, substituting g = 2 into f = X gives the constant 2, while comp of the truncations gives 0. Mathlib's exponential and logarithm are defined over ℚ-algebras, so those two correspondences assume one, and the exponential and logarithm over ℤ/pℤ described above have no Mathlib counterpart.

Mathlib has no square root of power series either. The companion proves that, given a square root r of the constant coefficient with 2r a unit, there is exactly one power series square root with constant coefficient r:

theorem

HexTruncatedSeriesTheory.exists_unique_sq.{u} {R : Type u} [CommRing R]
  (f : PowerSeries R) (r : R) (hr : r * r = PowerSeries.constantCoeff f)
  (hu : IsUnit (2 * r)) :
  ∃! s, s * s = f ∧ PowerSeries.constantCoeff s = r
HexTruncatedSeriesTheory.exists_unique_sq.{u}
  {R : Type u} [CommRing R]
  (f : PowerSeries R) (r : R)
  (hr :
    r * r = PowerSeries.constantCoeff f)
  (hu : IsUnit (2 * r)) :
  ∃! s,
    s * s = f ∧
      PowerSeries.constantCoeff s = r

A unit derivative at a chosen constant root gives exactly one square-root lift in the full power-series ring.