FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 26 definitions, 7 theorems, 19 propositions, 2 lemmas, 4 corollaries, 5 examples, 1 construction and 2 conventions.

Of the 66 statements checked against Lean, 1 are formalized somewhere and 65 are not.

Status	Statements	Share	What it means
not formalized	65	98%	A documented search found no Lean statement of it anywhere.
in Mathlib	1	2%	Mathlib states and proves it.
checked in total	66

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 16, FC08-C16-U001–FC08-C16-U066, exactly 66 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Search order: project at A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean 4.33.0), current upstream H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0, Lean 4.34.0-rc2), then targeted indexed/GitHub/external Lean searches. No project-existing, package-import, or reference-port owner survived strict whole-row checking.
C16 has 1 pinned mathlib row and 65 dated unmatched rows. The sole positive row is U023.
U023 is exact: EuclideanQuadrant n is the nonnegative coordinate orthant, range_euclideanQuadrant identifies its image with ∀ i, 0 ≤ y i, and modelWithCornersEuclideanQuadrant supplies the standard corners model.
P/H do contain strong adjacent analytic infrastructure: Lebesgue/Bochner integration, the Jacobian change-of-variables theorem (MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul), Henstock–Kurzweil box integration and a box divergence theorem, Haar measures, and general ModelWithCorners. None supplies Lee’s smooth oriented-manifold differential-form integral, its Stokes theorem, or the smooth density-bundle interface, so these ingredients are not promoted across a missing bridge.
C14 already established the central differential-form boundary: Mathlib has vector-space AlternatingMap forms and a continuous alternating-map bundle, but no smooth manifold DifferentialForm section/exterior-derivative layer. C15 additionally established the absence of a global smooth-manifold orientation API. C16 U001–U022 and U035–U046 depend essentially on those missing layers.
Mathlib’s manifold framework can use Euclidean quadrants as models with corners, but targeted searches found no corner-depth/stratification API matching Lee’s “more than one vanishing coordinate” corner points, no chart-invariance theorem for that notion, and no integration/Stokes theorem over corner faces. Hence U024–U034 remain unmatched despite U023.
Exact P/H searches for Density find only unrelated combinatorial/measure-theoretic uses; there is no linear determinant-density object, density bundle, or Riemannian density in Lee’s sense. Measure.withDensity is a Radon–Nikodym-style measure construction, not the source object. Thus U047–U066 are not identified with measure densities by terminology alone.
Targeted current external search found no compatible Mathlib-based implementation of the missing manifold integration/density layer. A current pure-Lean mathematical-physics project advertises differential forms/de Rham theory but deliberately has no Mathlib dependency and axiomatizes substantial analytic scaffolding; it does not satisfy the evidence/compatibility floor for package-import or reference-port here.
N=2026-09-07 marks dated unmatched decisions. Strict whole-row semantics apply uniformly.

Definition/convention — integral of

FC08-C16-U001 · Ch. 16, § Integration of Differential Forms; source L12064 · not formalized

Recall that a domain of integration in $\mathbb { R } ^ { n }$ is a bounded subset whose boundary has measure zero. Let $D \subseteq \mathbb { R } ^ { n }$ be a domain of integration, and let $\omega$ be a (continuous) n-form on $\bar { D }$ . Any such form can be written as $\omega = f d x ^ { 1 } \wedge \cdots \wedge d x ^ { n }$ for some continuous function $f \colon \bar { D } \mathbb { R }$ . We define the integral of ! over $\pmb { D }$ to be \[ \int_ {D} \omega = \int_ {D} f d V. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Lebesgue/Bochner/Henstock–Kurzweil integration and Jacobian change-of-variables theorems, but P/H has no integration theory for smooth manifold differential forms or Lee’s oriented-manifold integral. The available Euclidean measure-theory theorems do not own Lee’s n-form definitions, orientation signs, partition-of-unity independence, or parametrized sphere computation. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing converse directions, and substantive reconstruction from generic ingredients.

Definition/convention — source terminology/construction

FC08-C16-U002 · Ch. 16, § Integration of Differential Forms; source L12078 · not formalized

Somewhat more generally, let U be an open subset of ℝ ^n or ℍ ^n , and suppose ! is a compactly supported n-form on U . We define \[ \int_{U} \omega = \int_{D} \omega, \] where $D \subseteq \mathbb{R}^{n}$ or $\mathbb{H}^{n}$ is any domain of integration containing $\operatorname{supp}\omega$.

Proposition 16.1

FC08-C16-U003 · Ch. 16, § Integration of Differential Forms; source L12088 · not formalized

Proposition 16.1. Suppose D and E are open domains of integration in $\mathbb { R } ^ { n }$ or $\mathbb { H } ^ { n }$ and $G \colon { \bar { D } } { \bar { E } }$ is a smooth map that restricts to an orientation-preserving $o r$ orientation-reversing diffeomorphism from D to E. If ! is an n-form on $\overline { E }$ , then \[ \int_ {D} G ^ {*} \omega = \left\{ \begin{array}{l l} \int_ {E} \omega & \text {if G is orientation - preserving,} \\ - \int_ {E} \omega & \text {if G is orientation - reversing.} \end{array} \right. \] Proof.

Lemma 16.2

FC08-C16-U004 · Ch. 16, § Integration of Differential Forms; source L12104 · not formalized

Lemma 16.2. Suppose U is an open subset of $\mathbb { R } ^ { n } ~ o r ~ \mathbb { H } ^ { n }$ , and K is a compact subset of U . Then there is an open domain of integration D suc basis for $T _ { p } M$ .

Proposition 16.3

FC08-C16-U005 · Ch. 16, § Integration of Differential Forms; source L12111 · not formalized

Proposition 16.3. Suppose U , V are open subsets of $\mathbb { R } ^ { n }$ or H, and $G \colon U \to$ V is an orientation-preserving or orientation-reversing diffeomorphism. If ! is a compactly supported n-form on V , then \[ \int_ {V} \omega = \pm \int_ {U} G ^ {*} \omega , \] with the positive sign if G is orientation-preserving, and the negative sign orientation form for S if we can show that it never vanishes.

Definition/convention — integral of

FC08-C16-U006 · Ch. 16, § Integration on Manifolds; source L12123 · not formalized

Manifolds Using the results of the previous section, we can now make sense of the integral of a differential form over an oriented manifold. Let M be an oriented smooth nmanifold with or without boundary, and let ! be an n-form on M . Suppose first that ! is compactly supported in the domain of a single smooth chart $( U , \varphi )$ that is either positively or negatively oriented. We define the integral of ! over M to be \[ \int_ {M} \omega = \pm \int_ {\varphi (U)} \left(\varphi^ {- 1}\right) ^ {*} \omega ,\tag{16.1} \] with the positive sign for a positively oriented chart, and the negative sign otherwise. (See Fig. 16.6.) Since $( \varphi ^ { - 1 } ) ^ { * } \omega$ is a compactly supported n-form on the open subset $\varphi ( U ) \subseteq \mathbb { R } ^ { n }$ or H, its integral is defined as discussed earlier.

Proposition 16.4

FC08-C16-U007 · Ch. 16, § Integration on Manifolds; source L12131 · not formalized

Proposition 16.4. With ! as above, $\textstyle \int _ { M }$ ! does not depend on the choice of smooth chart whose domain contains supp !.

Proposition 16.5

FC08-C16-U008 · Ch. 16, § Integration on Manifolds; source L12152 · not formalized

The definition of textstyle int _M ! given above does not depend on the choice of open cover or partition of unity.

Definition/convention — oriented 0-manifold M

FC08-C16-U009 · Ch. 16, § Integration on Manifolds; source L12179 · not formalized

As usual, we have a special definition in the zero-dimensional case. The integral of a compactly supported 0-form (i.e., a real-valued function) f over an oriented 0-manifold M is defined to be the sum \[ \int_{M} f = \sum_{p \in M} \pm f(p), \] with the positive sign at the positively oriented points and the negative sign at the negatively oriented ones.

Proposition 16.6

FC08-C16-U010 · Ch. 16, § Integration on Manifolds; source L12194 · not formalized

Proposition 16.6 (Properties of Integrals of Forms). Suppose M and N are nonempty oriented smooth n-manifolds with or without boundary, and !; are compactly supported n-forms on M . (a) LINEARITY: If a; $b \in \mathbb { R }$ , then \[ \int_ {M} a \omega + b \eta = a \int_ {M} \omega + b \int_ {M} \eta . \] (b) ORIENTATION REVERSAL: $I f - M$ denotes M with the opposite orientation, then \[ \int_ {- M} \omega = - \int_ {M} \omega . \] (c) POSITIVITY: If ! is a positively oriented orientation form, then $\textstyle \int _ { M } \omega > 0$ (d) DIFFEOMORPHISM INVARIANCE: If $F \colon N \to M$ is an orientation-preserving or orientation-reversing diffeomorphism, then \[ \int_ {M} \omega = \left\{ \begin{array}{l l} \int_ {N} F ^ {*} \omega & \text {if F is orientation - preserving,} \\ - \int_ {N} F ^ {*} \omega & \text {if F is orientation - reversing.} \end{array} \right. \] Proof.

Proposition 16.8

FC08-C16-U011 · Ch. 16, § Integration on Manifolds; source L12226 · not formalized

Proposition 16.8 (Integration Over Parametrizations). Let M be an oriented smooth n-manifold with or without boundary, and let ! be a compactly supported $\scriptstyle { n - f o r m }$ on M . Suppose $D _ { 1 } , \ldots , D _ { k }$ are open domains of integration in $\mathbb { R } ^ { n }$ , and for $i = 1 , \ldots , k$ , we are given smooth maps $F _ { i } \colon { \bar { D } } _ { i } \to M$ satisfying (i) $F _ { i }$ restricts to an orientation-preserving diffeomorphism from $D _ { i }$ onto an open subset $W _ { i } \subseteq M$ ; (ii) $W _ { i } \cap W _ { j } = \emptyset$ when $i \neq j$ (iii) supp $\omega \subseteq { \overline { { W } } } _ { 1 } \cup \cdots \cup { \overline { { W } } } _ { k }$ Then \[ \int_ {M} \omega = \sum_ {i = 1} ^ {k} \int_ {D _ {i}} F _ {i} ^ {*} \omega .\tag{16.3} \] Proof. As in the preceding proof, it suffices to assume that $\omega$ is supported in the domain of a single oriented , called the Riemannian volume form, that satisfies \[ \omega_ {g} (E _ {1}, \ldots , E _ {n}) = 1\tag{15.2} \] for every local oriented orthonormal frame $( E _ { i } )$ for M .

Example 16.9

FC08-C16-U012 · Ch. 16, § Integration on Manifolds; source L12267 · after FC08-C15-U036, FC08-C16-U011 · not formalized

Example 16.9. Let us use this technique to compute the integral of a 2-form over $\mathbb { S } ^ { 2 }$ , oriented as the boundary of ${ \overline { { \mathbb { B } } } } ^ { 3 }$ . Let $\omega$ be the following 2-form on $\mathbb { R } ^ { 3 }$ : \[ \omega = x d y \wedge d z + y d z \wedge d x + z d x \wedge d y. \] Let D be the open rectangle $( 0 , \pi ) \times ( 0 , 2 \pi )$ , and let $F \colon \bar { D } \mathbb { S } ^ { 2 }$ be the spherical coordinate parametrization $F ( \varphi , \theta ) = ( \sin \varphi \cos \theta$ ; sin $\varphi$ sin $\theta .$ ; cos ’/. Example 15.28 showed that $F | _ { D }$ is orientation-preserving, so it satisfies the hypotheses of Proposition 16.8. Note that \[ F ^ {*} d x = \cos \varphi \cos \theta d \varphi - \sin \varphi \sin \theta d \theta , \] \[ F ^ {*} d y = \cos \varphi \sin \theta d \varphi + \sin \varphi \cos \theta d \theta , \] \[ F ^ {*} d z = - \sin \varphi d \varphi . \] Therefore, \[ \begin{array}{l} \int_ {\mathbb {S} ^ {2}} \omega = \int_ {D} \left(- \sin^ {3} \varphi \cos^ {2} \theta d \theta \wedge d \varphi + \sin^ {3} \varphi \sin^ {2} \theta d \varphi \wedge d \theta \right. \\ \qquad \left. + \cos^ {2} \varphi \sin \varphi \cos^ {2} \theta d \varphi \wedge d \theta - \cos^ {2} \varphi \sin \varphi \sin^ {2} \theta d \theta \wedge d \varphi\right) \\ = \int_ {D} \sin \varphi d \varphi \wedge d \theta = \int_ {0} ^ {2 \pi} \int_ {0} ^ {\pi} \sin \varphi d \varphi d \theta = 4 \pi . \end{array}\tag{//} \] It is worth remarking that the hypotheses of Proposition 16.8 can be relaxed somewhat. The requirement that each map $F _ { i }$ be smooth on $\textstyle { \overline { { D } } } _ { i }$ is included to ensure that the boundaries of the image sets $W _ { i }$ have measure zero and that the pullback forms $F _ { i } ^ { * } \omega$ are continuous on $\textstyle { \overline { { D } } } _ { i }$ . Provided the open subsets $W _ { i }$ together fill up all of M except for a set of measure zero, we can allow maps $F _ { i }$ that do not extend smoothly to the boundary, by interpreting the resulting integrals of unbounded forms either as improper Riemann integrals or as Lebesgue integrals. For example, if the closed upper hemisphere of $\mathbb { S } ^ { 2 }$ is parametrized by the map $\mathbf { \bar { \boldsymbol { F } } } \colon \mathbf { \overline { { \mathbb { B } } } } ^ { 2 } \to \mathbb { S } ^ { 2 }$ given by $F ( u , v ) = \left( u , v , \sqrt { 1 - u ^ { 2 } - v ^ { 2 } } \right)$ , then $F$ is continuous but not smooth up to the boundary, but the conclusion of the proposition still holds. We leave it to the interested reader to work out reasonable conditions under which such a generalization of Proposition 16.8 holds.

Definition/convention — left-invariant

FC08-C16-U013 · Ch. 16, § Integration on Lie Groups; source L12297 · not formalized

Let $G$ be a Lie group. A covariant tensor field $A$ on $G$ is left-invariant if $L_{g}^{*}A = A$ for all $g \in G$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Lie groups and Haar measures, but no left-invariant manifold covariant-tensor/orientation-form layer realizing Lee’s Haar volume form and normalized integral. Measure-theoretic Haar measure is an adjacent representation, not a checked bridge to this differential-form construction. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing converse directions, and substantive reconstruction from generic ingredients.

Proposition 16.10

FC08-C16-U014 · Ch. 16, § Integration on Lie Groups; source L12299 · not formalized

Proposition 16.10. Let G be a compact Lie group endowed with a left-invariant orientation. Then G has a unique positively oriented left-invariant n-form ! with the property that $\textstyle \int _ { G } \omega _ { G } = 1$

Definition/convention — Haar volume form

FC08-C16-U015 · Ch. 16, § Integration on Lie Groups; source L12328 · not formalized

orientation form with integral 1. Remark. The orientation form whose existence is asserted in this proposition is called the Haar volume form on G . Similarly, the map $f \mapsto \textstyle \int _ { G } f$ ! is called the Haar integral. Observe that the proof above did not use the fact that G was compact until the last paragraph; thus every Lie group has a left-invariant orientation form that is uniquely defined up to a constant multiple. It is only in the compact case, however, that we can use the volume normalization to single out a unique us, exactly one of the two choices of unit normal has negative $x ^ { n }$ -component, which is equivalent to being outward-pointing.

Theorem 16.11

FC08-C16-U016 · Ch. 16, § Stokes’s Theorem; source L12336 · not formalized

Theorem 16.11 (Stokes’s Theorem). Let M be an oriented smooth n-manifold with boundary, and let ! be a compactly supported smooth .n 1/-form on M . Then \[ \int_ {M} d \omega = \int_ {\partial M} \omega .\tag{16.4} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H has no manifold differential-form exterior derivative plus manifold integration package from which Lee’s Stokes theorem and these exact corollaries/Green theorem can be stated. Box-integral and measure-theoretic divergence theorems are special-purpose adjacent results, not the source theorem. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing converse directions, and substantive reconstruction from generic ingredients.

Example 16.12

FC08-C16-U017 · Ch. 16, § Stokes’s Theorem; source L12416 · after FC08-C11-U053 · not formalized

Example 16.12. Let M be a smooth manifold and suppose $\gamma \colon [ a , b ] \to M$ is a smooth embedding, so that $S = \gamma ( [ a , b ] )$ is an embedded 1-submanifold with boundary in M . If we give S the orientation such that $\gamma$ is orientation-preserving, then for any smooth function $f \in C ^ { \infty } ( M )$ , Stokes’s theorem says that \[ \int_ {\gamma} d f = \int_ {[ a, b ]} \gamma^ {*} d f = \int_ {S} d f = \int_ {\partial S} f = f (\gamma (b)) - f (\gamma (a)). \] Thus Stokes’s theorem reduces to the fundamental theorem for line integrals (Theorem 11.39) in this case. In particular, when $\gamma \colon [ a , b ] \mathbb { R }$ is the inclusion map, then Stokes’s theorem is just the ordinary fundamental theorem s that $\left( \pi | _ { W } \right) ^ { - 1 } ( U ) = \emptyset$ , which implies that $U \subseteq M \setminus \pi ( W )$ .

Corollary 16.13

FC08-C16-U018 · Ch. 16, § Stokes’s Theorem; source L12426 · not formalized

Corollary 16.13 (Integrals of Exact Forms). If M is a compact oriented smooth manifold without boundary, then the integral of every exact form over M is zero: \[ \int_ {M} d \omega = 0 \quad i f \partial M = \varnothing . \]

Corollary 16.14

FC08-C16-U019 · Ch. 16, § Stokes’s Theorem; source L12432 · not formalized

Corollary 16.14 (Integrals of Closed Forms over Boundaries). Suppose M is a compact oriented smooth manifold with boundary. If ! is a closed form on M; then the integral of ! over @M is zero: \[ \int_ {\partial M} \omega = 0 \quad i f d \omega = 0 o n M. \] These results have the following extremely useful applications to submanifolds.

Corollary 16.15

FC08-C16-U020 · Ch. 16, § Stokes’s Theorem; source L12440 · not formalized

Corollary 16.15. Suppose M is a smooth manifold with or without boundary, $S \subseteq M$ is an oriented compact smooth k-dimensional submanifold (without boundary), and ! is a closed k-form on M . If $\begin{array} { r } { \int _ { S } \omega \neq 0 . } \end{array}$ , then both of the following are true: (a) ! is not exact on $M$ (b) S is not the boundary of an oriented compact smooth submanifold with boundary in M .

Example 16.16

FC08-C16-U021 · Ch. 16, § Stokes’s Theorem; source L12446 · after FC08-C11-U049 · not formalized

By the computation of Example 11.36, the closed 1-form $\omega = (x\,dy - y\,dx)/(x^{2}+y^{2})$ has nonzero integral over $\mathbb{S}^{1}$, and is not exact on $\mathbb{R}^{2} \setminus \{0\}$. The preceding corollary adds that $\mathbb{S}^{1}$ is not the boundary of a compact regular domain in $\mathbb{R}^{2} \setminus \{0\}$.

Theorem 16.17

FC08-C16-U022 · Ch. 16, § Stokes’s Theorem; source L12450 · not formalized

Theorem 16.17 (Green’s Theorem). Suppose D is a compact regular domain in $\mathbb { R } ^ { 2 }$ , and $P , Q$ are smooth real-valued functions on D. Then \[ \int_ {D} \left(\frac {\partial Q}{\partial x} - \frac {\partial P}{\partial y}\right) d x d y = \int_ {\partial D} P d x + Q d y. \]

Definition/convention — source terminology/construction

FC08-C16-U023 · Ch. 16, § Manifolds with Corners; source L12462 · in Mathlib

Let $\overline { { \mathbb { R } } } _ { + } ^ { n }$ denote the subset of $\mathbb { R } ^ { n }$ where all of the coordinates are nonnegative: \[ \bar {\mathbb {R}} _ {+} ^ {n} = \left\{\left(x ^ {1}, \dots , x ^ {n}\right) \in \mathbb {R} ^ {n}: x ^ {1} \geq 0, \dots , x ^ {n} \geq 0 \right\}. \] This space is the model assume that the given orientation ${ \mathcal { O } } _ { p }$ is same as the orientation of $T _ { p } M$ determined by $\mathcal { O }$ .

Formalized. Mathlib/Geometry/Manifold/Instances/Real.lean::EuclideanQuadrant, range_euclideanQuadrant, modelWithCornersEuclideanQuadrant — EuclideanQuadrant n is exactly the subtype of Euclidean vectors whose coordinates are all nonnegative. range_euclideanQuadrant identifies its underlying subset with {y | ∀ i, 0 ≤ y i}, and modelWithCornersEuclideanQuadrant is the corresponding orthant model used for manifolds with corners. This is Lee’s \overline{ℝ}_+^n convention.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Definition/convention — chart

FC08-C16-U024 · Ch. 16, § Manifolds with Corners; source L12472 · not formalized

Suppose $M$ is a topological $n$-manifold with boundary. A chart with corners for $M$ is a pair $(U,\varphi)$ with $U \subseteq M$ open and $\varphi$ a homeomorphism from $U$ onto a relatively open subset $\widehat{U} \subseteq \overline{\mathbb{R}}^{n}_{+}$. Two charts with corners $(U,\varphi)$ and $(V,\psi)$ are smoothly compatible if $\varphi \circ \psi^{-1} \colon \psi(U \cap V) \to \varphi(U \cap V)$ is smooth, meaning it admits a smooth extension near each point.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib supports arbitrary ModelWithCorners and provides the Euclidean quadrant model, but it does not package Lee’s chart-with-corners maximal-atlas definition together with corner-depth points, their chart invariance, boundary-face decomposition, or Stokes integration on such boundaries. The model machinery is only a proper ingredient for this row. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing converse directions, and substantive reconstruction from generic ingredients.

Definition/convention — smooth manifold

FC08-C16-U025 · Ch. 16, § Manifolds with Corners; source L12474 · not formalized

means that it admits a smooth extension in an open neighborhood of each point.) A smooth structure with corners on a topological manifold with boundary is a maximal collection of smoothly compatible interior charts and charts with corners whose domains cover M . A topological manifold with boundary together with a smooth structure with corners is called a smooth manifold with corners. Any chart with corners in the given smooth structure with corners is called a smooth c

Example 16.19

FC08-C16-U026 · Ch. 16, § Manifolds with Corners; source L12476 · not formalized

Example 16.19. Any closed rectangle in $\mathbb { R } ^ { n }$ is a smooth n-manifold with corners.

Definition/convention — corner points of the model orthant

FC08-C16-U027 · Ch. 16, § Manifolds with Corners; source L12483 · not formalized

The boundary of $\overline{\mathbb{R}}^{n}_{+}$ in $\mathbb{R}^{n}$ is the set of points at which at least one coordinate vanishes; the points at which more than one coordinate vanishes are its corner points. For example, the corner points of $\overline{\mathbb{R}}^{3}_{+}$ are the origin together with the points on the positive $x$-, $y$- and $z$-axes.

Proposition 16.20

FC08-C16-U028 · Ch. 16, § Manifolds with Corners; source L12485 · not formalized

positive $x \mathrm { - } , y \mathrm { - } .$ , and z-axes. Proposition 16.20 (Invariance of Corner Points). Let M be a smooth n-manifold with corners, $n \geq 2$ , and let $p \in M$ $I f \varphi ( p )$ is a corner point for some smooth chart with corners $( U , \varphi )$ , then the same is true for every such chart whose domain contains $p$.

Definition/convention — corner point

FC08-C16-U029 · Ch. 16, § Manifolds with Corners; source L12496 · not formalized

If $M$ is a smooth manifold with corners, a point $p \in M$ is a corner point if $\varphi(p)$ is a corner point of $\overline{\mathbb{R}}^{n}_{+}$ for some, hence every, smooth chart with corners $(U,\varphi)$, and a boundary point if $\varphi(p) \in \partial\overline{\mathbb{R}}^{n}_{+}$ for some, hence every, such chart. For example, the corner points of the unit cube $[0,1]^{3} \subseteq \mathbb{R}^{3}$ are its eight vertices together with its twelve edges.

Definition/convention — smooth manifold

FC08-C16-U030 · Ch. 16, § Manifolds with Corners; source L12498 · not formalized

Every smooth manifold with or without boundary is also a smooth manifold with corners (but with no corner points). Conversely, a smooth manifold with corners is a smooth manifold with boundary if and only if it has no corner points. The boundary of a smooth manifold with corners, however, is in general not a smooth manifold with corners (e.g., think of the boundary of a cube). In fact, even the boundary of $\overline { { \mathbb { R } } } _ { + } ^ { n }$ itself is not a smooth manifold with corners. It is, however, a union of finitely many such: $\partial \mathbb { \overline { { R } } } _ { + } ^ { n } = H _ { 1 } \cup \cdots \cup H _ { n }$ , where \[ H _ {i} = \left\{\left(x ^ {1}, \dots , x ^ {n}\right) \in \overline {{\mathbb {R}}} _ {+} ^ {n}: x ^ {i} = 0 \right\}\tag{16.7} \] is an $( n - 1 )$ -dimensional smooth manifold with co 94335cc0f52adee7ce50.jpg) Fig.

Definition/convention — integral of

FC08-C16-U031 · Ch. 16, § Manifolds with Corners; source L12508 · not formalized

In addition, for Stokes’s theorem we need to integrate a differential form over the boundary of a smooth manifold with corners. Since the boundary is not itself a smooth manifold with corners, this requires a separate (albeit routine) definition. Let M be an oriented smooth n-manifold with corners, and suppose $\omega$ is an .n 1/- form on @M that is compactly supported in the domain of a single oriented smooth chart with corners $( U , \varphi )$ . We define the integral of ! over @M by Fig. 16.12 Parametrizing the boundary of the square \[ \int_ {\partial M} \omega = \sum_ {i = 1} ^ {n} \int_ {H _ {i}} \left(\varphi^ {- 1}\right) ^ {*} \omega , \] where $H _ { i }$ , defined by (16.7), is given the induced orientation as part of the boundary of the set where $x ^ { i } \geq 0$ . In other words, we simply integrate ! in coordinates over the codimension-1 portion of the boundary. Finally, if ! is an arbitrary compactly supported .n 1/-form on M; we define the integral of $\omega$ over @M by piecing together with a partition of unity just as in the case of a manifold with bo entation covering, which is an honest covering map in this case.

Proposition 16.21

FC08-C16-U032 · Ch. 16, § Manifolds with Corners; source L12521 · after FC08-C16-U011 · not formalized

analogue of Proposition 16.8. Proposition 16.21. The statement of Proposition 16.8 is true if M is replaced by the boundary of a compact, oriented, smooth n-manifold with corners. E

Example 16.23

FC08-C16-U033 · Ch. 16, § Manifolds with Corners; source L12525 · after FC08-C16-U032 · not formalized

Let $I \times I = [0,1] \times [0,1]$ be the unit square in $\mathbb{R}^{2}$ and $\omega$ a 1-form on $\partial(I \times I)$. The maps $F_{i} \colon I \to I \times I$ given by \[ F_{1}(t) = (t,0), \quad F_{2}(t) = (1,t), \quad F_{3}(t) = (1-t,1), \quad F_{4}(t) = (0,1-t) \tag{16.8} \] satisfy the hypotheses of Proposition 16.21 — in sequence they traverse the boundary counterclockwise — so \[ \int_{\partial(I \times I)} \omega = \int_{F_{1}} \omega + \int_{F_{2}} \omega + \int_{F_{3}} \omega + \int_{F_{4}} \omega. \]

Theorem 16.25

FC08-C16-U034 · Ch. 16, § Manifolds with Corners; source L12544 · not formalized

Theorem 16.25 (Stokes’s Theorem on Manifolds with Corners). Let M be an oriented smooth n-manifold with corners, and let ! be a compactly supported smooth .n 1/-form on M . Then \[ \int_ {M} d \omega = \int_ {\partial M} \omega . \]

Theorem 16.26

FC08-C16-U035 · Ch. 16, § Manifolds with Corners; source L12560 · not formalized

Suppose $M$ is a smooth manifold and $\gamma_{0}, \gamma_{1} \colon [a,b] \to M$ are path-homotopic piecewise smooth curve segments. Then for every closed 1-form $\omega$ on $M$, $\int_{\gamma_{0}} \omega = \int_{\gamma_{1}} \omega$.

Not formalized. none; no complete checked declaration under strict bundle semantics — These de Rham consequences require smooth manifold differential forms, exterior derivative, and integration/Stokes. P/H has no such manifold-level complex; generic path homotopy and simply-connected topology do not own the closed-form statements. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing converse directions, and substantive reconstruction from generic ingredients.

Corollary 16.27

FC08-C16-U036 · Ch. 16, § Manifolds with Corners; source L12611 · not formalized

On a simply connected smooth manifold, every closed 1-form is exact.

Definition/convention — volume of M by Vol beginarray r ( M )

FC08-C16-U037 · Ch. 16, § Integration of Functions on Riemannian Manifolds; source L12623 · not formalized

Suppose $( M , g )$ is an oriented Riemannian manifold with or without boundary, and let $\omega _ { g }$ denote its Riemannian volume form. If f is a compactly supported continuous real-valued function on M; then $f \omega _ { g }$ is a compactly supported n-form, so we can define the integral of f over M to be $\textstyle \int _ { M } f \omega _ { g }$ . If M itself is compact, we define the volume of M by Vol $\begin{array} { r } { ( M ) = \int _ { M } \omega _ { g } } \end{array}$

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has standard-tangent Riemannian metrics, volume-related linear algebra, vector fields, and specialized divergence results, but no checked Riemannian manifold volume-form/integration/divergence/curl package matching the row. The rows also inherit FC08’s unbridged point-derivation tangent model and, where relevant, the missing general submanifold layer. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing converse directions, and substantive reconstruction from generic ingredients.

Convention/notation — source terminology/construction

FC08-C16-U038 · Ch. 16, § Integration of Functions on Riemannian Manifolds; source L12625 · not formalized

$\begin{array} { r } { ( M ) = \int _ { M } \omega _ { g } } \end{array}$ Because of these definitions, the Riemannian volume form is often denoted by d $V _ { g }$ (or $d A _ { g }$ or $d s _ { g }$ in the 2-dimensional or 1-dimensional case, respectively). Then the integral of f over M is written $\textstyle { \int _ { M } f d V _ { g } }$ , and the volume of M as $\textstyle \int _ { M } d V _ { g }$ Be warned, however, that this notation is not meant to imply that the volume form is the exterior derivative of an .n 1/-form; in fact, as we will see when we study de Rham cohomology, this is never the case on a compact manifold. You should just interpret $d V _ { g }$ as a notatio g number by the same constant.

Proposition 16.28

FC08-C16-U039 · Ch. 16, § Integration of Functions on Riemannian Manifolds; source L12627 · not formalized

Proposition 16.28. Let $( M , g )$ be a nonempty oriented Riemannian manifold with or without boundary, and suppose f is a compactly supported continuous realvalued function on M satisfying $f \geq 0$ . Then $\textstyle { \int _ { M } f d V _ { g } \geq 0 }$ , with equality if and only ngth” to a curve by using this varying measuring scale along the points of the curve.

Definition/convention — smooth bundle isomorphism

FC08-C16-U040 · Ch. 16, § The Divergence Theorem; source L12653 · not formalized

In addition, as we did in Chapter 14 in the case of $\mathbb { R } ^ { 3 }$ , we define a smooth bundle isomorphism $\beta \colon { \mathfrak { X } } ( M ) \to \Omega ^ { n - 1 } ( M )$ as follows: \[ \beta (X) = X \lrcorner d V _ {g}.\tag{16.11} \]

Lemma 16.30

FC08-C16-U041 · Ch. 16, § The Divergence Theorem; source L12661 · not formalized

Let $(M,g)$ be an oriented Riemannian manifold with or without boundary. Suppose $S \subseteq M$ is an immersed hypersurface with the orientation determined by a unit normal vector field $N$, and $\widetilde{g}$ is the induced metric on $S$. Then for any vector field $X$ along $S$, \[ \iota_{S}^{*}(\beta(X)) = \langle X, N \rangle_{g}\, dV_{\widetilde{g}}. \tag{16.12} \]

Theorem 16.32

FC08-C16-U042 · Ch. 16, § The Divergence Theorem; source L12712 · not formalized

Theorem 16.32 (The Divergence Theorem). Let $( M , g )$ be an oriented Riemannian manifold with boundary. For any compactly supported smooth vector field X on M; \[ \int_ {M} (\operatorname{div} X) d V _ {g} = \int_ {\partial M} \langle X, N \rangle_ {g} d V _ {\widetilde {g}}, \] where N is the outward-pointing unit normal vector field along @M and $\widetilde g$ is the induc the definition of the integral of a 1-form over an interval, our definition of the integral of an n-form might look like a trick of notation.

Definition/convention — volume-increasing

FC08-C16-U043 · Ch. 16, § The Divergence Theorem; source L12728 · not formalized

Lemma 16.30. The term “divergence” is used because of the following geometric interpretation. A smooth flow on M is said to be volume-preserving if for every compact regular domain D, we have Vol $\left( \theta _ { t } ( D ) \right) = \mathrm { V o l } ( D )$ whenever the domain of $\theta _ { t }$ contains D. It is called volume-increasing, volume-decreasing, volume-nonincreasing, or volume-nondecreasing if for every such D, Vol $\left( \theta _ { t } ( D ) \right)$ is strictly increasing, strictly decreasing, nonincreasing, or nondecreasing, respectively, as a function of t. Note that the properties of flow domains ensure that if D is contained in the domain of $\theta _ { t }$ for some t , then the same is true for all t

Proposition 16.33

FC08-C16-U044 · Ch. 16, § The Divergence Theorem; source L12732 · not formalized

16.15). Proposition 16.33 (Geometric Interpretation of the Divergence). Let M be an oriented Riemannian manifold, let $X \in { \mathfrak { X } } ( M )$ , and let be the flow of X. Then is (a) volume-preserving if and only if div $X = 0$ everywhere on M . (b) volume-nondecreasing if and only if div $X \geq 0$ everywhere on M . (c) volume-nonincreasing if and only if div $X \le 0$ everywhere on M . (d) volume-increasing if and only if div $X > 0$ on a dense subset of M . (e) volume-decreasing if and only if div $X < 0$ on a dense subset t arbitrary open subsets or arbitrary compact subsets are domains of integration, we need the following lemma.

Definition/convention — source terminology/construction

FC08-C16-U045 · Ch. 16, § Surface Integrals; source L12794 · after FC08-C15-U040 · not formalized

Let $S \subseteq M$ be a compact 2-dimensional submanifold with or without boundary and $N$ a smooth unit normal vector field along $S$, and let $dA$ be the Riemannian volume form on $S$ for the induced metric $\iota_{S}^{*}g$ and the orientation determined by $N$, so that $dA = \iota_{S}^{*}(N \lrcorner\, dV_{g})$ by Proposition 15.32. For any smooth vector field $X$ defined on $M$, the surface integral of $X$ over $S$ is \[ \int_{S} \langle X, N \rangle_{g}\, dA. \]

Theorem 16.34

FC08-C16-U046 · Ch. 16, § Surface Integrals; source L12805 · not formalized

Theorem 16.34 (Stokes’s Theorem for Surface Integrals). Suppose M is an oriented Riemannian 3-manifold with or without boundary, and S is a compact oriented 2-dimensional smooth submanifold with boundary in M . For any smooth vector field X on M; \[ \int_ {S} \langle \operatorname{curl} X, N \rangle_ {g} d A = \int_ {\partial S} \langle X, T \rangle_ {g} d s, \] where N is the smooth unit normal vector field along S that determines its orientation, ds is the Riemannian volume form for @S (with respect to the metric and orientation induced from S), and T is the unique positively oriented unit tangent vector field along $\partial S$.

Definition/convention — objects

FC08-C16-U047 · Ch. 16, § Densities; source L12841 · after FC08-C16-U003 · not formalized

In the theory of integration of differential forms, the crucial place where orientations entered the picture was in our proof of the diffeomorphism-invariance of the integral (Proposition 16.1), because the transformation law for an n-form on an n-manifold under a change of coordinates involves the Jacobian determinant of the transition map, while the transformation law for integrals involves the absolute value of the determinant. We had to restrict attention to orientation-preserving diffeomorphisms so that we could freely remove the absolute value signs. In this section we define objects whose transformation law involves the absolute value of the determinant, so that we no longer have this sign problem.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H search finds no linear density type in Lee’s determinant-transformation sense, no smooth manifold density bundle, and no Riemannian-density integration layer. Measure withDensity and Jacobian absolute-determinant formulas are measure-theoretic notions with a different interface and do not realize the source construction. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing converse directions, and substantive reconstruction from generic ingredients.

Definition/convention — density

FC08-C16-U048 · Ch. 16, § Densities; source L12843 · not formalized

We begin, as always, in the linear-algebraic setting. Let V be an n-dimensional vector space. A density on V is a function \[ \mu \colon \underbrace{V \times \cdots \times V}_{n \text{ copies}} \to \mathbb{R} \] satisfying $\mu(Tv_{1},\dots,Tv_{n}) = |\det T|\,\mu(v_{1},\dots,v_{n})$ for every linear map $T \colon V \to V$.

Definition/convention — density

FC08-C16-U049 · Ch. 16, § Densities; source L12855 · not formalized

(Compare this with the corresponding formula (14.2) for n-forms.) Observe that a density is not a tensor, because it is not linear over R in any of its arguments. Let ${ \mathcal { D } } ( V )$ denote the set of all densities eft as an exercise.

Proposition 16.35

FC08-C16-U050 · Ch. 16, § Densities; source L12857 · not formalized

Proposition 16.35 (Properties of Densities). Let V be a vector space of dimension $n \geq 1$ (a) .V / is a vector space under the obvious vector operations: \[ (c _ {1} \mu_ {1} + c _ {2} \mu_ {2}) (v _ {1}, \dots , v _ {n}) = c _ {1} \mu_ {1} (v _ {1}, \dots , v _ {n}) + c _ {2} \mu_ {2} (v _ {1}, \dots , v _ {n}). \] (b) If $\mu _ { 1 } , \mu _ { 2 } \in \mathcal { D } ( V )$ and $\mu _ { 1 } ( E _ { 1 } , \ldots , E _ { n } ) = \mu _ { 2 } ( E _ { 1 } , \ldots , E _ { n } )$ for some basis $\left( E _ { i } \right)$ of V , then $\mu _ { 1 } = \mu _ { 2 }$ (c) If $\omega \in \Lambda ^ { n } ( V ^ { * } )$ , the map $| \omega | : V \times \cdots \times V \to \mathbb { R }$ defined by \[ | \omega | (v _ {1}, \dots , v _ {n}) = | \omega (v _ {1}, \dots , v _ {n}) | \] is a density. (d) ${ \mathcal { D } } ( V )$ is 1-dimensional, spanned by ! for any nonzero $\omega \in \Lambda ^ { n } ( V ^ { * } )$ Proof. Part (a) is immediate from the definition. For part (b), suppose $\mu _ { 1 }$ and $\mu _ { 2 }$ give the same value smooth chart on $N$ whose domain contains the support of $F ^ { * } \omega$ , and the result then follows immediately from Proposition 16.3.

Definition/convention — positive density

FC08-C16-U051 · Ch. 16, § Densities; source L12903 · not formalized

A positive density on V is a density $\mu$ satisfying $\mu ( v _ { 1 } , \ldots , v _ { n } ) > 0$ v _ { n } )$ is a linearly independent n-tuple. A negative density is defined similarly. If ! is a nonzero element of $\Lambda ^ { n } ( V ^ { * } )$ , then it is clear that ! is a positive density; more generally, a density $c \left| \omega \right|$ is positive, negative, or zero if and only if c has the same property. Thus, each density on V is either positive, negative, or zero, and the set of positive densities is a convex subset of ${ \mathcal { D } } ( V )$ (namely, a half-line). Now let M be a smooth manifold with or without boundary. The set \[ \mathcal {D} M = \coprod_ {p \in M} \mathcal {D} (T _ {p} M) \] is called the density bundle of M . Let $

Construction/definition — density bundle of M

FC08-C16-U052 · Ch. 16, § Densities; source L12905 · not formalized

Now let M be a smooth manifold with or without boundary. The set \[ \mathcal {D} M = \coprod_ {p \in M} \mathcal {D} (T _ {p} M) \] is called the density bundle of M . Let $\pi \colon { \mathcal { D } } M \to M$ be the natural projection map taking each element of $\mathcal { D } ( T _ { p } M )$

Proposition 16.36

FC08-C16-U053 · Ch. 16, § Densities; source L12913 · not formalized

Proposition 16.36. If M is a smooth manifold with or without boundary, its density bundle is a smooth line bundle over M . P

Definition/convention — density

FC08-C16-U054 · Ch. 16, § Densities; source L12937 · not formalized

If $M$ is a smooth $n$-manifold with or without boundary, a section of $DM$ is called a density on $M$. If $\mu$ is a density and $f$ a continuous real-valued function, then $f\mu$ is again a density, smooth when both are. A density is positive or negative if its value at each point is. Any nonvanishing $n$-form $\omega$ determines a positive density $|\omega|$ by $|\omega|_{p} = |\omega_{p}|$, and if $\omega$ is a nonvanishing $n$-form on an open subset $U \subseteq M$, every density $\mu$ on $U$ can be written $\mu = f|\omega|$ for a real-valued function $f$.

Proposition 16.37

FC08-C16-U055 · Ch. 16, § Densities; source L12941 · not formalized

Proposition 16.37. If M is a smooth manifold with or without boundary, there exists a smooth positive density on M . P

Definition/convention — density F

FC08-C16-U056 · Ch. 16, § Densities; source L12947 · not formalized

Densities pull back under smooth maps in the same way as differential forms: if $F \colon M \to N$ is a smooth map between $n$-manifolds, with or without boundary, and $\mu$ is a density on $N$, then $F^{*}\mu$ is the density on $M$ given by \[ (F^{*}\mu)_{p}(v_{1},\dots,v_{n}) = \mu_{F(p)}\big(dF_{p}(v_{1}),\dots,dF_{p}(v_{n})\big). \]

Proposition 16.38

FC08-C16-U057 · Ch. 16, § Densities; source L12953 · not formalized

Proposition 16.38. Let $G \colon P \to M$ and $F \colon M \to N$ be smooth maps between n-manifolds with or without boundary, and let be a density on $N$ (a) For any $f \in C ^ { \infty } ( N ) , F ^ { * } ( f \mu ) = ( f \circ F ) F ^ { * } \mu$ (b) If ! is an n-form on N , then $F ^ { * } | \omega | = | F ^ { * } \omega |$ (c) If is smooth, then $F ^ { * } \mu$ is a smooth density on M . (d) $( F \circ G ) ^ { * } \mu = G ^ { * } ( F ^ { * } \mu )$

Proposition 16.40

FC08-C16-U058 · Ch. 16, § Densities; source L12967 · not formalized

Proposition 16.40. Suppose $F \colon M \to N$ is a smooth map between n-manifolds with or without boundary. $H ( x ^ { i } )$ and $\left( y ^ { j } \right)$ are smooth coordinates on open subsets $U \subseteq M$ and $V \subseteq N$ , respectively, and u is a continuous real-valued function on $V ,$ then the following holds on $U \cap F ^ { - 1 } ( V )$ \[ F ^ {*} \left(u \left| d y ^ {1} \wedge \dots \wedge d y ^ {n} \right|\right) = (u \circ F) | \det D F | \left| d x ^ {1} \wedge \dots \wedge d x ^ {n} \right|,\tag{16.19} \] where DF represents the matrix of partial derivatives of $F$.

Definition/convention — integral of

FC08-C16-U059 · Ch. 16, § Densities; source L12981 · not formalized

If $D \subseteq \mathbb{R}^{n}$ is a domain of integration and $\mu$ a density on $\overline{D}$, then $\mu = f\,|dx^{1} \wedge \cdots \wedge dx^{n}|$ for a uniquely determined continuous $f \colon \overline{D} \to \mathbb{R}$, and the integral of $\mu$ over $D$ is \[ \int_{D} \mu = \int_{D} f\, dV, \] or more suggestively \[ \int_{D} f\,\left|dx^{1} \wedge \cdots \wedge dx^{n}\right| = \int_{D} f\, dx^{1} \cdots dx^{n}. \]

Definition/convention — source terminology/construction

FC08-C16-U060 · Ch. 16, § Densities; source L12993 · not formalized

Similarly, if U is an open subset of ℝ ^n or ℍ ^n and μ is compactly supported in U , we define \[ \int_{U} \mu = \int_{D} \mu, \] where $D$ is any domain of integration containing the support of $\mu$; this is diffeomorphism-invariant.

Proposition 16.41

FC08-C16-U061 · Ch. 16, § Densities; source L13001 · not formalized

Proposition 16.41. Suppose U and V are open subsets of $\mathbb { R } ^ { n }$ or $\mathbb { H } ^ { n }$ , and $G \colon U \to$ $V$ is a diffeomorphism. $I f \mu$ is a compactly supported density on $V$ , then \[ \int_ {V} \mu = \int_ {U} G ^ {*} \mu . \]

Definition/convention — density

FC08-C16-U062 · Ch. 16, § Densities; source L13009 · not formalized

Let $M$ be a smooth $n$-manifold with or without boundary. If $\mu$ is a density on $M$ whose support lies in the domain of a single smooth chart $(U,\varphi)$, the integral of $\mu$ over $M$ is \[ \int_{M} \mu = \int_{\varphi(U)} \left(\varphi^{-1}\right)^{*}\mu, \] and this is extended to arbitrary densities by a partition of unity $\{\psi_{i}\}$: \[ \int_{M} \mu = \sum_{i} \int_{M} \psi_{i}\mu. \]

Proposition 16.42

FC08-C16-U063 · Ch. 16, § Densities; source L13025 · not formalized

Proposition 16.42 (Properties of Integrals of Densities). Suppose M and N are smooth n-manifolds with or without boundary, and $\mu , \eta$ are compactly supported densities on M . (a) LINEARITY: If a; $b \in \mathbb { R }$ , then \[ \int_ {M} a \mu + b \eta = a \int_ {M} \mu + b \int_ {M} \eta . \] (b) POSITIVITY: $I f \mu$ is a positive density, then $\textstyle \int _ { M } \mu > 0$ (c) DIFFEOMORPHISM INVARIANCE: If $F \colon N \to M$ is a diffeomorphism, then $\textstyle \int _ { M } \mu = \int _ { N } F ^ { * } \mu$ Exercise 16.43. Prove Proposition 16.42. Just as for forms, integrals of densities are usually computed by cutting the manifold into pieces and parametrizing riented smooth n-manifold with boundary, and let !

Proposition 16.45

FC08-C16-U064 · Ch. 16, § The Riemannian Density; source L13047 · not formalized

Proposition 16.45 (The Riemannian Density). Let $( M , g )$ be a Riemannian manifold with or without boundary. There is a unique smooth positive density $\mu _ { g }$ on M; called the Riemannian density, with the property that \[ \mu_ {g} (E _ {1}, \dots , E _ {n}) = 1\tag{16.20} \] for any local orthonormal frame s really just a finite sum.

Convention/notation — source terminology/construction

FC08-C16-U065 · Ch. 16, § The Riemannian Density; source L13069 · not formalized

By Exercise 16.46(b) the Riemannian density is customarily written $dV_{g}$, the context saying whether a density or a form is meant. For a compactly supported continuous $f \colon M \to \mathbb{R}$, the integral of $f$ over $M$ is $\int_{M} f\,dV_{g}$. When $M$ is oriented either reading gives the same answer, since reversing the orientation changes the signs of both the integral and $dV_{g}$; when $M$ is nonorientable, only the density reading is available.

Theorem 16.48

FC08-C16-U066 · Ch. 16, § The Riemannian Density; source L13073 · not formalized

Theorem 16.48 (The Divergence Theorem in the Nonorientable Case). Suppose $( M , g )$ is a nonorientable Riemannian manifold with boundary. For any compactly supported smooth vector field X on M; \[ \int_ {M} (\mathrm{div} X) \mu_ {g} = \int_ {\partial M} \langle X, N \rangle_ {g} \mu_ {\widetilde {g}},\tag{16.21} \] where N is the outward-pointing unit normal vector field along @M; $\widetilde g$ is the induced Riemannian metric on @M; and $\mu _ { g } , \mu _ { \widetilde { g } }$ are the Riemannian densities of $g$ and $\widetilde { g }$ , respectively. Proof. Let $\widehat { \pi } \colon \widehat { M } \to M$ be the orientation covering of M . Problem 5-12 shows that $\hat { \pi }$ restricts to a smooth covering map from each component of $\partial \widehat { M }$ to a component of $\partial M$