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

Expanding bumps lose tightness

Statement refuted

Refuted claim. On $R^{n}$ a bounded family in $W^{1, p} (R^{n})$ that is uniformly translation continuous is relatively compact in $L^{p} (R^{n})$ ; in other words the tightness condition of the Fr'echet--Kolmogorov criterion would be automatic for $W^{1, p}$ -bounded families.

The witness spreads one unit of mass over balls of radius tending to infinity. The $L^{p}$ norm and the translation modulus are controlled, but no fixed ball carries any of the mass in the limit, and no subsequence can converge in $L^{p} (R^{n})$ .

Facts & Assumptions

Given: Countable Choice; $n \geq 1$ , $1 \leq p < \infty$ , a nonzero $φ \in C_{c}^{\infty} (R^{n})$ with $∥ φ ∥_{L^{p} (R^{n})} = 1$ (for instance a normalised smooth bump), and $f_{j} (x) : = j^{- n / p} φ (x / j)$ for $j \geq 1$ .

[F1]

Scaling. For every measurable nonnegative $h$ and $j > 0$ , $\int_{R^{n}} h (x / j) j^{- n} d x = \int_{R^{n}} h (y) d y$ ; equivalently $\int_{R^{n}} h (j x) j^{n} d x = \int h$ . (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)

[F2]

Segment bound. For $φ \in C^{1}$ and $y, y^{'} \in R^{n}$ , $φ (y) - φ (y^{'}) = \int_{0}^{1} \nabla φ (y^{'} + t (y - y^{'})) \cdot (y - y^{'}) d t$ ; hence $∣ φ (y) - φ (y^{'}) ∣ \leq ∣ y - y^{'} ∣ \int_{0}^{1} ∣ \nabla φ (y^{'} + t (y - y^{'})) ∣ d t$ . (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative)

[F3]

Minkowski and Tonelli. For measurable $F$ on a product of sigma-finite spaces with $\int ∥ F (\cdot, t) ∥_{p} d t < \infty$ , $∥ \int F (\cdot, t) d t ∥_{p} \leq \int ∥ F (\cdot, t) ∥_{p} d t$ , and the iterated integral of a nonnegative measurable function may be computed in either order. (Minkowski's integral inequality, Tonelli and Fubini for the completed product, with only almost-everywhere section measurability)

[F4]

Dominated convergence. If $∣ h_{j} ∣ \leq g$ with $g$ integrable and $h_{j} \to h$ pointwise almost everywhere, then $\int h_{j} \to \int h$ . (Dominated convergence)

[F5]

Translation and balls. $(τ_{h} f) (x) = f (x - h)$ and $B (0, r) = {∣ x ∣ < r}$ ; a ball of radius $r$ has finite Lebesgue measure. (Translation of a function on $R^{n}$ , Open ball, closed ball and sphere in a metric space, The space $L^{p} (μ)$ as the quotient by null functions)

Counterexample

technique · direct

1.1F1F4F5given

By [F1] applied to $∣ φ ∣^{p}$ and to $∣ D φ ∣^{p}$ , $∥ f_{j} ∥_{L^{p}} = j^{- n / p} \cdot j^{n / p} ∥ φ ∥_{L^{p}} = 1$ and $∥ D f_{j} ∥_{L^{p}} = j^{- 1} ∥ D φ ∥_{L^{p}} \leq ∥ D φ ∥_{L^{p}}$ , and the same scaling holds for every derivative component. The classical derivatives are the weak derivatives by Classical derivatives agree with weak derivatives, so $(f_{j})$ is bounded in $L^{p}$ and in $W^{1, p} (R^{n})$ ; moreover $\int_{B (0, R)} ∣ f_{j} ∣^{p} d x = \int_{B (0, R / j)} ∣ φ (y) ∣^{p} d y \to 0$ as $j \to \infty$ for each fixed $R$ by [F4], since $∣ φ ∣^{p} 1_{B (0, R / j)} \leq ∣ φ ∣^{p}$ and the indicators tend to zero except at the null point $0$ .

1.2F1F2F3given

For fixed $h$ the segment bound [F2] applied to $φ$ at $y = (x - h) / j$ and $y^{'} = x / j$ gives $∣ f_{j} (x - h) - f_{j} (x) ∣ \leq j^{- n / p} ∣ h ∣ j^{- 1} \int_{0}^{1} ∣ \nabla φ ((x - t h) / j) ∣ d t$ ; taking $L^{p}$ norms and applying [F3] together with the translation and scaling identities of [F1] yields $∥ τ_{h} f_{j} - f_{j} ∥_{L^{p}} \leq ∣ h ∣ j^{- 1} ∥ D φ ∥_{L^{p}} \leq ∣ h ∣ ∥ D φ ∥_{L^{p}}$ , a bound independent of $j$ that tends to $0$ with $∣ h ∣$ ; hence the family is uniformly translation continuous.

2.1F4F5step 1.1step 1.2∎

The family is not tight: by [F1], $\int_{∣ x ∣ > R} ∣ f_{j} ∣^{p} d x = \int_{∣ y ∣ > R / j} ∣ φ (y) ∣^{p} d y \to \int_{R^{n}} ∣ φ ∣^{p} = 1$ for every fixed $R$ by [F4], so no $R$ makes the tails uniformly small; and it is not relatively compact, because if a subsequence converged in $L^{p} (R^{n})$ to some $g$ , then $∥ g ∥_{L^{p}} = 1$ by continuity of the norm, while step 1.1 forces $g = 0$ almost everywhere on each ball $B (0, R)$ and hence on all of $R^{n}$ , a contradiction. So boundedness and uniform translation continuity alone do not give relative compactness on $R^{n}$ . Countable Choice is inherited through the scaling, Sobolev and completed-product interfaces.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

84 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 notes) (standard reference, not scraped)
Juha Kinnunen, Sobolev Spaces (Aalto University, 2026, complete graduate lecture notes) (standard reference, not scraped)