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.

Nondentability produces a vector measure without density

Statement

Assume the Axiom of Choice. If a Banach space X contains a nondentable nonempty bounded closed convex set, then on the Lebesgue interval there is an absolutely continuous bounded-variation X-valued vector measure whose range lies in a closed separable subspace of X and which has no Bochner density.

Facts & Assumptions

[A1]

The Axiom of Choice supplies arbitrary and recursive choices (The Axiom of Choice).

[L1]

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

[L2]

Under AC, dominated Hahn--Banach establishes HB, and under HB a point outside a nonempty closed convex set in a real or complex normed space can be uniformly strictly separated from it by a bounded functional (Hahn-Banach dominated extension theorem for real vector spaces, Relative geometric Hahn–Banach with the exact open, closed, and compact hypotheses).

[L3]

RNP requires a Bochner density for every absolutely continuous bounded-variation vector measure over a finite scalar measure (Radon--Nikodym property).

[L4]

A Bochner-integrable function has integrable simple approximants (Bochner-integrable function) and its integral obeys the norm inequality (Bochner integral norm inequality).

[L5]

Continuity from below and measurable set-difference calculus hold for measures (Continuity from below for measures, Measure of a set difference when the smaller set has finite measure), and the Lebesgue sigma-algebra is the completion of the Borel one (L(Rn) is exactly the completion of the restriction of λn to the Borel sets).

Proof

technique · contradiction

Given: A nondentable nonempty bounded closed convex set CX and AC.

1.1

Convert nondentability into a uniformly separated convex bush. Choose η>0 such that no slice of C has diameter below η, and put r=η/4. For xC, if xconv(CB(x,r)), [L2] gives a slice lying inside B(x,r) and hence of diameter at most 2r<η, a contradiction. Thus every xC belongs to that closed convex hull. Enlarge to D=C+B(0,r/2). Given z=x+yD, approximate x by a finite convex combination iαixi=x+e of points outside B(x,r) with error e satisfying e+y<r/2, and put zi=xi+ye. Then z=iαizi, every ziD, and zizre>r/2. With δ=r/2, [A1] recursively chooses such finite successor families from an initial z0C. The resulting node set is countable, bounded, and every child is at least δ from its parent.

givenA1L1L2construct
2.1

Realize the bush as a separated interval martingale. Starting with M0z0, partition every atom at level n1 into finitely many half-open subintervals in the successor proportions (αi), put the corresponding child value on each, and overlay the dyadic grid of mesh 2n. Let Pn be the resulting refining finite interval partition. Parent averages equal parent values, so (Mn) is a martingale on these finite algebras; it is uniformly bounded and MnMn1δ away from the finitely many endpoints. The union algebra R=nσ(Pn) contains every dyadic interval algebra.

A1step 1.1construct
3.1

Define and extend the dominated vector measure. For Aσ(Pn) set ν0(A)=AMndλ. The martingale identity makes this independent of n, and if K=supnMn, then ν0(A)ν0(B)Kλ(AB). The class of Borel sets approximable in symmetric-difference measure by R is a sigma-algebra: complements preserve the distance, and countable unions reduce by [L5] to one large finite union. It contains the dyadic algebra and hence all Borel sets; the completion clause in [L5] adds Lebesgue sets. Choose such approximants. Completeness of X gives a unique extension ν with ν(E)Kλ(E); the same estimate proves norm countable additivity. Summing it over finite partitions gives ν(E)Kλ(E), so νλ and has bounded variation. Every algebra value is a finite linear combination of bush nodes, hence every extended value lies in the closed separable span Y of the countable node set.

A1L5step 2.1
4.1

Assume a density and identify all its finite-partition averages. Suppose fL1([0,1];X) satisfies ν(E)=Ef for all Lebesgue E. For every atom A of Pn, the construction gives Af=ν(A)=AMn=λ(A)MnA. Thus the atomwise averaging operator Qn applied to f equals Mn.

assume-contraL3L4step 3.1
5.1

Prove that the atomwise averages of a Bochner density converge in L1. Choose an integrable simple s with fs<ε by [L4]. By the approximation proved in step 3.1 and finiteness of its level family, approximate the level sets of s by sets in R, obtaining an R-simple t with ft<2ε. For all sufficiently large n, Qnt=t. The norm inequality on each atom shows that Qn is an L1 contraction, so Qnff1Qn(ft)1+tf1<4ε. Hence Mn=Qnff in L1.

L4step 2.1step 3.1step 4.1
6.1

Contradict the fixed separation and conclude. [discharge-contradiction: step 5.1, L3, step 2.1, step 4.1, step 5.1] Step 5.1 would imply MnMn110, whereas step 2.1 gives MnMn11δ for every n. Thus no density exists. The measure in step 3.1 is the witness required by [L3], with separable range. The exact uses of [A1] are strict separation through [L2], recursive bush and partition choices, and the countable approximation choices in extending ν0. The empty interval endpoints form null sets; the one-child case cannot occur because every child is δ-separated.

L3step 2.1step 3.1contradiction: step 5.1

Depends on

Used by

Dependency tree · two levels

42 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