LemmaStatement: 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 Banach-valued simple integral is well defined

Statement

The integral of an integrable Banach-valued simple function is independent of its disjoint measurable representation. It is linear, is unchanged when the integrand is changed on a null set, and satisfies

$∥ \int_{E} s d μ ∥ \leq \int_{E} ∥ s ∥ d μ$

for every measurable $E$ .

Facts & Assumptions

[L1]

An integrable $X$ -valued simple function and its proposed integral are as in Banach-valued simple function and integral.

[L2]

A measure is countably, hence finitely, additive on disjoint measurable families and assigns measure zero to the empty set (Measures on sigma-algebras).

[L3]

The nonnegative simple integral is the coefficient--measure sum, with $0 \cdot \infty = 0$ (The integral of a nonnegative simple function).

Proof

technique · direct

Given: Integrable simple functions on a measure space with values in a Banach space, as in the Statement.

1.1

Form a finite common refinement. [given, L1] Suppose $s = \sum_{j = 1}^{m} x_{j} 1_{A_{j}} = \sum_{k = 1}^{n} y_{k} 1_{B_{k}}$ are two representations from [L1]. Because every displayed coefficient is nonzero, both unions $⋃_{j} A_{j}$ and $⋃_{k} B_{k}$ are the same set ${ω : s (ω) \neq 0}$ . Hence the cells $C_{j k} = A_{j} \cap B_{k}$ with $1 \leq j \leq m$ and $1 \leq k \leq n$ partition every $A_{j}$ and every $B_{k}$ . On every nonempty $C_{j k}$ , pointwise equality gives $x_{j} = y_{k}$ .

givenL1algebra

2.1

Compare the two integral sums. By finite additivity in [L2], step 1.1 gives

L1L2step 1.1

$\sum_{j} μ (A_{j}) x_{j} = \sum_{j, k} μ (C_{j k}) x_{j} = \sum_{j, k} μ (C_{j k}) y_{k} = \sum_{k} μ (B_{k}) y_{k} .$

Every $C_{j k}$ lies in the finite-measure cells $A_{j}$ and $B_{k}$ , so every scalar-vector product in this display is defined. No complement cell and no $0 \cdot \infty$ convention is used. This proves representation independence.

3.1

Prove linearity. [L1, step 2.1] For integrable $s, t$ and scalars $a, b$ , refine their finite level partitions. On each refined cell $a s + b t$ has coefficient $a x_{j} + b y_{k}$ . Every cell on which this coefficient is nonzero lies in the union of the finite-measure supports of $s$ and $t$ , so $a s + b t$ is integrable. Applying step 2.1 and distributing the finite vector sum yields $\int_{E} (a s + b t) = a \int_{E} s + b \int_{E} t$ .

L1step 2.1algebra

4.1

Prove null-insensitivity. [L2, step 3.1] If integrable simple functions $s, t$ agree off a null set $N$ , refine their level partitions as above. A refined cell on which their coefficients differ is contained in $N$ , hence has measure zero by [L2]. Its contribution to $\int_{E} (s - t)$ is zero, and linearity from step 3.1 gives $\int_{E} s = \int_{E} t$ .

L2step 3.1algebra

5.1

Prove the norm inequality and conclude. [L1, L3, step 4.1] Write $s = \sum_{j} x_{j} 1_{A_{j}}$ in its nonzero disjoint-level form. The triangle inequality in $X$ , [L3], and the finite-measure support rule give

L1L3

$∥ \int_{E} s d μ ∥ = ∥ \sum_{j} μ (E \cap A_{j}) x_{j} ∥ \leq \sum_{j} μ (E \cap A_{j}) ∥ x_{j} ∥ = \int_{E} ∥ s ∥ d μ .$

This also covers the empty representation and $E = \emptyset$ : both sides are zero. ∎

Depends on

Used by

Bochner-integrable function Definition
A Bochner density defines an absolutely continuous vector measure Lemma
Bochner integral norm inequality Lemma
Dentable average ranges give vector-measure densities Lemma
Bochner dominated convergence theorem Theorem
Bounded linear maps commute with Bochner integration Theorem

Cited to discharge well-definedness by Banach-valued simple function and integral.

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

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