mathlib documentation

topology.algebra.polynomial

Polynomials and limits

In this file we prove the following lemmas.

Tags

polynomial, 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)

theorem polynomial.continuous {R : Type u_1} [semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) :
continuous (λ (x : R), polynomial.eval x p)

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

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} :

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

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)

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

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} :

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 norm] (p : polynomial R) (h : 0 < p.degree) {l : filter α} {z : α → R} (hz : filter.tendsto (λ (x : α), z x) l filter.at_top) :