Polynomial evaluation poles are bounded by weighted height times coordinate poles

Proved

OAI.PiExponent.FormalInterpolation.polynomial_curve_aeval_pole_le_weighted_height

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrynumber-theoryopenai-pi-exponent-017

Let $\nu$ be a normalized place, let $w_i>0$ be weights, and let $F$ be a polynomial whose support has weighted degree at most $N\ge 0$ . Then the pole order of the evaluation $F(x)$ at $\nu$ satisfies

\max(-\operatorname{ord}_\nu(F(x)),0)\le N\cdot\mathrm{Pole}_\nu(x,w).

This is the placewise form of the weighted polynomial pole bound (compare OpenAI PolynomialPoleBound / WeightedPolynomialPole): each monomial of weight $\le N$ has valuation at least $-N\cdot\mathrm{Pole}_\nu$ , and the valuation of a sum is at least the minimum of the summands.

Preamble

import Definitions.Def_OAI_PiExponent_LogarithmicWordContact

open scoped BigOperators
open OAI.PiExponent OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.polynomial_curve_aeval_pole_le_weighted_height
    {d : Nat} {E : Type} [Field E] [Algebra Complex E]
    (nu : PolynomialCurvePlace E) (x : Fin d → E)
    (w : Fin d → Rat) (hw : ∀ i, 0 < (w i : Real))
    (N : Real) (hN : 0 ≤ N)
    (F : MvPolynomial (Fin d) Complex)
    (hF : logarithmicDegreeBound w N F) :
    max (-(polynomialCurveOrder nu (MvPolynomial.aeval x F) : Real)) 0 ≤
      N * polynomialCurvePole nu x w := by sorry

Source

OpenAI math repo lean/OAI/NumberTheory/PiExponent/Polynomials/PolynomialPoleBound.lean and WeightedPolynomialPole.lean (framePolynomial_order_lower); reduction obligation for polynomial_curve_zero_divisor_bound on Prove2Me.

View graph