Alphabeta Math
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.

Bochner integrability criterion

Statement

Let f:ΩX be strongly measurable. Then f is Bochner integrable if and only if

Ωfdμ<.

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

[L1]

Bochner integrability means L1 approximation by integrable simple functions and defines the integral as the norm limit of their integrals (Bochner-integrable function).

[L2]

Nonnegative integrals are monotone and positively homogeneous (Monotonicity and nonnegative homogeneity of the nonnegative integral) and additive (Additivity of the nonnegative Lebesgue integral).

[L3]

Pointwise limits and countable suprema of measurable scalar functions are measurable (Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable).

[L4]

Scalar dominated convergence gives convergence in L1 (Dominated convergence); its nonnegative foundation is monotone convergence (Monotone convergence for the integral).

Proof

technique · direct

Given: A strongly measurable f and the conventions in the Statement.

1.1

Prove necessity of scalar norm integrability. [given, L1, L2] Suppose first that f is Bochner integrable and choose (sn) as in [L1]. For some n, fsn<, while integrability of the simple function gives sn<. Since ffsn+sn, [L2] gives f<.

givenL1L2
1.2

Prove approximation independence. [given, L1] If (sn) and (tn) are any two defining approximations, the simple norm inequality gives sntnsntn, which is at most snf+ftn. Both terms tend to zero, so the two norm limits coincide.

givenL1
1.3

Construct dominated simple approximants for sufficiency. [given, L3, construct] Conversely assume f<. On the exceptional measurable null set of a strong approximation, replace both f and every approximant by zero (and call the representative again f). Thus measurable simple functions un converge pointwise to f; [L3] makes f measurable. Define sn=un1{un2f}. Then sn is simple and measurable, sn2f, and snf pointwise: when f(ω)0, the inequality defining the retained part holds eventually, while at a zero of f either retained values tend to zero or the replacement is zero.

givenL3construct
2.1

Verify that the constructed simple functions are integrable. [L2, step 1.3] Each sn is integrable. Indeed, if a nonzero value x occurs, its level set is contained in {2fx}, whose measure is at most 2f/x< by [L2].

L2step 1.3
3.1

Obtain convergence in L1. [L1, L4, step 1.3, step 2.1] The pointwise convergence in step 1.3 and fsn3f allow [L4] to be applied. Hence fsn0. Together with step 2.1 this is exactly the approximation required in [L1].

L1L4step 1.3step 2.1
4.1

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.

L1step 1.1step 1.2step 3.1

Depends on

Used by

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