Constructions relating polynomial functions and continuous functions. #

Main definitions #

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

Instances For

    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].)

    Instances For
      theorem Polynomial.aeval_continuousMap_apply {R : Type u_1} {α : Type u_2} [TopologicalSpace α] [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (g : Polynomial R) (f : C(α, R)) (x : α) :
      ↑(↑(Polynomial.aeval f) g) x = Polynomial.eval (f x) g
      theorem Polynomial.toContinuousMapAlgHom_apply {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : Polynomial R) :
      Polynomial.toContinuousMapAlgHom p = Polynomial.toContinuousMap p

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

      Instances For

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

        Instances For
          noncomputable def polynomialFunctions {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (X : Set R) :

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

          Instances For

            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.le_equalizer {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (s : Set R) (φ : C(s, R) →ₐ[R] A) (ψ : C(s, R) →ₐ[R] A) (h : φ (↑(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ (↑(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)) :