nLab real polynomial function

Contents

Context

Algebra

Analysis

Contents

Definition

A real polynomial function is a polynomial function in the real numbers, a function f:f:\mathbb{R} \to \mathbb{R} with a natural number nn \in \mathbb{N} and a list of length nn of real numbers a:[0,n) a:[0, n)_\mathbb{N} \to \mathbb{R} which satisfy one of these conditions:

  • for all xRx \in R,

    f(x)= i:[0,n) a(i)x if(x) = \sum_{i:[0, n)_\mathbb{N}} a(i) \cdot x^i

    where x ix^i is the ii-th power function for multiplication.

  • ff is a solution to the nn-th order linear homogeneous ordinary differential equation

    d nfdx n=0\frac{d^n f}{d x^n} = 0

    with initial conditions

    d ifdx i(0)=i!a(i)\frac{d^i f}{d x^i}(0) = i! \cdot a(i)

    for each natural number i:[0,n) i:[0, n)_\mathbb{N}

Properties

Degree

The degree of a real polynomial function is defined as the maximum natural number i<ni \lt n such that |a i|>0\vert a_i \vert \gt 0. In constructive mathematics, there exist real polynomial functions for which one cannot prove that a particular natural number i<ni \lt n is the degree of the real polynomial function: i.e. the function sub- \mathbb{R} -algebra of real polynomial functions is not a Euclidean domain.

Pointwise continuity

Given a real polynomial function f:f:\mathbb{R} \to \mathbb{R}, ff is a pointwise continuous function with respect to its metric topology defined through the absolute value function, subtraction, and its strict linear order.

Pointwise differentiability

Given a real polynomial function f:f:\mathbb{R} \to \mathbb{R}, ff is a pointwise differentiable function with respect to its metric topology defined through the absolute value function, subtraction, and its strict linear order.

Smoothness

Every real polynomial function is a smooth function. This could be shown coinductively: A smooth function is a pointwise differentiable function whose derivative is also smooth, and thus the nn-th derivative of a smooth function is a smooth function. The zero function f(x)=0f(x) = 0 is a smooth function, every real polynomial function is a pointwise differentiable function and the nn-th derivative of a polynomial function, with a natural number nn \in \mathbb{R} and a list of length nn of real numbers a:[0,n) a:[0, n)_\mathbb{N} \to \mathbb{R} such that one of the two conditions above is satisfied, is the zero function. Thus, every polynomial function is a smooth function.

See also

References

The proof of pointwise continuity using epsilontic analysis is spelled out for instance in

  • Kyle Miller, Polynomials are continuous functions, 2014 (pdf)

See also:

Created on June 2, 2022 at 07:41:10. See the history of this page for a list of all contributions to it.