Analytic tools for the Nullstellensatz: density of non-zeros, polynomial evaluation, roots

Three general facts about convergent power series used by the proof of Rückert's Nullstellensatz (Nullstellensatz.lean), none specific to it; they rest on Mathlib's identity theorem and on elementary estimates:

• the open polydisc is convex, and a nonzero convergent series takes a nonzero value on every nonempty open subset of its polydisc of convergence (exists_evalSeries_ne_zero_of_isOpen), the fact behind the "dense subset of a small neighbourhood of 0" in the proof of [Fre17, Ch. I, 5.1] and the negligible set of [Fre17, Ch. I, §9]: the identity theorem AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero on the connected polydisc plus the uniqueness of coefficients in the form Conv.ext_of_evalSeries_eventuallyEq (Subst.lean);
• near 0, evalSeries of a finite sum is the sum of the values (evalSeries_finsetSum_eventually), and convPolyEval Q, the series of a polynomial Q ∈ 𝒪_m[x_0], evaluates as the polynomial ∑_k Q_k(x') x_0^k (evalSeries_convPolyEval_eventually);
• a root of a monic polynomial over K whose lower coefficients have total norm < ε^d (ε ≤ 1) has norm < ε (norm_root_lt_of_monic): the continuity of the zeros of a Weierstrass polynomial, used repeatedly in [Fre17, Ch. I, 5.1, 8.1, 8.2], in the quantitative form the proofs need.

The polydisc is convex; a nonzero series does not vanish on any open subset

theorem Analytic.zero_mem_polydisc {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius m) : 0 ∈ polydisc K ρ

The origin lies in every open polydisc.

theorem Analytic.convex_polydisc {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius m) : Convex ℝ (polydisc K ρ)

The open polydisc {x | ∀ k, ‖x k‖ < ρ k} is convex (hence connected).

theorem Analytic.exists_evalSeries_ne_zero_of_isOpen {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) (hf0 : f ≠ 0) {V : Set (Fin m → K)} (hV : IsOpen V) (hVne : V.Nonempty) (hVρ : V ⊆ polydisc K ρ) : ∃ y ∈ V, evalSeries f y ≠ 0

A nonzero convergent series takes a nonzero value on every nonempty open subset of its polydisc of convergence (the identity theorem on the connected polydisc).

Evaluation of finite sums and of convPolyEval near 0

theorem Analytic.evalSeries_finsetSum_eventually {K : Type u_1} [RCLike K] {n : ℕ} {ι : Type u_2} (s : Finset ι) (F : ι → ↥(Conv K n)) : evalSeries (∑ i ∈ s, ↑(F i)) =ᶠ[nhds 0] fun (x : Fin n → K) => ∑ i ∈ s, evalSeries (↑(F i)) x

Near 0, the value of a finite sum of convergent series is the sum of the values (each summand converges on a neighbourhood of 0).

theorem Analytic.evalSeries_convPolyEval_eventually {K : Type u_1} [RCLike K] {m : ℕ} (Q : Polynomial ↥(Conv K m)) : evalSeries ↑((convPolyEval K) Q) =ᶠ[nhds 0] fun (x : Fin (m + 1) → K) => ∑ k ∈ Finset.range (Q.natDegree + 1), evalSeries (↑(Q.coeff k)) (Fin.tail x) * x 0 ^ k

Near 0, convPolyEval Q evaluates as the polynomial ∑ Q_k(x') x_0^k in the first coordinate with the coefficients evaluated at the tail.

Roots of a monic polynomial with small coefficients are small

theorem Analytic.norm_root_lt_of_monic {K : Type u_1} [RCLike K] {p : Polynomial K} (hp : p.Monic) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hsmall : ∑ i ∈ Finset.range p.natDegree, ‖p.coeff i‖ < ε ^ p.natDegree) {t : K} (ht : Polynomial.eval t p = 0) : ‖t‖ < ε

Continuity of roots at a Weierstrass polynomial, in the form used: a root t of a monic polynomial of degree d ≥ 1 whose lower coefficients have total norm < ε ^ d (with ε ≤ 1) satisfies ‖t‖ < ε.