Prove2Me

Subtracting a constant preserves coordinate pole degree

Proved
OAI.PiExponent.FormalInterpolation.coordinate_poles_invariant_sub_const

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

For a transcendental coordinate in a finite-type one-variable function field over Complex, subtracting any constant preserves its total pole degree.

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_poles_invariant_sub_const
    {E : Type} [Field E] [Algebra Complex E]
    [Algebra.EssFiniteType Complex E]
    (htrdeg : Algebra.trdeg Complex E = 1) (z : E)
    (hz : Transcendental Complex z) (b : Complex) :
    (∑ᶠ nu : PolynomialCurvePlace E,
      max (-(polynomialCurveOrder nu (z - algebraMap Complex E b) : Real)) 0) =
      ∑ᶠ nu : PolynomialCurvePlace E,
        max (-(polynomialCurveOrder nu z : Real)) 0 := by sorry

View graph