TheoremStatement: 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.

Interior $H^{2}$ regularity for divergence-form equations

Statement

Assume Countable Choice. Let $Ω \subseteq R^{n}$ be open, $n \geq 1$ , $K \in {R, C}$ , let $L, a$ be as in Uniformly elliptic divergence-form operators and their sesquilinear forms with constants $θ, M_{a}, M_{b}, M_{c}$ and with $a^{i j} \in W^{1, \infty} (Ω)$ satisfying $∥ D a^{i j} ∥_{\infty} \leq M_{1}$ , and let $f \in L_{l o c}^{2} (Ω)$ . If $u \in H^{1} (Ω)$ is a local weak solution of $L u = f$ on $Ω$ (Local weak solutions of a divergence-form operator), then $u \in H_{l o c}^{2} (Ω)$ , and for all open sets $Ω^{'} ⋐ Ω^{''} ⋐ Ω$ there is $C = C (n, θ, M_{a}, M_{b}, M_{c}, M_{1}, Ω^{'}, Ω^{''})$ with $∥ u ∥_{H^{2} (Ω^{'})} \leq C (∥ f ∥_{L^{2} (Ω^{''})} + ∥ u ∥_{L^{2} (Ω^{''})}) .$ Consequently the equation $L u = f$ holds pointwise almost everywhere with $D_{i} (a^{i j} D_{j} u)$ understood through the a.e. defined product $(D_{i} a^{i j}) D_{j} u + a^{i j} D_{i} D_{j} u$ , and the same estimate holds for complex-valued $u$ by taking real parts in the coercive energy bounds; no splitting of complex coefficients into real and imaginary equations is used. The scaffold wrote $∥ f ∥_{L^{2} (Ω)} + ∥ u ∥_{L^{2} (Ω)}$ on the right-hand side, which is ill-posed for a datum known only to lie in $L_{l o c}^{2} (Ω)$ (for instance $f = 1 / x$ on $Ω = (0, 1)$ is locally but not globally square-integrable); the nested formulation above is the well-posed local statement, and the quantitative content is otherwise unchanged.

Facts & Assumptions

Given: Countable Choice; the open set $Ω$ ; coefficients $a^{i j} \in W^{1, \infty} (Ω)$ with $∥ D a^{i j} ∥_{\infty} \leq M_{1}$ and the bounds and ellipticity of $L$ ; the datum $f \in L_{l o c}^{2} (Ω)$ ; and a local weak solution $u \in H^{1} (Ω)$ of $L u = f$ .

[F1]

Local weak solution: $a (u, φ) = \int_{Ω} f \overline{φ} d x$ for every $φ \in C_{c}^{\infty} (Ω)$ . (Local weak solutions of a divergence-form operator)

[F2]

Coefficient package: $∣ a^{i j} ∣ \leq M_{a}$ , $∣ b^{i} ∣ \leq M_{b}$ , $∣ c ∣ \leq M_{c}$ , $∣ D_{k} a^{i j} ∣ \leq M_{1}$ almost everywhere, and $Re (a^{i j} ξ_{j} \overline{ξ_{i}}) \geq θ ∣ ξ ∣^{2}$ . (Uniformly elliptic divergence-form operators and their sesquilinear forms)

[F3]

Localised difference-quotient pairing. Choose nested open sets $Ω^{'} ⋐ U_{1} ⋐ U_{2} ⋐ Ω^{''}$ and $η \in C_{c}^{\infty} (U_{2}; R)$ with $η = 1$ on $U_{1}$ . For sufficiently small $h \neq 0$ and a coordinate $k$ , the test $v = - δ_{- h}^{k} (η^{2} δ_{h}^{k} u)$ belongs to $H_{0}^{1} (U_{2})$ , and the local weak identity extends to it by density. Discrete integration by parts in the principal part gives $P_{h} + R_{a, h}$ , where $P_{h} = \int η^{2} a^{i j} (x + h e_{k}) (δ_{h}^{k} D_{j} u) \overline{(δ_{h}^{k} D_{i} u)}$ and $Re P_{h} \geq θ E_{h}$ for $E_{h} : = \int η^{2} ∣ δ_{h}^{k} D u ∣^{2}$ . The remainder contains only cutoff terms and first difference quotients of $a^{i j}$ ; since $a^{i j} \in W^{1, \infty}$ , $∣ δ_{h}^{k} a^{i j} ∣ \leq M_{1}$ , and for every $ε > 0$ , $∣ R_{a, h} ∣ \leq ε E_{h} + C_{ε} (∥ u ∥_{L^{2} (U_{2})}^{2} + ∥ D u ∥_{L^{2} (U_{2})}^{2})$ , uniformly in small $h$ . Furthermore, $∥ v ∥_{L^{2} (U_{2})} \leq C_{η} (E_{h}^{1 / 2} + ∥ D u ∥_{L^{2} (U_{2})})$ by $∥ δ_{- h} w ∥_{2} \leq ∥ D_{k} w ∥_{2}$ and the product rule. Therefore the lower-order and source pairings, estimated without differencing $b^{i}$ or $c$ , satisfy $∣ \int_{U_{2}} (b^{i} D_{i} u + c u - f) \overline{v} ∣ \leq ε E_{h} + C_{ε} (∥ D u ∥_{L^{2} (U_{2})}^{2} + ∥ u ∥_{L^{2} (U_{2})}^{2} + ∥ f ∥_{L^{2} (U_{2})}^{2})$ . (Local weak solutions of a divergence-form operator, The difference-quotient test function and its commutators, Young's inequality for conjugate real exponents, Holder's inequality for integrals, including the endpoint cases)

[F4]

Local Caccioppoli control on nested bounded sets. If $U_{2}$ is bounded with $\overline{U_{2}} ⋐ U_{3} ⋐ Ω$ , cover $\overline{U_{2}}$ by finitely many inner balls $B_{r_{ℓ}}$ whose concentric outer balls $B_{R_{ℓ}}$ are compactly contained in $U_{3}$ . Applying the ball Caccioppoli estimate on each pair and summing gives $∥ D u ∥_{L^{2} (U_{2})}^{2} \leq C (∥ u ∥_{L^{2} (U_{3})}^{2} + ∥ f ∥_{L^{2} (U_{3})}^{2})$ , with $C$ allowed to depend on the finite cover, hence on $U_{2}, U_{3}$ , as well as $n, θ, M_{a}, M_{b}, M_{c}$ (Scaled Caccioppoli inequality on concentric balls).

[F5]

Difference-quotient characterisation of $W^{1, p}$ , $1 < p < \infty$ : $∥ δ_{h}^{i} u ∥_{L^{p} (Ω_{1})} \leq ∥ D_{i} u ∥_{L^{p} (Ω_{2})}$ for $u \in W^{1, p} (Ω_{2})$ and $0 < ∣ h ∣ < dist (Ω_{1}, \partial Ω_{2})$ , and conversely a uniform bound $∥ δ_{h}^{i} u ∥_{L^{p} (Ω_{1})} \leq C$ for $0 < ∣ h ∣ < dist (Ω_{1}, \partial Ω_{2}) / 2$ implies $D_{i} u \in L^{p} (Ω_{1})$ with $∥ D_{i} u ∥_{L^{p} (Ω_{1})} \leq C$ . (The difference-quotient characterisation of $W^{1, p}$ for $1 < p < \infty$ , Uniformly bounded difference quotients represent a weak derivative).

[F6]

Young and Cauchy--Schwarz inequalities with a free $ε > 0$ . (Young's inequality for conjugate real exponents, Holder's inequality for integrals, including the endpoint cases)

[F7]

If $h \in L^{2} (Ω)$ satisfies $\int_{Ω} h \overline{φ} d x = 0$ for every $φ \in C_{c}^{\infty} (Ω)$ , then $h = 0$ ; more generally $C_{c}^{\infty} (Ω)$ is dense in $L^{2} (Ω)$ . (Smooth compactly supported functions of an open set are dense in $L^{2}$ )

Proof

technique · direct

1.1F1F3

Nested localization. Fix $Ω^{'} ⋐ Ω^{''} ⋐ Ω$ and choose $Ω^{'} ⋐ U_{1} ⋐ U_{2} ⋐ Ω^{''}$ . Take $η \in C_{c}^{\infty} (U_{2}; R)$ equal to one on $U_{1}$ . For each coordinate $k$ and sufficiently small $h \neq 0$ , the test class $v = - δ_{- h}^{k} (η^{2} δ_{h}^{k} u)$ is supported in $U_{2}$ and belongs to $H_{0}^{1} (U_{2})$ ; the weak identity extends from smooth tests to $v$ by density, since the form is bounded and $f \in L^{2} (U_{2})$ .

1.2F2F3F6algebra

Principal and lower-order terms. Write the principal pairing as $P_{h} + R_{a, h}$ as in [F3]. The weak equation gives $P_{h} + R_{a, h} = \int_{U_{2}} (f - b^{i} D_{i} u - c u) \overline{v}$ , so taking real parts and using [F3] bounds the right side directly, without differentiating $b^{i}$ or $c$ . Choosing $ε$ small relative to $θ$ and absorbing the error terms into $Re P_{h} \geq θ E_{h}$ gives $E_{h} \leq C (∥ u ∥_{L^{2} (U_{2})}^{2} + ∥ D u ∥_{L^{2} (U_{2})}^{2} + ∥ f ∥_{L^{2} (U_{2})}^{2}),$ with $C = C (n, θ, M_{a}, M_{b}, M_{c}, M_{1}, U_{1}, U_{2})$ , uniformly in sufficiently small $h$ . This estimate uses derivatives only of the principal coefficients; $b, c \in L^{\infty}$ enter without being differentiated. Young's inequality and Cauchy--Schwarz [F6] absorb the energy errors.

2.1F4step 1.2algebra

Removing the intermediate gradient. The Caccioppoli estimate [F4] applied to $U_{2} ⋐ Ω^{''}$ gives $∥ D u ∥_{L^{2} (U_{2})}^{2} \leq C (∥ u ∥_{L^{2} (Ω^{''})}^{2} + ∥ f ∥_{L^{2} (Ω^{''})}^{2})$ . Substitution into step 1.2 yields $E_{h} \leq C (∥ u ∥_{L^{2} (Ω^{''})}^{2} + ∥ f ∥_{L^{2} (Ω^{''})}^{2})$ uniformly in $h$ .

3.1F5step 2.1algebra

Recovering all second derivatives. Since $η = 1$ on $U_{1}$ and $Ω^{'} ⋐ U_{1}$ , step 2.1 bounds $∥ δ_{h}^{k} D_{j} u ∥_{L^{2} (Ω^{'})}$ uniformly for every $j, k$ . Applying the directional weak-limit criterion cited in [F5] with any positive threshold below the actual cutoff-support margin gives $D_{k} D_{j} u \in L^{2} (Ω^{'})$ with the same bound. Summing over $j, k$ proves $u \in H^{2} (Ω^{'})$ and $∥ u ∥_{H^{2} (Ω^{'})} \leq C (∥ f ∥_{L^{2} (Ω^{''})} + ∥ u ∥_{L^{2} (Ω^{''})})$ .

4.1step 3.1F1F7algebra

The strong form and the equation a.e. On $Ω^{'}$ , $u \in H^{2}$ by step 3.1, so the proved multiplier rule of The cutoff difference-quotient commutator estimate gives $a^{i j} D_{j} u \in H^{1} (Ω^{'})$ with weak derivative $(D_{i} a^{i j}) D_{j} u + a^{i j} D_{i} D_{j} u \in L^{2} (Ω^{'})$ . For every $φ \in C_{c}^{\infty} (Ω^{'})$ , integration by parts in [F1] gives $\int_{Ω^{'}} (f - (- D_{i} (a^{i j} D_{j} u) + b^{i} D_{i} u + c u)) \overline{φ} d x = 0$ . The bracket lies in $L^{2} (Ω^{'})$ , so it vanishes a.e. there by [F7]; as the pair $Ω^{'} ⋐ Ω^{''} ⋐ Ω$ was arbitrary, the equation $L u = f$ holds pointwise almost everywhere on $Ω$ with $D_{i} (a^{i j} D_{j} u)$ read as the a.e. product $(D_{i} a^{i j}) D_{j} u + a^{i j} D_{i} D_{j} u$ .

5.1step 3.1step 4.1∎

Conclusion. Every $u \in H^{1} (Ω)$ that solves $L u = f$ locally with $L$ uniformly elliptic, $a^{i j} \in W^{1, \infty} (Ω)$ and $f \in L_{l o c}^{2} (Ω)$ lies in $H_{l o c}^{2} (Ω)$ with the nested-domain estimate displayed in the Statement. The argument applies directly to complex-valued data and solutions by taking real parts in the coercive energy estimates, as in step 1.2.

Source notes

Hunter's Theorem 4.27 (printed pp. 112-113) assumes $C^{1}$ principal coefficients and proves interior $H^{2}$ regularity by difference quotients. The local proof above supplies the $W^{1, \infty}$ version and permits bounded lower-order coefficients. Laugesen's Theorem 5.6 (printed pp. 108-110) gives the constant-coefficient core. The scaffold's right-hand side $∥ f ∥_{L^{2} (Ω)}$ is not defined for $f \in L_{l o c}^{2} (Ω)$ when $Ω$ is unbounded or when $f$ blows up at a boundary point, as $f = 1 / x$ on $(0, 1)$ shows; the repaired statement uses the standard nested domains $Ω^{'} ⋐ Ω^{''} ⋐ Ω$ , matching the $L_{l o c}^{2}$ hypothesis and the estimates actually proved.

Interior $H^{2}$ regularity for divergence-form equations

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources

Interior H2H2 regularity for divergence-form equations

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources

Interior $H^{2}$ regularity for divergence-form equations