ExampleConstruction: Literature-sourcedVerification: 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.

Critical bubbles converge weakly but not strongly

Example

Assume Countable Choice. Let $n \geq 2$ , $1 \leq p < n$ , $p^{*} = \frac{n p}{n - p}$ , and choose a nonzero real $φ \in C_{c}^{\infty} (B (0, 1))$ with $∥ φ ∥_{L^{p^{*}} (R^{n})} = 1$ (for instance a normalised smooth bump). On $Ω = B (0, 1)$ put $u_{j} (x) = (j + 1)^{(n - p) / p} φ ((j + 1) x)$ for $j \geq 0$ . Then $u_{j} \in W_{0}^{1, p} (Ω)$ , $∥ u_{j} ∥_{L^{p^{*}} (Ω)} = 1$ , $∥ D u_{j} ∥_{L^{p} (Ω)} = ∥ D φ ∥_{L^{p} (R^{n})}$ and $∥ u_{j} ∥_{L^{p} (Ω)} = (j + 1)^{- 1} ∥ φ ∥_{L^{p} (R^{n})}$ . Moreover $u_{j} ⇀ 0$ in $L^{p^{*}} (Ω)$ and $u_{j} \to 0$ almost everywhere, but no subsequence converges strongly in $L^{p^{*}} (Ω)$ : the unit mass concentrates at the origin, while the weak limit is the zero class and the norms remain one.

Facts & Assumptions

Given: the Axiom of Countable Choice, $n \geq 2$ , $1 \leq p < n$ , $p^{*} = \frac{n p}{n - p}$ , a nonzero real $φ \in C_{c}^{\infty} (B (0, 1))$ with $∥ φ ∥_{p^{*}} = 1$ , and $u_{j} (x) = (j + 1)^{(n - p) / p} φ ((j + 1) x)$ on $Ω = B (0, 1)$ .

[F1]

Scaling. For measurable nonnegative $h$ and $j \geq 0$ , $\int h ((j + 1) x) (j + 1)^{n} d x = \int h (y) d y$ , and $supp (u_{j}) \subseteq B (0, 1 / (j + 1))$ . (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not, Integer-order Sobolev spaces and their norms)

[F2]

H"older's inequality. $\int ∣ f g ∣ \leq ∥ f ∥_{p^{*}} ∥ g ∥_{(p^{*})^{'}}$ for conjugate exponents. (Holder's inequality for integrals, including the endpoint cases)

[F3]

Duality of $L^{p^{*}}$ . Since $1 < p^{*} < \infty$ and $Ω$ has finite measure, every bounded linear functional on $L^{p^{*}} (Ω)$ is integration against some $g \in L^{(p^{*})^{'}} (Ω)$ . (For $1 < p < \infty$ , the same representation theorem holds on arbitrary measure spaces)

[F4]

Absolute continuity of the integral. If $∣ g ∣^{(p^{*})^{'}}$ is integrable, then $∥ g 1_{B (0, 1 / (j + 1))} ∥_{(p^{*})^{'}} \to 0$ as $j \to \infty$ . (Dominated convergence)

[F5]

Weak convergence. $u_{j} ⇀ 0$ in $L^{p^{*}}$ means $\int u_{j} g \to 0$ for every $g \in L^{(p^{*})^{'}}$ ; strong convergence implies weak convergence. (Weak convergence of nets and sequences)

[F6]

Membership in $W_{0}^{1, p}$ . The function $u_{j}$ is smooth and compactly supported in $Ω$ , hence belongs to $W_{0}^{1, p} (Ω)$ and its classical derivatives represent $D u_{j}$ . (Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms)

Verification

technique · direct

1.1F1F6given

By [F1], $∥ u_{j} ∥_{p^{*}}^{p^{*}} = (j + 1)^{(n - p) p^{*} / p} (j + 1)^{- n} ∥ φ ∥_{p^{*}}^{p^{*}} = 1$ , $∥ u_{j} ∥_{p} = (j + 1)^{(n - p) / p} (j + 1)^{- n / p} ∥ φ ∥_{p} = (j + 1)^{- 1} ∥ φ ∥_{p}$ , and $∥ D u_{j} ∥_{p} = (j + 1)^{(n - p) / p} (j + 1)^{1 - n / p} ∥ D φ ∥_{p} = ∥ D φ ∥_{p}$ ; [F6] gives $u_{j} \in W_{0}^{1, p} (Ω)$ , and $u_{j} (x) \to 0$ for every $x \neq 0$ because $φ ((j + 1) x) = 0$ once $(j + 1) ∣ x ∣ > 1$ .

2.1F2F3F4F5step 1.1

Let $g \in L^{(p^{*})^{'}} (Ω)$ and extend it by zero to $R^{n}$ . By [F2] and step 1.1, $∣ \int_{Ω} u_{j} g d x ∣ \leq ∥ u_{j} ∥_{p^{*}} ∥ g 1_{B (0, 1 / (j + 1))} ∥_{(p^{*})^{'}} = ∥ g 1_{B (0, 1 / (j + 1))} ∥_{(p^{*})^{'}}$ , which tends to $0$ by [F4]; by [F3] and [F5] this says $u_{j} ⇀ 0$ in $L^{p^{*}} (Ω)$ .

3.1F2F5step 1.1step 2.1∎

If a subsequence converged strongly in $L^{p^{*}} (Ω)$ to some $v$ , then $∥ v ∥_{p^{*}} = 1$ by continuity of the norm and step 1.1, while [F5] would give $v = 0$ because strong convergence and step 2.1 imply $\int_{Ω} v g = 0$ for every $g \in L^{(p^{*})^{'}}$ . Taking $g = sgn (v) ∣ v ∣^{p^{*} - 1}$ gives $\int ∣ v ∣^{p^{*}} = 0$ ; this contradiction shows that no subsequence converges strongly in $L^{p^{*}} (Ω)$ . The example therefore exhibits the failure of compactness at the critical exponent while for $1 \leq q < p^{*}$ the scaling exponent $(n - p) / p - n / q$ is negative, so the subcritical $L^{q}$ norms tend to zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

75 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, complete 168-page 2026 notes (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations, complete 242-page 2014 notes (standard reference, not scraped)