ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Radial powers approach the Morrey borderline exponent

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $n \geq 2$ , $n < p < \infty$ , $α_{0} = 1 - \frac{n}{p} \in (0, 1)$ , and for $0 < δ < \frac{n}{p}$ define $u_{δ} (x) = ∣ x ∣^{α_{0} + δ}$ on $B = B (0, 1)$ , with $u_{δ} (0) = 0$ . Then $u_{δ} \in W^{1, p} (B)$ and $∥ D u_{δ} ∥_{L^{p} (B)} = (α_{0} + δ) (\frac{σ (S^{n - 1})}{p δ})^{1 / p} .$ The function $u_{δ}$ is Holder of exponent $α_{0} + δ$ on $B$ with $[u_{δ}]_{C^{0, α_{0} + δ}} = 1$ , and the local Morrey estimate holds on each $B (0, r)$ with $2 r < 1$ ; as $δ ↓ 0$ the energy $∥ D u_{δ} ∥_{L^{p} (B)}^{p}$ diverges like $α_{0}^{p} σ (S^{n - 1}) / (p δ)$ , and the borderline function $∣ x ∣^{α_{0}}$ is not in $W^{1, p} (B)$ . The exponent $α_{0} = 1 - \frac{n}{p}$ is exactly the borderline produced by $p > n$ .

Facts & Assumptions

Given: The Axiom of Choice; $n \geq 2$ ; $n < p < \infty$ ; $α_{0} = 1 - n / p \in (0, 1)$ ; $0 < δ < n / p$ ; and $u_{δ} (x) = ∣ x ∣^{α_{0} + δ}$ on $B = B (0, 1)$ , $u_{δ} (0) = 0$ .

[F1]

Polar coordinates: for nonnegative Borel $h$ , $\int_{B} h = \int_{0}^{1} \int_{S^{n - 1}} h (r ω) r^{n - 1} d σ (ω) d r$ with $0 < σ (S^{n - 1}) < \infty$ (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, The polar surface set function on the unit sphere).

[F2]

For real $β$ the function $r \mapsto r^{β}$ is differentiable on $(0, \infty)$ with derivative $β r^{β - 1}$ , so for $β > - 1$ its antiderivative is $r^{β + 1} / (β + 1)$ ; Newton-Leibniz on $[ε, 1]$ combined with monotone convergence as $ε ↓ 0$ gives $\int_{0}^{1} r^{β} d r = 1 / (β + 1)$ (Continuity and derivatives of positive-base real powers, Newton–Leibniz remains valid across finitely many exceptional interior points when the primitive is continuous, A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral, Monotone convergence for the integral).

[F3]

The radial derivative off the origin is $D u_{δ} (x) = (α_{0} + δ) ∣ x ∣^{α_{0} + δ - 2} x$ , of modulus $(α_{0} + δ) ∣ x ∣^{α_{0} + δ - 1}$ ; $W^{1, p}$ consists of $L^{p}$ classes with weak gradient in $L^{p}$ (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions).

[F4]

For $0 < α < 1$ and $h \geq 0$ , the function $t \mapsto (t + h)^{α} - t^{α}$ decreases for $t > 0$ , since its derivative is $α ((t + h)^{α - 1} - t^{α - 1}) \leq 0$ . Continuity at $t = 0$ gives $(t + h)^{α} - t^{α} \leq h^{α}$ , hence $∣ s^{α} - t^{α} ∣ \leq ∣ s - t ∣^{α}$ for $s, t \geq 0$ ; the case $α = 1$ is equality (Continuity and derivatives of positive-base real powers). The Holder seminorm is the supremum of the difference quotients (Local Hölder and scaled C-two-alpha norms on balls).

[F5]

Morrey gives $[v]_{C^{0, α_{0}} (B (0, r))} \leq C (n, p) ∥ D v ∥_{L^{p} (B (0, 2 r))}$ for $2 r < 1$ (Morrey's inequality for $p > n$ ).

[F6]

Countable Choice is assumed; the vector-valued fundamental theorem (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz) gives integration by parts for smooth products on intervals, and Fubini (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability) integrates the section identities. Classical smooth derivatives are weak derivatives (Classical derivatives agree with weak derivatives).

Verification

technique · direct

1.1F1F2F3F6givenalgebra

The weak gradient and the energy. Off the origin $u_{δ}$ is smooth with radial derivative $D u_{δ} (x) = (α_{0} + δ) ∣ x ∣^{α_{0} + δ - 2} x$ of modulus $(α_{0} + δ) ∣ x ∣^{α_{0} + δ - 1}$ . For $α : = α_{0} + δ > 0$ , this gradient is in $L^{1} (B)$ because its radial exponent is $n + α - 2 > - 1$ , and $u_{δ}$ is bounded. Every coordinate line with nonzero transverse coordinate avoids the origin; apply the fundamental theorem to $u_{δ} φ$ on its interval in $B$ , with $φ$ a compactly supported test. Since $n \geq 2$ , the omitted transverse singleton is null, and Fubini [F6] gives the global weak derivative identity. With $r = ∣ x ∣$ and $β = p (α_{0} + δ - 1) + n - 1$ , polar coordinates [F1] and the power integral [F2] give $∥ D u_{δ} ∥_{L^{p} (B)}^{p} = σ (S^{n - 1}) (α_{0} + δ)^{p} \int_{0}^{1} r^{β} d r = σ (S^{n - 1}) (α_{0} + δ)^{p} / (β + 1)$ , and $β + 1 = p (α_{0} + δ) - p + n = p δ$ because $p α_{0} = p - n$ . Hence $∥ D u_{δ} ∥_{L^{p} (B)} = (α_{0} + δ) (σ (S^{n - 1}) / (p δ))^{1 / p}$ , and $u_{δ} \in W^{1, p} (B)$ by [F3] since both $u_{δ}$ and this gradient are in $L^{p} (B)$ .

1.2F4givenalgebra

The Holder exponent. For $x \neq y$ in $B$ , writing $s = ∣ x ∣$ , $t = ∣ y ∣$ and using the elementary inequality of [F4] with $α = α_{0} + δ \in (0, 1)$ , $∣ u_{δ} (x) - u_{δ} (y) ∣ = ∣ s^{α} - t^{α} ∣ \leq ∣ s - t ∣^{α} \leq ∣ x - y ∣^{α}$ , so $[u_{δ}]_{C^{0, α_{0} + δ}} \leq 1$ ; the value $1$ is attained by the pair $x = 0$ , $y$ with $∣ y ∣ = t \in (0, 1)$ , where the ratio is $t^{α} / t^{α} = 1$ . Hence $[u_{δ}]_{C^{0, α_{0} + δ}} = 1$ .

2.1F2F5step 1.1step 1.2givenalgebra∎

The borderline. Morrey [F5] applies on every $B (0, r)$ with $2 r < 1$ . The explicit function is also globally $α_{0}$ -Holder on $B$ : step 1.2 gives $[u_{δ}]_{C^{0, α_{0}}} \leq 2^{δ}$ . Step 1.1 gives $∥ D u_{δ} ∥_{p}^{p} = σ (S^{n - 1}) (α_{0} + δ)^{p} / (p δ) \sim σ (S^{n - 1}) α_{0}^{p} / (p δ)$ as $δ ↓ 0$ . For $δ = 0$ the same computation gives $β + 1 = 0$ , so $\int_{B} ∣ D (∣ x ∣^{α_{0}}) ∣^{p} = σ (S^{n - 1}) α_{0}^{p} \int_{0}^{1} r^{- 1} d r = + \infty$ and $∣ x ∣^{α_{0}} \notin W^{1, p} (B)$ ; the failure is exactly the divergence of the energy at the origin.

Source notes

For the positive powers $β > 0$ used here, the borderline computation is $∣ x ∣^{β} \in W^{1, p} (B)$ exactly when $p (β - 1) + n > 0$ , that is $β > 1 - n / p = α_{0}$ , with the derivative energy equal to $σ (S^{n - 1}) (α_{0} + δ)^{p} / (p δ)$ at $β = α_{0} + δ$ . Kinnunen's discussion around Theorem 3.23 and Remarks 3.25 and Laugesen's Theorem 3.21 with its moral give the Morrey estimate used for context; the displayed radial energy is computed directly above. The denominator $p δ$ is the exact value of $p (β - 1) + n$ at $β = α_{0} + δ$ ; the energy diverges like $1 / δ$ as $δ ↓ 0$ , so the $L^{p}$ norm diverges like $δ^{- 1 / p}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

98 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

Juha Kinnunen, Sobolev Spaces (Aalto University, 2026, complete graduate lecture notes) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, complete 158-page graduate notes) (standard reference, not scraped)