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 lemmas
polynomial.continuous_at_aeval,
polynomial.continuous_within_at_aeval,
polynomial.continuous_on_aeval`.polynomial.continuous
:polynomial.eval
defines a continuous functions; we also prove convenience lemmaspolynomial.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 and0 < 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 foris_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]
[topological_space R]
[topological_semiring R]
[semiring S]
(p : polynomial S)
(f : S →+* R) :
continuous (λ (x : R), polynomial.eval₂ f x p)
@[protected, continuity]
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)
@[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} :
continuous_within_at (λ (x : R), polynomial.eval x p) s a
@[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} :
continuous_within_at (λ (x : A), ⇑(polynomial.aeval x) p) s 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) :
filter.tendsto (λ (x : α), ∥polynomial.eval (z x) p∥) l filter.at_top
theorem
polynomial.exists_forall_norm_le
{R : Type u_2}
[normed_ring R]
[is_absolute_value has_norm.norm]
[proper_space R]
(p : polynomial R) :
∃ (x : R), ∀ (y : R), ∥polynomial.eval x p∥ ≤ ∥polynomial.eval y p∥
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 : polynomial.splits f p)
(h3 : ∀ (z : K), z ∈ (polynomial.map f p).roots → ∥z∥ ≤ B) :
∥(polynomial.map f p).coeff i∥ ≤ B ^ (p.nat_degree - i) * ↑(p.nat_degree.choose i)