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.

Smooth data give smooth interior solutions

Statement

Assume the Axiom of Choice for the Sobolev embedding used in the last step, and Countable Choice for the Sobolev interfaces. Let $Ω \subseteq R^{n}$ be open, $n \geq 1$ , $K \in {R, C}$ , and suppose the coefficients $a^{i j}, b^{i}, c$ and the datum $f$ are of class $C^{\infty} (Ω)$ . 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}^{m} (Ω)$ for every $m \in N$ , and consequently $u$ agrees almost everywhere with a function of class $C^{\infty} (Ω)$ , for which $L u = f$ holds pointwise in $Ω$ . No boundary condition is imposed, and the conclusion is interior only.

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; the smooth coefficients and datum; and the local weak solution $u \in H^{1} (Ω)$ .

[F1]

Interior $H^{k + 2}$ regularity: for every $k \geq 0$ and all $Ω^{'} ⋐ Ω^{''} ⋐ Ω$ , $u \in H^{k + 2} (Ω^{'})$ with a bound in terms of the principal coefficient bounds through order $k + 1$ , the lower-order coefficient bounds through order $k$ , and $∥ f ∥_{H^{k} (Ω^{''})} + ∥ u ∥_{L^{2} (Ω^{''})}$ ; the theorem is applied after restricting the equation to a relatively compact outer open set, where smooth coefficients supply all the required coefficient bounds. (Interior $H^{k + 2}$ elliptic regularity)

[F2]

The a.e. strong form: on each relatively compact open patch the smooth principal coefficients are $W^{1, \infty}$ and $u \in H_{l o c}^{2}$ , so the equation $L u = f$ holds pointwise almost everywhere with $D_{i} (a^{i j} D_{j} u) = (D_{i} a^{i j}) D_{j} u + a^{i j} D_{i} D_{j} u$ . (Interior $H^{2}$ regularity for divergence-form equations)

[F3]

Higher-order Sobolev embedding: for $n \geq 2$ , if $k \geq 1$ , $1 \leq p < \infty$ , $k p > n$ , then every class in $W^{k, p} (Ω_{0})$ for a bounded extension domain $Ω_{0}$ has a representative in $C^{m, α} (\overline{Ω_{0}})$ for integers $m \geq 0$ and $0 < α < 1$ with $m + α < k - n / p$ ; in particular $H^{k} (Ω_{0})$ for $k > n / 2$ has a continuous representative. Balls are bounded extension domains. (Higher-order Sobolev embedding, Sobolev extension domains and extension operators, Bounded C^k domains admit integer-order Sobolev extension, Local Hölder and scaled C-two-alpha norms on balls)

[F4]

Under the Axiom of Choice, in dimension one each $H^{1} (I)$ class on a bounded interval has a unique absolutely continuous representative, whose classical derivative agrees almost everywhere with its weak derivative. (One-dimensional $W^{1, p}$ functions have unique absolutely continuous representatives)

Proof

technique · direct

1.1F1

Every local Sobolev order. Fix $Ω^{'} ⋐ Ω$ and $m \in N$ , and choose $Ω^{''}$ with $Ω^{'} ⋐ Ω^{''} ⋐ Ω$ . Since $a^{i j}, b^{i}, c \in C^{\infty} (Ω)$ , their derivatives are bounded on $Ω^{''}$ by constants $M_{ℓ}$ for $ℓ \leq m + 1$ , and $f \in C^{\infty} (Ω)$ gives $f \in H^{m} (Ω^{''})$ ; restrict the equation to $Ω^{''}$ , where $u \in H^{1}$ and the coefficient derivatives have global bounds. Choose $Ω^{'} ⋐ G ⋐ Ω^{''}$ and apply [F1] with $k = m$ on this restricted domain and inner pair $(Ω^{'}, G)$ to obtain $u \in H^{m + 2} (Ω^{'}) \subseteq H^{m} (Ω^{'})$ . As $m$ and $Ω^{'}$ were arbitrary, $u \in H_{l o c}^{m} (Ω)$ for every $m$ .

2.1F3F4step 1.1algebra

Fix a ball $B ⋐ Ω$ . For $n \geq 2$ and any integer $m \geq 0$ , choose an integer $s > m + n / 2$ and $0 < α < \min (1, s - m - n / 2)$ . Step 1.1 gives $u \in H^{s} (B)$ , and [F3] applied directly to $u$ gives a $C^{m, α} (\overline{B})$ representative. Representatives obtained for different $m$ agree everywhere on $B$ , since they are continuous and represent the same almost-everywhere class; therefore this one representative is smooth. For $n = 1$ , take bounded open intervals $I ⋐ Ω$ . Every $D^{j} u$ belongs to $H^{1} (I)$ by step 1.1, so [F4] gives continuous absolutely continuous representatives $g_{j}$ with $g_{j} (y) - g_{j} (x) = \int_{x}^{y} g_{j + 1} (t) d t$ . Continuity of $g_{j + 1}$ makes $g_{j}$ classically differentiable with derivative $g_{j + 1}$ , proving smoothness by iteration. These representatives agree on overlaps, again by continuity and almost-everywhere equality, and hence give a smooth representative on all of $Ω$ .

3.1F2step 1.1step 2.1

The equation pointwise. For the smooth representative, step 1.1 gives $u \in H_{l o c}^{2} (Ω)$ , so [F2] gives $L u = f$ pointwise almost everywhere, the expression $D_{i} (a^{i j} D_{j} u)$ being the a.e. function $(D_{i} a^{i j}) D_{j} u + a^{i j} D_{i} D_{j} u$ . Both sides are continuous for the smooth representative and $f$ is continuous, and two continuous functions that agree almost everywhere on an open set agree everywhere; hence $L u = f$ holds pointwise in $Ω$ .

4.1step 2.1step 3.1∎

Conclusion. Smooth coefficients and smooth interior data propagate the interior regularity to every order and upgrade the weak solution to a classical one on $Ω$ ; no boundary condition is imposed and no statement is made about the boundary. The Axiom of Choice supplies the higher-order Sobolev embedding in dimensions $n \geq 2$ and the absolutely-continuous representative interface [F4] in dimension one. Countable Choice enters through the Sobolev interfaces of [F1].

Source notes

Hunter's Corollary 4.29 (printed p. 114) and Laugesen's Theorem 5.9 (printed p. 112) draw precisely this conclusion: iterate the interior higher-order estimate and apply the Sobolev embedding. The scaffold listed Morrey's inequality alongside the higher-order embedding; the proof uses only the embedding (on balls, which are bounded extension domains), so the Morrey citation is not needed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

74 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 graduate 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)