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 is Bochner integrable and , then is a norm-countably additive vector measure, , and
for every measurable .
Facts & Assumptions
Vector measures, variation, and absolute continuity have the stated norm and partition meanings (Banach-valued vector measure and variation).
Bochner integrals satisfy the norm inequality (Bochner integral norm inequality).
For an integrable scalar function, its indefinite integral is countably additive (The indefinite integral of an integrable function is countably additive on measurable sets).
A Bochner-integrable function has integrable scalar norm and one defining simple approximation (Bochner integrability criterion, Bochner-integrable function). If is integrable simple, then (Banach-valued simple function and integral), and this integral is representation-independent and linear (The Banach-valued simple integral is well defined).
Bounded variation makes variation a finite measure (Bounded variation of a vector measure is a finite measure).
Proof
Given: A Bochner-integrable and the set function in the Statement.
Establish scalar control and absolute continuity. By [L4], is integrable. Put . By [L3], is a finite positive measure. By [L2], , so . For every finite partition of , summing the same inequality gives ; hence by [L1].
Fix a simple approximation for the reverse variation bound. Choose integrable simple with as supplied by [L4]. For fixed , partition into the nonzero level sets of and the remaining zero cell.
Prove norm countable additivity without a new choice. For disjoint with union , finite additivity follows from simple approximation and [L4]. Moreover by countable additivity of the finite measure . Thus is norm-countably additive.
Prove the reverse variation inequality. On the partition from step 1.2, [L2] and [L4] give . The pointwise inequality then yields . Letting proves .
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 ; step 2.1 gives the required vector measure. In particular variation is finite (consistently with [L5]). For , , or a one-level simple density, the equality reduces respectively to , , or .
Depends on
- Banach-valued vector measure and variation
- Bounded variation of a vector measure is a finite measure
- Bochner integral norm inequality
- Bochner-integrable function
- Bochner integrability criterion
- Banach-valued simple function and integral
- The Banach-valued simple integral is well defined
- The indefinite integral of an integrable function is countably additive on measurable sets
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
- Gilles Pisier, Martingales in Banach Spaces (standard reference, not scraped)