LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

C^k boundary flattening preserves local W^{k,p}

Statement

Assume Countable Choice. Let $k \geq 1$ , $1 \leq p \leq \infty$ and $K \in {R, C}$ . Let $U, V \subseteq R^{n}$ be open and let $Φ : U \to V$ be a $C^{k}$ diffeomorphism with inverse $Ψ : = Φ^{- 1} : V \to U$ . Fix open sets $U_{0} \subset \subset U$ and $V_{0} \subset \subset V$ with $Φ (U_{0}) \subseteq V_{0}$ , and suppose that on $\overline{U_{0}}$ the derivatives of $Φ$ through order $k$ are bounded and that on $\overline{V_{0}}$ the derivatives of $Ψ$ through order $k$ are bounded; in the situation of Bounded C^k domains and boundary charts these are exactly the compact patches on which the flattening chart and its inverse have bounded derivatives through order $k$ . Then:

for every $u \in W^{k, p} (V_{0}; K)$ the composition $u \circ Φ$ belongs to $W^{k, p} (U_{0}; K)$ , and for every $1 \leq ∣ α ∣ \leq k$ its weak derivatives satisfy, almost everywhere on $U_{0}$ , $D^{α} (u \circ Φ) = \sum_{1 \leq ∣ β ∣ \leq ∣ α ∣} ((D^{β} u) \circ Φ) P_{α β} (D Φ, \dots, D^{k} Φ),$ where $P_{α β}$ is a universal polynomial with integer coefficients, whose values on $\overline{U_{0}}$ are bounded by a constant depending only on $n, k$ and the stated bounds for $Φ$ ;
there is a constant $C$ , depending only on $n$ , $k$ , $p$ and the two sets of chart bounds, with $∥ u \circ Φ ∥_{W^{k, p} (U_{0})} \leq C ∥ u ∥_{W^{k, p} (V_{0})} for all u \in W^{k, p} (V_{0}; K) .$ If in addition $Ψ (V_{0}) \subseteq U_{0}$ (equivalently, under the stated $Φ (U_{0}) \subseteq V_{0}$ , $Φ (U_{0}) = V_{0}$ ), the same assertion holds for composition with $Ψ$ from $W^{k, p} (U_{0})$ to $W^{k, p} (V_{0})$ .

For $k = 1$ only the first derivatives of $Φ$ and $Ψ$ enter, so bounded $C^{1}$ chart and inverse data suffice; no $C^{1}$ -only claim is made for $k > 1$ .

Facts & Assumptions

Given: Countable Choice; $k \geq 1$ ; $1 \leq p \leq \infty$ ; $K \in {R, C}$ ; the $C^{k}$ diffeomorphism $Φ : U \to V$ with inverse $Ψ$ ; open sets $U_{0} \subset \subset U$ , $V_{0} \subset \subset V$ with $Φ (U_{0}) \subseteq V_{0}$ ; and bounded derivatives through order $k$ of $Φ$ on $\overline{U_{0}}$ and of $Ψ$ on $\overline{V_{0}}$ .

[F1]

The flattening charts of Bounded C^k domains and boundary charts are built from a rigid motion and the graph function $h \in C^{k}$ and have Jacobian determinant $\det Q \in {- 1, 1}$ , hence absolute determinant $1$ ; only the coordinate shear has determinant $1$ ; their derivatives through order $k$ are bounded on every compactly contained patch, and this boundedness is exactly the hypothesis used below.

[F2]

$C^{1}$ change of variables: for a $C^{1}$ diffeomorphism $T : U^{'} \to V^{'}$ of open sets and every nonnegative measurable $f$ , $\int_{V^{'}} f (y) d y = \int_{U^{'}} f (T (x)) ∣ \det D T (x) ∣ d x$ (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

[F3]

A $C^{1}$ diffeomorphism maps Lebesgue null sets to Lebesgue null sets, so composition of almost-everywhere classes with $Φ$ or $Ψ$ is well defined independently of representatives (A C^1 diffeomorphism maps Lebesgue null sets to Lebesgue null sets).

[F4]

Chain rule: iterating The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ gives, for $u \in C^{k} (V; K)$ , the classical identity for $1 \leq ∣ α ∣ \leq k$ $D^{α} (u \circ Φ) (x) = \sum_{1 \leq ∣ β ∣ \leq ∣ α ∣} (D^{β} u) (Φ (x)) P_{α β} (x)$ , where $P_{α β} (x)$ is a universal integer-coefficient polynomial in the partial derivatives $D^{γ} Φ (x)$ , $1 \leq ∣ γ ∣ \leq ∣ α ∣$ , and in particular $∣ P_{α β} (x) ∣ \leq C_{α}$ on $\overline{U_{0}}$ with $C_{α}$ determined by the bounds on $Φ$ ; for $k = 1$ this is $D_{i} (u \circ Φ) = \sum_{j} (D_{j} u) \circ Φ \cdot D_{i} Φ_{j}$ . At order zero, $D^{0} (u \circ Φ) = u \circ Φ$ directly.

[F5]

Meyers--Serrin density on an arbitrary open set: for $u \in W^{k, q} (V_{0}; K)$ and $1 \leq q < \infty$ there are $u_{m} \in C^{\infty} (V_{0}; K) \cap W^{k, q} (V_{0}; K)$ with $u_{m} \to u$ in $W^{k, q} (V_{0}; K)$ (Meyers–Serrin density on an arbitrary open set).

[F6]

Classical derivatives of a $C^{k}$ function are its weak derivatives (Classical derivatives agree with weak derivatives).

[F7]

Weak stability: if $w_{m} \to w$ in $L_{l o c}^{p} (U^{'})$ and $z_{m} \to z$ in $L_{l o c}^{q} (U^{'})$ with $z_{m} = D^{α} w_{m}$ weakly and $1 \leq p, q \leq \infty$ , then $z = D^{α} w$ weakly on $U^{'}$ (Weak derivatives persist under local Lp limits).

[F8]

Bounded open sets have finite Lebesgue measure, and on a finite measure space every essentially bounded function is in every $L^{q}$ , with $∥ f ∥_{L^{q}} \leq ∣ V_{0} ∣^{1 / q} ∥ f ∥_{L^{\infty}}$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, Holder's inequality for integrals, including the endpoint cases).

[F9]

Norm conventions: $∥ w ∥_{W^{k, p}}^{p} = \sum_{∣ α ∣ \leq k} ∥ D^{α} w ∥_{L^{p}}^{p}$ for $p < \infty$ and $∥ w ∥_{W^{k, \infty}} = \max_{∣ α ∣ \leq k} ∥ D^{α} w ∥_{L^{\infty}}$ (Integer-order Sobolev spaces and their norms).

Choice use. Countable Choice is used through the density interface [F5] and the weak-derivative interface [F7]; the chart bounds are given.

Proof

technique · direct

1.1F1F2F3given

Since $Ψ$ has bounded first derivatives on $\overline{V_{0}}$ , [F2] gives, for every nonnegative measurable $f$ on $V_{0}$ and $1 \leq p < \infty$ , $\int_{U_{0}} ∣ f (Φ (x)) ∣^{p} d x = \int_{Φ (U_{0})} ∣ f (y) ∣^{p} ∣ \det D Ψ (y) ∣ d y \leq C \int_{V_{0}} ∣ f (y) ∣^{p} d y .$ For $p = \infty$ , [F3] makes composition well defined on a.e. classes and gives $∥ f \circ Φ ∥_{L^{\infty} (U_{0})} \leq ∥ f ∥_{L^{\infty} (V_{0})}$ . Thus pullback by $Φ$ is bounded on the stated $L^{p}$ spaces. The analogous estimate for $Ψ$ holds when $Ψ (V_{0}) \subseteq U_{0}$ .

1.2F4given

Classical composition formula: if $u \in C^{k} (V_{0}; K)$ , then $u \circ Φ \in C^{k} (U_{0}; K)$ ; for $1 \leq ∣ α ∣ \leq k$ , [F4] gives $D^{α} (u \circ Φ) = \sum_{1 \leq ∣ β ∣ \leq ∣ α ∣} ((D^{β} u) \circ Φ) P_{α β}$ on $U_{0}$ , with $∣ P_{α β} ∣ \leq C_{α}$ determined by the bounds on $Φ$ . For $α = 0$ the identity is $D^{0} (u \circ Φ) = u \circ Φ$ .

2.1F9step 1.1step 1.2

Smooth-case estimate. Let $u \in C^{k} (V_{0}; K) \cap W^{k, p} (V_{0}; K)$ . For $α = 0$ , step 1.1 bounds $u \circ Φ$ . For $1 \leq ∣ α ∣ \leq k$ , step 1.2 and the bounded coefficients give $∥ D^{α} (u \circ Φ) ∥_{L^{p} (U_{0})} \leq C_{α} \sum_{1 \leq ∣ β ∣ \leq ∣ α ∣} ∥ (D^{β} u) \circ Φ ∥_{L^{p} (U_{0})} \leq C \sum_{1 \leq ∣ β ∣ \leq ∣ α ∣} ∥ D^{β} u ∥_{L^{p} (V_{0})}$ for finite $p$ by step 1.1, and the same estimate with essential suprema for $p = \infty$ . The Sobolev norm formula [F9] and the finiteness of the index sets then give $∥ u \circ Φ ∥_{W^{k, p} (U_{0})} \leq C ∥ u ∥_{W^{k, p} (V_{0})}$ .

3.1F5F6F7step 1.1step 1.2step 2.1

Finite exponent, general class. Let $1 \leq p < \infty$ and $u \in W^{k, p} (V_{0}; K)$ . By [F5] choose $u_{m} \in C^{\infty} (V_{0}; K) \cap W^{k, p} (V_{0}; K)$ with $u_{m} \to u$ in $W^{k, p} (V_{0})$ . For each $m$ , step 1.2 gives the classical derivative formulas, and step 2.1 gives $∥ u_{m} \circ Φ ∥_{W^{k, p} (U_{0})} \leq C ∥ u_{m} ∥_{W^{k, p} (V_{0})}$ . By step 1.1, $u_{m} \circ Φ \to u \circ Φ$ in $L^{p} (U_{0})$ and $(D^{β} u_{m}) \circ Φ \to (D^{β} u) \circ Φ$ in $L^{p} (U_{0})$ for every $∣ β ∣ \leq k$ . Since each $P_{α β}$ is bounded, the derivative fields converge to $h_{α} : = \sum_{1 \leq ∣ β ∣ \leq ∣ α ∣} ((D^{β} u) \circ Φ) P_{α β}$ for $1 \leq ∣ α ∣ \leq k$ . By [F7], each $h_{α}$ is the weak derivative $D^{α} (u \circ Φ)$ ; the order-zero derivative is $u \circ Φ$ . Thus $u \circ Φ \in W^{k, p} (U_{0})$ with the stated formulas, and the bound follows by passing the smooth estimates to the limit.

4.1F3F8F9step 3.1

Exponent $p = \infty$ . Let $u \in W^{k, \infty} (V_{0}; K)$ . Since $V_{0}$ has finite measure, [F8] gives $u \in W^{k, q} (V_{0})$ for any finite $q \geq 1$ , so step 3.1 yields the same weak derivative formulas for $u \circ Φ$ in one such $W^{k, q} (U_{0})$ . Each formula field $h_{α}$ is in $L^{\infty} (U_{0})$ because its factors $(D^{β} u) \circ Φ$ are essentially bounded by [F3] and its coefficients are bounded; also $u \circ Φ \in L^{\infty} (U_{0})$ by [F3]. Hence these weak derivatives lie in $L^{\infty}$ , giving $u \circ Φ \in W^{k, \infty} (U_{0})$ and the claimed norm bound.

5.1F4step 1.2step 2.1step 3.1step 4.1∎

If $Ψ (V_{0}) \subseteq U_{0}$ , then the two patch inclusions force $Φ (U_{0}) = V_{0}$ . Applying steps 1.1–4.1 with the roles of $Φ$ and $Ψ$ interchanged gives the asserted inverse estimate. For $k = 1$ the formula of [F4] involves only first derivatives, so bounded $C^{1}$ data for $Φ$ and $Ψ$ suffice; at order $k > 1$ the polynomials $P_{α β}$ involve derivatives of the chart through order $∣ α ∣$ , and no $C^{1}$ -only statement is claimed.

Depends on

Used by

Dependency tree · two levels

70 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

Sung-Jin Oh, Lecture Notes for Math 222A (2024), §11.3 (standard reference, not scraped)
Juha Kinnunen, Sobolev Spaces (2026), proof of Theorem 1.25 (standard reference, not scraped)