How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Inverse function theorem for Banach spaces
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let , be real Banach spaces, let be open, let be of class with (C k map between Banach spaces), and let . If is a bounded linear isomorphism — that is, is bijective and its inverse is bounded — then there are open sets with and with such that is a bijection and its inverse is of class , with
Facts & Assumptions
Given: AC, real Banach spaces , an open , , a map with , and a bounded linear isomorphism .
means the recursive operator-norm condition of C k map between Banach spaces: is , its -st derivative exists as a differentiable map, and is continuous; in particular is continuous and every differentiable map is continuous.
Mean value estimate: on an open convex set, a differentiable map whose derivative is bounded by on a segment is -Lipschitz along that segment (Banach mean value estimate on a convex set); applied under AC.
A contraction of a nonempty complete metric space has exactly one fixed point in it (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).
Neumann series: if then is invertible with , and if is invertible with then is invertible with and (Neumann series and small perturbations of bounded inverses).
Chain rule and its linear special case: a bounded linear map equals its own derivative at every point, so , and the derivative of a composite of differentiable maps is the composite of the derivatives (Chain sum product and composition rules for Banach derivatives).
Operator norm and composition: and (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Composition satisfies |ST|\le|S|,|T|); a Banach space is complete (Banach space).
A closed subset of a complete metric space is complete in the subspace metric (Closed subspaces of complete metric spaces are complete; the converse under countable choice, claim 2, in ZF); a closed ball is a closed subset of , being (Open ball, closed ball and sphere in a metric space).
is characterised by the - remainder estimate of the Fréchet derivative (Fréchet derivative between Banach spaces).
Proof
(Affine changes of variable preserve the class.) Let be of class on an open set, let be a translation, and let . Then is of class with , and is of class with , for every : by [L5] the first derivatives are and , and the induction step differentiates these identities, the derivative of the translation being the identity and that of the bounded linear postcomposition being itself, with by [L6] ensuring continuity of the resulting expressions.
If , then the isomorphism forces and the theorem is immediate with and ; hence assume , so . Since is continuous at by [L1], choose such that and Put . Then , and on . Thus is invertible there by [L4], with .
Put on ; by [L5], , so , , and is of class by [step 1.1]. Put also on ; then , so for every .
For their segment lies in , so [L2] applied to on the open convex set gives . Since , also . In particular, is injective on .
Fix and define on . For one has because , so [step 3.1] yields ; thus maps into , and it is a contraction with constant by [step 3.1]. By [L7] the closed ball is a nonempty complete metric space, so [L3] gives a unique fixed point of , and is equivalent to ; hence has exactly one preimage under in .
The set is open and contains , and is a bijection with inverse : it is injective by [step 3.1], and surjective by [step 4.1], which for each produces with . Moreover is Lipschitz with constant : [step 3.1] gives .
For put ; by [step 1.2] and [L4] the operator is invertible with . Let be small with and put , so that by [step 5.1] and with by [L8]; applying gives , and , which is ; hence is differentiable at with .
The derivative formula of [step 6.1] is continuous in : the map is continuous because is continuous by [L1] and [step 2.1] and is continuous by [step 5.1]; inversion is continuous at each invertible operator, since for the bound from [L4] and [L6] tends to with . Hence is of class .
(Higher regularity.) Inversion is of class on the open set of invertible operators in : for , [L4] gives with , whence ; that formula is continuous in by [L4] and [L6], and iterating the expansion differentiates it again, so is for every . Now let and let be of class ; then is of class by [L1] and by [step 6.1] and [L5]. If is of class for some with , then , a composite of maps, is of class and hence is of class ; the case is [step 7.1], so induction gives of class .
Transfer to : by [step 5.1] the set is an open neighbourhood of contained in , and is an open neighbourhood of ; the restriction is a bijection onto with inverse , which is of class by [step 1.1] and [step 8.1] as a composite of the bounded linear map and the map .
For the map equals the identity near , so the chain rule [L5] differentiates it to ; multiplying on the right by gives , which is the displayed derivative formula for the statement's inverse , here the map of [step 9.1].
Depends on
C k map between Banach spaces
Banach mean value estimate on a convex set
A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point
Neumann series and small perturbations of bounded inverses
The Axiom of Choice
Fréchet derivative between Banach spaces
Open ball, closed ball and sphere in a metric space
Closed subspaces of complete metric spaces are complete; the converse under countable choice
Banach space
Composition satisfies |ST|\le|S|,|T|
The operator norm as the least bound and as the unit-sphere or unit-ball supremum
Chain sum product and composition rules for Banach derivatives