LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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 local Sobolev chain rule for C^1 postcomposition

Statement

Assume Countable Choice. Let $U, V \subseteq C$ be open, let $u : U \to V$ be continuous and belong to $W_{l o c}^{1, 2} (U; C)$ , and let $G : V \to C$ be $C^{1}$ as a map of real planes. Then $G \circ u \in W_{l o c}^{1, 2} (U; C)$ and its real weak derivative satisfies $D (G \circ u) = D G (u) D u almost everywhere on U .$

Facts & Assumptions

Given: Countable Choice; open sets $U, V \subseteq C$ ; a continuous map $u : U \to V$ in $W_{l o c}^{1, 2} (U; C)$ ; and a real- $C^{1}$ map $G : V \to C$ .

[F1]

The $W^{1, 2}$ class and its weak derivative are as in Integer-order Sobolev spaces and their norms. For every open set $W \subseteq R^{2}$ and every $v \in W^{1, 2} (W; C)$ there are $v_{j} \in C^{\infty} (W; C) \cap W^{1, 2} (W; C)$ with $v_{j} \to v$ in $W^{1, 2}$ , by Meyers–Serrin density (Meyers–Serrin density on an arbitrary open set).

[F2]

If $K \subseteq V$ is compact, there is $χ \in C_{c}^{\infty} (V)$ equal to $1$ on a neighborhood of $K$ (Test function cutoffs and euclidean localization).

[F3]

An $L^{2}$ -convergent sequence has a subsequence of representatives converging almost everywhere under Countable Choice (Assuming Countable Choice, $L^{p}$ -convergent sequences have almost-everywhere convergent subsequences).

[F4]

If measurable functions converge almost everywhere and are dominated by an integrable function, their integrals converge (Dominated convergence).

[F5]

A $C^{1}$ function's classical first derivatives are its weak derivatives (Classical derivatives agree with weak derivatives).

[F6]

If functions and their proposed first weak derivatives converge locally in $L^{2}$ , the limits satisfy the same weak-derivative identities (Weak derivatives persist under local Lp limits).

[F7]

A real- $C^{1}$ map has a total derivative at each point ( $C^{k}$ maps and multi-index derivative notation in Euclidean space, If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative), and the classical derivative of a composition of differentiable maps is the product of their total derivatives (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F8]

Every bounded open subset of $R^{2}$ has finite Lebesgue measure under Countable Choice (Lebesgue measure is sigma-finite, and every metrically bounded subset of $R^{n}$ has finite outer measure).

[F9]

Countable Choice says that every countable family of nonempty sets has a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Choice use. Countable Choice is used through [F1], [F3], [F5] and [F6], and to interpret local Sobolev and measure classes. The cutoff is supplied by an explicit ZF construction. The proof uses no full Axiom of Choice.

Proof

technique · local smooth approximation and passage of the classical chain rule to weak derivatives

1.1F2given

Fix $U_{0} ⋐ U$ . Its closure is compact, so continuity gives a compact set $K : = u (\overline{U_{0}}) \subset V$ . By [F2] choose $χ \in C_{c}^{\infty} (V)$ equal to $1$ on a neighborhood of $K$ . Define $\tilde{G} = χ G$ on $V$ and extend it by $0$ to $C ∖ V$ . Since $χ$ has compact support in $V$ , $\tilde{G}$ is globally $C^{1}$ , bounded, and has bounded derivative, and it agrees with $G$ on a neighborhood of $K$ .

1.2F1F5F7F9given

The restriction $u ∣_{U_{0}}$ belongs to $W^{1, 2} (U_{0}; C)$ . By [F1] choose $u_{j} \in C^{\infty} (U_{0}; C)$ converging to it in $W^{1, 2} (U_{0})$ . Each $\tilde{G} \circ u_{j}$ is $C^{1}$ and its classical derivative is $D \tilde{G} (u_{j}) D u_{j}$ by [F7]; by [F5] this is also its weak derivative.

2.1F3F4F8F9step 1.1given

Since $u_{j} \to u$ in $L^{2} (U_{0})$ , [F3] gives a subsequence, still denoted $u_{j}$ , converging to $u$ almost everywhere. Thus $\tilde{G} (u_{j}) \to \tilde{G} (u)$ almost everywhere. The functions are uniformly bounded by $∥ \tilde{G} ∥_{\infty}$ , and $U_{0}$ has finite measure by [F8]; dominated convergence gives $\tilde{G} (u_{j}) \to \tilde{G} (u)$ in $L^{2} (U_{0})$ .

3.1F1F4F5step 1.2step 2.1

Continuity of $D \tilde{G}$ gives $D \tilde{G} (u_{j}) \to D \tilde{G} (u)$ almost everywhere along the subsequence of step 2.1, and these matrices are bounded by $M : = ∥ D \tilde{G} ∥_{\infty}$ . Write $D \tilde{G} (u_{j}) D u_{j} - D \tilde{G} (u) D u = D \tilde{G} (u_{j}) (D u_{j} - D u) + (D \tilde{G} (u_{j}) - D \tilde{G} (u)) D u .$ The first term tends to $0$ in $L^{2}$ because $D u_{j} \to D u$ in $L^{2}$ and the matrices have norm at most $M$ . The second tends to $0$ in $L^{2}$ by [F4], since it converges almost everywhere and its squared norm is bounded by $4 M^{2} ∣ D u ∣^{2} \in L^{1} (U_{0})$ . Therefore the weak derivatives of $\tilde{G} \circ u_{j}$ converge in $L^{2} (U_{0})$ to $D \tilde{G} (u) D u$ .

4.1F6step 1.1step 2.1step 3.1given∎

Apply [F6] to the function convergence in step 2.1 and the derivative convergence in step 3.1. It gives $\tilde{G} \circ u \in W^{1, 2} (U_{0})$ with weak derivative $D \tilde{G} (u) D u$ . Since $u (U_{0}) \subseteq K$ and $\tilde{G} = G$ on a neighborhood of $K$ , this is $G \circ u$ with derivative $D G (u) D u$ . As $U_{0} ⋐ U$ was arbitrary, the asserted local Sobolev membership and chain rule hold on $U$ . The empty-domain case is vacuous.

Depends on

Used by

Weak solutions of the Beltrami equation Definition

Dependency tree · two levels

73 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

Juha Kinnunen, Sobolev Spaces (2026) (standard reference, not scraped)