ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Dunford--Pettis: dominated and concentrating families

Example

Assume the Axiom of Choice, and let $I = [0, 1]$ carry restricted Lebesgue measure. Two contrasting families in real $L^{1} (I)$ are as follows.

If $g \in L^{1} (I)$ is nonnegative and $K_{g} \subseteq {f \in L^{1} (I) : ∣ f ∣ \leq g almost everywhere}$ , then $K_{g}$ is uniformly integrable and relatively weakly compact.
The concentrating sequence $f_{n} = n 1_{(0, 1 / n)}$ , $n \geq 1$ , is bounded in $L^{1} (I)$ but is neither uniformly integrable nor relatively weakly compact.

Facts & Assumptions

[A1]

AC holds and supplies Countable Choice (The Axiom of Choice, AC supplies the countable and dependent choices used in Banach integration).

[L1]

Under Countable Choice, Lebesgue measure is complete and intervals have their lengths; restriction to a measurable set is again a measure (Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ , Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, Restriction of a measure to a measurable set, The restriction of a measure to a measurable set is a measure).

[L2]

Real $L^{1}$ consists of almost-everywhere classes with the integral norm, and the integral of a nonnegative simple function is its finite weighted sum (The space $L^{p} (μ)$ as the quotient by null functions, The $L^{p}$ norm descends to the quotient and makes $L^{p}$ a normed space for $1 \leq p \leq \infty$ , The integral of a nonnegative simple function).

[L3]

Every individual $L^{1}$ function has absolutely continuous integral (Absolute continuity of the integral).

[L4]

Under AC, a family in real $L^{1}$ on a finite measure space is relatively weakly compact exactly when it is uniformly integrable, equivalently norm bounded with uniformly absolutely continuous integrals (Dunford--Pettis for real $L^{1}$ on a finite measure space).

Verification

technique · counterexample

Given: AC, the restricted Lebesgue interval, a nonnegative $g \in L^{1}$ , a dominated family $K_{g}$ , and the displayed spike sequence.

1.1

Fix the finite quotient-space model. Let $λ_{I} (E) = λ (E \cap I)$ on the ambient Lebesgue sigma-algebra. By [L1] this is a finite measure with $λ_{I} (I) = 1$ . We use the quotient $L^{1} (λ_{I})$ from [L2], so changes outside $I$ or on null endpoints do not change a class.

givenA1L1L2

2.1

Prove uniform integrability of the dominated family. For $f \in K_{g}$ , domination gives $∥ f ∥_{1} \leq \int_{I} g$ , uniformly in $f$ . Given $ε > 0$ , [L3] supplies $δ > 0$ such that $λ_{I} (E) < δ$ implies $\int_{E} g < ε$ . Then $\int_{E} ∣ f ∣ \leq \int_{E} g < ε$ for every $f \in K_{g}$ . Thus the two conditions in [L4] hold, so $K_{g}$ is uniformly integrable and relatively weakly compact.

L2L3L4step 1.1

2.2

Calculate the concentrating sequence. For every $n \geq 1$ , the nonnegative simple-integral formula and interval length give

L1L2step 1.1construct

$∥ f_{n} ∥_{1} = n λ_{I} ((0, 1 / n)) = n \cdot \frac{1}{n} = 1.$

Hence $(f_{n})$ is $L^{1}$ bounded. But for $E_{n} = (0, 1 / n)$ one has $λ_{I} (E_{n}) = 1 / n \to 0$ while $\int_{E_{n}} ∣ f_{n} ∣ = 1$ .

3.1

Fail uniform integrability and weak compactness. Taking, for example, $ε = 1 / 2$ , step 2.2 shows that no single $δ > 0$ works for the uniform absolute-continuity condition: choose $n > 1 / δ$ . Therefore the family ${f_{n} : n \geq 1}$ is not uniformly integrable. The reverse implication in [L4] then shows that it is not relatively weakly compact.

A1L4step 2.2

4.1

Audit the endpoints and degenerate families. [A1, L1, L2, L3, L4, step 1.1, step 2.1, step 2.2, step 3.1] If $K_{g} = \emptyset$ , both conclusions in part 1 are vacuous. If $g = 0$ , every dominated $L^{1}$ class is zero, so the conclusion is the compact singleton case. Open, closed, or half-open spike intervals define the same class because their endpoint differences are null. The spikes are real and nonnegative; their obstruction is concentration on shrinking positive-measure sets, not unbounded $L^{1}$ norm. AC is used exactly through [L4] and to supply the Countable Choice in the Lebesgue model [L1].

givenA1L1L2L3L4step 1.1step 2.1step 2.2step 3.1∎

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

Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (standard reference, not scraped)