LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

A $C^1$ map uniformly close to the identity derivative sandwiches a cube between contracted and expanded cubes

Statement

Let $n\ge1$ , let $C(a,r)=\{x:\|x-a\|_\infty\le r\}$ with $r>0$ , let $W\subseteq\mathbb R^n$ be convex and open with $C(a,r)\subseteq W$ , and let $F:W\to\mathbb R^n$ be $C^1$ . Assume $F(a)=a$ and, for some $0\le q<1$ , $\|(DF(z)-I)v\|_2\le \frac q{\sqrt n}\|v\|_2$ for every $z\in W$ and $v\in\mathbb R^n$ . Then $C(a,(1-q)r)\subseteq F(C(a,r))\subseteq C(a,(1+q)r).$ Moreover, $F$ is injective on $C(a,r)$ .

Facts & Assumptions

Given: The cube, the $C^1$ map, and the strict derivative error bound in the statement.

[L1]

A uniform bound on total derivatives over a convex open set gives the corresponding Euclidean Lipschitz bound (On a convex open set, a uniform bound $\|Df(z)v\|_2\le M\|v\|_2$ implies $\|f(y)-f(x)\|_2\le M\|y-x\|_2$ ).

[L2]

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

[L3]

Euclidean space is complete and every closed subspace of a complete metric space is complete ( $\mathbb{R}$ and $\mathbb{R}^n$ for $n \ge 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $\mathbb{R}$ , A subspace of a complete metric space is complete iff it is closed, and a complete subspace of any metric space is closed).

[L4]

The Euclidean and sup norms satisfy $\|w\|_\infty\le\|w\|_2\le\sqrt n\|w\|_\infty$ (Each $\lVert\cdot\rVert_p$ is a norm on $\mathbb{R}^n$ , and the induced metrics are exactly $d_1$ , $d_2$ and $d_\infty$ of the published metric-spaces page).

Proof

technique · fixed-point

1.1

L1L4given

2.1

Fix $z\in C(a,(1-q)r)$ and define $S_z(x)=z-R(x)$ . Step 1.1 gives $S_z(C(a,r))\subseteq C(a,r)$ and makes $S_z$ a $q$ -contraction. The cube is a nonempty closed subset of complete Euclidean space, so [L2]--[L3] give $x\in C(a,r)$ with $S_z(x)=x$ , equivalently $F(x)=z$ . This proves the inner containment.

L2L3step 1.1

3.1

If $F(x)=F(y)$ , then $x-y=R(y)-R(x)$ , so step 1.1 gives $\|x-y\|_\infty\le q\|x-y\|_\infty$ . Since $q<1$ , $x=y$ . The assumptions $r>0$ and $q<1$ are essential to the nondegenerate fixed-point argument.

step 1.1algebra∎

Depends on

Used by

On a small cube, a C¹ diffeomorphism distorts Jordan content by factors arbitrarily close to its linearized absolute determinant Lemma

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 176 results over 33 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

A. Leibman, Multidimensional Real Analysis, Lemma 5.5.5 (standard reference, not scraped)

A C1C^1C1 map uniformly close to the identity derivative sandwiches a cube between contracted and expanded cubes