LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Bounded restriction and cutoff localisation in Sobolev spaces

Sources

Juha Kinnunen, Sobolev Spaces, Chapter 1 §§1.2–1.3, Lemma 1.14(4)–(5), printed pp. 9–11 (PDF pp. 11–13). The source states restriction to open subsets and the smooth-factor Leibniz formula. This item derives the contractive and bounded-operator norm estimates for the library's finite Sobolev norm, including both exponent endpoints and complex scalars.

Statement

Assume the Axiom of Choice. Let $Ω \subseteq R^{n}$ be open, $n \geq 1$ , $k \in N_{0}$ , $1 \leq p \leq \infty$ , and $K \in {R, C}$ . If $U \subseteq Ω$ is open, then restriction defines a contraction $W^{k, p} (Ω; K) ⟶ W^{k, p} (U; K), u ⟼ u ∣_{U} .$ If $η \in C_{c}^{\infty} (Ω; K)$ , multiplication defines a bounded map $u \mapsto η u$ on $W^{k, p} (Ω; K)$ . More precisely, for $α \in N_{0}^{n}$ with $∣ α ∣ \leq k$ put $C_{α} (η) : = \sum_{β \leq α} (\binom{α}{β}) ∥ D^{β} η ∥_{L^{\infty} (Ω)} .$ Then $∥ η u ∥_{W^{k, p}} \leq {\begin{cases} {(\sum_{∣ α ∣ \leq k} C_{α} (η)^{p})}^{1 / p} ∥ u ∥_{W^{k, p}}, & 1 \leq p < \infty, \\ \max_{∣ α ∣ \leq k} C_{α} (η) ∥ u ∥_{W^{k, \infty}}, & p = \infty . \end{cases}$ The displayed constants involve only finitely many sup norms of derivatives of $η$ through order $k$ . AC is used only to invoke the Countable Choice interfaces for weak-derivative uniqueness, the Sobolev quotient norm, and the smooth-factor Leibniz rule.

If $Ω = \emptyset$ , then $U = \emptyset$ and both maps are the unique maps on the zero Sobolev space.

Facts & Assumptions

Given: AC, an open $Ω \subseteq R^{n}$ , $n \geq 1$ , an open $U \subseteq Ω$ , $k \in N_{0}$ , $1 \leq p \leq \infty$ , $K \in {R, C}$ , $u \in W^{k, p} (Ω; K)$ , and $η \in C_{c}^{\infty} (Ω; K)$ .

[F1]

$W^{k, p}$ consists of a.e. classes with each weak derivative of order at most $k$ in $L^{p}$ , and its displayed norm is the finite- $p$ sum or the $p = \infty$ maximum (Integer-order Sobolev spaces and their norms).

[F2]

The Sobolev formula is independent of representatives and is a definite norm under Countable Choice (The Sobolev norm descends to equivalence classes).

[F3]

A weak derivative restricts to every open subset, with its value class restricted there (Linearity, locality, and commutation of weak derivatives).

[F4]

If all derivatives of $u$ through order $k$ lie in $L^{p}$ and the derivatives of a smooth multiplier through order $k$ are bounded, then $η u \in W^{k, p}$ and $D^{α} (η u) = \sum_{β \leq α} (\binom{α}{β}) (D^{β} η) D^{α - β} u$ for every $∣ α ∣ \leq k$ (Weak Leibniz rule with a smooth factor).

[F5]

The real $L^{p}$ quotient norm is well defined and satisfies the triangle inequality for all $1 \leq p \leq \infty$ (The $L^{p}$ norm descends to the quotient and makes $L^{p}$ a normed space for $1 \leq p \leq \infty$ ).

[F6]

The complex $L^{p}$ quotient norm is well defined and satisfies the triangle inequality for all $1 \leq p \leq \infty$ (Complex Holder, Minkowski, and the quotient norm).

[F7]

For a nonnegative measurable $h$ and measurable $E$ , $\int_{E} h = \int h 1_{E}$ ; the nonnegative integral is monotone (Integral over a measurable subset, Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F8]

The essential supremum is the infimum of the almost-everywhere upper bounds; for complex classes the $L^{\infty}$ norm uses the modulus, and a bound on $Ω$ remains a bound on measurable $U \subseteq Ω$ (The essential supremum of a measurable function with respect to a measure, Complex Lp classes and Euclidean test-function conventions).

[F9]

A member of $C_{c}^{\infty} (Ω)$ is smooth with compact support in $Ω$ (Test function space d of an open set).

[F10]

Continuous real functions are bounded on nonempty compact metric spaces; for a complex-valued function apply this to its real and imaginary parts, using $∣ z ∣ \leq ∣ Re z ∣ + ∣ Im z ∣$ (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F11]

AC supplies Countable Choice (The Axiom of Choice, AC supplies the countable and dependent choices used in Banach integration).

Proof

technique · Restrict each weak derivative and estimate the finite Leibniz sum

1.1F1F2F3F5F6F7F8F11given

If $Ω = \emptyset$ or $U = \emptyset$ , restriction is the zero map on the zero domain or into the zero Sobolev space, respectively. Otherwise [F3] identifies each weak derivative of $u ∣_{U}$ with $(D^{α} u) ∣_{U}$ . For finite $p$ , [F7] gives $∥ f ∣_{U} ∥_{p}^{p} = \int_{Ω} ∣ f ∣^{p} 1_{U} d x \leq \int_{Ω} ∣ f ∣^{p} d x$ ; for $p = \infty$ , every a.e. bound on $Ω$ remains a bound on $U$ , so [F8] gives $∥ f ∣_{U} ∥_{\infty} \leq ∥ f ∥_{\infty}$ . Apply these estimates to all components in [F1]; [F2], [F5] and [F6] ensure these are well-defined class norms. AC is used by [F11] only to supply Countable Choice to the weak-derivative restriction and Sobolev norm interfaces [F2] and [F3].

1.2F9F10given

If $η = 0$ , all its derivatives vanish. Otherwise its support $K$ is compact in $Ω$ by [F9]; every derivative vanishes outside $K$ and is continuous on $K$ , so the real and imaginary parts are bounded there by [F10]. Thus $∥ D^{β} η ∥_{L^{\infty} (Ω)} < \infty$ for every $∣ β ∣ \leq k$ .

2.1F1F4F5F6F7F8F10F11givenstep 1.2∎

By step 1.2 and [F4], for every $∣ α ∣ \leq k$ the weak derivative of $η u$ is the finite Leibniz sum. The product estimate $∥ D^{β} η D^{α - β} u ∥_{p} \leq ∥ D^{β} η ∥_{\infty} ∥ D^{α - β} u ∥_{p}$ follows from [F7] when $p < \infty$ and [F8] when $p = \infty$ (with [F10] for complex moduli); the triangle inequalities [F5] and [F6] therefore give $∥ D^{α} (η u) ∥_{p} \leq C_{α} (η) ∥ u ∥_{W^{k, p}}$ . Applying the finite- $p$ sum or the $p = \infty$ maximum in [F1] yields exactly the asserted operator bound. This includes the zero class, $k = 0$ , and both endpoints $p = 1, \infty$ . AC is used through [F11] only to supply Countable Choice for the Leibniz interface [F4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 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), Chapter 1 §§1.2–1.3 (standard reference, not scraped)