Polynomial.coeff_bdd_of_roots_le
theorem Polynomial.coeff_bdd_of_roots_le :
∀ {F : Type u_3} {K : Type u_4} [inst : CommRing F] [inst_1 : NormedField K] {B : ℝ} {d : ℕ} (f : F →+* K)
{p : Polynomial F},
p.Monic →
Polynomial.Splits f p →
p.natDegree ≤ d →
(∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) →
∀ (i : ℕ), ‖(Polynomial.map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
The theorem `Polynomial.coeff_bdd_of_roots_le` states that the coefficients of the monic polynomials, which have a bounded degree and bounded roots, are uniformly bounded. Given a ring homomorphism `f` from field `F` to a normed field `K`, a monic polynomial `p` of field `F` that splits (i.e., it is zero or all of its irreducible factors have degree 1), and a real number `B` and a natural number `d` such that the degree of `p` is less than or equal to `d` and all roots of `p` mapped with `f` are less than or equal to `B` in norm, then for every natural number `i`, the norm of the `i`-th coefficient of the polynomial obtained by mapping `p` with `f` is less than or equal to the maximum of `B` and 1 raised to the power `d` times the binomial coefficient "d choose (d/2)".
More concisely: Given a monic polynomial of degree d over a field with bounded roots in a normed field, the norms of its coefficients are bounded by the maximum of the root bound and the norm of 1 raised to d times the binomial coefficient d choose (d/2).
|
Polynomial.continuous_aeval
theorem Polynomial.continuous_aeval :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : TopologicalSpace A] [inst_4 : TopologicalSemiring A] (p : Polynomial R),
Continuous fun x => (Polynomial.aeval x) p
The theorem `Polynomial.continuous_aeval` states that for any given commutative semiring `R`, semiring `A`, algebra structure of `A` over `R`, topological space structure on `A`, and topological semiring structure on `A`, and any polynomial `p` with coefficients in `R`, the function that evaluates `p` at an element `x` of `A` using the algebra evaluation function `Polynomial.aeval` is a continuous function. In mathematical terms, this theorem guarantees the continuity of the function $f(x) = p(a)$ where $a \in A$ and $p$ is a polynomial in `R[X]` with the topology defined on `A`.
More concisely: The polynomial evaluation function `Polynomial.aeval` is continuous with respect to the given topological semiring structure on an algebra `A` over a commutative semiring `R`.
|
Polynomial.continuous
theorem Polynomial.continuous :
∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSemiring R]
(p : Polynomial R), Continuous fun x => Polynomial.eval x p
The theorem `Polynomial.continuous` states that for any semiring `R` with a topological structure, that is also a topological semiring, the evaluation function, `Polynomial.eval`, is continuous for any given polynomial `p` of type `Polynomial R`. This means that for any point `x` in the semiring, the values of `Polynomial.eval` for points close to `x` are close to the value of `Polynomial.eval` at `x`. This is a property required in mathematical analysis to ensure that the polynomial functions behave well under limits and continuity operations.
More concisely: For any topological semiring `R` and polynomial `p` over `R`, the evaluation function `Polynomial.eval p` is continuous.
|