TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Lewy–Stampacchia distribution bound for bounded-coefficient obstacle forms

Statement

Assume Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice), inherited through the existence, density, truncation and sign suppliers cited below. Let $n \geq 1$ and let $Ω \subseteq R^{n}$ be a bounded open set of the two kinds of The closed convex obstacle set and the obstacle variational inequality: a bounded interval when $n = 1$ , and a bounded $C^{1}$ domain when $n \geq 2$ (Bounded C^k domains and boundary charts). Let $L$ be a real symmetric uniformly elliptic divergence-form operator with bounded measurable real coefficients and coercive form $a$ (Uniformly elliptic divergence-form operators and their sesquilinear forms), let $f \in L^{2} (Ω; R)$ , and let the real obstacle $ψ \in H^{2} (Ω; R) \cap H_{0}^{1} (Ω; R)$ (The notation $H^{k}$ and the reserved zero-boundary symbol, Integer-order Sobolev spaces and their norms) satisfy the additional hypothesis that its distributional image $L ψ$ is represented by an $L^{2} (Ω; R)$ function; put $h : = L ψ - f \in L^{2} (Ω; R)$ . Let $u \in K = {v \in H_{0}^{1} (Ω; R) : v \geq ψ}$ solve the obstacle problem (Existence and uniqueness for the obstacle problem, Zero-boundary Sobolev space as a norm closure) with reaction $Λ_{u} (φ) = a (u, φ) - \int_{Ω} f φ$ on test functions (Obstacle complementarity in distribution form, Distribution, Test function space d of an open set). Then, in the sense of distributions, $0 \leq Λ_{u} \leq (L ψ - f)^{+},$ that is, $Λ_{u}$ is a nonnegative distribution bounded above by the $L^{2}$ function $h^{+}$ .

Facts & Assumptions

Given: The bounded open set $Ω$ of the two kinds above with $n \geq 1$ ; a real symmetric uniformly elliptic divergence-form operator $L = - D_{i} (a^{i j} D_{j} \cdot) + b^{i} D_{i} \cdot + c \cdot$ with bounded measurable real coefficients and coercive form $a (u, v) = \int_{Ω} (a^{i j} D_{j} u D_{i} v + b^{i} D_{i} u v + c u v) d x$ of Uniformly elliptic divergence-form operators and their sesquilinear forms; $f \in L^{2} (Ω; R)$ and the functional $F (v) = \int_{Ω} f v$ ; the obstacle $ψ \in H^{2} (Ω; R) \cap H_{0}^{1} (Ω; R)$ with $L ψ$ represented by an $L^{2}$ function; $h = L ψ - f$ ; the admissible set $K = {v \in H_{0}^{1} (Ω; R) : v \geq ψ a.e.}$ and the unique obstacle solution $u \in K$ with reaction $Λ_{u} (φ) = a (u, φ) - F (φ)$ .

[F1]

The closed convex obstacle set and the obstacle variational inequality, Existence and uniqueness for the obstacle problem: $K$ is nonempty and $u \in K$ satisfies $a (u, v - u) \geq F (v - u)$ for every $v \in K$ ; in particular $u \geq ψ$ almost everywhere on $Ω$ . The form $a$ is symmetric, bounded and coercive.

[F2]

Uniformly elliptic divergence-form operators and their sesquilinear forms, The elliptic form is well defined and bounded on $H^{1}$ : the form $a$ is a well-defined bounded bilinear form on $H^{1} (Ω)$ with $∣ a (u, v) ∣ \leq M ∥ u ∥_{H^{1}} ∥ v ∥_{H^{1}}$ , and for every $w \in H^{1} (Ω)$ and every $φ \in C_{c}^{\infty} (Ω)$ the distribution $L w$ pairs as $⟨ L w, φ ⟩ = a (w, φ)$ ; the calculation below retains the bounded drift term, and does not require it to vanish.

[F3]

Zero-boundary Sobolev space as a norm closure, Test function space d of an open set: $H_{0}^{1} (Ω)$ is the closure of $C_{c}^{\infty} (Ω)$ in the $H^{1}$ norm, so $C_{c}^{\infty} (Ω)$ is dense in $H_{0}^{1} (Ω)$ ; every $H^{1}$ class vanishing almost everywhere outside a compact subset of $Ω$ lies in $H_{0}^{1} (Ω)$ : extend it by zero using Compactly supported Sobolev functions extend by zero in every integer order, approximate the extension by Compactly supported smooth functions are dense in W^{k,p}(R^n), and multiply the approximants by a fixed interior smooth cutoff equal to one near its support (Test function cutoffs and euclidean localization, Bounded restriction and cutoff localisation in Sobolev spaces). The resulting interior tests converge in $H^{1}$ .

[F4]

Positive-part truncation calculus and admissible cut-off weak tests: truncations and compactly supported cutoff products have the stated $H^{1}$ / $H_{0}^{1}$ membership and gradient formulas. Its weak-test interface extends a local inequality to a cutoff test when the local source is in $L^{2}$ , and permits a global $H_{0}^{1}$ test when the source functional is continuous on $H_{0}^{1}$ ; it does not pair a general $L_{l o c}^{1}$ source with an arbitrary $H_{0}^{1}$ function.

[F5]

Weak Leibniz rule with a smooth factor: for $η \in C_{c}^{\infty} (Ω)$ and $z \in H^{1} (Ω)$ the product $η z$ lies in $H^{1} (Ω)$ with $D (η z) = η D z + z D η$ a.e.

[F6]

Uniformly elliptic divergence-form operators and their sesquilinear forms: uniform ellipticity gives $a^{i j} D_{j} w D_{i} w \geq θ ∣ D w ∣^{2} \geq 0$ a.e. for every real $w \in H^{1} (Ω)$ .

[F7]

Dominated convergence: if measurable functions converge pointwise a.e. and are dominated in absolute value by one integrable function, their integrals converge.

[F8]

A function with nonnegative test pairings is nonnegative a.e.: an $L^{2}$ class whose pairings with all nonnegative test functions are nonnegative is itself nonnegative almost everywhere.

[F9]

The space $L^{p} (μ)$ as the quotient by null functions, Holder's inequality for integrals, including the endpoint cases: for $h \in L^{2} (Ω)$ and $φ \in C_{c}^{\infty} (Ω)$ the product $h φ$ is in $L^{1} (Ω)$ , and $h 1_{E} \leq h^{+}$ pointwise for every measurable set $E$ , with both classes in $L^{2} (Ω)$ ; all pointwise statements are read on representatives and hold a.e. independently of the representative.

[F10]

The reaction $Λ_{u} (v) = a (u, v) - \int_{Ω} f v$ is a bounded functional on $H_{0}^{1} (Ω)$ : boundedness of $a$ is [F2], and $f \in L^{2}$ acts continuously by Cauchy--Schwarz and $∥ v ∥_{L^{2}} \leq ∥ v ∥_{H^{1}}$ . Under the real specialization of The negative Sobolev space $H^{- 1} (Ω)$ , this is exactly an $H^{- 1}$ source functional, so the global test-extension clause of [F4] applies.

Proof

technique · direct

Given: The setting above, the obstacle solution $u \in K$ , the class $w : = u - ψ \in H_{0}^{1} (Ω; R)$ , and the reaction functional $Λ (v) : = a (u, v) - F (v)$ defined on $H_{0}^{1} (Ω)$ .

1.1givenF1

For every $q \in H_{0}^{1} (Ω; R)$ with $q \geq 0$ a.e. one has $u + q \in K$ , because $u + q \in H_{0}^{1} (Ω)$ and $(u + q) - ψ = w + q \geq 0$ a.e. by [F1]; testing the variational inequality [F1] at $v = u + q$ gives $Λ (q) \geq 0$ .

1.2givenF1F2F3F9

The classes $w = u - ψ$ and $q = w$ satisfy $w \in H_{0}^{1} (Ω)$ and $w \geq 0$ a.e. by [F1]. For every $v \in C_{c}^{\infty} (Ω)$ the definition of $L ψ$ gives $a (ψ, v) = ⟨ L ψ, v ⟩ = \int_{Ω} (L ψ) v$ [F2]; both $v \mapsto a (ψ, v)$ and $v \mapsto \int_{Ω} (L ψ) v$ are bounded linear functionals on $H_{0}^{1} (Ω)$ — the first by [F2], the second because $∥ v ∥_{L^{2}} \leq ∥ v ∥_{H^{1}}$ and $L ψ \in L^{2}$ — and they agree on the dense subspace $C_{c}^{\infty} (Ω)$ [F3], so they agree on all of $H_{0}^{1} (Ω)$ . Hence, for every $v \in H_{0}^{1} (Ω)$ , $Λ (v) = a (w, v) + \int_{Ω} h v$ by bilinearity of $a$ and $u = w + ψ$ .

1.3givenF1

Testing the variational inequality at $v = ψ \in K$ gives $a (u, ψ - u) \geq F (ψ - u)$ , that is $- Λ (w) \geq 0$ or $Λ (w) \leq 0$ ; testing at $v = u + w = 2 u - ψ \in K$ , which is admissible because $(2 u - ψ) - ψ = 2 w \geq 0$ a.e., gives $Λ (w) \geq 0$ . Hence $Λ (w) = 0$ .

1.4givenF4

For $δ > 0$ put $θ_{δ} : = (1 - w / δ)^{+} = δ^{- 1} (w - δ)^{-}$ and $m_{δ} : = 1 - θ_{δ} = \min {w / δ, 1}$ ; these are the truncations of [F4] at the level $δ$ , so $θ_{δ}, m_{δ} \in H^{1} (Ω; R)$ with $0 \leq θ_{δ}, m_{δ} \leq 1$ , $m_{δ} = w / δ$ on ${w \leq δ}$ , and $D θ_{δ} = - δ^{- 1} 1_{{0 < w < δ}} D w, D m_{δ} = δ^{- 1} 1_{{0 < w < δ}} D w a.e.,$ the indicator being restricted to ${0 < w < δ}$ because $D w = 0$ a.e. on the level set ${w = 0}$ [F4]; moreover $D w = 0$ a.e. on $E : = {w = 0}$ .

2.1step 1.1step 1.3F1F3F4F5F10

Let $φ \in C_{c}^{\infty} (Ω)$ with $φ \geq 0$ and let $δ > 0$ . The products $φ m_{δ}$ and $(∥ φ ∥_{\infty} / δ) w - φ m_{δ}$ lie in $H_{0}^{1} (Ω)$ by [F3] and [F5], and both are nonnegative a.e.: the first because $φ \geq 0$ and $m_{δ} \geq 0$ , the second because $φ m_{δ} \leq ∥ φ ∥_{\infty} m_{δ} \leq (∥ φ ∥_{\infty} / δ) w$ . The global H $^{- 1}$ test clause of [F4] applies by [F10]; independently, [F1] states the obstacle variational inequality for every such $H_{0}^{1}$ competitor. Thus step 1.1 gives $Λ (φ m_{δ}) \geq 0$ and $Λ ((∥ φ ∥_{\infty} / δ) w - φ m_{δ}) \geq 0$ ; by linearity and $Λ (w) = 0$ of step 1.3 the second inequality reads $- Λ (φ m_{δ}) \geq 0$ . Hence $Λ (φ m_{δ}) = 0$ , and since $φ θ_{δ} = φ - φ m_{δ}$ , linearity gives $Λ (φ θ_{δ}) = Λ (φ)$ .

2.2step 1.2step 1.4F5

Expanding the form and using $D (φ θ_{δ}) = θ_{δ} D φ + φ D θ_{δ}$ [F5] and the decomposition of step 1.2, for every $φ \in C_{c}^{\infty} (Ω)$ and $δ > 0$ one has $Λ (φ θ_{δ}) = \int_{Ω} θ_{δ} a^{i j} D_{j} w D_{i} φ - δ^{- 1} \int_{{0 < w < δ}} φ a^{i j} D_{j} w D_{i} w + \int_{Ω} b^{i} D_{i} w φ θ_{δ} + \int_{Ω} c w φ θ_{δ} + \int_{Ω} h φ θ_{δ} .$

3.1step 1.1step 2.1step 2.2F6F7F9

Fix $φ \in C_{c}^{\infty} (Ω)$ with $φ \geq 0$ and abbreviate the five terms of step 2.2 as $A_{δ}$ , $- T_{δ}$ , $B_{δ}$ , $C_{δ}$ , $H_{δ}$ , so that $Λ (φ) = Λ (φ θ_{δ}) = A_{δ} - T_{δ} + B_{δ} + C_{δ} + H_{δ}$ by steps 2.1 and 2.2, with $T_{δ} \geq 0$ because $φ a^{i j} D_{j} w D_{i} w \geq θ φ ∣ D w ∣^{2} \geq 0$ a.e. by [F6]. As $δ ↓ 0$ : $A_{δ} \to 0$ by [F7], since $θ_{δ} \to 1_{E}$ a.e., $∣ θ_{δ} a^{i j} D_{j} w D_{i} φ ∣ \leq n M_{a} ∣ D w ∣ ∣ D φ ∣ \in L^{1} (Ω)$ , and $D w = 0$ a.e. on $E$ ; $B_{δ} \to 0$ by [F7], since $∣ b^{i} D_{i} w φ θ_{δ} ∣ \leq n M_{b} ∣ D w ∣ ∣ φ ∣$ is integrable and the pointwise limit vanishes on $E$ via $D w = 0$ a.e. there; $C_{δ} \to 0$ by [F7], since $∣ c w φ θ_{δ} ∣ \leq M_{c} ∣ φ ∣ δ / 4 \leq M_{c} ∣ φ ∣ / 4$ for $δ \leq 1$ and $w θ_{δ} \leq δ / 4$ ; and $H_{δ} \to \int_{E} h φ$ by [F7], since $h φ$ is integrable [F9] and $θ_{δ} \to 1_{E}$ a.e. Therefore $T_{δ} = A_{δ} + B_{δ} + C_{δ} + H_{δ} - Λ (φ)$ converges to $\int_{E} h φ - Λ (φ)$ , and $T_{δ} \geq 0$ gives $\int_{E} h φ \geq Λ (φ)$ ; with $Λ (φ) \geq 0$ from step 1.1, $0 \leq Λ (φ) \leq \int_{E} h φ$ .

4.1step 3.1F8F9

The class $g : = h 1_{E}$ lies in $L^{2} (Ω)$ by [F9], and step 3.1 gives $\int_{Ω} g φ = \int_{E} h φ \geq Λ (φ) \geq 0$ for every $φ \in C_{c}^{\infty} (Ω)$ with $φ \geq 0$ ; by [F8] therefore $g \geq 0$ a.e. on $Ω$ , that is $h \geq 0$ a.e. on $E$ .

5.1step 1.1step 3.1step 4.1F1F3F4F8F9∎

For every $φ \in C_{c}^{\infty} (Ω)$ with $φ \geq 0$ one has $\int_{E} h φ = \int_{Ω} (h 1_{E}) φ \leq \int_{Ω} h^{+} φ$ because $h 1_{E} \leq h^{+}$ pointwise [F9], while steps 1.1 and 3.1 give $0 \leq Λ (φ) \leq \int_{E} h φ$ ; hence $0 \leq Λ (φ) \leq \int_{Ω} h^{+} φ$ for every nonnegative test function, which is precisely the distributional statement $0 \leq Λ_{u} \leq (L ψ - f)^{+}$ . Countable Choice is consumed through the existence theorem [F1], the density of $C_{c}^{\infty} (Ω)$ in $H_{0}^{1} (Ω)$ [F3] and the sign lemma [F8], and the Axiom of Choice through the ACL-based truncation calculus [F4] and the trace conventions of the obstacle setting [F1]; no further choice principle is used.

Source note

The cited article [OU] proves the Lewy–Stampacchia inequality in the entropy-solution class under a hypothesis that the obstacle’s positive part is bounded and without lower-order terms; it corroborates the principal-part case but is not used to justify the bounded drift and potential terms, which are handled here by the explicit truncation calculation above. The additional hypothesis that $L ψ$ be represented by an $L^{2}$ function is what makes $h = L ψ - f$ an honest $L^{2}$ object and the upper bound an $L^{2}$ function.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

100 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

Stanislas Ouaro and Sado Traore, Entropy solutions to the obstacle problem for nonlinear elliptic problems with variable exponent and L1-data (complete publisher-hosted article, vol. 5 no. 1, 2009, pp. 127-141; received 7 September 2007, accepted 22 November 2008) (standard reference, not scraped)