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
…
…
synthetic differential geometry
Introductions
from point-set topology to differentiable manifolds
geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry
Differentials
Tangency
The magic algebraic facts
Theorems
Axiomatics
Models
differential equations, variational calculus
Chern-Weil theory, ∞-Chern-Weil theory
Cartan geometry (super, higher)
The inverse function theorem says that given any sequentially Cauchy complete Archimedean field and a continuously differentiable function from an open interval such that for all points ,
the inverse function exists and is unique and is defined by the first-order nonlinear ordinary differential equation
with initial condition . Classically, is essentially unique, but constructively, there are multiple inequivalent sequentially Cauchy complete Archimedean fields.
To be done…
This proof is adapted from the Wikipedia article on the inverse function theorem, in the section “A proof using the contraction mapping principle”, the contraction mapping principle being another name for the Banach fixed-point theorem.
Let denote an open interval in with radius and centre . If is a map such that and there exists a rational constant such that for all and , then is injective on and
where is the identity map on the real numbers, restricted in the domain to , and given an open interval , is the image of under .
First, the map is injective on , since if , then and so , which is a contradiction unless . Next we show
The idea is to note that this is equivalent to, given a point in , find a fixed point of the map
defined as where such that and the bar means a closed ball. To find a fixed point, we use the Banach fixed-point theorem and checking that is a well-defined strict-contraction mapping is straightforward. Finally, we have:
since
Now that we have established the lemma, we could proved the main theorem:
It is enough to prove the special case when and . Let . The mean value theorem applied to says:
Since and is continuous, we can find an such that
for all in . Then the earlier lemma says that is injective on and . Then
is bijective and thus has the inverse, where given an open interval , is the inverse image of over .
to be continued…
The given proof of the inverse function theorem above relies on the mean value theorem, which in constructive mathematics is only true for uniformly differentiable functions. There might be other proofs which might not rely on the mean value theorem and could prove the inverse function theorem for continuously differentiable functions.
While continuously differentiable functions and locally uniformly differentiable functions are well-defined in every Archimedean ordered field, the inverse function theorem does not hold in all Archimedean ordered fields. One could instead consider adding the inverse function theorem as an axiom to an arbitrary Archimedean ordered field . There are a few axioms which could be used here
For any Archimedean ordered field , the continuously differentiable inverse function axiom for states that given any differentiable function on an open subinterval such that its derivative is pointwise continuous and always apart from zero, there is a unique differentiable function called the inverse function with pointwise continuous derivative such that and for all elements and
For any Archimedean ordered field , the locally uniformly differentiable inverse function axiom for states that given any differentiable function on an open subinterval such that its derivative is locally uniformly continuous and always apart from zero, there is a unique differentiable function called the inverse function with locally uniformly continuous derivative such that and for all elements and
The former is stronger than the latter, although they are equivalent in the presence of excluded middle. If satisfies the locally uniformly continuous inverse function axiom, then is a real closed field.
There is also a third possible axiom in dependent type theory, which uses the shape modality. Given an Archimedean ordered field , let be the shape modality, the localization at . A type is shapewise contractible if its shape is contractible. Given an open interval , a function is shapewise continuous if the graph of , the set of all pairs in such that , is shapewise contractible:
See also:
Last revised on December 14, 2022 at 18:22:29. See the history of this page for a list of all contributions to it.