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.
The single-direction flux identity on a simple solid region
Statement
Let be a simple description of a solid in the direction and let be a boundary presentation adapted to it (Boundary presentations adapted to a simple solid region in a coordinate direction). Let be a real function of class on an open set containing and let be the field whose th coordinate is and whose other two coordinates are zero. Then the flux of over the presentation equals the integral of the th partial derivative of over :
Facts & Assumptions
Given: The simple description of , the adapted presentation with its supplied sublists , and the function of class on an open . Write , , for the point with -projection and th coordinate , and for .
For a compatible finite patch presentation, the oriented flux is the sum of the patch values, each patch value being (Finitely patched regular surfaces, their area, scalar integrals, and flux, Unit normal fields, orientations, and flux through a regular surface patch).
For the th coordinate of vanishes on the interior of ; the projected images of the upper sublist are pairwise disjoint and fill up to content zero, and the same holds for the lower sublist (Boundary presentations adapted to a simple solid region in a coordinate direction).
A regular patch has a compact Jordan parameter region that is the closure of its nonempty interior, and its parametrization is on an open neighbourhood of that region (Regular parametrized surface patches on compact Jordan parameter regions).
The simple solid region described by is with compact Jordan and continuous on , and carries onto the solid between the graphs of and over (Simple solid regions in a coordinate direction and their cyclic coordinate projection).
For , (The Euclidean inner product on ); a function has continuous first partial derivatives ( Euclidean maps and diffeomorphisms); and is the th partial derivative appearing in the divergence of Divergence and curl of a vector field.
Integration over a bounded Jordan measurable set is integration of the zero extension over a bounding rectangle (The Riemann integral of a bounded function over a bounded Jordan measurable set).
For the flux of through is , and for it is ; each is a bounded open Jordan measurable subset of and the base integrand is integrable over it (The flux of a single-component field through a graph face is a base integral of its trace).
Let be bounded Jordan measurable, let and let be bounded Jordan sets with pairwise intersections of content zero and with of content zero; if is bounded on and integrable over and over each , then (Additivity of the integral over finitely many Jordan pieces that fill a Jordan set up to content zero).
For compact Jordan , continuous on and , the solid is compact and Jordan measurable and every continuous satisfies (A solid between continuous graphs over a compact Jordan base is Jordan measurable and integrates by vertical sections).
For a cyclic coordinate permutation of and compact Jordan , the set is compact Jordan and for bounded integrable on either side (A cyclic permutation of the coordinates of preserves Jordan measurability and integrals).
If is differentiable at every point of with and is integrable on , then (The second fundamental theorem: if is differentiable on with and is integrable, then ).
Every continuous real function on a compact Jordan measurable set is Riemann integrable over it (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).
For a map of two variables into , (Each coordinate of the oriented area vector is the Jacobian determinant of the matching cyclic projection).
Proof
Let . By [F5] the flux integrand of through is , which is continuous on because is there by [F3] and is continuous. By [F2] its second factor vanishes on , and is the closure of by [F3], so a continuous function vanishing on vanishes on . Hence that patch's flux is .
By [F4] the set is compact and Jordan measurable and . The function is continuous on , since is continuous on by [F5] and is linear, and on . So [L4] applied with gives , both integrals existing by [L3] and [L6].
Fix and put , defined and differentiable for every with , with because varying moves only the th coordinate. If then is differentiable on , whose points lie in by [F4], and is continuous there hence integrable, so [L5] gives . If instead then the interval is degenerate, so the integral is , and the increment is also ; the identity holds in that case too.
The functions and are continuous on the compact Jordan base , hence bounded and integrable over by [L6] and [F6]. By [L1] each with is a bounded Jordan subset of over which is integrable, and by [F2] those sets are pairwise disjoint — so their pairwise intersections are empty and have content zero — and their union omits from only a set of content zero. So [L2] gives , and by [L1] the left side is the sum of the upper faces' fluxes.
The same argument applied to the lower sublist gives , and by [L1] each lower face's flux is , so the lower faces' fluxes sum to .
By step 1.3 the inner integral in [L3] is for every , a continuous function of ; so [L3] applied to on and step 1.2 give , the last step by linearity of the integral over .
By [F1] the flux over the presentation is the sum of the patch fluxes, which splits along the three supplied sublists. Step 1.1 makes the lateral sum zero, step 1.4 makes the upper sum and step 1.5 makes the lower sum , so the total is .
Steps 2.1 and 2.2 give the same number for the two sides of the asserted identity, so it holds.
Remarks
-
The degenerate slice needs its own line. Where the two graph functions agree, the second fundamental theorem is unavailable, since it requires a nondegenerate interval; step 1.3 handles that case separately, and both sides are zero there. Folding it into the main computation would apply [L5] with .
-
Nothing here says the normals point outward. The identity is proved from the sign conditions of the adapted presentation alone. Reading its right-hand side as an outward flux is At interior base points, the graph faces of an adapted presentation induce the outward unit normal and Every patch of an elementary solid region's presentation is a graph face in some direction, and at interior base points its normal is outward, and no step above depends on them.
Depends on
- Boundary presentations adapted to a simple solid region in a coordinate direction
- The flux of a single-component field through a graph face is a base integral of its trace
- Additivity of the integral over finitely many Jordan pieces that fill a Jordan set up to content zero
- A solid between continuous graphs over a compact Jordan base is Jordan measurable and integrates by vertical sections
- A cyclic permutation of the coordinates of $\mathbb R^3$ preserves Jordan measurability and integrals
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- Finitely patched regular surfaces, their area, scalar integrals, and flux
- Regular parametrized surface patches on compact Jordan parameter regions
- A continuous real function on a compact Jordan measurable set is Riemann integrable over that set
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Simple solid regions in a coordinate direction and their cyclic coordinate projection
- Unit normal fields, orientations, and flux through a regular surface patch
- The Riemann integral of a bounded function over a bounded Jordan measurable set
- Divergence and curl of a $C^1$ vector field
- $C^k$ Euclidean maps and diffeomorphisms
- Each coordinate of the oriented area vector is the Jacobian determinant of the matching cyclic projection
Used by
Dependency tree · two levels
77 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
- G. Strang and E. Herman, Calculus Volume 3 (OpenStax), section 6.8 (standard reference, not scraped)
- J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus (University of British Columbia), Theorem 4.2.2 (standard reference, not scraped)