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.

Pettis measurability criterion for strong measurability

Statement

Assume the Axiom of Choice, let (Ω,A,μ) be a complete measure space, and let X be a real or complex Banach space. A function f:Ω→X is strongly measurable if and only if both conditions hold:

  1. f is weakly measurable: x∗∘f is scalar measurable for every x∗∈X∗;
  2. f is essentially separably valued: there are a null set N and a separable closed subspace Y⊆X such that f(Ω∖N)⊆Y.

Facts & Assumptions

[A1]

The Axiom of Choice holds (The Axiom of Choice).

[L1]

Strong measurability is a.e. pointwise norm approximation by measurable simple functions (Strongly measurable Banach-valued function).

[L2]

The dual consists of bounded scalar-valued linear functionals (The dual space X^* of a normed space and its dual norm).

[L3]

On a complete measure space, every subset of a measurable null set is measurable (Complete measure spaces), and measurability means that Borel preimages are measurable (A measurable function between measurable spaces).

[L4]

Separability means existence of an at most countable dense subset (Separability: the existence of an at most countable dense subset).

[L5]

Under AC, a dominated real linear functional extends to the whole real space (Hahn-Banach dominated extension theorem for real vector spaces).

Proof

technique · direct

Given: The assumptions and the two conditions in the Statement.

1.1givenL1L4

Strong measurability gives an essentially separable range. [given, L1, L4] Assume first that f is strongly measurable, witnessed by sn and N as in [L1]. The union of the finite ranges of the sn is countable. Its closed linear span Y is separable by [L4], and every f(ω) with ω∉N is a norm limit of points of Y. Thus f is essentially separably valued.

1.2givenL1L2L3

Strong measurability gives weak measurability. [given, L1, L2, L3] For x∗∈X∗, [L2] gives x∗(sn(ω))→x∗(f(ω)) off N. Each x∗∘sn is scalar simple and measurable. A pointwise scalar limit is measurable off N, and [L3] makes its arbitrary values on subsets of N measurable as well. Hence f is weakly measurable.

1.3givenL4choose

Fix countable dense data for the reverse implication. [given, L4, choose] Conversely assume conditions 1 and 2. If Y={0}, the constant zero simple functions converge to f off N, so suppose Y≠{0}. By [L4] choose a sequence (ym) dense in Y and a sequence (zk) dense in its unit sphere.

2.1A1L2L5step 1.3

Construct a countable norming family. [A1, L2, L5, step 1.3] For each k, in the complex case define on the underlying real plane Czk the norm-one real functional uk(azk)=Re⁡a; in the real case use uk(azk)=a on Rzk. Apply [L5] and [A1] to extend these simultaneously to real functionals Uk on the underlying real space of X. In the complex case put xk∗(x)=Uk(x)−iUk(ix); in the real case put xk∗=Uk. Then xk∗∈X∗, ∥xk∗∥=1, and xk∗(zk)=1. Consequently, for y∈Y,

∥y∥=sup⁡k∣xk∗(y)∣.

Indeed the upper bound is immediate, while a unit vector arbitrarily close to some zk makes the corresponding value arbitrarily close to 1.

3.1L3step 2.1

Norm distances to fixed centres are measurable. [L3, step 2.1] For fixed y∈Y, step 2.1 and weak measurability give, off N, ∥f−y∥=sup⁡k∣xk∗(f−y)∣. The right side is the supremum of a countable family of measurable scalar functions. With any values assigned on N, [L3] therefore makes ω↦∥f(ω)−y∥ measurable.

4.1L1step 1.3step 3.1

Build finite-valued nearest-centre approximants. [L1, step 1.3, step 3.1] For each n≥1 and ω∉N, choose the least m∈{1,…,n} minimizing ∥f(ω)−ym∥; put sn(ω)=ym there and sn=0 on N. The finitely many tie-broken Voronoi cells are measurable by step 3.1, so sn is a measurable simple function. Density of (ym) gives ∥sn(ω)−f(ω)∥→0 for every ω∉N.

5.1A1L1step 1.1step 1.2step 4.1∎

Steps 1.1--1.2 prove the forward implication, and step 4.1 supplies the simple approximants required by [L1] for the reverse implication. The only non-finite choice is [A1]: it supplies the Hahn--Banach extensions in step 2.1 (and hence also covers their countable simultaneous selection).

Depends on

Used by

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