Coordinate and weighted pole functions have finite support

Proved

OAI.PiExponent.FormalInterpolation.coordinateWeightedPole_support_finite

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

Only finitely many normalized places contribute to either the selected coordinate pole sum or the weighted pole sum.

Preamble

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

open scoped BigOperators
open OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.coordinateWeightedPole_support_finite {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) : Set.Finite {nu : PolynomialCurvePlace E | max (-(polynomialCurveOrder nu (x k) : Real)) 0 ≠ 0} ∧ Set.Finite {nu : PolynomialCurvePlace E | polynomialCurvePole nu x w ≠ 0} := by sorry

View graph