LemmaStatement: AI-adaptedProof: 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.

On a small cube, a $C^1$ diffeomorphism distorts Jordan content by factors arbitrarily close to its linearized absolute determinant

Statement

Let $n\ge1$ , let $g:U\to\mathbb R^n$ be $C^1$ on an open set, let $a\in U$ , and suppose $A=Dg(a)$ is invertible. For every $0<\varepsilon<1$ there is a closed cube $Q$ centred at $a$ , of positive radius and contained in $U$ , such that every Jordan set $E\subseteq Q$ has Jordan image and $|\det Dg(a)|(1-\varepsilon)^n\operatorname{cont}(E)\le \operatorname{cont}(g(E))\le |\det Dg(a)|(1+\varepsilon)^n\operatorname{cont}(E).$ The cube may be chosen inside any prescribed neighborhood of $a$ .

Facts & Assumptions

Given: The $C^1$ map, the point $a$ , invertible $A=Dg(a)$ , and $0<\varepsilon<1$ .

[L1]

A linear endomorphism maps Jordan sets to Jordan sets and scales content by its absolute determinant (A linear endomorphism of $\mathbb R^n$ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant).

[L2]

A map whose derivative is uniformly close enough to the identity sandwiches each sufficiently small cube between concentric contracted and expanded cubes (A $C^1$ map uniformly close to the identity derivative sandwiches a cube between contracted and expanded cubes).

[L3]

Jordan inner and outer content approximate Jordan sets by finite rectangular figures (Jordan inner and outer content and Jordan measurable bounded sets in $\mathbb{R}^m$ ).

[L4]

A derivative bound on a convex open set gives a 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$ ); an everywhere-invertible derivative gives local $C^1$ inverses (The Euclidean inverse function theorem); Lipschitz self-maps preserve null sets (A Lipschitz map $\mathbb{R}^m\to\mathbb{R}^m$ sends null sets to null sets); and bounded sets are Jordan exactly when their boundaries are null (A bounded set in $\mathbb{R}^m$ is Jordan measurable iff its boundary is null, equivalently of content zero).

[L5]

Jordan content is finitely additive across Jordan pieces whose overlaps have content zero (Jordan content is finitely additive when the overlap has content zero).

Proof

technique · reduction

1.1

Normalize at $a$ by the affine map $H(x)=a+A^{-1}(g(x)-g(a)).$ Choose $0<q<\varepsilon$ and a slightly larger cube inside $U$ on which $\|D H-I\|_{2\to2}\le q/\sqrt n$ . The mean-value bound in [L4] makes $H-I$ a $q$ -contraction in the sup norm, so $H$ is injective and bi-Lipschitz there. The derivative bound also makes every $DH$ invertible; the inverse function theorem in [L4] therefore makes $H$ a homeomorphism on a neighborhood of the smaller positive-radius cube $Q$ . Here $H(a)=a$ and $DH(a)=I$ ; continuity of $Dg$ permits the stated choice inside any prescribed neighborhood.

L4given

2.1

If $E\subseteq Q$ is Jordan, the homeomorphism in step 1.1 gives $\partial H(E)=H(\partial E)$ . Compose $H$ on the larger cube with coordinatewise clamping onto that cube to obtain a global Lipschitz map. Since $\partial E$ is null, [L4] makes $H(\partial E)$ null and hence makes $H(E)$ Jordan.

L4step 1.1

3.1

Refine inner and outer figures from [L3] into finite unions of sufficiently small, interior-disjoint cubes $P\subseteq E\subseteq R$ with arbitrarily small content gap. After translating at each cube centre, [L2] sandwiches its $H$ -image between cubes with factors $(1-q)^n$ and $(1+q)^n$ . Step 2.1 makes those images Jordan, injectivity makes their interiors disjoint, and [L5] adds their contents. Letting the figure gap vanish gives the stronger bounds with $q$ ; since $q<\varepsilon$ , these imply the displayed bounds for $H(E)$ . Finally $g(E)=g(a)+A(H(E)-a)$ , so [L1] multiplies every content by $|\det A|=|\det Dg(a)|$ .

L1L2L3L5step 1.1step 2.1∎

Depends on

Used by

Change of variables for an injective C¹ map on a compact Jordan set Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 199 results over 27 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.6 and Theorem 5.5.7 (standard reference, not scraped)

On a small cube, a C1C^1C1 diffeomorphism distorts Jordan content by factors arbitrarily close to its linearized absolute determinant