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

The dual of ell-infinity is ba

Statement

The map

$Φ : (ℓ^{\infty})^{*} ⟶ b a (P (N)), Φ (φ) (A) : = φ (1_{A}),$

is a linear isometric isomorphism. Its inverse sends $ν$ to the finitely additive integral $I_{ν}$ .

Facts & Assumptions

[L1]

For each finite-variation charge, $I_{ν}$ is a bounded functional and $∥ I_{ν} ∥ = ∣ ν ∣ (N)$ (The finitely additive integral is well-defined and isometric).

[L2]

The dual consists of bounded scalar-valued linear functionals with the operator norm (The dual space X^* of a normed space and its dual norm).

Proof

technique · direct

Given: The objects and hypotheses in the Statement.

1.1

Let $φ \in (ℓ^{\infty})^{*}$ and put $ν_{φ} (A) = φ (1_{A})$ . Linearity and $1_{A ⊔ B} = 1_{A} + 1_{B}$ give finite additivity. For a finite partition $(A_{j})$ choose scalar phases $c_{j}$ with $c_{j} ν_{φ} (A_{j}) = ∣ ν_{φ} (A_{j}) ∣$ . Then $∥ \sum_{j} c_{j} 1_{A_{j}} ∥_{\infty} = 1$ and [L2] gives

givenL2

$\sum_{j} ∣ ν_{φ} (A_{j}) ∣ = φ (\sum_{j} c_{j} 1_{A_{j}}) \leq ∥ φ ∥ .$

Thus $ν_{φ} \in b a$ and $∥ ν_{φ} ∥_{b a} \leq ∥ φ ∥$ . [L2, finite additivity, phases]

2.1

By construction, $I_{ν_{φ}} (1_{A}) = φ (1_{A})$ . [given, L1, step 1.1] Linearity gives equality on finite-range sequences, and density plus boundedness gives $I_{ν_{φ}} = φ$ on $ℓ^{\infty}$ .

L1step 1.1algebra

3.1

Conversely, $Φ (I_{ν}) (A) = I_{ν} (1_{A}) = ν (A)$ , so the two maps are [given, L1, step 2.1] inverse. Finally [L1] gives $∥ I_{ν} ∥ = ∥ ν ∥_{b a}$ , proving isometry and completing both surjectivity and injectivity.

L1step 2.1∎

Depends on

Used by

The countably additive part of ba is ell-one Corollary
Ell-one and ell-infinity are not reflexive Counterexample
A Banach mean revisited as a charge Example

Dependency tree · two levels

9 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

Michael Müger, Introduction to Functional Analysis (standard reference, not scraped)