analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
In real analysis, the notion of lifting a function from the real numbers to some sequentially Cauchy complete pseudometric space of real numbers equipped with computational structure. The pseudometric space comes with a function whose image is the Cauchy real numbers. The computational structures which can be used for lifting functions include
Cauchy sequences of rational numbers, with modulus of continuity or defined constructively using the BHK interpretation,
base signed-digit representations, for a given natural number greater than .
Let be a sequentially Cauchy complete Archimedean ordered field, and let
be the set of all pairs of real numbers and locators, with canonical projection function . This projection function is not an injection because in general a real number may have more than one locator; however, the image of this projection function is the Cauchy real numbers , which is a subset of and thus does have an injection into . A function lifts to locators if it comes with a function such that the following square in Set commutes:
Let be a sequentially Cauchy complete Archimedean ordered field, and let
be the set consisting of a real number and a Cauchy sequence of rational numbers constructively converging to the real number, in the sense of the BHK interpretation, with canonical function . A function lifts to Cauchy sequences of rational numbers if it comes with a function such that the following square in Set commutes:
Alternatively, one can define the set directly as the set of Cauchy sequences of rational numbers, defined constructively using the BHK interpretation
Quotienting by a suitable equivalence relation - there are many different options available used in the constructive analysis literature, yields the Cauchy real numbers with a quotient map , and the Cauchy real numbers embed into any sequentially Cauchy complete Archimedean ordered field , with unique ring homomorphism , yielding a function . A function lifts to Cauchy sequences of rational numbers if it comes with a function such that the following square in Set commutes:
The field operations on lifts to locators or Cauchy sequences of rational numbers
Hence, any real polynomial function or rational function lifts to locators or Cauchy sequences of rational numbers.
Given any convergent sequence of functions such that each lifts to locators or Cauchy sequences of rational numbers, then the limit function lifts to locators or Cauchy sequences of rational numbers, since for each real number equipped with a locator or Cauchy sequence of real numbers, the limit of the pointwise sequence also comes with a locator or Cauchy sequence of real numbers.
Hence, any smooth function or analytic function lifts to locators or Cauchy sequences of rational numbers.
The absolute value, minimum and maximum lattice operations, real square root, and more generally real -th root partial functions all lift to locators or Cauchy sequences of rational numbers. These (partial) functions aren’t smooth at , but can nevertheless be defined as the limit of a convergent sequence of functions.
Auke Booij, Extensional constructive real analysis via locators, (abs:1805.06781)
Auke Booij, Analysis in univalent type theory (2020) etheses:10411, pdf
Last revised on July 19, 2024 at 17:04:57. See the history of this page for a list of all contributions to it.