LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck pass

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 finitely additive integral is well-defined and isometric

Statement

For every $ν \in b a (P (N))$ , the finite-range formula $I_{ν}^{0}$ is representation-independent and has a unique bounded linear extension $I_{ν} \in (ℓ^{\infty})^{*}$ . Moreover

$∥ I_{ν} ∥ = ∣ ν ∣ (N) .$

Consequently $ν \mapsto I_{ν}$ is a linear isometry into $(ℓ^{\infty})^{*}$ .

Facts & Assumptions

[L1]

Finite-range sequences are uniformly dense in $ℓ^{\infty}$ , and the finite-range integral is the partition formula (The finitely additive integral on ell-infinity).

[L2]

The scalar fields $R$ and $C$ are complete (The reals are complete, The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts).

Proof

technique · direct

Given: The objects and hypotheses in the Statement.

1.1L1algebra

Two partition representations of $s$ have the common refinement [given, L1] $(A_{j} \cap B_{k})_{j, k}$ . Finite additivity replaces each original summand by its sum over the refinement; because both coefficients equal $s_{n}$ on a nonempty cell, the two refined sums agree. Thus $I_{ν}^{0}$ is well-defined and linear.

2.1L1givenalgebra

For a partition representation, [given, L1, step 1.1] $∣ I_{ν}^{0} (s) ∣ \leq \sum_{j} ∣ c_{j} ∣ ∣ ν (A_{j}) ∣ \leq ∥ s ∥_{\infty} ∣ ν ∣ (N) .$ Hence $I_{ν}^{0}$ is bounded with norm at most $∣ ν ∣ (N)$ .

3.1L2step 2.1algebra

Use the fixed dyadic grid to define a finite-range quantization $q_{k} (x)$ [given, L2, step 2.1] with $∥ q_{k} (x) - x ∥_{\infty} \leq 2^{- k}$ ; over $C$ , use squares of side $2^{- k - 1}$ , whose diameter is less than $2^{- k}$ . Step 2.1 makes $(I_{ν}^{0} (q_{k} (x)))_{k}$ Cauchy; [L2] supplies its limit. The same estimate shows independence of any approximating finite-range sequence, linearity, uniqueness, and the bound $∥ I_{ν} ∥ \leq ∣ ν ∣ (N)$ .

4.1step 1.1step 3.1givenchoose∎

Given $ε > 0$ , choose a finite partition $(A_{j})$ with [given, step 3.1] $\sum_{j} ∣ ν (A_{j}) ∣ > ∣ ν ∣ (N) - ε$ . Put $c_{j} = 1$ when $ν (A_{j}) = 0$ and otherwise $c_{j} = \overline{ν (A_{j})} / ∣ ν (A_{j}) ∣$ (the same sign formula over $R$ ). Then $∥ \sum_{j} c_{j} 1_{A_{j}} ∥_{\infty} = 1$ and its integral is $\sum_{j} ∣ ν (A_{j}) ∣$ . Thus $∥ I_{ν} ∥ \geq ∣ ν ∣ (N) - ε$ ; letting $ε ↓ 0$ proves equality. Linearity in $ν$ is immediate from the formula.

Depends on

Used by

The dual of ell-infinity is ba Theorem

Cited to discharge well-definedness by The finitely additive integral on ell-infinity.

Dependency tree · two levels

23 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)