LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Positive-part truncation calculus and admissible cut-off weak tests

Statement

Assume Countable Choice together with the Axiom of Choice, inherited through the published ACL characterisation and the chain-rule interfaces cited below. Let $n \geq 1$ , let $Ω \subseteq R^{n}$ be open, let $u \in H^{1} (Ω; R)$ and $k \in R$ , and put $u_{k} : = (u - k)^{+}$ and $u_{k}^{-} : = (u - k)^{-}$ on measurable representatives. Then $u_{k}, u_{k}^{-} \in H_{l o c}^{1} (Ω; R)$ with $D u_{k} = 1_{{u > k}} D u, D u_{k}^{-} = - 1_{{u < k}} D u a.e. on Ω,$ and $D u_{k} = 0$ a.e. on ${u \leq k}$ . If $∣ Ω ∣ < \infty$ , then $u_{k}, u_{k}^{-} \in H^{1} (Ω)$ ; more generally, either truncation belongs to $H^{1} (Ω)$ whenever that truncation is in $L^{2} (Ω)$ . In particular, $u_{k} \in H^{1} (Ω)$ for $k \geq 0$ , and $u_{k}^{-} \in H^{1} (Ω)$ for $k \leq 0$ . If $n \geq 2$ , $Ω$ is bounded and $C^{1}$ , and $u_{k} \in H_{0}^{1} (Ω)$ , then this membership is the boundary condition $u \leq k$ on $\partial Ω$ in the sense of Weak subsolutions and supersolutions of a divergence-form equation. For every $η \in C_{c}^{\infty} (Ω)$ the product $η^{2} u_{k}$ lies in $H_{0}^{1} (Ω)$ with $D (η^{2} u_{k}) = 2 η u_{k} D η + η^{2} D u_{k} a.e. on Ω,$ so $η^{2} u_{k}$ belongs to the Sobolev test space. It is admissible in the global $H^{- 1}$ formulation when the source pairing is continuous; for a local inequality with $f \in L_{l o c}^{2}$ , its pairing extends by density on a bounded neighborhood of the cutoff support. No pairing with a general $L_{l o c}^{1}$ source and an arbitrary $H_{0}^{1}$ test is asserted. The same membership conclusions hold for $k$ -translates of $u^{+}$ and for the cut-off functions $η^{2} u_{k}$ with $η \in W_{c}^{1, \infty} (Ω)$ .

Facts & Assumptions

Given: Countable Choice and the Axiom of Choice; an open set $Ω \subseteq R^{n}$ with $n \geq 1$ ; a real class $u \in H^{1} (Ω; R)$ ; a real level $k$ ; and $u_{k} = (u - k)^{+}$ , $u_{k}^{-} = (u - k)^{-}$ .

[F1]

$H^{1} (Ω; R) = W^{1, 2} (Ω; R)$ consists of the classes in $L^{2} (Ω; R)$ whose first weak derivatives exist as $L^{2}$ classes; the weak-derivative formula is the signed test identity (The notation $H^{k}$ and the reserved zero-boundary symbol, Integer-order Sobolev spaces and their norms).

[F2]

Assume the Axiom of Choice. For $u \in W^{1, p} (Ω; R)$ and $F : R \to R$ Lipschitz: $F \circ u \in W_{l o c}^{1, p} (Ω)$ with $D_{i} (F \circ u) = F^{'} (u) D_{i} u$ almost everywhere where $F$ is differentiable at $u$ , the product being taken as $0$ on the null level set $N_{F}$ ; moreover $F \circ u \in W^{1, p} (Ω)$ exactly when $F (u) \in L^{p} (Ω)$ (Chain rule for globally Lipschitz scalar maps of Sobolev functions).

[F3]

Assume the Axiom of Choice. For $w \in W^{1, p} (Ω; R)$ , $w^{+}, w^{-} \in W^{1, p} (Ω; R)$ with $D_{i} w^{+} = 1_{{w > 0}} D_{i} w$ , $D_{i} w^{-} = - 1_{{w < 0}} D_{i} w$ and $D_{i} w = 0$ almost everywhere on ${w = 0}$ (Positive, negative, and truncated Sobolev functions).

[F4]

Assume the Axiom of Choice. For $η \in C_{c}^{\infty} (Ω)$ and $w \in W^{1, p} (Ω)$ , the product $η w$ lies in $W^{1, p} (Ω)$ and $D_{i} (η w) = η D_{i} w + w D_{i} η$ almost everywhere (Weak Leibniz rule with a smooth factor, Bounded restriction and cutoff localisation in Sobolev spaces).

[F5]

Assume Countable Choice. If $w \in H^{1} (Ω)$ vanishes almost everywhere outside a compact set $K_{0} \subset Ω$ , then its zero extension lies in $H^{1} (R^{n})$ and is approximated in the $H^{1}$ norm by compactly supported smooth functions; choosing mollifier radii smaller than $dist (K_{0}, \partial Ω)$ and restricting the approximants exhibits $w$ as an $H^{1} (Ω)$ -limit of $C_{c}^{\infty} (Ω)$ functions, hence $w \in H_{0}^{1} (Ω)$ (Compactly supported Sobolev functions extend by zero in every integer order, Compactly supported smooth functions are dense in W^{k,p}(R^n), Zero-boundary Sobolev space as a norm closure).

[F6]

Weak boundary order: when $n \geq 2$ and $Ω$ is a bounded $C^{1}$ domain, $u \leq k$ on $\partial Ω$ means $(u - k)^{+} \in H_{0}^{1} (Ω)$ (Weak subsolutions and supersolutions of a divergence-form equation).

[F7]

Assume the Axiom of Choice. ACL product rule: if $η \in W_{c}^{1, \infty} (Ω; R)$ and $w \in H^{1} (Ω; R)$ , then $η w \in H^{1} (Ω; R)$ with $D_{i} (η w) = η D_{i} w + w D_{i} η$ almost everywhere. Indeed $η$ and $w$ have ACL representatives whose sections are absolutely continuous on almost every line (The ACL characterisation of $W^{1, p}$ ), the ordinary product rule holds along those lines, and the resulting a.e. line derivatives determine the weak derivative by the reconstruction lemma (ACL representatives recover their weak gradients by Fubini).

Proof

technique · direct; the truncations are produced by the globally Lipschitz chain rule, and the cut-off tests by the product rules and the compact-support characterisation of $H^1_0$

1.1givenF1F2

The function $F (t) : = (t - k)^{+}$ is Lipschitz with constant $1$ and differentiable off $k$ ; the chain rule [F2] gives $u_{k} \in H_{l o c}^{1} (Ω)$ and $D_{i} u_{k} = 1_{{u > k}} D_{i} u$ locally a.e. If $∣ Ω ∣ < \infty$ , the bound $u_{k} \leq ∣ u ∣ + ∣ k ∣$ gives $u_{k} \in L^{2} (Ω)$ and hence $H^{1} (Ω)$ ; if $k \geq 0$ , then $0 \leq u_{k} \leq u^{+}$ , which gives global membership without a finite-measure assumption. In general, global membership follows whenever $u_{k} \in L^{2} (Ω)$ , since its weak gradient is bounded by $∣ D u ∣$ .

1.2givenF1F2

Likewise $G (t) : = (t - k)^{-} = \max {k - t, 0}$ is Lipschitz with constant $1$ and differentiable off $k$ ; the chain rule gives $u_{k}^{-} \in H_{l o c}^{1} (Ω)$ and $D_{i} u_{k}^{-} = - 1_{{u < k}} D_{i} u$ locally a.e. If $∣ Ω ∣ < \infty$ , then $u_{k}^{-} \in L^{2} (Ω)$ and hence $H^{1} (Ω)$ ; if $k \leq 0$ , then $0 \leq u_{k}^{-} \leq u^{-}$ . In general, global membership follows whenever $u_{k}^{-} \in L^{2} (Ω)$ .

2.1step 1.1step 1.2F3

On ${u \leq k}$ the indicator $1_{{u > k}}$ vanishes, so the almost-everywhere identity of step 1.1 gives $D_{i} u_{k} = 0$ almost everywhere on ${u \leq k}$ , and a fortiori almost everywhere on ${u < k}$ ; at level $k = 0$ this is exactly the positive-part calculus of [F3] for $w = u$ , whose formula $D_{i} w^{+} = 1_{{w > 0}} D_{i} w$ agrees with step 1.1. The same argument applied to step 1.2 gives $D_{i} u_{k}^{-} = 0$ almost everywhere on ${u \geq k}$ .

2.2step 1.1F6given

If $n \geq 2$ and $Ω$ is a bounded $C^{1}$ domain, the equivalence " $u_{k} \in H_{0}^{1} (Ω)$ if and only if $u \leq k$ on $\partial Ω$ " is the definition of the weak boundary order in [F6], read with $u_{k} = (u - k)^{+}$ ; no pointwise boundary values are involved.

2.3step 1.1F4F5

Let $η \in C_{c}^{\infty} (Ω)$ and put $v : = η^{2} u_{k}$ . Choose a bounded neighborhood $V$ of $supp η$ with $\overline{V} \subset Ω$ . By step 1.1, $u_{k} \in H^{1} (V)$ ; the product rule [F4] gives $v \in H^{1} (Ω)$ with $D_{i} v = 2 η u_{k} D_{i} η + η^{2} D_{i} u_{k}$ almost everywhere. Its support is compact in $Ω$ , so [F5] gives $v \in H_{0}^{1} (Ω)$ . Since $η^{2} \geq 0$ and $u_{k} \geq 0$ , it is a nonnegative Sobolev test. If the source is in $L_{l o c}^{2}$ on $V$ , density extends the local inequality to this test; it is also valid for the global formulation whenever the source defines a continuous functional on $H_{0}^{1}$ . For a general $L_{l o c}^{1}$ source, membership alone does not assert that the pairing is defined.

3.1step 2.3F5F7

Now let $η \in W_{c}^{1, \infty} (Ω)$ . On a bounded neighborhood $V$ of its support, the ACL product rule [F7] applied twice gives $η^{2} u_{k} \in H^{1} (Ω)$ with $D_{i} (η^{2} u_{k}) = 2 η u_{k} D_{i} η + η^{2} D_{i} u_{k}$ almost everywhere. Its compact support and nonnegativity again give $η^{2} u_{k} \in H_{0}^{1} (Ω)$ ; admissibility in an inequality requires the same source-pairing condition as in step 2.3.

4.1step 1.1step 1.2step 2.3step 3.1F3∎

Apply steps 1.1-3.1 to $v = u^{+}$ and $v = u^{-}$ , both of which lie in $H^{1} (Ω; R)$ by [F3]. For every $κ \in R$ , each truncation $(v - κ)^{\pm}$ lies in $H_{l o c}^{1} (Ω)$ with the corresponding level-set gradient formula, and its cutoff products with $η \in C_{c}^{\infty} (Ω)$ or $η \in W_{c}^{1, \infty} (Ω)$ lie in $H_{0}^{1} (Ω)$ . Global $H^{1} (Ω)$ membership holds when $∣ Ω ∣ < \infty$ or when that truncation is in $L^{2} (Ω)$ ; in particular $(v - κ)^{+} \in H^{1} (Ω)$ for $κ \geq 0$ , while $(v - κ)^{-} = 0$ for $κ \leq 0$ because $v \geq 0$ . Admissibility in a weak inequality still requires the source pairing to extend continuously to the test space, as specified in the Definition. All steps use only Countable Choice and the Axiom of Choice as declared in [F2]-[F5] and [F7].

Depends on

Used by

Dependency tree · two levels

106 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

Leon Simon, Lectures on Partial Differential Equations (Stanford University; complete author scan, 118 sheets reproducing the 223 printed pages of the manuscript, two logical pages per sheet) (standard reference, not scraped)
Bozhidar Velichkov, Elliptic PDEs: Teorema di De Giorgi (Universita di Pisa; complete 7-page note, in Italian) (standard reference, not scraped)