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 integrability criterion
Statement
Let be strongly measurable. Then is Bochner integrable if and only if
Here an a.e.-defined scalar function is integrated through any measurable representative supplied by the strong simple approximation. Moreover the Bochner integral is independent of the approximating sequence in its definition.
Facts & Assumptions
Bochner integrability means approximation by integrable simple functions and defines the integral as the norm limit of their integrals (Bochner-integrable function).
Nonnegative integrals are monotone and positively homogeneous (Monotonicity and nonnegative homogeneity of the nonnegative integral) and additive (Additivity of the nonnegative Lebesgue integral).
Pointwise limits and countable suprema of measurable scalar functions are measurable (Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable).
Scalar dominated convergence gives convergence in (Dominated convergence); its nonnegative foundation is monotone convergence (Monotone convergence for the integral).
Proof
Given: A strongly measurable and the conventions in the Statement.
Prove necessity of scalar norm integrability. [given, L1, L2] Suppose first that is Bochner integrable and choose as in [L1]. For some , , while integrability of the simple function gives . Since , [L2] gives .
Prove approximation independence. [given, L1] If and are any two defining approximations, the simple norm inequality gives , which is at most . Both terms tend to zero, so the two norm limits coincide.
Construct dominated simple approximants for sufficiency. [given, L3, construct] Conversely assume . On the exceptional measurable null set of a strong approximation, replace both and every approximant by zero (and call the representative again ). Thus measurable simple functions converge pointwise to ; [L3] makes measurable. Define . Then is simple and measurable, , and pointwise: when , the inequality defining the retained part holds eventually, while at a zero of either retained values tend to zero or the replacement is zero.
Verify that the constructed simple functions are integrable. [L2, step 1.3] Each is integrable. Indeed, if a nonzero value occurs, its level set is contained in , whose measure is at most by [L2].
Obtain convergence in . [L1, L4, step 1.3, step 2.1] The pointwise convergence in step 1.3 and allow [L4] to be applied. Hence . Together with step 2.1 this is exactly the approximation required in [L1].
Step 1.1 proves necessity, step 3.1 proves sufficiency, and step 1.2 proves that the resulting integral is approximation-independent. The zero function, the empty measure space, and a single simple function are included by taking the constant zero or constant simple approximation.
Depends on
- Bochner-integrable function
- Monotone convergence for the integral
- Dominated convergence
- Additivity of the nonnegative Lebesgue integral
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
Used by
- Bochner integral of a countably valued function Example
- Vector measure induced by an L-one function Example
- 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
- RNP and almost-everywhere differentiability of Lipschitz curves Theorem
- Separable dual spaces have the Radon--Nikodym property Theorem
Cited to discharge well-definedness by Bochner-integrable function.
Dependency tree · two levels
25 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)