Exponential monomial row test as a power-series coefficient

Proved

OAI.PiExponent.LiteralAnalytic.TranslatedExpansion.exponentialMonomial_rowTest_eq_series

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

number-theoryopenai-pi-exponent-017

The analytic row test of an exponential monomial centered at the integer period is the corresponding coefficient of its power-series expansion in the logarithmic coordinate.

Preamble

import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_TranslatedExpansion_CollisionAnalyticHelpers
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_TranslatedExpansionTerms

open scoped BigOperators Topology
open OAI.PiExponent.LiteralAnalytic.TranslatedExpansion
open OAI.PiExponent.LiteralAnalytic.TranslatedExpansion.CollisionAnalytic

Formal statement

theorem OAI.PiExponent.LiteralAnalytic.TranslatedExpansion.exponentialMonomial_rowTest_eq_series
    (b : ℂ) (j h d ell : ℕ) :
    rowTest ell (fun t => exponentialMonomial b (h : ℂ) d
      ((j : ℂ) * OAI.PiExponent.LiteralAnalytic.TranslatedExpansion.period +
        Complex.log (1 + t))) =
    PowerSeries.coeff ell
      (PowerSeries.C b * (1 + PowerSeries.X) ^ h *
        (PowerSeries.C ((j : ℂ) *
          OAI.PiExponent.LiteralAnalytic.TranslatedExpansion.period) +
          PowerSeries.log ℂ) ^ d) := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/LiteralAnalyticSummand.lean#L177-L199

View graph