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.
Weighted interval volume
Example
On take . For , This density has finite mass on compact subsets of but infinite total mass.
Facts & Assumptions
Given: Assume . Manifolds are Hausdorff, second countable and smooth, with boundary allowed; is allowed unless excluded. Densities are pointwise Borel, , and . Weighted interval; logarithmic finite pieces and explicit divergent exhaustion.
Intrinsic density measure and its chart restriction: Measure in the identity chart is the coefficient integral.
Positive smooth densities give Radon volume: A positive finite smooth density has compact-finite measure.
Borel Darboux integrands in finite dimension: Bounded Borel Riemann integrands on boxes have equal Lebesgue integrals.
Monotone convergence for the integral: Increasing nonnegative integrands satisfy monotone convergence.
A nonnegative integral over a null set vanishes: A nonnegative measurable integrand integrates to zero over a measurable null set.
A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in : A singleton is Lebesgue-null in dimension one.
Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: For positive , ; log is increasing and onto the reals.
Verification
The function is positive, finite and smooth on . On it is continuous and bounded; the logarithmic integral identity gives its Riemann integral . The Borel Darboux bridge equates the Lebesgue integral to this value. Removing the two null endpoints does not change it, so the chart formula gives . For example gives .
Every compact subset of has finite measure by the positive smooth density theorem. More explicitly, it lies in and is bounded in measure by . The increasing sets , , exhaust and have mass . Monotone convergence applied to their indicators gives . This divergence also follows without any limit identity for log: each interval contributes at least to , so these logarithms are unbounded.
Empty intervals and singletons have zero mass by the null-set formula. There is no endpoint value of the density at zero or one because neither belongs to the manifold; its blowup at the omitted zero endpoint is consistent with local finiteness.
Depends on
- Measurable integration extends smooth density integration
- Positive smooth densities give Radon volume
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- Monotone convergence for the integral
- Borel Darboux integrands in finite dimension
- Intrinsic density measure and its chart restriction
- A nonnegative integral over a null set vanishes
- A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in $\mathbb{R}^n$
- Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm
Used by
Dependency tree · two levels
58 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
- Folland, Real Analysis, second edition, §11.4 pp.361–363; Theorems 2.14–2.15 pp.50–51 (standard reference, not scraped)