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.
Agreement of Borel overlap integrals
Statement
For a density as in Pointwise Borel nonnegative densities, charts and , and every Borel ,
Facts & Assumptions
Given: Assume . Manifolds are Hausdorff, second countable and smooth, with boundary allowed; is allowed unless excluded. Densities are pointwise Borel, , and . Two supplied charts and Borel E; substitution only on their interiors.
Pointwise Borel nonnegative densities: The pointwise transition law has the absolute determinant and permits infinite coefficients.
Borel change of variables from the compact-support formula and Radon uniqueness: For a diffeomorphism of open Euclidean sets and nonnegative Borel , .
Smooth invariance of the manifold boundary: Transitions preserve boundary and interior.
The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra: Subspace Borel sets are traces of ambient Borel sets.
Assuming countable choice, every Borel subset of is Lebesgue measurable: Euclidean Borel sets are Lebesgue measurable under countable choice.
A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in : Coordinate faces are Lebesgue-null for positive dimension.
A nonnegative integral over a null set vanishes: A nonnegative measurable function has integral zero on a null set, even if infinite there.
Proof
For put and . These are open in . Boundary invariance makes a smooth diffeomorphism. The images of are Borel: charts are homeomorphisms and the trace sigma-algebra agrees with relative Borel sets.
On take , with the zero-times-infinity convention. It is nonnegative Borel. For , . Applying the Borel substitution formula to these exact domains and this integrand equates the two interior integrals.
The remaining coordinate pieces of lie in the face , or are empty for an interior chart. Their integrals vanish by nullity, without boundedness of or . Adding them back proves the formula for .
For each nonempty chart has one point. Thus is empty or the common singleton. Both integrals are respectively zero or the same weight, because the transition determinant is one. This proves the formula in every dimension, including zero or infinite weight.
Depends on
- Pointwise Borel nonnegative densities
- Borel change of variables from the compact-support formula and Radon uniqueness
- Assuming countable choice, every Borel subset of $\mathbb{R}^n$ is Lebesgue measurable
- The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra
- Smooth invariance of the manifold boundary
- A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in $\mathbb{R}^n$
- A nonnegative integral over a null set vanishes
Used by
Dependency tree · two levels
50 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
- Gerald B. Folland, Real Analysis, 2nd ed. (standard reference, not scraped)
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)