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.
Surface integration on compact C1 hypersurfaces
Definition
Assume the convention of Bounded C1 domains and their outward normals. Let S be a compact embedded hypersurface in , . Choose finitely many regular injective parametrizations with coordinate transitions, and an ambient partition from Finite ambient partitions near compact sets, with supports compactly contained in the corresponding chart neighborhoods. Put , using The Gram matrix and Gram determinant, with empty value .
For a nonnegative Borel f on S define , where the integrals on the right are those of The nonnegative Lebesgue integral and . Set for Borel A. For signed f with use the difference of the positive and negative integrals. The same chart formula restricts to a compact Borel face contained in a regular patch. The empty surface has zero integral. Independence and finiteness are established by the following chart-independence lemma.
Source notes
Hunter, §1.10.2, printed p. 15 (PDF p. 21), Gram surface density and partition patching.
Depends on
Used by
- Stein-Tomas for compact hypersurfaces with nonzero curvature Corollary
- Uniqueness of classical Dirichlet and compatible Neumann solutions Corollary
- Zero-Dirichlet Green representation for Poisson data Corollary
- Arbitrary L² boundary data need not have an H¹ lifting Counterexample
- Critical traces fail compactness under boundary dilation Counterexample
- Neumann Poisson data require a flux compatibility equation Counterexample
- The trace estimate fails on an outward cusp above the critical sharpness Counterexample
- Fourier restriction and adjoint extension operators Definition
- Mean-zero NtD map and smoothed kernel observation Definition
- The fractional Sobolev space on a compact C¹ boundary Definition
- The Hardy boundary space, Szegő projection and Szegő kernel on a smoothly bounded domain Definition
- Flux normalization on every centered sphere Example
- Newton shell theorem from harmonic mean values Example
- Newtonian potential of radial compact data Example
- Quantitative concentration of the ball Poisson kernel Example
- The polydisc boundary is not a smooth hypersurface, so the Szegő definition does not apply Example
- The trace of an affine function on a ball is its classical restriction Example
- The two-dimensional logarithmic kernel has unit normalized flux Example
- Cap and complement estimate for the ball Poisson integral Lemma
- Chart and partition independence of surface measure Lemma
- Heat-ball representation formula Lemma
- Mean-zero weak Neumann problem for uniformly elliptic conductivities Lemma
- Polynomial traces, monomial basis and bounded evaluation for the ball Hardy space Lemma
- Scaling the perimeter of a disk inclusion Lemma
- Smoothness, parity and zero-radius limits of spherical means Lemma
- Sphere graph charts, surface density, and a finite partition Lemma
- Sphere integrals of a cylindrical function project to weighted ball integrals Lemma
- Stokes for complex forms on a bounded C1 Euclidean domain Lemma
- The boundary fundamental lemma of the calculus of variations Lemma
- The mean-value L² bound for holomorphic functions on a polydisc Lemma
- The trace agrees with classical restriction for continuous Sobolev functions Lemma
- The trace commutes with smooth cutoffs and is chart local Lemma
- Weighted monomial integrals and monomial norms for the disc, ball and polydisc Lemma
- The Green identities used here are Euclidean Remark
- Continuous Dirichlet problem on a ball Theorem
- Green and harmonic-measure representation with the 2π sign Theorem
- Green representation for classical Poisson data Theorem
- Harmonic functions are real analytic Theorem
- Hölder data give a classical Newtonian solution Theorem
- Interior derivative estimates for harmonic functions Theorem
…and 6 more results.
Dependency tree · two levels
16 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)