Polynomials and limits

In this file we prove the following lemmas.

• Polynomial.continuous_eval₂: Polynomial.eval₂ defines a continuous function.
• Polynomial.continuous_aeval: Polynomial.aeval defines a continuous function; we also prove convenience lemmas Polynomial.continuousAt_aeval, Polynomial.continuousWithinAt_aeval, Polynomial.continuousOn_aeval.
• Polynomial.continuous: Polynomial.eval defines a continuous functions; we also prove convenience lemmas Polynomial.continuousAt, Polynomial.continuousWithinAt, Polynomial.continuousOn.
• Polynomial.tendsto_norm_atTop: fun x ↦ ‖Polynomial.eval (z x) p‖ tends to infinity provided that fun x ↦ ‖z x‖ tends to infinity and 0 < degree p;
• Polynomial.tendsto_abv_eval₂_atTop, Polynomial.tendsto_abv_atTop, Polynomial.tendsto_abv_aeval_atTop: a few versions of the previous statement for IsAbsoluteValue abv instead of norm.

Tags

Polynomial, continuity

theorem Polynomial.continuous_eval₂ {R : Type u_1} {S : Type u_2} [Semiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [Semiring S] (p : Polynomial S) (f : S →+* R) : Continuous fun (x : R) => eval₂ f x p

theorem Polynomial.continuous {R : Type u_1} [Semiring R] [TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R) : Continuous fun (x : R) => eval x p

theorem Polynomial.continuousAt {R : Type u_1} [Semiring R] [TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R) {a : R} : ContinuousAt (fun (x : R) => eval x p) a

theorem Polynomial.continuousWithinAt {R : Type u_1} [Semiring R] [TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R) {s : Set R} {a : R} : ContinuousWithinAt (fun (x : R) => eval x p) s a

theorem Polynomial.continuousOn {R : Type u_1} [Semiring R] [TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R) {s : Set R} : ContinuousOn (fun (x : R) => eval x p) s

theorem Polynomial.continuous_aeval {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalSemiring A] (p : Polynomial R) : Continuous fun (x : A) => (aeval x) p

theorem Polynomial.continuousAt_aeval {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalSemiring A] (p : Polynomial R) {a : A} : ContinuousAt (fun (x : A) => (aeval x) p) a

theorem Polynomial.continuousWithinAt_aeval {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalSemiring A] (p : Polynomial R) {s : Set A} {a : A} : ContinuousWithinAt (fun (x : A) => (aeval x) p) s a

theorem Polynomial.continuousOn_aeval {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalSemiring A] (p : Polynomial R) {s : Set A} : ContinuousOn (fun (x : A) => (aeval x) p) s

theorem Polynomial.tendsto_abv_eval₂_atTop {R : Type u_1} {S : Type u_2} {k : Type u_3} {α : Type u_4} [Semiring R] [Ring S] [Field k] [LinearOrder k] [IsStrictOrderedRing k] (f : R →+* S) (abv : S → k) [IsAbsoluteValue abv] (p : Polynomial R) (hd : 0 < p.degree) (hf : f p.leadingCoeff ≠ 0) {l : Filter α} {z : α → S} (hz : Filter.Tendsto (abv ∘ z) l Filter.atTop) : Filter.Tendsto (fun (x : α) => abv (eval₂ f (z x) p)) l Filter.atTop

theorem Polynomial.tendsto_abv_atTop {R : Type u_1} {k : Type u_2} {α : Type u_3} [Ring R] [Field k] [LinearOrder k] [IsStrictOrderedRing k] (abv : R → k) [IsAbsoluteValue abv] (p : Polynomial R) (h : 0 < p.degree) {l : Filter α} {z : α → R} (hz : Filter.Tendsto (abv ∘ z) l Filter.atTop) : Filter.Tendsto (fun (x : α) => abv (eval (z x) p)) l Filter.atTop

theorem Polynomial.tendsto_abv_aeval_atTop {R : Type u_1} {A : Type u_2} {k : Type u_3} {α : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [Field k] [LinearOrder k] [IsStrictOrderedRing k] (abv : A → k) [IsAbsoluteValue abv] (p : Polynomial R) (hd : 0 < p.degree) (h₀ : (algebraMap R A) p.leadingCoeff ≠ 0) {l : Filter α} {z : α → A} (hz : Filter.Tendsto (abv ∘ z) l Filter.atTop) : Filter.Tendsto (fun (x : α) => abv ((aeval (z x)) p)) l Filter.atTop

theorem Polynomial.tendsto_norm_atTop {α : Type u_1} {R : Type u_2} [NormedRing R] [IsAbsoluteValue norm] (p : Polynomial R) (h : 0 < p.degree) {l : Filter α} {z : α → R} (hz : Filter.Tendsto (fun (x : α) => ‖z x‖) l Filter.atTop) : Filter.Tendsto (fun (x : α) => ‖eval (z x) p‖) l Filter.atTop

theorem Polynomial.exists_forall_norm_le {R : Type u_2} [NormedRing R] [IsAbsoluteValue norm] [ProperSpace R] (p : Polynomial R) : ∃ (x : R), ∀ (y : R), ‖eval x p‖ ≤ ‖eval y p‖

theorem Polynomial.eq_one_of_roots_le {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {p : Polynomial F} {f : F →+* K} {B : ℝ} (hB : B < 0) (h1 : p.Monic) (h2 : Splits f p) (h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B) : p = 1

theorem Polynomial.coeff_le_of_roots_le {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {p : Polynomial F} {f : F →+* K} {B : ℝ} (i : ℕ) (h1 : p.Monic) (h2 : Splits f p) (h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B) : ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)

theorem Polynomial.coeff_bdd_of_roots_le {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {B : ℝ} {d : ℕ} (f : F →+* K) {p : Polynomial F} (h1 : p.Monic) (h2 : Splits f p) (h3 : p.natDegree ≤ d) (h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B) (i : ℕ) : ‖(map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))

The coefficients of the monic polynomials of bounded degree with bounded roots are uniformly bounded.