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

De Giorgi-Nash interior Holder regularity for divergence-form equations

Statement

Assume Countable Choice and the Axiom of Choice. Let $n \geq 2$ , let $Ω \subseteq R^{n}$ be open, and let $A$ , $L_{0}$ be as in De Giorgi local boundedness of homogeneous subsolutions, with measurable symmetric uniformly elliptic coefficients and constants $θ, M_{a}$ . Let $u \in H^{1} (Ω; R)$ be a weak solution of $L_{0} u = 0$ on $Ω$ . Then there are $α = α (n, θ, M_{a}) \in (0, 1)$ and, for every $α^{'} \in (0, α)$ , a class $u^{*} \in C_{l o c}^{0, α^{'}} (Ω)$ (Local Hölder and scaled C-two-alpha norms on balls, Hölder spaces $C^{k, α}$ , closure and interior scaled norms, and $C^{k, α}$ domains) with $u^{*} = u$ a.e. on $Ω$ , and for every ball $B_{R_{0}} (x_{0}) ⋐ Ω$ , $[u^{*}]_{0, α^{'}; B_{R_{0} / 2} (x_{0})} \leq C (n, θ, M_{a}, α^{'}) R_{0}^{- α^{'}} (\frac{1}{∣ B_{R_{0}} (x_{0}) ∣} \int_{B_{R_{0}} (x_{0})} u^{2} d x)^{1 / 2},$ and $∥ u^{*} ∥_{L^{\infty} (B_{R_{0} / 2} (x_{0}))} \leq C R_{0}^{- n / 2} ∥ u ∥_{L^{2} (B_{R_{0}} (x_{0}))}$ . In particular every real weak solution of the homogeneous scalar equation with the symmetric bounded measurable uniformly elliptic principal coefficients specified above has a locally Holder continuous representative, and the representative is unique up to equality everywhere on $Ω$ .

Facts & Assumptions

Given: Countable Choice and the Axiom of Choice; an open $Ω \subseteq R^{n}$ , $n \geq 2$ ; measurable symmetric uniformly elliptic coefficients $A$ with constants $θ, M_{a}$ ; the principal operator $L_{0} u = - D_{i} (a^{i j} D_{j} u)$ with form $a_{0}$ ; a real weak solution $u \in H^{1} (Ω; R)$ ; and a ball $B_{R_{0}} (x_{0}) ⋐ Ω$ .

[F1]

One-step oscillation reduction: there is $η = η (n, θ, M_{a}) \in (0, 1)$ such that for each ball $B_{R} (x)$ with $B_{2 R} (x) ⋐ Ω$ , ${ess osc}_{B_{R / 2} (x)} u \leq η {ess osc}_{B_{R} (x)} u$ (De Giorgi oscillation reduction: one half-level set is small).

[F2]

Local boundedness for a nonnegative subsolution: for every nonnegative weak subsolution $w$ of $L_{0} w = 0$ and every ball $B_{R} (x) ⋐ Ω$ , $0 < ρ < 1$ and $p > 0$ , ${ess sup}_{B_{ρ R} (x)} w \leq C (n, θ, M_{a}, ρ, p) (\frac{1}{∣ B_{R} (x) ∣} \int_{B_{R} (x)} w^{p})^{1 / p}$ (De Giorgi local boundedness of homogeneous subsolutions).

[F3]

Extend $u \in L^{2} (Ω)$ by zero off $Ω$ . The extension lies in $L^{2} (R^{n})$ and hence $L_{l o c}^{1} (R^{n})$ by Holder on bounded sets. The cited Lebesgue-point theorem applies to this extension; restriction back to $Ω$ gives a full-measure Lebesgue set, dense because every nonempty open subset has positive measure (Almost every point is a Lebesgue point of a locally integrable function, Lebesgue points and the Lebesgue set of an $L_{l o c}^{1}$ class, The average of a locally integrable function over a Euclidean ball).

[F4]

The target $R$ is complete by The reals are complete. Apply the dense-set extension theorem on each smaller ball, where the local Holder bound gives uniform continuity; the extensions agree on overlaps because they agree on the dense Lebesgue set. This gives a unique continuous extension on the ambient open set and passes the local Holder bounds to it (A uniformly continuous map from a dense subspace into a complete metric space extends uniquely to a uniformly continuous map on the whole space, Complete metric space: every Cauchy sequence converges in the space).

[F5]

For continuous functions, pointwise supremum and infimum on an open ball equal the essential supremum and infimum of the corresponding almost-everywhere class; the Holder seminorm and norm are those of Local Hölder and scaled C-two-alpha norms on balls and Hölder spaces $C^{k, α}$ , closure and interior scaled norms, and $C^{k, α}$ domains (The essential supremum of a measurable function with respect to a measure).

[F6]

Positive parts of a real weak solution of the homogeneous equation are weak subsolutions. For $v = u$ or $v = - u$ , the zero-source identity extends from $C_{c}^{\infty}$ tests to $H_{0}^{1}$ by density and boundedness of the form (Zero-boundary Sobolev space as a norm closure, The elliptic form is well defined and bounded on $H^{1}$ ). Thus test with the nonnegative $H_{0}^{1}$ function $ϕ χ_{ϵ} (v)$ , where $ϕ \in C_{c}^{\infty} (Ω)$ is nonnegative and $χ_{ϵ} (t) = \min {1, t^{+} / ϵ}$ . The chain and product rules give $a_{0} (v, ϕ χ_{ϵ} (v)) = \int χ_{ϵ} (v) A D v \cdot D ϕ + \int ϕ χ_{ϵ}^{'} (v) A D v \cdot D v = 0$ ; the second term is nonnegative. Dominated convergence in the first term as $ϵ ↓ 0$ gives $a_{0} (v^{+}, ϕ) \leq 0$ (Chain rule for globally Lipschitz scalar maps of Sobolev functions, Weak Leibniz rule with a smooth factor, Positive-part truncation calculus and admissible cut-off weak tests).

Proof

technique · iterate the one-step oscillation reduction on smaller interior balls, transfer its dyadic decay to Lebesgue values, extend those values continuously, and use local boundedness of the positive and negative parts for the quantitative norm estimate

1.1givenF2F6

Local boundedness of the positive and negative parts. For $v = u$ and $v = - u$ , [F6] shows that $v^{+}$ is a nonnegative weak subsolution. Given any ball $B_{S} (x) ⋐ Ω$ , choose $S^{'} > S$ with $B_{S^{'}} (x) ⋐ Ω$ and apply [F2] on $B_{S^{'}} (x)$ with inner ratio $S / S^{'}$ and exponent $p = 2$ . Since $v^{+} \in H^{1} (Ω)$ , its $L^{2} (B_{S^{'}})$ mean is finite, so both $u^{+}$ and $(- u)^{+}$ are essentially bounded on $B_{S} (x)$ . Consequently $u$ has finite essential oscillation on every compactly contained ball.

2.1step 1.1F1algebra

Geometric oscillation decay. Fix $B_{R} (x_{0}) ⋐ Ω$ . By [F1], applying the one-step estimate first with outer ball $B_{R / 2}$ and then with successive dyadic outer balls gives ${ess osc}_{B_{R / 2^{k + 1}} (x_{0})} u \leq η^{k} {ess osc}_{B_{R} (x_{0})} u$ for every integer $k \geq 0$ . By monotonicity of essential oscillation, if $0 < r \leq R / 4$ , choosing $k$ so that $R / 2^{k + 2} < r \leq R / 2^{k + 1}$ gives ${ess osc}_{B_{r} (x_{0})} u \leq C_{0} (r / R)^{α_{0}} {ess osc}_{B_{R} (x_{0})} u, α_{0} : = \frac{\log (1 / η)}{\log 2} > 0,$ with $C_{0} = 4^{α_{0}}$ ; for $R / 4 < r \leq R$ the same inequality follows from monotonicity and this choice of $C_{0}$ . This argument applies to any ball compactly contained in $Ω$ , and all oscillations are finite by step 1.1.

3.1step 2.1F3algebra

Holder modulus at Lebesgue points. Fix $0 < ρ < 1$ and $x, y \in B_{ρ R} (x_{0})$ that are Lebesgue points of $u$ . Put $m : = (1 - ρ) R / 2$ and $d : = ∣ x - y ∣$ . If $0 < d < m / 4$ , then $B_{2 d} (x) \subset B_{2 m} (x) ⋐ B_{R} (x_{0})$ . The decay of step 2.1 applied to $B_{2 m} (x)$ gives ${ess osc}_{B_{2 d} (x)} u \leq C_{0} (d / m)^{α_{0}} {ess osc}_{B_{R} (x_{0})} u .$ For sufficiently small $s > 0$ , both $B_{s} (x)$ and $B_{s} (y)$ lie in $B_{2 d} (x)$ ; their averages lie between its essential infimum and supremum. Passing to the Lebesgue limits gives $∣ u^{*} (x) - u^{*} (y) ∣ \leq {ess osc}_{B_{2 d} (x)} u$ . If instead $d \geq m / 4$ , the bound $∣ u^{*} (x) - u^{*} (y) ∣ \leq {ess osc}_{B_{R} (x_{0})} u$ suffices. In either case, $∣ u^{*} (x) - u^{*} (y) ∣ \leq C_{ρ} (d / R)^{α_{0}} {ess osc}_{B_{R} (x_{0})} u,$ where $C_{ρ}$ depends only on $η, ρ$ .

4.1step 3.1F3F4

The continuous representative. The Lebesgue set of $u$ is dense by [F3]. Step 3.1 makes the Lebesgue representative locally Holder on its intersection with each smaller ball $B_{ρ R} (x_{0})$ . The extension theorem [F4] gives a unique continuous extension on $Ω$ , still denoted $u^{*}$ , which agrees with $u$ a.e. and retains these local Holder bounds.

5.1step 3.1step 4.1F2F5algebra

Holder and supremum estimates. Let $R : = R_{0}$ and apply step 3.1 on the outer ball $B_{3 R / 4} (x_{0})$ with inner ratio $2 / 3$ . Applying [F2] with $p = 2$ and outer ball $B_{R}$ to the positive parts $u^{+}$ and $(- u)^{+}$ from step 1.1 gives ${ess sup}_{B_{3 R / 4}} ∣ u ∣ \leq C (\frac{1}{∣ B_{R} ∣} \int_{B_{R}} u^{2})^{1 / 2} .$ Hence ${ess osc}_{B_{3 R / 4}} u \leq 2 C (\frac{1}{∣ B_{R} ∣} \int_{B_{R}} u^{2})^{1 / 2}$ . Steps 3.1 and 4.1 give the corresponding increment bound with exponent $α_{0}$ . Set $α : = \min {α_{0}, 1 / 2} \in (0, 1)$ ; weakening the exponent to $α$ preserves the estimate. For $0 < α^{'} < α$ , interpolate that Holder increment with the supremum bound: $\min {C M (∣ x - y ∣ / R)^{α}, 2 M} \leq C^{'} (α^{'}) M (∣ x - y ∣ / R)^{α^{'}}$ , where $M = (\frac{1}{∣ B_{R} ∣} \int_{B_{R}} u^{2})^{1 / 2}$ . Thus $[u^{*}]_{0, α^{'}; B_{R / 2}} \leq C R^{- α^{'}} (\frac{1}{∣ B_{R} ∣} \int_{B_{R}} u^{2})^{1 / 2}, ∥ u^{*} ∥_{L^{\infty} (B_{R / 2})} \leq C R^{- n / 2} ∥ u ∥_{L^{2} (B_{R})} .$ The constants depend only on $n, θ, M_{a}, α^{'}$ .

6.1F3F4∎

Uniqueness. If two continuous representatives agree with $u$ a.e., they agree on a full-measure, hence dense, subset of $Ω$ ; continuity makes them equal everywhere. All arguments use only the declared choice principles.

Depends on

Used by

Dependency tree · two levels

152 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

Brian Krummel, Consequences of De Giorgi-Nash-Moser (4 March 2016; complete 7-page notes) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford University; complete author scan, 118 sheets reproducing the 223 printed pages of the manuscript, two logical pages per sheet) (standard reference, not scraped)
Bozhidar Velichkov, Elliptic PDEs: Teorema di De Giorgi (Universita di Pisa; complete 7-page note, in Italian) (standard reference, not scraped)