LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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 \geq 1$ , let $C (a, r) = {x : ∥ x - a ∥_{\infty} \leq r}$ with $r > 0$ , let $W \subseteq R^{n}$ be convex and open with $C (a, r) \subseteq W$ , and let $F : W \to R^{n}$ be $C^{1}$ . Assume $F (a) = a$ and, for some $0 \leq q < 1$ , $∥ (D F (z) - I) v ∥_{2} \leq \frac{q}{\sqrt{n}} ∥ v ∥_{2}$ for every $z \in W$ and $v \in 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 $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq 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 ( $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ , Closed subspaces of complete metric spaces are complete; the converse under countable choice).

[L4]

The Euclidean and sup norms satisfy $∥ w ∥_{\infty} \leq ∥ w ∥_{2} \leq \sqrt{n} ∥ w ∥_{\infty}$ (Each $∥ \cdot ∥_{p}$ is a norm on $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

Put $R = F - I$ and use [L1] with the Euclidean--sup norm comparison [L4] to obtain the contraction estimate $∥ R (x) - R (y) ∥_{\infty} \leq q ∥ x - y ∥_{\infty}$ on the cube. In particular $∥ R (x) ∥_{\infty} \leq q r$ , so $F (x) = x + R (x)$ lies in $C (a, (1 + q) r)$ .

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} \leq 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 · two levels

67 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

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

A C1C1 map uniformly close to the identity derivative sandwiches a cube between contracted and expanded cubes