mathlib3 documentation

topology.algebra.polynomial

Polynomials and limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove the following lemmas.

Tags #

polynomial, continuity

@[protected, continuity]
theorem polynomial.continuous_eval₂ {R : Type u_1} {S : Type u_2} [semiring R] [topological_space R] [topological_semiring R] [semiring S] (p : polynomial S) (f : S →+* R) :
continuous (λ (x : R), polynomial.eval₂ f x p)
@[protected, continuity]
@[protected]
theorem polynomial.continuous_at {R : Type u_1} [semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) {a : R} :
continuous_at (λ (x : R), polynomial.eval x p) a
@[protected]
theorem polynomial.continuous_within_at {R : Type u_1} [semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) {s : set R} {a : R} :
@[protected]
theorem polynomial.continuous_on {R : Type u_1} [semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) {s : set R} :
continuous_on (λ (x : R), polynomial.eval x p) s
@[protected, continuity]
theorem polynomial.continuous_aeval {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] [topological_space A] [topological_semiring A] (p : polynomial R) :
continuous (λ (x : A), (polynomial.aeval x) p)
@[protected]
theorem polynomial.continuous_at_aeval {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] [topological_space A] [topological_semiring A] (p : polynomial R) {a : A} :
continuous_at (λ (x : A), (polynomial.aeval x) p) a
@[protected]
theorem polynomial.continuous_within_at_aeval {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] [topological_space A] [topological_semiring A] (p : polynomial R) {s : set A} {a : A} :
@[protected]
theorem polynomial.continuous_on_aeval {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] [topological_space A] [topological_semiring A] (p : polynomial R) {s : set A} :
continuous_on (λ (x : A), (polynomial.aeval x) 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] [linear_ordered_field k] (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 (polynomial.eval₂ f (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] [linear_ordered_field k] (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} [comm_semiring R] [ring A] [algebra R A] [linear_ordered_field k] (abv : A k) [is_absolute_value abv] (p : polynomial R) (hd : 0 < p.degree) (h₀ : (algebra_map R 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] [is_absolute_value has_norm.norm] (p : polynomial R) (h : 0 < p.degree) {l : filter α} {z : α R} (hz : filter.tendsto (λ (x : α), z x) l filter.at_top) :
theorem polynomial.eq_one_of_roots_le {F : Type u_3} {K : Type u_4} [comm_ring F] [normed_field K] {p : polynomial F} {f : F →+* K} {B : } (hB : B < 0) (h1 : p.monic) (h2 : polynomial.splits f p) (h3 : (z : K), z (polynomial.map f p).roots z B) :
p = 1
theorem polynomial.coeff_le_of_roots_le {F : Type u_3} {K : Type u_4} [comm_ring F] [normed_field K] {p : polynomial F} {f : F →+* K} {B : } (i : ) (h1 : p.monic) (h2 : polynomial.splits f p) (h3 : (z : K), z (polynomial.map f p).roots z B) :
theorem polynomial.coeff_bdd_of_roots_le {F : Type u_3} {K : Type u_4} [comm_ring F] [normed_field K] {B : } {d : } (f : F →+* K) {p : polynomial F} (h1 : p.monic) (h2 : polynomial.splits f p) (h3 : p.nat_degree d) (h4 : (z : K), z (polynomial.map f p).roots z B) (i : ) :

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