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.
Chart and partition independence of surface measure
Statement
Assume . Every regular chart density is continuous and strictly positive. The chart integral on a compact embedded hypersurface defines a finite Borel measure independent of the finite charts and subordinate partitions. In graph coordinates its density is . On a one-sided domain boundary the outward unit normal agrees on chart overlaps and is continuous.
Facts & Assumptions
Given: Assume . Use the proposed chart integral on a compact embedded hypersurface. In the normal assertion this is the one-sided boundary of the specified domain.
The proposed integral is a finite sum of weighted chart integrals. (Surface integration on compact C1 hypersurfaces).
The derivative of a coordinate composition is the product of its differentials. (The chain rule for total derivatives: ).
Determinants multiply. (For same-sized finite square matrices over a commutative ring, ).
A transpose has the same determinant. (For every square matrix over a commutative ring, ).
Regular tangent columns have positive Gram determinant. (A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent).
Nonnegative Borel substitution holds for a C1 diffeomorphism between open Euclidean sets. (Borel change of variables from the compact-support formula and Radon uniqueness).
Increasing nonnegative measurable functions have integrals increasing to the integral of their limit. (Monotone convergence for the integral).
Proof
On an overlap write , where T is the C1 coordinate transition. F2 gives , so F3–F5 yield . Both Gram determinants are positive because the tangent columns have full rank. F6 in dimension n-1, applied to any nonnegative Borel f supported in this overlap, now gives . Restriction to Borel subsets is obtained by multiplying f by their indicators. Continuity of DX and the polynomial determinant, followed by the positive square root, also proves continuity of each J. For a two-dimensional surface with Gram matrix , the same definition reads .
For two partitions chi_j and eta_k, insert into each chi_j integral in F1. This produces the finite sum of integrals of on overlaps. Step 1.1 transfers each term to the eta_k chart. Summing first in j gives , recovering exactly the second proposed integral. Every term is nonnegative, so this works also for infinite integrals. Applying the conclusion to positive and negative parts gives agreement for integrable signed f.
Each chart term defines a measure: for disjoint Borel sets the indicators of the finite partial unions increase to the indicator of the union, and monotone convergence of the weighted chart integrals gives countable additivity. For finiteness, the parameter preimage of the support of chi_j on S is compact inside V_j because X_j is a homeomorphism onto the chart image. J_X is continuous and bounded there and the compact set is bounded, so its weighted integral is finite. There are finitely many charts. Empty S gives the zero measure.
For a graph the tangent columns are , so with . Expanding its determinant by columns leaves the identity term one and the terms with exactly one replaced column, namely ; terms with two replaced columns vanish because those columns are proportional to v. Thus its determinant is , including v=0. The vector is orthogonal to every tangent column, and points out of the subgraph because its derivative on is . The two unit vectors normal to the common tangent space have opposite sides, so the exterior-side condition selects the same one in every chart. The displayed formula is continuous, proving normal continuity. In dimension three the cross product is orthogonal to both tangent vectors and has squared length equal to their Gram determinant. Its normalized value gives the outward normal exactly when it points to the exterior side; otherwise its negative does. Thus a parametrization alone does not fix the outward sign.
Source notes
Hunter, §1.10.2–1.10.3, printed pp. 15–16, Gram density and graph normal. Overlap independence is proved by the full determinant and Borel substitution calculation.
Depends on
- Surface integration on compact C1 hypersurfaces
- A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent
- For same-sized finite square matrices over a commutative ring, $\det(AB)=\det(A)\det(B)$
- For every square matrix over a commutative ring, $\det(A^{\mathsf T})=\det(A)$
- Borel change of variables from the compact-support formula and Radon uniqueness
- The chain rule for total derivatives: $D(g\circ f)(a)=Dg(f(a))\circ Df(a)$
- Monotone convergence for the integral
Used by
- Specified finite piecewise C1 boundary presentations Definition
- Graph density and outward orientation Example
- Agreement with the existing polar sphere measure Lemma
- Cutoffs around surface-null edges Lemma
- The local graph flux calculation Lemma
- Divergence on a bounded C1 Euclidean domain Theorem
Cited to discharge well-definedness by Bounded C1 domains and their outward normals and Surface integration on compact C1 hypersurfaces.
Dependency tree · two levels
49 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
- Hunter, Notes on Partial Differential Equations (standard reference, not scraped)