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

Dentable average ranges give vector-measure densities

Statement

Assume the Axiom of Choice. If every nonempty bounded closed convex subset of a Banach space X is dentable, then X has the Radon--Nikodym property.

Facts & Assumptions

[A1]

The Axiom of Choice supplies choices from arbitrary nonempty families (The Axiom of Choice).

[L1]

RNP asks for a Bochner density of every bounded-variation vector measure absolutely continuous with respect to a finite scalar measure (Radon--Nikodym property).

[L2]

Dentability means existence of slices of arbitrarily small norm diameter (Dentable bounded set and slice).

[L3]

The variation of a bounded-variation vector measure is a finite positive measure (Bounded variation of a vector measure is a finite measure).

[L4]

Under AC, an absolutely continuous finite scalar measure has an integrable Radon--Nikodym density (A sigma-finite signed measure that is absolutely continuous with respect to a sigma-finite positive measure has a unique almost-everywhere density), and integration against that density agrees with integration for the density measure (Integrating against a density agrees with integrating the product).

[L5]

A Bochner density measure has variation equal to the integral of its norm (A Bochner density defines an absolutely continuous vector measure).

[L6]

Strong measurability plus finite norm integral is equivalent to Bochner integrability (Bochner integrability criterion); nonnegative monotone convergence controls increasing sums (Monotone convergence for the integral).

[L7]

Simple Banach-valued integrals are linear and computed level by level (The Banach-valued simple integral is well defined).

Proof

technique · direct

Given: The dentability hypothesis and data (Ω,A,μ,ν) from [L1].

1.1givenA1L1L3L4

Normalize by the variation measure. Put ρ=∣ν∣. By [L3], ρ is finite, and ν≪μ implies ρ≪μ by refining subsets of a μ-null set. If ρ(Ω)=0, ν=0 has the zero density. Otherwise [L4], using [A1], gives w≥0 with ρ=w dμ. We first construct a density with respect to ρ, for which ∣ν∣≤ρ holds tautologically.

1.2givenL2

Pass dentability to every average range. For A with ρ(A)>0, put xA=ν(A)/ρ(A) and DA={xB:B⊆A, ρ(B)>0}. Then ∥xB∥≤1. The closed convex hull CA is nonempty, bounded, and dentable by hypothesis. A small slice of CA meets DA, because its defining supremum over CA equals the supremum over DA; its intersection with DA has no larger diameter. Thus every DA is dentable.

2.1A1L2step 1.2

Find a positive subset with a small average range. Fix ε>0 and positive A. If every positive B⊆A had diam⁡DB>2ε, then for each such B and every x∈X some positive C⊆B would satisfy ∥x−xC∥>ε. Using [A1] and a maximal-disjoint-family argument, choose disjoint positive Bj⊆B with ∥xB−xBj∥>ε which exhaust B modulo ρ. Norm countable additivity gives xB=∑jρ(Bj)xBj/ρ(B), so xB lies in the closed convex hull of points of DA more than ε away. A slice of DA of diameter less than ε cannot contain both xB and a member of this convex combination above the same slice threshold, contradicting step 1.2. Hence some positive B⊆A has diam⁡DB≤2ε.

3.1A1L5L6step 2.1construct

Exhaust the space by good pieces and estimate the error. Choose a maximal disjoint family (Aj) of positive sets with diam⁡DAj≤2ε. Step 2.1 forces it to cover Ω modulo ρ; finiteness of ρ makes the family countable. Put gε=∑j1AjxAj. Its finite partial sums show strong measurability, and ∥gε∥≤1, so [L6] gives Bochner integrability. For measurable E, ν(E)−∫Egε dρ is the sum over j of ρ(E∩Aj)(xE∩Aj−xAj) (zero intersections omitted). Consequently every finite partition of E gives the variation estimate ∣ν−gερ∣(E)≤2ερ(E).

4.1A1L5step 3.1

Produce an L1(ρ;X)-Cauchy sequence. Use [A1] to choose gn=g2−n for all n. By [L5] and the triangle inequality for variation, ∫∥gn−gn−1∥ dρ≤∣ν−gnρ∣(Ω)+∣ν−gn−1ρ∣(Ω)≤6⋅2−nρ(Ω). Thus the series of L1 differences is summable.

5.1L5L6step 3.1step 4.1

Construct and identify the normalized density. By [L6], monotone convergence applied to ∑n=1N∥gn−gn−1∥ shows that the norm series is finite a.e. Hence, by completeness of X, g0+∑n≥1(gn−gn−1) converges a.e. to a strongly measurable h, and the same tail estimate gives gn→h in L1(ρ;X). The criterion in [L6] makes h Bochner integrable. For every E, step 3.1 and the norm integral inequality give ∥ν(E)−∫Eh dρ∥≤21−nρ(E)+∫E∥gn−h∥ dρ→0. Thus ν(E)=∫Eh dρ.

6.1L4L6L7step 1.1step 5.1

Transfer the density back to the original control measure. Set f=wh (and f=0 where w=0). Products of scalar and vector simple approximants show that f is strongly measurable. By [L4], ∫∥f∥ dμ=∫∥h∥ dρ<∞, so [L6] makes f Bochner integrable. If sn→h in L1(ρ;X) are simple, [L7] and [L4] give ∫Ewsn dμ=∫Esn dρ level by level, while [L4] identifies the two L1 errors. Passing to the limit yields ∫Ef dμ=∫Eh dρ=ν(E).

7.1A1L1step 1.1step 6.1∎

Conclude RNP and record the choice cost. [A1, L1, step 6.1] The construction applies to arbitrary data in [L1], so X has RNP. The exact non-finite uses of [A1] are scalar Radon--Nikodym in step 1.1, maximal disjoint families in steps 2.1 and 3.1, and simultaneous selection of the sequence (gn) in step 4.1. Empty and zero-variation cases were settled in step 1.1; one-piece exhaustions are included in step 3.1.

Depends on

Used by

Dependency tree · two levels

41 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