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.

Existence and uniqueness for the obstacle problem

Statement

Assume the Axiom of Choice and Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )), inherited from the obstacle setting and Hilbert-space supplier. Let $Ω$ , $ψ$ , $K$ , $a$ and $F$ be as in The closed convex obstacle set and the obstacle variational inequality, with $a$ symmetric as well as bounded and coercive (Bounded, coercive and symmetric sesquilinear forms) and $F \in H^{- 1} (Ω)$ (The negative Sobolev space $H^{- 1} (Ω)$ ), and let $J (v) = \frac{1}{2} a (v, v) - F (v)$ be the energy. Then $J$ attains its infimum on $K$ at exactly one $u \in K$ , and $u$ is the unique solution of the obstacle variational inequality $a (u, v - u) \geq F (v - u) (v \in K) .$ Equivalently: $u \in K$ minimises $J$ on $K$ if and only if $u$ solves the variational inequality.

Facts & Assumptions

Given: The obstacle setting of The closed convex obstacle set and the obstacle variational inequality: the admissible set $K \subseteq H_{0}^{1} (Ω)$ (Zero-boundary Sobolev space as a norm closure, The notation $H^{k}$ and the reserved zero-boundary symbol, Integer-order Sobolev spaces and their norms), a symmetric bounded coercive bilinear form $a$ with constants $M, α > 0$ , a functional $F \in H^{- 1} (Ω)$ , and the energy $J (v) = \frac{1}{2} a (v, v) - F (v)$ .

[A1]

The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ ): the Axiom of Choice and Countable Choice are available, as required by the obstacle setting and Hilbert-space supplier.

[F1]

The obstacle admissible set is nonempty, convex, closed and weakly closed: $K$ is nonempty, convex and closed in the norm of $H_{0}^{1} (Ω)$ , hence weakly sequentially closed.

[F2]

Stampacchia's variational inequality: for a nonempty closed convex $K \subseteq H_{0}^{1} (Ω)$ and a bounded coercive bilinear form $a$ (no symmetry needed) there is exactly one $u \in K$ with $a (u, v - u) \geq F (v - u)$ for every $v \in K$ .

[F3]

Bounded, coercive and symmetric sesquilinear forms: $a$ is bilinear and symmetric with $a (w, w) \geq α ∥ w ∥^{2} \geq 0$ and $∣ a (w_{1}, w_{2}) ∣ \leq M ∥ w_{1} ∥ ∥ w_{2} ∥$ for all $w, w_{1}, w_{2}$ ; consequently $a (u + t w, u + t w) = a (u, u) + 2 t a (u, w) + t^{2} a (w, w)$ for all real $t$ .

[F4]

The negative Sobolev space $H^{- 1} (Ω)$ : $F$ is a bounded linear functional on $H_{0}^{1} (Ω)$ , so $F$ is linear and $J$ is a real-valued function on $H_{0}^{1} (Ω)$ .

[F5]

$H^{k}$ is a Hilbert space under the derivative-sum inner product, Zero-boundary Sobolev space as a norm closure, A closed subspace of a Banach space is Banach: under the Axiom of Choice, $H^{1} (Ω; R)$ is a real Hilbert space; its closed linear subspace $H_{0}^{1} (Ω; R)$ is complete with the restricted inner product and hence is a real Hilbert space.

Proof

technique · direct

Given: The setting above, with $K$ nonempty closed convex by [F1] and $a$ symmetric bounded coercive.

1.1givenA1F1F2F5

By [F5] the space $H_{0}^{1} (Ω; R)$ is a real Hilbert space. By [F2] applied to the admissible set $K$ of [F1] there is exactly one $u^{*} \in K$ with $a (u^{*}, v - u^{*}) \geq F (v - u^{*})$ for every $v \in K$ ; call it the variational solution.

1.2givenF3F4

Every variational solution minimises $J$ on $K$ : if $u \in K$ satisfies the inequality and $v \in K$ with $w : = v - u$ , then $J (v) - J (u) = \frac{1}{2} a (v, v) - \frac{1}{2} a (u, u) - F (w) = \frac{1}{2} a (w, w) + a (u, w) - F (w)$ by the symmetry and bilinearity of [F3], and this is at least $\frac{α}{2} ∥ w ∥^{2} \geq 0$ because $a (w, w) \geq α ∥ w ∥^{2}$ and $a (u, w) - F (w) \geq 0$ by the inequality and the linearity of $F$ [F4].

1.3givenF1F3F4algebra

Every minimiser solves the variational inequality: let $u$ minimise $J$ on $K$ , let $v \in K$ , put $w : = v - u$ , and for $0 < t \leq 1$ let $v_{t} : = u + t w \in K$ , which lies in $K$ by convexity [F1]. Then $0 \leq J (v_{t}) - J (u) = t (a (u, w) - F (w)) + \frac{t^{2}}{2} a (w, w)$ by [F3, F4]. If $c : = a (u, w) - F (w)$ were negative, then $a (w, w) \geq 0$ would give $0 \leq c + \frac{t}{2} a (w, w)$ for all $t$ ; choosing $t \leq 1$ with $t a (w, w) \leq ∣ c ∣$ when $a (w, w) > 0$ , and any $t$ when $a (w, w) = 0$ , yields $c + \frac{t}{2} a (w, w) \leq c + \frac{∣ c ∣}{2} = \frac{c}{2} < 0$ , a contradiction; hence $c \geq 0$ , that is $a (u, w) \geq F (w)$ .

2.1step 1.1step 1.2step 1.3A1∎

By step 1.1 there is exactly one variational solution $u^{*}$ , and it minimises $J$ by step 1.2. Conversely, if $u \in K$ minimises $J$ , then step 1.3 makes $u$ a variational solution, hence $u = u^{*}$ by the uniqueness in step 1.1. Therefore $J$ attains its infimum on $K$ at exactly one point, namely the variational solution $u^{*}$ , and $u$ minimises $J$ if and only if $u$ solves the variational inequality; the quantitative form $J (v) - J (u^{*}) \geq \frac{α}{2} ∥ v - u^{*} ∥^{2}$ of step 1.2 makes the minimiser unique as well. Countable Choice is consumed by [F2]; the Axiom of Choice supplies the obstacle trace conventions of [F1] and the Hilbert-space prerequisite [F5].

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

John Andersson, The Obstacle Problem, KTH lecture notes, 16 December 2015 (complete 52-page notes) (standard reference, not scraped)
J. T. Oden and N. Kikuchi, Theory of variational inequalities with applications to problems of flow through porous media, International Journal of Engineering Science 18 (1980), 1173-1284 (standard reference, not scraped)