Documentation

Mathlib.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] [TopologicalSpace R] [TopologicalSemiring R] [Semiring S] (p : Polynomial S) (f : S →+* R) :
Continuous fun (x : R) => Polynomial.eval₂ f x p
theorem Polynomial.continuousAt {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : Polynomial R) {a : R} :
ContinuousAt (fun (x : R) => Polynomial.eval x p) a
theorem Polynomial.continuousWithinAt {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : Polynomial R) {s : Set R} {a : R} :
ContinuousWithinAt (fun (x : R) => Polynomial.eval x p) s a
theorem Polynomial.continuousOn {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : Polynomial R) {s : Set R} :
ContinuousOn (fun (x : R) => Polynomial.eval x p) s
theorem Polynomial.continuousAt_aeval {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [TopologicalSemiring A] (p : Polynomial R) {a : A} :
ContinuousAt (fun (x : A) => (Polynomial.aeval x) p) a
theorem Polynomial.continuousWithinAt_aeval {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [TopologicalSemiring A] (p : Polynomial R) {s : Set A} {a : A} :
ContinuousWithinAt (fun (x : A) => (Polynomial.aeval x) p) s a
theorem Polynomial.continuousOn_aeval {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [TopologicalSemiring A] (p : Polynomial R) {s : Set A} :
ContinuousOn (fun (x : A) => (Polynomial.aeval x) p) s
theorem Polynomial.tendsto_abv_eval₂_atTop {R : Type u_1} {S : Type u_2} {k : Type u_3} {α : Type u_4} [Semiring R] [Ring S] [LinearOrderedField k] (f : R →+* S) (abv : Sk) [IsAbsoluteValue abv] (p : Polynomial R) (hd : 0 < p.degree) (hf : f p.leadingCoeff 0) {l : Filter α} {z : αS} (hz : Filter.Tendsto (abv z) l Filter.atTop) :
Filter.Tendsto (fun (x : α) => abv (Polynomial.eval₂ f (z x) p)) l Filter.atTop
theorem Polynomial.tendsto_abv_atTop {R : Type u_1} {k : Type u_2} {α : Type u_3} [Ring R] [LinearOrderedField k] (abv : Rk) [IsAbsoluteValue abv] (p : Polynomial R) (h : 0 < p.degree) {l : Filter α} {z : αR} (hz : Filter.Tendsto (abv z) l Filter.atTop) :
Filter.Tendsto (fun (x : α) => abv (Polynomial.eval (z x) p)) l Filter.atTop
theorem Polynomial.tendsto_abv_aeval_atTop {R : Type u_1} {A : Type u_2} {k : Type u_3} {α : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [LinearOrderedField k] (abv : Ak) [IsAbsoluteValue abv] (p : Polynomial R) (hd : 0 < p.degree) (h₀ : (algebraMap R A) p.leadingCoeff 0) {l : Filter α} {z : αA} (hz : Filter.Tendsto (abv z) l Filter.atTop) :
Filter.Tendsto (fun (x : α) => abv ((Polynomial.aeval (z x)) p)) l Filter.atTop
theorem Polynomial.tendsto_norm_atTop {α : Type u_1} {R : Type u_2} [NormedRing R] [IsAbsoluteValue norm] (p : Polynomial R) (h : 0 < p.degree) {l : Filter α} {z : αR} (hz : Filter.Tendsto (fun (x : α) => z x) l Filter.atTop) :
Filter.Tendsto (fun (x : α) => Polynomial.eval (z x) p) l Filter.atTop
theorem Polynomial.eq_one_of_roots_le {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {p : Polynomial F} {f : F →+* K} {B : } (hB : B < 0) (h1 : p.Monic) (h2 : Polynomial.Splits f p) (h3 : 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} [CommRing F] [NormedField K] {p : Polynomial F} {f : F →+* K} {B : } (i : ) (h1 : p.Monic) (h2 : Polynomial.Splits f p) (h3 : z(Polynomial.map f p).roots, z B) :
(Polynomial.map f p).coeff i B ^ (p.natDegree - i) * (p.natDegree.choose i)
theorem Polynomial.coeff_bdd_of_roots_le {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {B : } {d : } (f : F →+* K) {p : Polynomial F} (h1 : p.Monic) (h2 : Polynomial.Splits f p) (h3 : p.natDegree d) (h4 : z(Polynomial.map f p).roots, z B) (i : ) :
(Polynomial.map f p).coeff i max B 1 ^ d * (d.choose (d / 2))

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