Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

The Banach inverse theorem for a small Lipschitz perturbation of the identity

Example

Assume the Axiom of Choice (The Axiom of Choice). Let X be a real Banach space (Banach space) and let g:X→X be Lipschitz with constant q and 0≤q<1 (Lipschitz map, α-Hölder map for rational 0<α≤1, and contraction). Then F:=IX+g is bijective and its inverse is Lipschitz with constant at most (1−q)−1. If in addition g is of class Ck for some k≥1 (C k map between Banach spaces), then F is a global Ck diffeomorphism of X onto X.

Facts & Assumptions

Given: AC, a real Banach space X, a Lipschitz map g:X→X with constant q∈[0,1), and F:=IX+g.

[L1]

Lipschitz with constant q: ∥g(u)−g(v)∥≤q∥u−v∥ for all u,v (Lipschitz map, α-Hölder map for rational 0<α≤1, and contraction).

[L2]

A contraction of a nonempty complete metric space has a unique fixed point; a Banach space is a nonempty complete metric space (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point, Banach space).

[L3]

Neumann: ∥R∥<1 implies I−R invertible with ∥(I−R)−1∥≤(1−∥R∥)−1 (Neumann series and small perturbations of bounded inverses).

[L4]

A derivative is a norm limit of difference quotients, so a global Lipschitz constant q bounds the derivative by q wherever it exists (Fréchet derivative between Banach spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[L5]

Sum rule D(IX+g)(x)=IX+Dg(x), Ck-ness of IX+g for a Ck map g, and the inverse function theorem for Ck maps between Banach spaces, k≥1 (Chain sum product and composition rules for Banach derivatives, C k map between Banach spaces, Inverse function theorem for Banach spaces).

Verification

technique · direct
1.1L1L2

Fix y∈X and put Ty(x):=y−g(x). Then ∥Ty(x)−Ty(x′)∥=∥g(x′)−g(x)∥≤q∥x−x′∥ by [L1], so Ty is a contraction of the nonempty complete metric space X; by [L2] it has exactly one fixed point, and x=Ty(x) is equivalent to F(x)=y.

2.1step 1.1L1algebra

Consequently F is bijective with F−1(y) the unique fixed point of Ty for each y. If xi:=F−1(yi) for i=1,2, then ∥x1−x2∥=∥(y1−y2)−(g(x1)−g(x2))∥≤∥y1−y2∥+q∥x1−x2∥, hence ∥F−1(y1)−F−1(y2)∥≤(1−q)−1∥y1−y2∥ because 1−q>0.

2.2step 1.1L3L4L5algebra

Now assume g is of class Ck with k≥1; then F is of class Ck and DF(x)=IX+Dg(x) by [L5]. The derivative of g satisfies ∥Dg(x)∥≤q by [L4], so ∥−Dg(x)∥≤q<1 and [L3] makes DF(x)=IX−(−Dg(x)) invertible with ∥DF(x)−1∥≤(1−q)−1 at every x.

3.1step 2.1step 2.2L5algebra

By the inverse function theorem [L5] applied at each x, and using that F is a bijection by [step 2.1], the global inverse F−1 agrees near each y with the Ck local inverse of F; being locally of class Ck, F−1 is of class Ck. Hence F is a global Ck diffeomorphism.

4.1step 2.1step 2.2step 3.1∎

Steps 2.1, 2.2 and 3.1 prove all the assertions of the example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources