ExampleConstruction: AI-generatedVerification: AI-generatedprecheck 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.

Bochner integral of a countably valued function

Example

Let $(S, A, μ)$ be a measure space, let $X$ be a real or complex Banach space, let $(A_{n})_{n \geq 1}$ be pairwise disjoint measurable sets, and let $(x_{n})_{n \geq 1}$ be a sequence in $X$ such that

$\sum_{n = 1}^{\infty} μ (A_{n}) ∥ x_{n} ∥ < \infty .$

With the convention that the value is zero off $⋃_{n} A_{n}$ , the pointwise sum

$f = \sum_{n = 1}^{\infty} x_{n} 1_{A_{n}}$

is Bochner integrable. Its integral, and more generally every restricted integral, is the absolutely convergent vector series

$\int_{E} f d μ = \sum_{n = 1}^{\infty} μ (E \cap A_{n}) x_{n} (E \in A) .$

As in the simple-integral definition, a term with $x_{n} = 0$ is zero even when $μ (A_{n}) = \infty$ .

Facts & Assumptions

[L1]

Integrable Banach-valued simple functions have the stated finite-sum integral, and their integrals satisfy the norm inequality (Banach-valued simple function and integral, Bochner integral norm inequality).

[L2]

A strongly measurable function with integrable norm is Bochner integrable, and its integral is the limit obtained from any defining $L^{1}$ -simple approximation (Bochner integrability criterion, Bochner-integrable function).

[L3]

Monotone convergence calculates integrals of increasing nonnegative partial sums (Monotone convergence for the integral).

Verification

technique · direct

Given: the measure space, Banach space, disjoint sets, vectors, and finite weighted norm series in the Statement.

1.1

Form the finite simple approximants. For $N \geq 1$ , put $s_{N} = \sum_{n = 1}^{N} x_{n} 1_{A_{n}}$ . If $x_{n} \neq 0$ , the finiteness of the displayed series forces $μ (A_{n}) < \infty$ ; zero levels need no finite-measure hypothesis. Thus every $s_{N}$ is an integrable simple function in the precise sense of [L1]. Pairwise disjointness gives $s_{N} (t) \to f (t)$ for every $t$ : at most one summand is nonzero at any point.

givenL1

2.1

Calculate the scalar approximation error. Pointwise disjointness gives $∥ f - s_{N} ∥ = \sum_{n > N} ∥ x_{n} ∥ 1_{A_{n}}$ . Applying monotone convergence in [L3] to its finite partial sums yields

givenL3step 1.1

$\int_{S} ∥ f - s_{N} ∥ d μ = \sum_{n > N} μ (A_{n}) ∥ x_{n} ∥ ⟶ 0.$

The same calculation with $N = 0$ shows $\int_{S} ∥ f ∥ = \sum_{n} μ (A_{n}) ∥ x_{n} ∥ < \infty$ .

3.1

Establish Bochner integrability and identify the unrestricted integral. The everywhere simple convergence in step 1.1 proves strong measurability, and step 2.1 gives integrability of the norm. Hence [L2] makes $f$ Bochner integrable. Moreover, $(s_{N})$ is a defining $L^{1}$ -simple approximation, so

L1L2step 1.1step 2.1

$\int_{S} f d μ = \lim_{N \to \infty} \int_{S} s_{N} d μ = \lim_{N \to \infty} \sum_{n = 1}^{N} μ (A_{n}) x_{n} .$

This vector limit exists absolutely because the sum of the norms of its terms is the assumed finite scalar series; completeness of $X$ is used here.

4.1

Calculate every restricted integral and audit the boundary cases. [L1, L2, step 2.1, step 3.1] For measurable $E$ , the functions $1_{E} s_{N}$ approximate $1_{E} f$ in $L^{1}$ , since their error integral is at most the tail in step 2.1. The simple calculation from [L1] therefore gives $\int_{E} f = \sum_{n} μ (E \cap A_{n}) x_{n}$ . If $E = \emptyset$ , if every $A_{n}$ is empty, or if every $x_{n} = 0$ , both sides are zero. A single nonzero level reduces to the defining simple-function formula. Infinite-measure zero levels cause no undefined product, while a nonzero level automatically has finite measure.

givenL1L2step 1.1step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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