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 problem with prescribed fractional Sobolev boundary data

Statement

Assume the Axiom of Choice and Countable Choice as declared by the trace and Sobolev suppliers (The Axiom of Choice). Let $Ω \subset R^{3}$ be a bounded $C^{1}$ domain, let $ε$ be a measurable symmetric uniformly elliptic coefficient as in the lift lemma (Weak Dirichlet existence for a prescribed lift and uniformly elliptic coefficient), let $ρ \in L^{2} (Ω)$ , and prescribe $g \in H^{1 / 2} (\partial Ω) = W^{1 / 2, 2} (\partial Ω)$ , the fractional Sobolev space of the boundary definition, defined by a finite graph atlas and partition with norm given by the finite sums of localised $L^{2}$ norms and Gagliardo seminorms (The fractional Sobolev space on a compact $C^{1}$ boundary, The $L^{p}$ trace operator on a bounded $C^{1}$ domain). Then there is exactly one $u \in H^{1} (Ω)$ with trace $T u = g$ solving

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

and the solution depends continuously on $(ρ, g)$ : $∥ u ∥_{H^{1}} \leq C (∥ ρ ∥_{L^{2}} + ∥ g ∥_{H^{1 / 2}})$ . The prescribed trace is exact and no classical $C^{2}$ boundary regularity is inferred.

Facts & Assumptions

Given: A bounded $C^{1}$ domain $Ω \subseteq (- L, L)^{3}$ with trace operator $T$ , a uniformly elliptic coefficient $ε$ with constants $0 < α \leq β < \infty$ , data $ρ \in L^{2} (Ω)$ and $g \in H^{1 / 2} (\partial Ω)$ , and the weak equation of the Statement.

[F1]

Sharp trace and bounded right inverse. Under the Axiom of Choice, $T : W^{1, 2} (Ω) \to W^{1 / 2, 2} (\partial Ω)$ is bounded and onto (The sharp trace theorem: boundedness and range in the fractional space), and there is a bounded linear right inverse $R : H^{1 / 2} (\partial Ω) \to H^{1} (Ω)$ with $T R g = g$ and $∥ R g ∥_{H^{1}} \leq C ∥ g ∥_{H^{1 / 2}}$ (A bounded right inverse of the trace, supported in a prescribed collar); the fractional space is defined by the finite chart/Gagliardo construction (The fractional Sobolev space on a compact $C^{1}$ boundary).

[F2]

Trace kernel. ${u \in W^{1, 2} (Ω) : T u = 0} = H_{0}^{1} (Ω)$ (The kernel of the trace is the closure of the test functions, The Axiom of Choice).

[F3]

Lift existence and integral bound. For every specified lift $G \in H^{1} (Ω)$ and bounded $F$ on $H_{0}^{1}$ , there is a unique $u \in G + H_{0}^{1}$ with $\int \nabla v \cdot ε \nabla u = F (v)$ for all $v \in H_{0}^{1}$ (Weak Dirichlet existence for a prescribed lift and uniformly elliptic coefficient). Cauchy-Schwarz gives $∣ \int f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ (Cauchy-Schwarz inequality for $L^{2}$ ). For the positive symmetric pointwise form $b_{x} (ξ, η) = ξ \cdot ε (x) η$ , nonnegativity of $b_{x} (ξ + t η, ξ + t η)$ for all $t \in R$ gives $∣ b_{x} (ξ, η) ∣ \leq β ∣ ξ ∣ ∣ η ∣$ . Thus $∣ a (G, v) ∣ \leq β ∥ \nabla G ∥_{2} ∥ \nabla v ∥_{2}$ .

[F4]

Zero-boundary coercivity. Under AC and $Ω \subseteq (- L, L)^{3}$ , $H_{0}^{1}$ is a complete Hilbert space, $∥ v ∥_{2} \leq 2 L ∥ \nabla v ∥_{2}$ and $∥ \nabla v ∥_{2} \leq ∥ v ∥_{H^{1}} \leq \sqrt{1 + (2 L)^{2}} ∥ \nabla v ∥_{2}$ for $v \in H_{0}^{1}$ (The gradient norm dominates the H-one norm on zero-boundary Sobolev space). In particular $∣ \int ρ v ∣ \leq 2 L ∥ ρ ∥_{2} ∥ \nabla v ∥_{2}$ by [F3].

Proof

technique · direct

1.1givenF1algebra

By [F1] choose the bounded right inverse $R$ and put $G = R g \in H^{1} (Ω)$ ; then $T G = T (R g) = g$ , so $G$ is an exact $H^{1}$ lift of the prescribed fractional datum.

2.1step 1.1F2algebra

A function $u \in H^{1} (Ω)$ satisfies $T u = g$ exactly when $u - G \in H_{0}^{1} (Ω)$ : indeed $T (u - G) = g - g = 0$ is equivalent to $u - G \in H_{0}^{1}$ by [F2].

3.1step 1.1step 2.1F3F4algebra

Apply the lift existence theorem [F3] with the specified lift $G = R g$ and the functional $F (v) = \int ρ v$ : there is a unique $u = G + w$ , $w \in H_{0}^{1}$ , with $\int \nabla v \cdot ε \nabla u = F (v)$ for every $v \in H_{0}^{1}$ ; by step 2.1 its trace is exactly $g$ , and uniqueness of $w$ gives uniqueness of $u$ among $H^{1}$ functions with trace $g$ solving the equation.

4.1step 3.1F1F3F4algebra

Continuous dependence: for two data sets $(ρ_{i}, g_{i})$ , $i = 1, 2$ , put $G_{i} = R g_{i}$ and $w_{i} = u_{i} - G_{i}$ ; subtracting the weak equations and testing with $v = w_{1} - w_{2}$ gives $α ∥ \nabla (w_{1} - w_{2}) ∥_{2}^{2} \leq (2 L ∥ ρ_{1} - ρ_{2} ∥_{2} + β ∥ \nabla R (g_{1} - g_{2}) ∥_{2}) ∥ \nabla (w_{1} - w_{2}) ∥_{2}$ by [F3] and [F4], hence $∥ \nabla (w_{1} - w_{2}) ∥_{2} \leq α^{- 1} (2 L ∥ ρ_{1} - ρ_{2} ∥_{2} + β ∥ \nabla R (g_{1} - g_{2}) ∥_{2})$ ; adding $∥ R (g_{1} - g_{2}) ∥_{H^{1}} \leq C ∥ g_{1} - g_{2} ∥_{H^{1 / 2}}$ by [F1] and using the equivalence of the gradient and full norms on $H_{0}^{1}$ [F4] yields the stated bound $∥ u ∥_{H^{1}} \leq C (∥ ρ ∥_{2} + ∥ g ∥_{H^{1 / 2}})$ with the case $(ρ_{2}, g_{2}) = (0, 0)$ .

5.1step 3.1step 4.1F1algebra∎

The prescribed trace is membership in the affine class $G + H_{0}^{1}$ and its identification $T u = g$ through the bounded trace operator [F1], not a classical $C^{2}$ boundary regularity statement; this proves existence, exactness of the trace, uniqueness and continuous dependence.

Depends on

Dependency tree · 2 levels

Sources

J. K. Hunter, Notes on Partial Differential Equations (University of California, Davis; revised 6/18/2014), Chapter 4 (weak formulations, H^{-1}) and Chapter 3.9 (boundary values of Sobolev functions)