Generation form implies representative form of eventual weighted sections

Proved

OAI.PiExponent.FormalInterpolation.eventual_weighted_generation_implies_eventual_surjective_weighted_sections

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

If the quotient map from the subtype of polynomials of weight ≤ n(rho+eps) onto R/I^n is surjective for all large n, then every polynomial admits a representative modulo I^n of weight ≤ n(rho+eps) for all large n.

Preamble

import Mathlib.Algebra.MvPolynomial.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.RingTheory.Ideal.Quotient.Operations

open scoped BigOperators

Formal statement

theorem OAI.PiExponent.FormalInterpolation.eventual_weighted_generation_implies_eventual_surjective_weighted_sections
    {d : Nat} (I : Ideal (MvPolynomial (Fin d) Complex))
    (w : Fin d → Rat) (rho : Rat) (eps : Real)
    (hgen : ∃ N : Nat, ∀ n : Nat, N ≤ n →
      Function.Surjective
        (fun q : {q : MvPolynomial (Fin d) Complex //
              ∀ a ∈ q.support,
                ∑ i, (w i : Real) * (a i : Real) ≤
                  (n : Real) * ((rho : Real) + eps)} =>
          Ideal.Quotient.mk (I ^ n) q.1)) :
    ∃ N : Nat, ∀ n : Nat, N ≤ n →
      ∀ p : MvPolynomial (Fin d) Complex,
        ∃ q : MvPolynomial (Fin d) Complex,
          p - q ∈ I ^ n ∧
          ∀ a ∈ q.support,
            ∑ i, (w i : Real) * (a i : Real) ≤
              (n : Real) * ((rho : Real) + eps) := by sorry

Source

Unpacking Function.Surjective of Ideal.Quotient.mk on the weighted subtype.

View graph