# 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} [] [] [] (p : ) (f : S →+* R) :
Continuous fun (x : R) =>
theorem Polynomial.continuous {R : Type u_1} [] [] (p : ) :
Continuous fun (x : R) =>
theorem Polynomial.continuousAt {R : Type u_1} [] [] (p : ) {a : R} :
ContinuousAt (fun (x : R) => ) a
theorem Polynomial.continuousWithinAt {R : Type u_1} [] [] (p : ) {s : Set R} {a : R} :
ContinuousWithinAt (fun (x : R) => ) s a
theorem Polynomial.continuousOn {R : Type u_1} [] [] (p : ) {s : Set R} :
ContinuousOn (fun (x : R) => ) s
theorem Polynomial.continuous_aeval {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] [] (p : ) :
Continuous fun (x : A) => () p
theorem Polynomial.continuousAt_aeval {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] [] (p : ) {a : A} :
ContinuousAt (fun (x : A) => () p) a
theorem Polynomial.continuousWithinAt_aeval {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] [] (p : ) {s : Set A} {a : A} :
ContinuousWithinAt (fun (x : A) => () p) s a
theorem Polynomial.continuousOn_aeval {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] [] (p : ) {s : Set A} :
ContinuousOn (fun (x : A) => () p) s
theorem Polynomial.tendsto_abv_eval₂_atTop {R : Type u_1} {S : Type u_2} {k : Type u_3} {α : Type u_4} [] [Ring S] (f : R →+* S) (abv : Sk) [] (p : ) (hd : 0 < p.degree) (hf : f p.leadingCoeff 0) {l : } {z : αS} (hz : Filter.Tendsto (abv z) l Filter.atTop) :
Filter.Tendsto (fun (x : α) => abv (Polynomial.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] (abv : Rk) [] (p : ) (h : 0 < p.degree) {l : } {z : αR} (hz : Filter.Tendsto (abv z) l Filter.atTop) :
Filter.Tendsto (fun (x : α) => abv (Polynomial.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} [] [Ring A] [Algebra R A] (abv : Ak) [] (p : ) (hd : 0 < p.degree) (h₀ : () p.leadingCoeff 0) {l : } {z : αA} (hz : Filter.Tendsto (abv z) l Filter.atTop) :
Filter.Tendsto (fun (x : α) => abv ((Polynomial.aeval (z x)) p)) l Filter.atTop
theorem Polynomial.tendsto_norm_atTop {α : Type u_1} {R : Type u_2} [] [IsAbsoluteValue norm] (p : ) (h : 0 < p.degree) {l : } {z : αR} (hz : Filter.Tendsto (fun (x : α) => z x) l Filter.atTop) :
Filter.Tendsto (fun (x : α) => Polynomial.eval (z x) p) l Filter.atTop
theorem Polynomial.exists_forall_norm_le {R : Type u_2} [] [IsAbsoluteValue norm] [] (p : ) :
∃ (x : R), ∀ (y : R),
theorem Polynomial.eq_one_of_roots_le {F : Type u_3} {K : Type u_4} [] [] {p : } {f : F →+* K} {B : } (hB : B < 0) (h1 : p.Monic) (h2 : ) (h3 : z().roots, z B) :
p = 1
theorem Polynomial.coeff_le_of_roots_le {F : Type u_3} {K : Type u_4} [] [] {p : } {f : F →+* K} {B : } (i : ) (h1 : p.Monic) (h2 : ) (h3 : z().roots, z B) :
().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} [] [] {B : } {d : } (f : F →+* K) {p : } (h1 : p.Monic) (h2 : ) (h3 : p.natDegree d) (h4 : z().roots, z B) (i : ) :
().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.