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

Uniformly supported families have vanishing tails

Statement

Let $1 \leq p < \infty$ , let $E \subseteq R^{n}$ be bounded and let $F \subseteq L^{p} (R^{n})$ be a family such that every $f \in F$ vanishes Lebesgue-almost everywhere outside $E$ . In the displayed nonnegative supremum, take the value $0$ if $F = \emptyset$ . Then for every $ε > 0$ there is $R > 0$ with $\sup_{f \in F} \int_{∣ x ∣ > R} ∣ f (x) ∣^{p} d x < ε .$ In particular the tightness hypothesis of the Fr'echet--Kolmogorov criterion is automatic for families supported in one bounded set.

Facts & Assumptions

Given: $1 \leq p < \infty$ , a bounded set $E \subseteq R^{n}$ , and a family $F \subseteq L^{p} (R^{n})$ whose every member vanishes almost everywhere outside $E$ .

[F1]

Bounded sets lie in balls. $E \subseteq R^{n}$ is bounded in the metric sense of Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space if and only if there is a centre $x_{0}$ and a radius $r > 0$ with $E \subseteq B (x_{0}, r)$ ; a ball is contained in the ball about the origin of radius $∣ x_{0} ∣ + r$ . (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Open ball, closed ball and sphere in a metric space)

[F2]

Restriction to a measurable tail. If $A \subseteq E^{c}$ is measurable and $f$ vanishes almost everywhere on $E^{c}$ , then for any measurable representative $g$ the function $∣ g ∣^{p} 1_{A}$ is measurable and zero almost everywhere. (The space $L^{p} (μ)$ as the quotient by null functions, Measure-null sets and almost-everywhere statements relative to a measure)

[F3]

Zero integral and almost-everywhere vanishing. A nonnegative measurable $h$ satisfies $\int h d x = 0$ if and only if $h = 0$ almost everywhere. (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere)

Proof

Proof technique: Choose a ball containing $E$ and use the given almost-everywhere vanishing on the measurable tail outside that ball.

1.1F1F2F3given

By [F1] fix $R > 0$ with $E \subseteq B (0, R)$ and put $A : = {∣ x ∣ > R}$ . The set $A$ is measurable and is contained in $E^{c}$ . If $F = \emptyset$ then its tail supremum is $0 < ε$ . Otherwise, for each $f \in F$ the hypothesis says that $f$ vanishes almost everywhere on $E^{c}$ , hence on $A$ ; by [F2] the measurable function $∣ g ∣^{p} 1_{A}$ is zero almost everywhere for any representative $g$ of $f$ , so [F3] gives $\int_{A} ∣ f ∣^{p} d x = 0$ .

2.1step 1.1given∎

Every member of $F$ has tail integral $0$ by step 1.1, so $\sup_{f \in F} \int_{∣ x ∣ > R} ∣ f ∣^{p} d x = 0 < ε$ . Since $ε > 0$ was arbitrary, the tightness condition of the Fr'echet--Kolmogorov criterion holds. The argument uses no choice principle: $R$ is obtained from the single bounded set $E$ and the supremum is evaluated at the constant value $0$ .

Depends on

Used by

Dependency tree · two levels

26 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)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (archived 2025 author manuscript) (standard reference, not scraped)