# mathlibdocumentation

topology.algebra.polynomial

# Polynomials and limits #

In this file we prove the following lemmas.

• polynomial.continuous_eval₂:polynomial.eval₂ defines a continuous function.
• polynomial.continuous_aeval:polynomial.aevaldefines a continuous function; we also prove convenience lemmaspolynomial.continuous_at_aeval,polynomial.continuous_within_at_aeval,polynomial.continuous_on_aeval.
• polynomial.continuous: polynomial.eval defines a continuous functions; we also prove convenience lemmas polynomial.continuous_at, polynomial.continuous_within_at, polynomial.continuous_on.
• polynomial.tendsto_norm_at_top: λ x, ∥polynomial.eval (z x) p∥ tends to infinity provided that λ x, ∥z x∥ tends to infinity and 0 < degree p;
• polynomial.tendsto_abv_eval₂_at_top, polynomial.tendsto_abv_at_top, polynomial.tendsto_abv_aeval_at_top: a few versions of the previous statement for is_absolute_value abv instead of norm.

## Tags #

polynomial, continuity

@[protected, continuity]
theorem polynomial.continuous_eval₂ {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (p : polynomial S) (f : S →+* R) :
continuous (λ (x : R), p)
@[protected, continuity]
theorem polynomial.continuous {R : Type u_1} [semiring R] (p : polynomial R) :
continuous (λ (x : R), p)
@[protected]
theorem polynomial.continuous_at {R : Type u_1} [semiring R] (p : polynomial R) {a : R} :
continuous_at (λ (x : R), p) a
@[protected]
theorem polynomial.continuous_within_at {R : Type u_1} [semiring R] (p : polynomial R) {s : set R} {a : R} :
continuous_within_at (λ (x : R), p) s a
@[protected]
theorem polynomial.continuous_on {R : Type u_1} [semiring R] (p : polynomial R) {s : set R} :
continuous_on (λ (x : R), p) s
@[protected, continuity]
theorem polynomial.continuous_aeval {R : Type u_1} {A : Type u_2} [semiring A] [ A] (p : polynomial R) :
continuous (λ (x : A), p)
@[protected]
theorem polynomial.continuous_at_aeval {R : Type u_1} {A : Type u_2} [semiring A] [ A] (p : polynomial R) {a : A} :
continuous_at (λ (x : A), p) a
@[protected]
theorem polynomial.continuous_within_at_aeval {R : Type u_1} {A : Type u_2} [semiring A] [ A] (p : polynomial R) {s : set A} {a : A} :
continuous_within_at (λ (x : A), p) s a
@[protected]
theorem polynomial.continuous_on_aeval {R : Type u_1} {A : Type u_2} [semiring A] [ A] (p : polynomial R) {s : set A} :
continuous_on (λ (x : A), p) s
theorem polynomial.tendsto_abv_eval₂_at_top {R : Type u_1} {S : Type u_2} {k : Type u_3} {α : Type u_4} [semiring R] [ring S] (f : R →+* S) (abv : S → k) [is_absolute_value abv] (p : polynomial R) (hd : 0 < p.degree) (hf : f p.leading_coeff 0) {l : filter α} {z : α → S} (hz : filter.tendsto (abv z) l filter.at_top) :
filter.tendsto (λ (x : α), abv (z x) p)) l filter.at_top
theorem polynomial.tendsto_abv_at_top {R : Type u_1} {k : Type u_2} {α : Type u_3} [ring R] (abv : R → k) [is_absolute_value abv] (p : polynomial R) (h : 0 < p.degree) {l : filter α} {z : α → R} (hz : filter.tendsto (abv z) l filter.at_top) :
filter.tendsto (λ (x : α), abv (polynomial.eval (z x) p)) l filter.at_top
theorem polynomial.tendsto_abv_aeval_at_top {R : Type u_1} {A : Type u_2} {k : Type u_3} {α : Type u_4} [ring A] [ A] (abv : A → k) [is_absolute_value abv] (p : polynomial R) (hd : 0 < p.degree) (h₀ : A) p.leading_coeff 0) {l : filter α} {z : α → A} (hz : filter.tendsto (abv z) l filter.at_top) :
filter.tendsto (λ (x : α), abv ((polynomial.aeval (z x)) p)) l filter.at_top
theorem polynomial.tendsto_norm_at_top {α : Type u_1} {R : Type u_2} [normed_ring R] (p : polynomial R) (h : 0 < p.degree) {l : filter α} {z : α → R} (hz : filter.tendsto (λ (x : α), z x) l filter.at_top) :
theorem polynomial.exists_forall_norm_le {R : Type u_2} [normed_ring R] [proper_space R] (p : polynomial R) :
∃ (x : R), ∀ (y : R),
theorem polynomial.coeff_le_of_roots_le {F : Type u_3} {K : Type u_4} [field F] [normed_field K] {p : polynomial F} {f : F →+* K} {B : } (i : ) (h1 : p.monic) (h2 : p) (h3 : ∀ (z : K), z p).rootsz B) :