Module

PolynomialRootProximity.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PolynomialRootProximity

2 declarations indexed from sourceView source ↗

Module documentation

A root-proximity estimate over a discrete valuation ring

If a monic polynomial splits over a discrete valuation ring, one of its roots is at least as close to a given point as the polynomial value, after accounting for the derivative at that root. The proof selects a root of maximal additive valuation and compares the remaining factors by the ultrametric inequality.

Repeated roots and zero derivative values are allowed; the statement is in ℕ∞, so the estimate also covers infinite additive valuations.

Imports3

Mathlib.Algebra.Polynomial.Splits
Mathlib.Data.Finset.Max
Mathlib.RingTheory.DiscreteValuationRing.Basic

Imported by3

theorem

addVal_multiset_prod_le

L34 ↗

Polynomial.Splits.addVal_multiset_prod_le

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
universe u
namespace Polynomial.Splits

Lean source · statement

theorem addVal_multiset_prod_le
    {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {α : Type*} (s : Multiset α) (f g : α → R)
    (h :
      ∀ z ∈ s,
        IsDiscreteValuationRing.addVal R (f z) ≤
          IsDiscreteValuationRing.addVal R (g z)) :
    IsDiscreteValuationRing.addVal R ((s.map f).prod) ≤
      IsDiscreteValuationRing.addVal R ((s.map g).prod)

theorem

exists_root_addVal_eval_le_sub_add_derivative

L64 ↗

Polynomial.Splits.exists_root_addVal_eval_le_sub_add_derivative

Documentation

Let p be a nonconstant monic polynomial that splits over a discrete valuation ring. For every x, some root y satisfies

v(p(x)) ≤ v(x - y) + v(p'(y)).

Choosing y with maximal v(x-y) makes every other factor x-z no deeper than y-z; multiplying those inequalities gives the result.