Scaled zero-divisor comparison against weighted coordinate poles

Proved

OAI.PiExponent.FormalInterpolation.polynomial_curve_scaled_divisor_comparison

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

For a nonzero polynomial evaluation on a generating one-variable complex function field, any nonnegative branch mass bounded by its scaled positive orders has total mass bounded by the polynomial's weighted height times the weighted coordinate pole degree.

Preamble

import Definitions.Def_OAI_PiExponent_LogarithmicWordContact
import Definitions.Def_OAI_PiExponent_LogarithmicInterpolationNumerics

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

Formal statement

theorem OAI.PiExponent.FormalInterpolation.polynomial_curve_scaled_divisor_comparison
    {d : Nat} (E : Type) [Field E] [Algebra Complex E]
    [Algebra.EssFiniteType Complex E]
    (htrdeg : Algebra.trdeg Complex E = 1) (x : Fin d → E)
    (hgen : IntermediateField.adjoin Complex (Set.range x) = ⊤)
    (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)
    (hne : MvPolynomial.aeval x F ≠ 0)
    (a r : Real) (ha : 0 < a) (hr : 0 < r)
    (b : PolynomialCurvePlace E → Real) (hb : ∀ nu, 0 ≤ b nu)
    (hlocal : ∀ nu, 0 < b nu →
      a * b nu ≤ r * (polynomialCurveOrder nu (MvPolynomial.aeval x F) : Real)) :
    a * (∑ᶠ nu : PolynomialCurvePlace E, b nu) ≤
      r * N * (∑ᶠ nu : PolynomialCurvePlace E, polynomialCurvePole nu x w) := by sorry

View graph