ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 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.

Reflexivity of $ℓ^{p}$ and $L^{p}$

Statement

Assume countable choice ${A C}_{ω}$ . For every measure space $(S, A, μ)$ and every $1 < p < \infty$ , both real and complex $L^{p} (μ)$ are reflexive. In particular, real and complex $ℓ^{p}$ are reflexive in this exponent range.

The open range is essential. Real and complex $c_{0}$ are not reflexive. If, in addition to ${A C}_{ω}$ , the ultrafilter lemma, dependent choice, and the relative Hahn--Banach principle are assumed, then real and complex $ℓ^{1}$ and $ℓ^{\infty}$ are not reflexive. In particular, counting measure gives an $L^{\infty}$ endpoint counterexample.

Facts & Assumptions

Given: Countable choice, an arbitrary measure space, an exponent $1 < p < \infty$ , and a scalar field $K \in {R, C}$ ; for the $ℓ^{1}$ endpoint clause also the ultrafilter lemma, DC, and relative HB.

[F1]

Under ${A C}_{ω}$ , real and complex $L^{p}$ over an arbitrary measure space are reflexive for $1 < p < \infty$ (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Reflexivity of Lp for one less p less infinity).

[F2]

On counting measure on $N$ , real $L^{p}$ is exactly real $ℓ^{p}$ with the same norm. For complex functions, the complex $L^{p}$ definition uses the same integral of the real nonnegative modulus $∣ f ∣^{p}$ ; applying the counting-measure identity to that modulus gives $∥ f ∥_{p}^{p} = \sum_{k} ∣ f (k) ∣^{p}$ . Since counting measure has no nonempty null set, its a.e. quotient is equality everywhere, so complex $L^{p}$ is isometrically complex $ℓ^{p}$ as well ( $ℓ^{p}$ is the $L^{p}$ space of counting measure, Complex Lp classes and Euclidean test-function conventions).

[F3]

Under the ultrafilter lemma, DC, and relative HB, neither real nor complex $ℓ^{1}$ is reflexive (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The real dominated-extension principle as an additional hypothesis over ZF, Ell one is not reflexive).

[F4]

Real and complex $c_{0}$ are Banach without choice (Real and complex $c_{0}$ are Banach). A Banach space is reflexive exactly when its canonical evaluation map $J_{X} : X \to X^{* *}$ is onto (Reflexivity is surjectivity of the canonical map). The bilinear sequence-pairing identifications give $c_{0} (K)^{*} = ℓ^{1} (K)$ ; the real dual of $ℓ^{1}$ is $ℓ^{\infty}$ by counting-measure duality, and the complex dual is $ℓ^{\infty} (C)$ by the complex sequence theorem (The continuous dual of c0 is ell-one, Counting measure specializes the representation theorem to $ℓ^{p}$ and $ℓ^{q}$ , The complex continuous dual of ell-one is ell-infinity). A sequence lies in $c_{0}$ exactly when it tends to zero, while $ℓ^{\infty}$ contains every bounded sequence (The sequence spaces c_0 and ell-infinity).

[F5]

$c_{0} (K)$ is a closed linear subspace of $ℓ^{\infty} (K)$ (c_0 is a closed subspace of ell-infinity). Under the assumed relative Hahn--Banach principle, every closed linear subspace of a reflexive real or complex Banach space is reflexive (Closed subspaces of reflexive spaces are reflexive).

Proof

technique · Specialize arbitrary-measure reflexivity to counting measure, then compute the canonical image of $c_0$ under the published bilinear duality identifications

1.1

The first assertion is exactly [F1]: under ${A C}_{ω}$ , both scalar versions of $L^{p} (μ)$ are reflexive for every measure space and every $1 < p < \infty$ . Empty and zero measure spaces are included; their $L^{p}$ spaces are zero and the cited theorem still applies.

F1given

1.2

Under the three additional principles stated for the endpoint clause, [F3] gives nonreflexivity of both real and complex $ℓ^{1}$ . Those principles are used here only through that cited corollary.

F3given

1.3

The $c_{0}$ conclusion needs none of those additional principles. Fix $K$ . By [F4], $c_{0} (K)$ is a Banach space. Let $T : ℓ^{1} (K) \to c_{0} (K)^{*}$ be the isometric bijection in [F4], so $T (a) (x) = \sum_{n} a_{n} x_{n}$ . Identify $(ℓ^{1} (K))^{*}$ with $ℓ^{\infty} (K)$ by [F4], using the same bilinear series pairing. For $x \in c_{0}$ and $a \in ℓ^{1}$ , $J_{c_{0}} (x) (T (a)) = T (a) (x) = \sum_{n} a_{n} x_{n} .$ Thus, under the composite identification $c_{0}^{* *} ≅ ℓ^{\infty}$ , the canonical image $J_{c_{0}} (x)$ is exactly the bounded sequence $x$ . The constant sequence $1 = (1, 1, \dots)$ belongs to $ℓ^{\infty}$ but not to $c_{0}$ by [F4], so it is a concrete bidual element outside $J_{c_{0}} (c_{0})$ . Hence $J_{c_{0}}$ is not onto and [F4] proves that real and complex $c_{0}$ are not reflexive.

Under relative Hahn--Banach, suppose $ℓ^{\infty} (K)$ were reflexive. Then it would be a reflexive Banach space, and [F5] would make its closed subspace $c_{0} (K)$ reflexive, contradicting the preceding canonical-image calculation. Hence $ℓ^{\infty} (K)$ is not reflexive, for either scalar field. The ultrafilter lemma and DC in the endpoint hypotheses are needed for the selected $ℓ^{1}$ proof, not for this $ℓ^{\infty}$ argument. [F4, F5]

2.1

Give $N$ counting measure. By [F2], the real or complex $L^{p}$ space in step 1.1 is isometrically the corresponding $ℓ^{p}$ . Reflexivity therefore gives the asserted sequence-space specialization.

step 1.1F2

For counting measure, no nonempty subset is null, so the essential-supremum norm on $L^{\infty} (N)$ is the ordinary supremum norm and its a.e. equivalence is equality. Thus $L^{\infty} (N; K)$ is isometrically $ℓ^{\infty} (K)$ ; Step 1.3 supplies the claimed $L^{\infty}$ endpoint counterexample under its exact assumptions. [F2, F4, step 1.3]

3.1

Steps 1.1 and 2.1 prove the positive result in the entire open exponent range, while steps 1.2, 1.3, and 2.1 provide the promised failures outside it. Countable choice is used through the arbitrary-measure $L^{p}$ theorem. The ultrafilter lemma, DC, and relative HB are additionally used only for the selected $ℓ^{1}$ proof; the direct canonical-image proof for $c_{0}$ is choice-free. No assertion about reflexivity of $L^{1}$ or $L^{\infty}$ on every measure space is made.

step 1.1step 2.1step 1.2step 1.3F1F3F5∎

Remarks

The ultrafilter lemma is a hypothesis of the $ℓ^{1}$ endpoint clause, not a result consumed from its proof: the clause above states the assumption in full. The library states the ultrafilter lemma, and proves it from AC, as The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter; this example assumes the lemma and inherits no part of that AC-based proof.

Source notes

Teschl's sequence-space examples after Theorem 4.20 identify reflexivity of $ℓ^{p}$ for $1 < p < \infty$ and compute the canonical image of $c_{0}$ as the proper inclusion $c_{0} \subset ℓ^{\infty}$ (printed p. 116). The arbitrary-measure and complex-scalar claims here use the stronger local suppliers listed above. The $ℓ^{1}$ endpoint retains the exact assumptions of the library's selected Schur/Eberlein--Smulian proof rather than silently weakening them from the source's classical setting.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 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

Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)

Reflexivity of ℓpℓp and LpLp