CorollaryStatement: Literature-sourcedProof: 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.

Weak solutions depend continuously on the data

Statement

Assume the Axiom of Choice and Countable Choice, and take the hypotheses of The inhomogeneous weak Dirichlet problem by a trace lifting with one fixed right inverse $R$ and coercivity constant $α = α_{0} / (1 + C_{P}^{2})$ (the constant displayed there, where $α_{0} = θ - \sqrt{n} C_{P} M_{b} - C_{P}^{2} M_{c}$ ). If $u_{i}$ solve the weak Dirichlet problems with data $(F_{i}, g_{i}) \in H^{- 1} (Ω) \times H^{1 / 2} (\partial Ω)$ , $i = 1, 2$ , then $∥ u_{1} - u_{2} ∥_{H^{1}} \leq (1 + \frac{C_{a}}{α}) ∥ R (g_{1} - g_{2}) ∥_{H^{1}} + \frac{∥ F_{1} - F_{2} ∥_{H^{- 1}}}{α} \leq C (Ω, a) (∥ F_{1} - F_{2} ∥_{H^{- 1}} + ∥ g_{1} - g_{2} ∥_{W^{1 / 2, 2}}),$ where $C_{a} = n M_{a} + n M_{b} + M_{c}$ is the full $H^{1}$ bound of the form and $C (Ω, a)$ depends only on the domain, the coefficients, the coercivity constant and the fixed right inverse. Thus the solution map is Lipschitz on the product of the data spaces, and $u_{1} = u_{2}$ when the data agree.

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; a bounded $C^{1}$ domain $Ω \subset R^{n}$ , $n \geq 2$ ; a divergence form $a$ bounded on $H^{1} (Ω)$ with constant $C_{a}$ and coercive on $H_{0}^{1} (Ω)$ with constant $α > 0$ ; a fixed bounded right inverse $R$ of the trace with $T \circ R = i d$ ; and solutions $u_{1}, u_{2} \in H^{1} (Ω)$ of the weak problems with data $(F_{i}, g_{i})$ .

[F1]

Each $u_{i}$ satisfies $T u_{i} = g_{i}$ and $a (u_{i}, v) = F_{i} (v)$ for every $v \in H_{0}^{1} (Ω)$ , and solve the problem via the lifting construction: $u_{i} = R g_{i} + w_{i}$ with $w_{i} \in H_{0}^{1} (Ω)$ (The inhomogeneous weak Dirichlet problem by a trace lifting, Weak Dirichlet solutions for a divergence-form operator).

[F2]

Linearity and boundedness: the same $C_{a}$ from The elliptic form is well defined and bounded on $H^{1}$ bounds $a$ on all of $H^{1} (Ω) \times H^{1} (Ω)$ , and hence also on the restriction to $H_{0}^{1} (Ω)$ . Thus $v \mapsto (F_{1} - F_{2}) (v) - a (R (g_{1} - g_{2}), v)$ is a bounded conjugate-linear functional on $H_{0}^{1} (Ω)$ of norm at most $∥ F_{1} - F_{2} ∥_{H^{- 1}} + C_{a} ∥ R (g_{1} - g_{2}) ∥_{H^{1}}$ (The negative Sobolev space $H^{- 1} (Ω)$ , The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F3]

A priori bound: any $w \in H_{0}^{1} (Ω)$ with $a (w, v) = \tilde{F} (v)$ for all $v \in H_{0}^{1} (Ω)$ satisfies $α ∥ w ∥_{H^{1}} \leq ∥ \tilde{F} ∥_{H^{- 1}}$ (Testing a coercive weak solution with itself gives the energy bound, Lax--Milgram solvability for coercive divergence-form equations).

[F4]

Right-inverse bound: $∥ R (g_{1} - g_{2}) ∥_{H^{1}} \leq ∥ R ∥ ∥ g_{1} - g_{2} ∥_{W^{1 / 2, 2}}$ (A bounded right inverse of the trace, supported in a prescribed collar, The fractional Sobolev space on a compact $C^{1}$ boundary, Integer-order Sobolev spaces and their norms).

[F5]

The abstract estimate is the operator-norm bound for the Lax--Milgram solution operator (The Lax--Milgram solution operator has norm at most $1 / α$ , The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

Proof

1.1F1F2algebra

The difference solves a shifted problem: put $g : = g_{1} - g_{2}$ , $F : = F_{1} - F_{2}$ and $w : = (u_{1} - u_{2}) - R g$ . Then $T w = T (u_{1} - u_{2}) - T R g = g_{1} - g_{2} - g = 0$ , so $w \in H_{0}^{1} (Ω)$ , and for every $v \in H_{0}^{1} (Ω)$ first-slot linearity gives $a (w, v) = a (u_{1}, v) - a (u_{2}, v) - a (R g, v) = F (v) - a (R g, v) = : \tilde{F} (v) .$

1.2F2

Bound on the shifted datum: by [F2] the functional $\tilde{F}$ is bounded and conjugate-linear with $∥ \tilde{F} ∥_{H^{- 1}} \leq ∥ F ∥_{H^{- 1}} + C_{a} ∥ R g ∥_{H^{1}}$ .

2.1F3F4step 1.2algebra

Energy estimate and conclusion: the a priori bound [F3] applied to $w$ and $\tilde{F}$ gives $∥ w ∥_{H^{1}} \leq ∥ \tilde{F} ∥_{H^{- 1}} / α$ , hence by the triangle inequality and [F4] $∥ u_{1} - u_{2} ∥_{H^{1}} \leq ∥ R g ∥_{H^{1}} + \frac{∥ F ∥_{H^{- 1}} + C_{a} ∥ R g ∥_{H^{1}}}{α} \leq (1 + \frac{C_{a}}{α}) ∥ R ∥ ∥ g_{1} - g_{2} ∥_{W^{1 / 2, 2}} + \frac{∥ F_{1} - F_{2} ∥_{H^{- 1}}}{α},$ which is the first display; the second follows by absorbing $1 + C_{a} / α$ and $∥ R ∥$ into the constant $C (Ω, a)$ . If the data agree then $g = 0$ , $F = 0$ , $\tilde{F} = 0$ and $w = 0$ , so $u_{1} = u_{2}$ .

3.1F5step 2.1∎

Operator form: the same estimate is the statement that the solution map $(F, g) \mapsto u$ is Lipschitz on $H^{- 1} (Ω) \times H^{1 / 2} (\partial Ω)$ with the displayed constant; the abstract mechanism is the norm bound $∥ S ∥ \leq 1 / α$ for the Lax--Milgram solution operator on the zero-boundary part.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

60 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

Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)