Coordinate pole divisor is bounded by weighted curve poles

Proved

OAI.PiExponent.FormalInterpolation.coordinate_pole_divisor_le_weighted

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

For positive coordinate weights, the total pole order of any chosen coordinate is at most its weight times the total weighted pole quantity. At each place this follows from the coordinate's entry in the supremum defining polynomialCurvePole, together with its zero entry; the proof must establish the finite-support facts needed for the finsum comparison.

Preamble

import Definitions.Def_OAI_PiExponent_TruncatedPolynomialJets
import Definitions.Def_OAI_PiExponent_LogarithmicInterpolationNumerics
import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion
import Mathlib.RingTheory.Algebraic.Defs

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

Formal statement

theorem OAI.PiExponent.FormalInterpolation.coordinate_pole_divisor_le_weighted
    {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)) (k : Fin d) :
    (∑ᶠ nu : PolynomialCurvePlace E,
      max (-(polynomialCurveOrder nu (x k) : Real)) 0) ≤
      (w k : Real) *
        (∑ᶠ nu : PolynomialCurvePlace E, polynomialCurvePole nu x w) := by sorry

View graph