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.
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.evaldefines 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 abvinstead 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.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) :
‖(polynomial.map f p).coeff i‖ ≤ B ^ (p.nat_degree - i) * ↑(p.nat_degree.choose i)
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.