Alphabeta Math
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 H2 regularity for divergence-form equations

Statement

Assume Countable Choice. Let Ω⊆Rn be open, n≥1, K∈{R,C}, let L,a be as in Uniformly elliptic divergence-form operators and their sesquilinear forms with constants θ,Ma,Mb,Mc and with aij∈W1,∞(Ω) satisfying ∥Daij∥∞≤M1, and let f∈Lloc2(Ω). If u∈H1(Ω) is a local weak solution of Lu=f on Ω (Local weak solutions of a divergence-form operator), then u∈Hloc2(Ω), and for all open sets Ω′⋐Ω′′⋐Ω there is C=C(n,θ,Ma,Mb,Mc,M1,Ω′,Ω′′) with ∥u∥H2(Ω′)≤C(∥f∥L2(Ω′′)+∥u∥L2(Ω′′)). Consequently the equation Lu=f holds pointwise almost everywhere with Di(aijDju) understood through the a.e. defined product (Diaij)Dju+aijDiDju, 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∥L2(Ω)+∥u∥L2(Ω) on the right-hand side, which is ill-posed for a datum known only to lie in Lloc2(Ω) (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 aij∈W1,∞(Ω) with ∥Daij∥∞≤M1 and the bounds and ellipticity of L; the datum f∈Lloc2(Ω); and a local weak solution u∈H1(Ω) of Lu=f.

[F1]

Local weak solution: a(u,φ)=∫Ωfφ‾ dx for every φ∈Cc∞(Ω). (Local weak solutions of a divergence-form operator)

[F2]

Coefficient package: ∣aij∣≤Ma, ∣bi∣≤Mb, ∣c∣≤Mc, ∣Dkaij∣≤M1 almost everywhere, and Re⁡(aijξjξi‾)≥θ∣ξ∣2. (Uniformly elliptic divergence-form operators and their sesquilinear forms)

[F3]

Localised difference-quotient pairing. Choose nested open sets Ω′⋐U1⋐U2⋐Ω′′ and η∈Cc∞(U2;R) with η=1 on U1. For sufficiently small h≠0 and a coordinate k, the test v=−δ−hk(η2δhku) belongs to H01(U2), and the local weak identity extends to it by density. Discrete integration by parts in the principal part gives Ph+Ra,h, where Ph=∫η2aij(x+hek)(δhkDju)(δhkDiu)‾ and Re⁡Ph≥θEh for Eh:=∫η2∣δhkDu∣2. The remainder contains only cutoff terms and first difference quotients of aij; since aij∈W1,∞, ∣δhkaij∣≤M1, and for every ε>0, ∣Ra,h∣≤εEh+Cε(∥u∥L2(U2)2+∥Du∥L2(U2)2), uniformly in small h. Furthermore, ∥v∥L2(U2)≤Cη(Eh1/2+∥Du∥L2(U2)) by ∥δ−hw∥2≤∥Dkw∥2 and the product rule. Therefore the lower-order and source pairings, estimated without differencing bi or c, satisfy ∣∫U2(biDiu+cu−f)v‾∣≤εEh+Cε(∥Du∥L2(U2)2+∥u∥L2(U2)2+∥f∥L2(U2)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 U2 is bounded with U2‾⋐U3⋐Ω, cover U2‾ by finitely many inner balls Brℓ whose concentric outer balls BRℓ are compactly contained in U3. Applying the ball Caccioppoli estimate on each pair and summing gives ∥Du∥L2(U2)2≤C(∥u∥L2(U3)2+∥f∥L2(U3)2), with C allowed to depend on the finite cover, hence on U2,U3, as well as n,θ,Ma,Mb,Mc (Scaled Caccioppoli inequality on concentric balls).

[F5]

Difference-quotient characterisation of W1,p, 1<p<∞: ∥δhiu∥Lp(Ω1)≤∥Diu∥Lp(Ω2) for u∈W1,p(Ω2) and 0<∣h∣<dist⁡(Ω1,∂Ω2), and conversely a uniform bound ∥δhiu∥Lp(Ω1)≤C for 0<∣h∣<dist⁡(Ω1,∂Ω2)/2 implies Diu∈Lp(Ω1) with ∥Diu∥Lp(Ω1)≤C. (The difference-quotient characterisation of W1,p for 1<p<∞, Uniformly bounded difference quotients represent a weak derivative).

[F7]

If h∈L2(Ω) satisfies ∫Ωhφ‾ dx=0 for every φ∈Cc∞(Ω), then h=0; more generally Cc∞(Ω) is dense in L2(Ω). (Smooth compactly supported functions of an open set are dense in L2)

Proof

technique · direct
1.1F1F3

Nested localization. Fix Ω′⋐Ω′′⋐Ω and choose Ω′⋐U1⋐U2⋐Ω′′. Take η∈Cc∞(U2;R) equal to one on U1. For each coordinate k and sufficiently small h≠0, the test class v=−δ−hk(η2δhku) is supported in U2 and belongs to H01(U2); the weak identity extends from smooth tests to v by density, since the form is bounded and f∈L2(U2).

1.2F2F3F6algebra

Principal and lower-order terms. Write the principal pairing as Ph+Ra,h as in [F3]. The weak equation gives Ph+Ra,h=∫U2(f−biDiu−cu)v‾, so taking real parts and using [F3] bounds the right side directly, without differentiating bi or c. Choosing ε small relative to θ and absorbing the error terms into Re⁡Ph≥θEh gives Eh≤C(∥u∥L2(U2)2+∥Du∥L2(U2)2+∥f∥L2(U2)2), with C=C(n,θ,Ma,Mb,Mc,M1,U1,U2), uniformly in sufficiently small h. This estimate uses derivatives only of the principal coefficients; b,c∈L∞ 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 U2⋐Ω′′ gives ∥Du∥L2(U2)2≤C(∥u∥L2(Ω′′)2+∥f∥L2(Ω′′)2). Substitution into step 1.2 yields Eh≤C(∥u∥L2(Ω′′)2+∥f∥L2(Ω′′)2) uniformly in h.

3.1F5step 2.1algebra

Recovering all second derivatives. Since η=1 on U1 and Ω′⋐U1, step 2.1 bounds ∥δhkDju∥L2(Ω′) 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 DkDju∈L2(Ω′) with the same bound. Summing over j,k proves u∈H2(Ω′) and ∥u∥H2(Ω′)≤C(∥f∥L2(Ω′′)+∥u∥L2(Ω′′)).

4.1step 3.1F1F7algebra

The strong form and the equation a.e. On Ω′, u∈H2 by step 3.1, so the proved multiplier rule of The cutoff difference-quotient commutator estimate gives aijDju∈H1(Ω′) with weak derivative (Diaij)Dju+aijDiDju∈L2(Ω′). For every φ∈Cc∞(Ω′), integration by parts in [F1] gives ∫Ω′(f−(−Di(aijDju)+biDiu+cu))φ‾ dx=0. The bracket lies in L2(Ω′), so it vanishes a.e. there by [F7]; as the pair Ω′⋐Ω′′⋐Ω was arbitrary, the equation Lu=f holds pointwise almost everywhere on Ω with Di(aijDju) read as the a.e. product (Diaij)Dju+aijDiDju.

5.1step 3.1step 4.1∎

Conclusion. Every u∈H1(Ω) that solves Lu=f locally with L uniformly elliptic, aij∈W1,∞(Ω) and f∈Lloc2(Ω) lies in Hloc2(Ω) 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 C1 principal coefficients and proves interior H2 regularity by difference quotients. The local proof above supplies the W1,∞ 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∥L2(Ω) is not defined for f∈Lloc2(Ω) 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 Lloc2 hypothesis and the estimates actually proved.

Depends on

Used by

Dependency tree · two levels

87 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