Approximate roots and polynomials in a normed field

In this file, we prove several approximation lemmas on a normed field.

Main results

• Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_lt : Continuity of Roots. Let f and g be two monic polynomials such that g splits. If the coefficients of two polynomials f and g are sufficiently close, then every root of f has a corresponding root of g nearby.

• Polynomial.exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt : Let K be a dense subfield of a normed field L. Every monic polynomial in L can be approximated by a monic polynomial in K of the same degree.

TODO

Use the fact that f.discr is polynomial of the coefficients of f to show that every polynomial f can be approximated by a separable polynomial. This result can be used to show that the completion a separably closed field is algebraically closed, upgrading the current theorem IsAlgClosed.of_denseRange.

Tags

Approximation, polynomial, normed field, continuity of roots

theorem Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_lt {K : Type u_1} [NormedField K] {f g : Polynomial K} {ε : ℝ} (hε : 0 < ε) {a : K} (ha : eval a f = 0) (hfm : f.Monic) (hgm : g.Monic) (hdeg : g.natDegree = f.natDegree) (hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε) (hg : g.Splits) : ∃ b ∈ g.roots, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1

Continuity of Roots. Let f and g be two monic polynomials with g splits. If the coefficients of two polynomials f and g are sufficiently close, then every root of f has a corresponding root of g nearby.

theorem Polynomial.exists_aroots_norm_sub_lt_of_norm_coeff_sub_lt {K : Type u_1} {L : Type u_2} [NormedField K] [NormedField L] [NormedAlgebra K L] {f g : Polynomial K} {ε : ℝ} (hε : 0 < ε) {a : L} (ha : (aeval a) f = 0) (hfm : f.Monic) (hgm : g.Monic) (hdeg : g.natDegree = f.natDegree) (hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε) (hg : (map (algebraMap K L) g).Splits) : ∃ b ∈ g.aroots L, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1

Continuity of Roots. A variation of Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_lt allowing roots of g lives in a field extension.

theorem Polynomial.exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt {K : Type u_1} {L : Type u_2} [Field K] [NormedField L] [Algebra K L] (hd : DenseRange ⇑(algebraMap K L)) {f : Polynomial L} (hf : f.Monic) {ε : ℝ} (hε : ε > 0) : ∃ (g : Polynomial K), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖(map (algebraMap K L) g).coeff n - f.coeff n‖ < ε

If K is a dense subfield of L, then every monic polynomial in L can be approximated by a monic polynomial in K of the same degree.