# Constructions relating polynomial functions and continuous functions. #

## Main definitions #

• Polynomial.toContinuousMapOn p X: for X : Set R, interprets a polynomial p as a bundled continuous function in C(X, R).
• Polynomial.toContinuousMapOnAlgHom: the same, as an R-algebra homomorphism.
• polynomialFunctions (X : Set R) : Subalgebra R C(X, R): polynomial functions as a subalgebra.
• polynomialFunctions_separatesPoints (X : Set R) : (polynomialFunctions X).SeparatesPoints: the polynomial functions separate points.
@[simp]
theorem Polynomial.toContinuousMap_apply {R : Type u_1} [] [] (p : ) (x : R) :
p.toContinuousMap x =
def Polynomial.toContinuousMap {R : Type u_1} [] [] (p : ) :
C(R, R)

Every polynomial with coefficients in a topological semiring gives a (bundled) continuous function.

Equations
• p.toContinuousMap = { toFun := fun (x : R) => , continuous_toFun := }
Instances For
theorem Polynomial.toContinuousMap_X_eq_id {R : Type u_1} [] [] :
Polynomial.X.toContinuousMap =
@[simp]
theorem Polynomial.toContinuousMapOn_apply {R : Type u_1} [] [] (p : ) (X : Set R) (x : X) :
(p.toContinuousMapOn X) x = p.toContinuousMap x
def Polynomial.toContinuousMapOn {R : Type u_1} [] [] (p : ) (X : Set R) :
C(X, R)

A polynomial as a continuous function, with domain restricted to some subset of the semiring of coefficients.

(This is particularly useful when restricting to compact sets, e.g. [0,1].)

Equations
• p.toContinuousMapOn X = { toFun := fun (x : X) => p.toContinuousMap x, continuous_toFun := }
Instances For
theorem Polynomial.toContinuousMapOn_X_eq_restrict_id {R : Type u_1} [] [] (s : Set R) :
Polynomial.X.toContinuousMapOn s =
@[simp]
theorem Polynomial.aeval_continuousMap_apply {R : Type u_1} {α : Type u_2} [] [] [] (g : ) (f : C(α, R)) (x : α) :
(() g) x = Polynomial.eval (f x) g
@[simp]
theorem Polynomial.toContinuousMapAlgHom_apply {R : Type u_1} [] [] (p : ) :
Polynomial.toContinuousMapAlgHom p = p.toContinuousMap

The algebra map from R[X] to continuous functions C(R, R).

Equations
• Polynomial.toContinuousMapAlgHom = { toFun := fun (p : ) => p.toContinuousMap, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem Polynomial.toContinuousMapOnAlgHom_apply {R : Type u_1} [] [] (X : Set R) (p : ) :
= p.toContinuousMapOn X
def Polynomial.toContinuousMapOnAlgHom {R : Type u_1} [] [] (X : Set R) :
→ₐ[R] C(X, R)

The algebra map from R[X] to continuous functions C(X, R), for any subset X of R.

Equations
• = { toFun := fun (p : ) => p.toContinuousMapOn X, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
noncomputable def polynomialFunctions {R : Type u_1} [] [] (X : Set R) :

The subalgebra of polynomial functions in C(X, R), for X a subset of some topological semiring R.

Equations
Instances For
@[simp]
theorem polynomialFunctions_coe {R : Type u_1} [] [] (X : Set R) :
theorem polynomialFunctions_separatesPoints {R : Type u_1} [] [] (X : Set R) :
.SeparatesPoints

The preimage of polynomials on [0,1] under the pullback map by x ↦ (b-a) * x + a is the polynomials on [a,b].

theorem polynomialFunctions.eq_adjoin_X {R : Type u_1} [] [] (s : Set R) :