Lifted formal logarithm agrees with its finite sum below the cutoff

Proved

OAI.PiExponent.AdmissibleFormalInterpolation.liftLogSeries_log_coeff_finite_sum

by Eyal1990 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryopenai-pi-exponent-017

The lifted logarithm and its finite logarithmic sum have equal coefficients whenever the first-coordinate exponent is strictly below the cutoff. Both have zero coefficients involving later variables, and their constant coefficients vanish.

Preamble

import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation

open scoped BigOperators
open OAI.PiExponent.AdmissibleFormalInterpolation

Formal statement

theorem OAI.PiExponent.AdmissibleFormalInterpolation.liftLogSeries_log_coeff_finite_sum
    {m : ℕ} (T : ℕ) (a : Fin (m + 1) →₀ ℕ) (ha : a 0 < T) :
    MvPowerSeries.coeff a (liftLogSeries m (PowerSeries.log ℂ)) =
      MvPowerSeries.coeff a
        (∑ k ∈ Finset.range T,
          (if k = 0 then 0 else
            (((-1 : ℂ) ^ (k + 1)) / (k : ℂ)) •
              (MvPowerSeries.X 0 : MvPowerSeries (Fin (m + 1)) ℂ) ^ k)) := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph