CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

The inhomogeneous weak Dirichlet problem by a trace lifting

Statement

Assume the Axiom of Choice (through the published Sobolev trace results) together with Countable Choice. Let $Ω \subset R^{n}$ , $n \geq 2$ , be a bounded $C^{1}$ domain, let $g \in H^{1 / 2} (\partial Ω) = W^{1 / 2, 2} (\partial Ω)$ and $F \in H^{- 1} (Ω)$ , and let $a$ be the divergence form of Uniformly elliptic divergence-form operators and their sesquilinear forms satisfying the coercivity condition of Lax--Milgram solvability for coercive divergence-form equations on $H_{0}^{1} (Ω)$ ; write $α : = α_{0} / (1 + C_{P}^{2}) > 0$ for its coercivity constant, where $α_{0} = θ - \sqrt{n} C_{P} M_{b} - C_{P}^{2} M_{c}$ . Fix a bounded right inverse $R : H^{1 / 2} (\partial Ω) \to H^{1} (Ω)$ of the trace, $T \circ R = i d$ , as in A bounded right inverse of the trace, supported in a prescribed collar. Then there is a unique $u \in H^{1} (Ω)$ with $T u = g and a (u, v) = F (v) for every v \in H_{0}^{1} (Ω),$ and with $C_{a} = n M_{a} + n M_{b} + M_{c}$ the bound of The elliptic form is well defined and bounded on $H^{1}$ on all of $H^{1}$ , $∥ u ∥_{H^{1}} \leq ∥ R g ∥_{H^{1}} + \frac{∥ F ∥_{H^{- 1}} + C_{a} ∥ R g ∥_{H^{1}}}{α} \leq C (Ω, a, R) (∥ g ∥_{W^{1 / 2, 2}} + ∥ F ∥_{H^{- 1}}) .$ The solution is independent of the choice of lifting; the displayed estimate depends on the fixed right inverse $R$ . Boundary data outside the trace range $H^{1 / 2} (\partial Ω)$ are not admissible: no $H^{1}$ function has such a trace, the trace range being exactly $H^{1 / 2} (\partial Ω)$ (The sharp trace theorem: boundedness and range in the fractional space).

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; a bounded $C^{1}$ domain $Ω \subset R^{n}$ , $n \geq 2$ ; boundary data $g \in H^{1 / 2} (\partial Ω) = W^{1 / 2, 2} (\partial Ω)$ ; $F \in H^{- 1} (Ω)$ ; a divergence form $a$ on $H^{1} (Ω)$ whose restriction to $H_{0}^{1} (Ω)$ satisfies the coercivity condition of Lax--Milgram solvability for coercive divergence-form equations with $α = α_{0} / (1 + C_{P}^{2}) > 0$ , $α_{0} = θ - \sqrt{n} C_{P} M_{b} - C_{P}^{2} M_{c}$ , and bounded with constant $C_{a}$ ; and a bounded right inverse $R$ of the trace $T$ with $T \circ R = i d$ .

[F1]

The trace operator $T : H^{1} (Ω) \to H^{1 / 2} (\partial Ω)$ is bounded and its kernel is exactly $H_{0}^{1} (Ω)$ (The kernel of the trace is the closure of the test functions, The fractional Sobolev space on a compact $C^{1}$ boundary, Bounded C^k domains and boundary charts).

[F2]

The right inverse satisfies $T (R g) = g$ and $∥ R g ∥_{H^{1}} \leq ∥ R ∥ ∥ g ∥_{W^{1 / 2, 2}}$ (A bounded right inverse of the trace, supported in a prescribed collar, Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure).

[F3]

The divergence-form solvability theorem: for every datum in $H^{- 1} (Ω)$ there is a unique $w \in H_{0}^{1} (Ω)$ with $a (w, v) = G (v)$ for all $v \in H_{0}^{1} (Ω)$ , satisfying $∥ w ∥_{H_{0}^{1}} \leq ∥ G ∥_{H^{- 1}} / α$ (Lax--Milgram solvability for coercive divergence-form equations, Weak Dirichlet solutions for a divergence-form operator).

[F4]

Boundedness on all $H^{1}$ slots: with $C_{a} = n M_{a} + n M_{b} + M_{c}$ , $∣ a (u, v) ∣ \leq C_{a} ∥ u ∥_{H^{1}} ∥ v ∥_{H^{1}}$ for every $u, v \in H^{1} (Ω)$ (The elliptic form is well defined and bounded on $H^{1}$ , The negative Sobolev space $H^{- 1} (Ω)$ , Complex Lp classes and Euclidean test-function conventions, Holder's inequality for integrals, including the endpoint cases).

[F5]

Admissibility is exactly trace-range membership: the trace operator $T : H^{1} (Ω) \to H^{1 / 2} (\partial Ω)$ has range exactly $H^{1 / 2} (\partial Ω)$ (The $L^{p}$ trace operator on a bounded $C^{1}$ domain, The sharp trace theorem: boundedness and range in the fractional space, The fractional Sobolev space on a compact $C^{1}$ boundary), so a datum outside $H^{1 / 2} (\partial Ω)$ is the trace of no $H^{1}$ function and the inhomogeneous problem admits no solution for it.

Proof

1.1F2F4algebra

Lift and shift: put $u_{0} : = R g$ , so $T u_{0} = g$ and $∥ u_{0} ∥_{H^{1}} \leq ∥ R ∥ ∥ g ∥$ ; define $\tilde{F} (v) : = F (v) - a (u_{0}, v)$ for $v \in H_{0}^{1} (Ω)$ . Then $\tilde{F}$ is conjugate-linear, and by [F4] $∥ \tilde{F} ∥_{H^{- 1}} \leq ∥ F ∥_{H^{- 1}} + C_{a} ∥ u_{0} ∥_{H^{1}} .$

2.1F3step 1.1

Zero-boundary correction: by [F3] applied to $\tilde{F}$ there is a unique $w \in H_{0}^{1} (Ω)$ with $a (w, v) = \tilde{F} (v)$ for all $v \in H_{0}^{1} (Ω)$ , and $∥ w ∥_{H^{1}} \leq ∥ \tilde{F} ∥_{H^{- 1}} / α$ .

3.1F1step 2.1algebra

The sum solves the inhomogeneous problem: let $u : = u_{0} + w$ . Since $w \in H_{0}^{1} (Ω) = \ker T$ by [F1], $T u = T u_{0} + T w = g$ . For $v \in H_{0}^{1} (Ω)$ , additivity of $a$ in the first slot gives $a (u, v) = a (u_{0}, v) + a (w, v) = a (u_{0}, v) + \tilde{F} (v) = F (v)$ .

3.2F2step 1.1step 2.1algebra

Estimate: $∥ u ∥_{H^{1}} \leq ∥ u_{0} ∥_{H^{1}} + ∥ w ∥_{H^{1}} \leq ∥ R g ∥_{H^{1}} + (∥ F ∥_{H^{- 1}} + C_{a} ∥ R g ∥_{H^{1}}) / α$ , and the right-inverse bound $∥ R g ∥_{H^{1}} \leq ∥ R ∥ ∥ g ∥_{W^{1 / 2, 2}}$ makes the right-hand side at most $C (Ω, a, R) (∥ g ∥_{W^{1 / 2, 2}} + ∥ F ∥_{H^{- 1}})$ for an explicit constant depending only on $Ω$ , $a$ and $R$ .

4.1F1step 3.1

Uniqueness independent of the lifting: if $u_{1}, u_{2}$ are solutions, then $z : = u_{1} - u_{2}$ has $T z = 0$ , so $z \in H_{0}^{1} (Ω)$ by [F1], and $a (z, v) = 0$ for every $v \in H_{0}^{1} (Ω)$ . Testing $v = z$ and using coercivity gives $α ∥ z ∥_{H^{1}}^{2} \leq Re a (z, z) = 0$ , so $z = 0$ .

5.1F5given∎

Admissibility: the construction needs $g$ in the trace range; by [F5] a datum outside $H^{1 / 2} (\partial Ω)$ is the trace of no $H^{1}$ function, so the inhomogeneous problem has no solution for it and the trace-range hypothesis cannot be dropped.

Depends on

Used by

Weak solutions depend continuously on the data Corollary
Smooth interior data do not repair incompatible Dirichlet corner values Counterexample
Regularity estimates do not create boundary compatibility Remark
Global Schauder regularity for the weak Dirichlet Laplacian Theorem
The Dirichlet principle for the Poisson equation Theorem

Dependency tree · two levels

95 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 K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes) (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)