nLab real polynomial function

Redirected from "real polynomial functions are pointwise continuous".
Contents

Context

Algebra

Analysis

Contents

Definition

Without scalar coefficients

A real polynomial function is a polynomial function in the real numbers, a function f:f:\mathbb{R} \to \mathbb{R} such that

  • ff is in the image of the function j: *()j:\mathbb{R}^* \to (\mathbb{R} \to \mathbb{R}) from the free monoid *\mathbb{R}^* on \mathbb{R}, i.e. the set of lists of real numbers, to the function algebra \mathbb{R} \to \mathbb{R}, such that

    • j(ϵ)=0j(\epsilon) = 0, where 00 is the zero function.
    • for all a *a \in \mathbb{R}^* and b *b \in \mathbb{R}^*, j(ab)=j(a)+j(b)() len(a)j(a b) = j(a) + j(b) \cdot (-)^{\mathrm{len}(a)}, where () n(-)^n is the nn-th power function for nn \in \mathbb{N}
    • for all rr \in \mathbb{R}, j(r)=c rj(r) = c_r, where c rc_r is the constant function whose value is always rr.
  • ff is in the image of the canonical ring homomorphism i:[x]()i:\mathbb{R}[x] \to (\mathbb{R} \to \mathbb{R}) from the real polynomial ring in one indeterminant [x]\mathbb{R}[x] to the function algebra \mathbb{R} \to \mathbb{R}, which takes constant polynomials in [x]\mathbb{R}[x] to constant functions in \mathbb{R} \to \mathbb{R} and the indeterminant xx in [x]\mathbb{R}[x] to the identity function id \mathrm{id}_\mathbb{R} in \mathbb{R} \to \mathbb{R}

  • There exists a natural number nn such that the nn-th order derivative of ff is equal to the zero function:

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

With scalar coefficients

A real polynomial function is 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

Without scalar coefficients

Given a non-zero real polynomial function f:f:\mathbb{R} \to \mathbb{R}, the degree of ff is the maximum natural number nn where the nn-th derivative of ff is not the zero-function:

deg(f)max n,d nfdx n0(n)\mathrm{deg}(f) \coloneqq \max_{n \in \mathbb{N}, \frac{d^{n} f}{d x^{n}} \neq 0}(n)

With scalar coefficients

The degree of a real polynomial function, with additional data of 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}, 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

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 total 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 total 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:

Last revised on August 21, 2024 at 01:52:29. See the history of this page for a list of all contributions to it.