Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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 X, Y be real Banach spaces, let U⊆X be open, let f:U→Y be of class Ck with k≥1 (C k map between Banach spaces), and let a∈U. If Df(a):X→Y is a bounded linear isomorphism — that is, Df(a) is bijective and its inverse Df(a)−1:Y→X is bounded — then there are open sets U0⊆U with a∈U0 and V0⊆Y with f(a)∈V0 such that f∣U0:U0→V0 is a bijection and its inverse g:=(f∣U0)−1:V0→U0 is of class Ck, with

Dg(f(x))=Df(x)−1for every x∈U0.

Facts & Assumptions

Given: AC, real Banach spaces X,Y, an open U⊆X, a∈U, a Ck map f:U→Y with k≥1, and a bounded linear isomorphism A:=Df(a):X→Y.

[L1]

Ck means the recursive operator-norm condition of C k map between Banach spaces: f is Ck−1, its (k−1)-st derivative exists as a differentiable map, and Dkf is continuous; in particular Df is continuous and every differentiable map is continuous.

[L2]

Mean value estimate: on an open convex set, a differentiable map whose derivative is bounded by M on a segment is M-Lipschitz along that segment (Banach mean value estimate on a convex set); applied under AC.

[L4]

Neumann series: if ∥R∥<1 then I−R is invertible with ∥(I−R)−1∥≤(1−∥R∥)−1, and if A is invertible with ∥A−1E∥<1 then A+E is invertible with (A+E)−1=(I+A−1E)−1A−1 and ∥(A+E)−1∥≤∥A−1∥(1−∥A−1E∥)−1 (Neumann series and small perturbations of bounded inverses).

[L5]

Chain rule and its linear special case: a bounded linear map equals its own derivative at every point, so D(L∘F)(x)=L∘DF(x), and the derivative of a composite of differentiable maps is the composite of the derivatives (Chain sum product and composition rules for Banach derivatives).

[L6]

Operator norm and composition: ∥Tu∥≤∥T∥ ∥u∥ and ∥ST∥≤∥S∥ ∥T∥ (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).

[L7]

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 Bˉ(a,r) is a closed subset of X, being {x:∥x−a∥≤r} (Open ball, closed ball and sphere in a metric space).

[L8]

DΦ(x) is characterised by the ε-δ remainder estimate of the Fréchet derivative (Fréchet derivative between Banach spaces).

Proof

technique · direct
1.1L1L5L6algebra

(Affine changes of variable preserve the class.) Let F be of class Ck on an open set, let τ(x)=x0+x be a translation, and let L∈B(Y,Z). Then F∘τ is of class Ck with Dj(F∘τ)(x)=DjF(τ(x)), and L∘F is of class Ck with Dj(L∘F)(x)=L∘DjF(x), for every j≤k: by [L5] the first derivatives are D(F∘τ)(x)=DF(τ(x)) and D(L∘F)(x)=L∘DF(x), and the induction step differentiates these identities, the derivative of the translation being the identity and that of the bounded linear postcomposition S↦L∘S being itself, with ∥L∘S∥≤∥L∥ ∥S∥ by [L6] ensuring continuity of the resulting expressions.

1.2L1L4L6choose

If X={0}, then the isomorphism A:X→Y forces Y={0} and the theorem is immediate with U0=U={0} and V0=Y; hence assume X≠{0}, so ∥A−1∥>0. Since Df is continuous at a by [L1], choose ρ>0 such that B(a,ρ)⊆U and ∥Df(x)−A∥<12∥A−1∥(x∈B(a,ρ)). Put r:=ρ/3. Then Bˉ(a,r)⊆B(a,2r)⊆B(a,ρ)⊆U, and ∥A−1(Df(x)−A)∥≤12 on B(a,2r). Thus Df(x) is invertible there by [L4], with ∥Df(x)−1∥≤2∥A−1∥.

2.1step 1.2L1L5L6algebra

Put Φ:=A−1∘f on U; by [L5], DΦ(x)=A−1∘Df(x), so Φ(a)=A−1f(a)=:b, DΦ(a)=IX, and Φ is of class Ck by [step 1.1]. Put also Ψ(x):=x−Φ(x) on B(a,2r); then DΨ(x)=IX−A−1Df(x)=−A−1(Df(x)−A), so ∥DΨ(x)∥≤∥A−1∥ ∥Df(x)−A∥<12 for every x∈B(a,2r).

3.1step 1.2step 2.1L2algebra

For x,z∈Bˉ(a,r) their segment lies in Bˉ(a,r)⊂B(a,2r), so [L2] applied to Ψ on the open convex set B(a,2r) gives ∥Ψ(x)−Ψ(z)∥≤12∥x−z∥. Since Φ(x)−Φ(z)=(x−z)−(Ψ(x)−Ψ(z)), also ∥Φ(x)−Φ(z)∥≥12∥x−z∥. In particular, Φ is injective on B(a,r).

4.1step 3.1L3L7algebra

Fix y∈B(b,r/4) and define Ty(x):=y+x−Φ(x)=y+Ψ(x) on Bˉ(a,r). For x∈Bˉ(a,r) one has Ty(x)−a=(y−b)+Ψ(x)−Ψ(a) because a−Φ(a)=Ψ(a), so [step 3.1] yields ∥Ty(x)−a∥≤∥y−b∥+12∥x−a∥<r4+r2<r; thus Ty maps Bˉ(a,r) into B(a,r), and it is a contraction with constant 12 by [step 3.1]. By [L7] the closed ball is a nonempty complete metric space, so [L3] gives a unique fixed point g(y)∈B(a,r) of Ty, and Ty(x)=x is equivalent to Φ(x)=y; hence y has exactly one preimage under Φ in B(a,r).

5.1step 3.1step 4.1L1algebra

The set W:=B(a,r)∩Φ−1(B(b,r/4)) is open and contains a, and Φ∣W:W→B(b,r/4) is a bijection with inverse g: it is injective by [step 3.1], and surjective by [step 4.1], which for each y∈B(b,r/4) produces g(y)∈B(a,r) with Φ(g(y))=y. Moreover g is Lipschitz with constant 2: [step 3.1] gives ∥g(y)−g(z)∥≤∥Φ(g(y))−Φ(g(z))−(g(y)−g(z))∥+∥y−z∥≤12∥g(y)−g(z)∥+∥y−z∥.

6.1step 1.2step 5.1L4L6L8algebra

For y∈B(b,r/4) put x:=g(y); by [step 1.2] and [L4] the operator DΦ(x) is invertible with ∥DΦ(x)−1∥≤2. Let h be small with y+h∈B(b,r/4) and put k:=g(y+h)−g(y), so that ∥k∥≤2∥h∥ by [step 5.1] and h=Φ(x+k)−Φ(x)=DΦ(x)k+rΦ(k) with ∥rΦ(k)∥=o(∥k∥) by [L8]; applying DΦ(x)−1 gives k−DΦ(x)−1h=−DΦ(x)−1rΦ(k), and ∥DΦ(x)−1rΦ(k)∥≤2∥rΦ(k)∥, which is o(∥k∥)=o(∥h∥); hence g is differentiable at y with Dg(y)=DΦ(x)−1=Df(g(y))−1A.

7.1step 5.1step 6.1L1L4L6algebra

The derivative formula of [step 6.1] is continuous in y: the map y↦DΦ(g(y)) is continuous because DΦ is continuous by [L1] and [step 2.1] and g is continuous by [step 5.1]; inversion is continuous at each invertible operator, since for ∥A−1E∥≤12 the bound ∥(A+E)−1−A−1∥≤∥(A+E)−1∥ ∥E∥ ∥A−1∥≤2∥A−1∥2∥E∥ from [L4] and [L6] tends to 0 with ∥E∥. Hence g is of class C1.

8.1step 7.1L1L4L5L6

(Higher regularity.) Inversion inv(A):=A−1 is of class C∞ on the open set of invertible operators in B(X): for ∥A−1H∥<1, [L4] gives (A+H)−1=A−1−A−1HA−1+R(H) with ∥R(H)∥≤∥A−1∥3∥H∥21−∥A−1H∥, whence D inv(A)H=−A−1HA−1; that formula is continuous in A by [L4] and [L6], and iterating the expansion differentiates it again, so inv is Cr for every r. Now let k≥2 and let Φ be of class Ck; then DΦ is of class Ck−1 by [L1] and Dg=inv∘DΦ∘g by [step 6.1] and [L5]. If g is of class Cj−1 for some j with 2≤j≤k, then Dg, a composite of Cj−1 maps, is of class Cj−1 and hence g is of class Cj; the case j=1 is [step 7.1], so induction gives g of class Ck.

9.1step 5.1step 1.1step 8.1L6algebra

Transfer to f: by [step 5.1] the set U0:=W is an open neighbourhood of a contained in U, and V0:=f[U0]=A[Φ[W]]=A[B(b,r/4)] is an open neighbourhood of f(a); the restriction f∣U0 is a bijection onto V0 with inverse F(y):=g(A−1y), which is of class Ck by [step 1.1] and [step 8.1] as a composite of the bounded linear map A−1 and the Ck map g.

10.1step 9.1step 5.1L5algebra∎

For x∈U0 the map F∘f equals the identity near x, so the chain rule [L5] differentiates it to DF(f(x)) Df(x)=IX; multiplying on the right by Df(x)−1 gives DF(f(x))=Df(x)−1, which is the displayed derivative formula for the statement's inverse g, here the map F of [step 9.1].

Depends on

Dependency tree · 2 levels

Sources