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

Sobolev level-set step: energy decay with explicit level gap and radius loss

Statement

Assume Countable Choice and the Axiom of Choice. Let $n \geq 3$ , let $B_{R} \subset R^{n}$ be a ball, and let $u \in H^{1} (B_{R}; R)$ . Suppose there is $C_{0} \geq 1$ such that for every $0 < ρ < R$ and every level $k$ $\int_{B_{ρ}} ∣ D (u - k)^{+} ∣^{2} d x \leq C_{0} (R - ρ)^{- 2} \int_{B_{R}} (u - k)^{+ 2} d x,$ i.e. the truncated Caccioppoli estimate of Caccioppoli inequality for truncated subsolutions holds with $f = 0$ on $B_{R}$ . Then there is $C = C (n, C_{0})$ such that for all $0 < r < R$ and all $h < k$ : $\int_{B_{r}} (u - k)^{+ 2} d x \leq C (R - r)^{- 2} (k - h)^{- 4 / n} (\int_{B_{R}} (u - h)^{+ 2} d x)^{1 + 2 / n},$ and consequently, for $u \geq 0$ and $h > 0$ , $∣ {u > k} \cap B_{r} ∣ \leq C (k - h)^{- 2} (R - r)^{- 2} h^{- 4 / n} (\int_{B_{R}} u^{2} d x)^{1 + 2 / n} .$ For $n = 2$ and each $0 < δ < 1$ , the same conclusions hold with $1 + δ$ in place of $1 + 2 / n$ , $(k - h)^{- 2 δ}$ and $h^{- 2 δ}$ in place of the powers $- 4 / n$ , and the common factor $(R - r)^{- 2}$ replaced by $R^{2 - 2 δ} (R - r)^{- 2}$ . Here the constant may also depend on $δ$ . Indeed, the critical Sobolev inequality on $B_{R}$ has the scaled form $∥ v ∥_{L^{κ} (B_{R})} \leq S_{κ} R^{2 / κ} ∥ D v ∥_{L^{2} (B_{R})}$ for finite $κ > 2$ , and choosing $κ = 2 / (1 - δ)$ gives $δ = 1 - 2 / κ$ . Thus the open range $0 < δ < 1$ is exactly the range supplied by finite $κ$ , and the radius factor is the one dictated by dilation (The critical Sobolev embedding into every finite $L^{q}$ , The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction).

Facts & Assumptions

Given: Countable Choice and the Axiom of Choice; $n \geq 2$ ; a ball $B_{R}$ ; a real class $u \in H^{1} (B_{R}; R)$ ; a constant $C_{0} \geq 1$ with $\int_{B_{ρ}} ∣ D (u - k)^{+} ∣^{2} \leq C_{0} (R - ρ)^{- 2} \int_{B_{R}} (u - k)^{+ 2}$ for every $0 < ρ < R$ and every level $k$ ; radii $0 < r < R$ and levels $h < k$ .

[F1]

Assume Countable Choice. For $k \in R$ the class $u_{k} = (u - k)^{+}$ lies in $H^{1} (B_{R}; R)$ , and for $η \in C_{c}^{\infty} (B_{R})$ the product $η u_{k}$ lies in $H_{0}^{1} (B_{R})$ with $D (η u_{k}) = η D u_{k} + u_{k} D η$ almost everywhere (Positive-part truncation calculus and admissible cut-off weak tests, Integer-order Sobolev spaces and their norms).

[F2]

Assume the Axiom of Choice. Sobolev inequality: for $n \geq 3$ there is $S = S (n) < \infty$ with $∥ v ∥_{L^{2^{*}} (B_{R})} \leq S ∥ D v ∥_{L^{2} (B_{R})}$ for every $v \in H_{0}^{1} (B_{R})$ , where $2^{*} = 2 n / (n - 2)$ (The Sobolev inequality for zero-boundary Sobolev closures on open sets, The Sobolev conjugate exponent and the scaling identity).

[F3]

Assume the Axiom of Choice. On the unit ball in $R^{2}$ , the critical embedding into every finite $L^{κ}$ , combined with Poincaré's inequality for $H_{0}^{1}$ , gives $∥ v ∥_{L^{κ} (B_{1})} \leq S_{κ} ∥ D v ∥_{L^{2} (B_{1})}$ for finite $κ > 2$ . Dilation therefore gives $∥ v ∥_{L^{κ} (B_{R})} \leq S_{κ} R^{2 / κ} ∥ D v ∥_{L^{2} (B_{R})}$ for $v \in H_{0}^{1} (B_{R})$ (The critical Sobolev embedding into every finite $L^{q}$ , The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction).

[F4]

Chebyshev's inequality: for a nonnegative measurable $v$ and $t > 0$ , $∣ {v > t} ∣ \leq t^{- 2} \int v^{2}$ ; and Hölder's inequality gives $\int_{E} f^{2} \leq ∣ E ∣^{2 / n} ∥ f ∥_{L^{2^{*}}}^{2}$ for measurable $E$ of finite measure (Chebyshev-Markov inequality for the integral, Holder's inequality for integrals, including the endpoint cases, The space $L^{p} (μ)$ as the quotient by null functions).

[F5]

The radial cutoff used in the ball-form Caccioppoli estimate has a universal gradient constant: for $0 < r < ρ$ , take $s = (r + ρ) / 2$ and $η (x) = σ ((s^{2} - ∣ x ∣^{2}) / (s^{2} - r^{2}))$ . Then $η \in C_{c}^{\infty} (B_{ρ})$ , $0 \leq η \leq 1$ , $η = 1$ on $B_{r}$ , and $∣ D η ∣ \leq C_{U} / (ρ - r)$ with $C_{U} = 4 ∥ σ^{'} ∥_{\infty}$ , since on the support $∣ x ∣ \leq s$ and $s - r = (ρ - r) / 2$ ; this is the explicit cutoff calculation in Caccioppoli inequality for truncated subsolutions.

Proof

technique · direct; combine the truncated Caccioppoli estimate with the Sobolev embedding and Chebyshev's inequality, then iterate the resulting measure–energy inequality once

1.1givenF4

Put $w : = (u - k)^{+}$ and $v : = (u - h)^{+}$ . Since $h < k$ one has $0 \leq w \leq v$ , and ${w > 0} = {u > k} = {v > k - h} \subseteq {v > 0}$ . Applying Chebyshev's inequality to the nonnegative function $v$ at level $k - h > 0$ gives $∣ {w > 0} \cap B_{r} ∣ \leq ∣ {v > k - h} ∣ \leq (k - h)^{- 2} \int_{B_{R}} v^{2} d x$ .

1.2givenF1F5algebra

Choose $ρ : = (R + r) / 2 \in (r, R)$ and the bump $η$ of [F5] with $0 \leq η \leq 1$ , $η = 1$ on $B_{r}$ , $supp η \subseteq B_{ρ}$ and $∣ D η ∣ \leq C_{U} / (ρ - r) = 2 C_{U} / (R - r)$ . By [F1], $η w \in H_{0}^{1} (B_{R})$ , and $D (η w) = η D w + w D η$ almost everywhere, so the Caccioppoli hypothesis at radius $ρ$ and level $k$ , together with the elementary bound $(a + b)^{2} \leq 2 a^{2} + 2 b^{2}$ , gives $\int_{B_{R}} ∣ D (η w) ∣^{2} d x \leq 2 \int_{B_{ρ}} η^{2} ∣ D w ∣^{2} d x + 2 \int_{B_{ρ}} w^{2} ∣ D η ∣^{2} d x \leq \frac{8 (C_{0} + C_{U}^{2})}{(R - r)^{2}} \int_{B_{R}} w^{2} d x .$

2.1step 1.1F2F4algebra

Assume $n \geq 3$ and let $2^{*} = 2 n / (n - 2)$ . Applying the Sobolev inequality [F2] to $η w \in H_{0}^{1} (B_{R})$ and then Hölder's inequality [F4] on the support of $η w$ , which is contained in ${w > 0} \cap B_{ρ}$ up to a null set, gives $\int_{B_{r}} w^{2} d x \leq \int_{B_{R}} (η w)^{2} d x \leq ∣ {w > 0} \cap B_{ρ} ∣^{2 / n} S^{2} \int_{B_{R}} ∣ D (η w) ∣^{2} d x$ .

3.1step 1.1step 1.2step 2.1algebra

Substituting the bound of step 1.2 into step 2.1 and then the Chebyshev bound of step 1.1, and using $\int_{B_{R}} w^{2} \leq \int_{B_{R}} v^{2}$ , yields $\int_{B_{r}} (u - k)^{+ 2} d x \leq C (n, C_{0}) (R - r)^{- 2} (k - h)^{- 4 / n} (\int_{B_{R}} (u - h)^{+ 2} d x)^{1 + 2 / n}$ , which is the first displayed estimate.

3.2step 1.1step 1.2step 2.1F3F4algebra

Assume $n = 2$ and fix a finite exponent $κ > 2$ , put $δ : = 1 - 2 / κ \in (0, 1)$ , and fix $η$ and $w$ as in steps 1.1-1.2. Replacing $2^{*}$ by $κ$ in step 2.1, using the scaled inequality [F3] and Hölder in the form $\int_{E} f^{2} \leq ∣ E ∣^{1 - 2 / κ} ∥ f ∥_{L^{κ}}^{2}$ , and inserting steps 1.1 and 1.2 gives $\int_{B_{r}} (u - k)^{+ 2} d x \leq C (κ, C_{0}) R^{2 - 2 δ} (R - r)^{- 2} (k - h)^{- 2 δ} (\int_{B_{R}} (u - h)^{+ 2} d x)^{1 + δ}$ . As finite $κ > 2$ varies, $δ = 1 - 2 / κ$ ranges over exactly $(0, 1)$ ; the factor $R^{2 - 2 δ}$ is precisely the dilation factor from [F3].

4.1step 3.1step 3.2F4algebra

For the measure clause assume $u \geq 0$ and $h > 0$ . On ${u > k} \cap B_{r}$ one has $(u - h)^{+} > k - h > 0$ , so Chebyshev's inequality gives $∣ {u > k} \cap B_{r} ∣ \leq (k - h)^{- 2} \int_{B_{r}} (u - h)^{+ 2} d x$ , and the first estimate applied with levels $0 < h$ bounds the integral by the displayed energy expression, since $u \geq 0$ ; multiplying the two bounds gives the displayed measure estimate. For $n = 2$ the same argument carries the factor $R^{2 - 2 δ} (R - r)^{- 2} h^{- 2 δ}$ from step 3.2.

5.1step 3.1step 3.2step 4.1∎

Both displayed estimates follow from steps 3.1-4.1 with constants depending only on $n$ , the Sobolev constants and $C_{0}$ ; the hypothesis list uses the Caccioppoli estimate of Caccioppoli inequality for truncated subsolutions and the declared Countable Choice and Axiom of Choice only, so no further choice principle is used.

Depends on

Used by

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

Bozhidar Velichkov, Elliptic PDEs: Teorema di De Giorgi (Universita di Pisa; complete 7-page note, in Italian) (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)