LemmaStatement: AI-adaptedProof: 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.

Weak Dirichlet existence for a prescribed lift and uniformly elliptic coefficient

Statement

Assume the Axiom of Choice (The Axiom of Choice), supplying the completeness and Countable-Choice interfaces of the two variational suppliers. Let $L > 0$ and let $Ω \subseteq (- L, L)^{3}$ be bounded and open, let $ε$ be a measurable symmetric real $3 \times 3$ matrix field on $Ω$ with $α ∣ ξ ∣^{2} \leq ξ \cdot ε (x) ξ \leq β ∣ ξ ∣^{2}$ for a.e. $x$ and all $ξ \in R^{3}$ , $0 < α \leq β < \infty$ , let $G \in H^{1} (Ω)$ be a specified lift, and let $F \in (H_{0}^{1} (Ω))^{*}$ be bounded. Then there is exactly one $u \in G + H_{0}^{1} (Ω)$ with

$\int_{Ω} \nabla v \cdot ε \nabla u = F (v) for every v \in H_{0}^{1} (Ω),$

where $H_{0}^{1} = W_{0}^{1, 2} (Ω)$ carries the gradient norm. For $F (v) = \int_{Ω} ρ v$ with $ρ \in L^{2} (Ω)$ this is the weak Poisson solution $- div (ε \nabla u) = ρ$ , with the homogeneous boundary datum represented by membership of $H_{0}^{1}$ rather than by an unproved classical trace. No boundary datum outside the specified lift class is assumed attainable; classical boundary regularity, general Neumann lifts and transmission regularity remain later obligations.

Facts & Assumptions

Given: The Axiom of Choice, $L > 0$ , a bounded open $Ω \subseteq (- L, L)^{3}$ , a uniformly elliptic symmetric measurable coefficient field $ε$ with constants $0 < α \leq β < \infty$ , a lift $G \in H^{1} (Ω)$ , a bounded functional $F$ on $H_{0}^{1} (Ω)$ with the gradient norm, and on $H_{0}^{1}$ the forms $a (w, v) = \int_{Ω} \nabla v \cdot ε \nabla w$ and $ℓ (v) = F (v) - a (G, v)$ .

[F1]

Zero-boundary coercivity. Under AC, $H_{0}^{1} (Ω)$ is complete for the full $W^{1, 2}$ norm, has the Hilbert structure of its coordinate $L^{2}$ pairings, and $∥ \nabla v ∥_{2} \leq ∥ v ∥_{W^{1, 2}} \leq (1 + (2 L)^{2})^{1 / 2} ∥ \nabla v ∥_{2}$ for $v \in H_{0}^{1}$ ; in particular the gradient norm is equivalent to the full norm and $∥ v ∥_{2} \leq 2 L ∥ \nabla v ∥_{2}$ (The gradient norm dominates the H-one norm on zero-boundary Sobolev space).

[F2]

Symmetric coercive solver. With Countable Choice, a symmetric bounded bilinear form on a real Hilbert space with $a (v, v) \geq α ∥ v ∥^{2}$ and a bounded linear functional admit a unique solution $u$ with $a (u, v) = ℓ (v)$ for all $v$ , and the solver uses no further choice (Unique solution of a symmetric coercive variational problem on a Hilbert space).

[F3]

Cauchy-Schwarz for $L^{2}$ . $\int ∣ f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ (Cauchy-Schwarz inequality for $L^{2}$ ); real $L^{2}$ with the integral pairing is a real Hilbert space ( $L^{2}$ with the integral pairing is a Hilbert space).

[F4]

Distributional derivative. For a distribution $u$ , $⟨ \partial_{j} u, φ ⟩ = - ⟨ u, \partial_{j} φ ⟩$ (Distributional derivative, Distribution); for an $L^{2}$ vector field $V$ , the distributional divergence is the functional $φ \mapsto - \sum_{j} \int V_{j} \partial_{j} φ$ , so $⟨ - div V, φ ⟩ = \int \nabla φ \cdot V$ for $φ \in C_{c}^{\infty} (Ω)$ .

Proof

technique · direct

1.1givenF1F3algebra

The gradient form $a_{0} (w, v) = \int_{Ω} \nabla w \cdot \nabla v$ is a symmetric bilinear form on $H_{0}^{1}$ with $a_{0} (v, v) = ∥ \nabla v ∥_{2}^{2}$ ; it is positive definite, because $a_{0} (v, v) = 0$ forces $\nabla v = 0$ and then $∥ v ∥_{2} \leq 2 L ∥ \nabla v ∥_{2} = 0$ by [F1], so $v = 0$ in $H_{0}^{1}$ ; the parallelogram law for $∥ \nabla v ∥_{2}$ follows from the linearity of $v \mapsto \nabla v$ and the inner-product structure of real $L^{2}$ [F3], and completeness of $H_{0}^{1}$ for the gradient norm follows from its equivalence with the complete full norm [F1]; thus $H_{0}^{1}$ with the gradient norm is a real Hilbert space.

2.1step 1.1givenF1F3algebra

The coefficient bounds make $a$ symmetric and bounded on this Hilbert space: $∣ a (w, v) ∣ \leq \int ∣ \nabla v \cdot ε \nabla w ∣ \leq β \int ∣ \nabla v ∣ ∣ \nabla w ∣ \leq β ∥ \nabla v ∥_{2} ∥ \nabla w ∥_{2}$ by the following elementary form bound and Cauchy-Schwarz [F3]: for the positive symmetric form $b_{x} (ξ, η) = ξ \cdot ε (x) η$ , nonnegativity of $b_{x} (ξ + t η, ξ + t η)$ for all real $t$ implies $∣ b_{x} (ξ, η) ∣^{2} \leq b_{x} (ξ, ξ) b_{x} (η, η) \leq β^{2} ∣ ξ ∣^{2} ∣ η ∣^{2}$ , while coercivity holds with $a (v, v) \geq α ∥ \nabla v ∥_{2}^{2}$ ; also $ℓ$ is bounded, since $∣ F (v) ∣ \leq ∥ F ∥ ∥ \nabla v ∥_{2}$ and $∣ a (G, v) ∣ \leq β ∥ \nabla G ∥_{2} ∥ \nabla v ∥_{2}$ , so $∥ ℓ ∥ \leq ∥ F ∥ + β ∥ \nabla G ∥_{2}$ .

3.1step 2.1F2algebra

Applying the symmetric coercive solver [F2] (Countable Choice is available under the AC standing hypothesis of [F1]) with coercivity constant $α$ gives a unique $w \in H_{0}^{1}$ with $a (w, v) = ℓ (v)$ for every $v \in H_{0}^{1}$ , that is $a (w, v) + a (G, v) = F (v)$ ; hence $u : = G + w$ satisfies $\int_{Ω} \nabla v \cdot ε \nabla u = F (v)$ for every $v \in H_{0}^{1}$ .

4.1step 3.1givenF1algebra

Uniqueness in the affine class: if $u_{1} = G + w_{1}$ and $u_{2} = G + w_{2}$ both solve, then subtracting the equations gives $a (w_{1} - w_{2}, v) = 0$ for all $v \in H_{0}^{1}$ ; testing with $v = w_{1} - w_{2}$ gives $α ∥ \nabla (w_{1} - w_{2}) ∥_{2}^{2} \leq a (w_{1} - w_{2}, w_{1} - w_{2}) = 0$ , so $\nabla (w_{1} - w_{2}) = 0$ and, by the Poincare bound of [F1], $w_{1} - w_{2} = 0$ in $H_{0}^{1}$ , hence $u_{1} = u_{2}$ .

5.1step 3.1F1F3F4algebra∎

Distributional form: for $F (v) = \int_{Ω} ρ v$ with $ρ \in L^{2} (Ω)$ the functional is bounded because $∣ F (v) ∣ \leq ∥ ρ ∥_{2} ∥ v ∥_{2} \leq 2 L ∥ ρ ∥_{2} ∥ \nabla v ∥_{2}$ by [F1] and [F3], so the existence conclusion applies; testing the solution identity with $v = φ \in C_{c}^{\infty} (Ω) \subseteq H_{0}^{1}$ gives $\int_{Ω} \nabla φ \cdot ε \nabla u = \int_{Ω} ρ φ$ , and since $ε \nabla u \in L^{2} (Ω; R^{3})$ the distributional divergence of [F4] satisfies $⟨ - div (ε \nabla u), φ ⟩ = \int \nabla φ \cdot ε \nabla u = \int ρ φ$ for every test function, that is $- div (ε \nabla u) = ρ$ distributionally.

The homogeneous boundary datum is membership of $u - G$ in $H_{0}^{1}$ , not a classical trace statement; an arbitrary bounded $F$ may contain interface sheet sources, so no normal-flux continuity follows for general $F$ , even when one-sided classical traces exist. Classical boundary regularity, general Neumann lifts and transmission jump laws remain later obligations.

Depends on

Dependency tree · 2 levels

Sources

J. K. Hunter, Notes on Partial Differential Equations (University of California, Davis; revised 6/18/2014), Chapters 4.1-4.5 (weak formulation, H^{-1} and existence)