Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

A Bochner density defines an absolutely continuous vector measure

Statement

If f:ΩX is Bochner integrable and νf(E):=Efdμ, then νf is a norm-countably additive vector measure, νfμ, and

νf(E)=Efdμ

for every measurable E.

Facts & Assumptions

[L1]

Vector measures, variation, and absolute continuity have the stated norm and partition meanings (Banach-valued vector measure and variation).

[L2]

Bochner integrals satisfy the norm inequality (Bochner integral norm inequality).

[L3]

For an integrable scalar function, its indefinite integral is countably additive (The indefinite integral of an integrable function is countably additive on measurable sets).

[L4]

A Bochner-integrable function has integrable scalar norm and one defining L1 simple approximation (Bochner integrability criterion, Bochner-integrable function). If s=jxj1Aj is integrable simple, then Es=jμ(EAj)xj (Banach-valued simple function and integral), and this integral is representation-independent and linear (The Banach-valued simple integral is well defined).

[L5]

Bounded variation makes variation a finite measure (Bounded variation of a vector measure is a finite measure).

Proof

technique · direct

Given: A Bochner-integrable f and the set function νf in the Statement.

1.1

Establish scalar control and absolute continuity. By [L4], f is integrable. Put ρ(E)=Ef. By [L3], ρ is a finite positive measure. By [L2], νf(E)ρ(E), so νfμ. For every finite partition (Ej) of E, summing the same inequality gives jνf(Ej)ρ(E); hence νf(E)ρ(E) by [L1].

givenL1L2L3L4
1.2

Fix a simple approximation for the reverse variation bound. Choose integrable simple sn with fsn0 as supplied by [L4]. For fixed E, partition E into the nonzero level sets of sn and the remaining zero cell.

L4choose
2.1

Prove norm countable additivity without a new choice. For disjoint (Ek) with union E, finite additivity follows from simple approximation and [L4]. Moreover νf(E)k=1Nνf(Ek)=νf(Ek=1NEk)ρ(Ek=1NEk)0 by countable additivity of the finite measure ρ. Thus νf is norm-countably additive.

L2L3step 1.1
2.2

Prove the reverse variation inequality. On the partition from step 1.2, [L2] and [L4] give νf(E)EsnEfsn. The pointwise inequality snffsn then yields νf(E)ρ(E)2Efsn. Letting n proves νf(E)ρ(E).

L2L4step 1.1step 1.2
3.1

Combine the bounds and close all cases. [L1, L5, step 1.1, step 2.1, step 2.2] Steps 1.1 and 2.2 give νf=ρ; step 2.1 gives the required vector measure. In particular variation is finite (consistently with [L5]). For E=, f=0, or a one-level simple density, the equality reduces respectively to 0=0, 0=0, or μ(EA)x=μ(EA)x.

L1L5step 1.1step 2.1step 2.2

Depends on

Used by

Dependency tree · two levels

22 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