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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 12 definitions, 7 theorems, 9 propositions, 5 lemmas, 1 corollary and 3 examples.

Of the 37 statements checked against Lean, 0 are formalized somewhere and 37 are not.

Status	Statements	Share	What it means
not formalized	37	100%	A documented search found no Lean statement of it anywhere.
checked in total	37

Which versions of Lean and Mathlib were searched

Canonical block: FC08-C19-U001–FC08-C19-U037, 37 contiguous unique rows.
Search order: project A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0; Lean 4.33.0), current H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0; Lean 4.34.0-rc2), then indexed/current/external Lean search.
Result: 0 positive routes, 37 dated unmatched rows.
P/H contain tangent bundles, smooth vector fields, VectorField.mlieBracket, GroupLieAlgebra, left-invariant vector fields, and abstract LieSubalgebra; searches for smooth tangent subbundles/distributions, involutive/integral manifolds, Frobenius, foliations, and Lie-subalgebra integration found no source-level owner.
U011–U017 also depend on the missing differential-form/exterior-derivative layer from C14–C17. U035–U037 require the missing Frobenius/Pfaffian multivariable integrability theorem, not merely local ODE existence.
N=2026-09-07 marks all negative decisions; strict whole-row semantics apply.

Definition/convention — smooth distribution

FC08-C19-U001 · Ch. 19, § Distributions and Involutivity; source L14751 · not formalized

Let M be a smooth manifold. A distribution on M of rank k is a rank-k subbundle of TM . It is called a smooth distribution if it is a smooth subbundle. Distributions are also sometimes called tangent distributions (especially if there is any opportunity for confusion with the use of the term distribution for generalized functions in analysis), k-plane fields, or tangent subbundles.

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have tangent bundles, smooth vector fields, and the manifold Lie bracket, but no smooth tangent-subbundle/distribution object, integral-manifold predicate, or involutivity interface; these adjacent ingredients do not own the row. Strict whole-row semantics reject proper subsets and unbridged reconstruction.

Definition/convention — rank-k distribution

FC08-C19-U002 · Ch. 19, § Distributions and Involutivity; source L14753 · after FC08-C10-U046 · not formalized

Often a rank-k distribution is described by specifying for each $p \in M$ a linear subspace $D _ { p } \subseteq T _ { p } M$ of dimension k, and letting $\textstyle D = \bigcup _ { p \in M } D _ { p }$ . It then follows from the local frame criterion for subbundles (Lemma 10.32) that D is a smooth distribution if and only if each point of M has a neighborhood $U$ on which there are smooth vector fields $X _ { 1 } , \dots , X _ { k } \colon U T M$ such that $X _ { 1 } | _ { q } , \ldots , X _ { k } | _ { q }$ form a basis for $D _ { q }$ at each $q \in U$ . In this case, we say that $D$ is the distribution (locally) spanned by the vector fields $X _ { 1 } , \ldots , X _ { k }$

Definition/convention — integral manifold of D

FC08-C19-U003 · Ch. 19, § Integral Manifolds and Involutivity; source L14757 · not formalized

Suppose $D \subseteq TM$ is a smooth distribution. A nonempty immersed submanifold $N \subseteq M$ is an integral manifold of $D$ if $T_{p}N = D_{p}$ at each $p \in N$. The main question of this chapter is the existence of integral manifolds.

Example 19.1

FC08-C19-U004 · Ch. 19, § Integral Manifolds and Involutivity; source L14761 · after FC08-C10-U047, FC08-C10-U050 · not formalized

Example 19.1 (Distributions and Integral Manifolds). (a) If V is a nowhere-vanishing smooth vector field on a manifold M; then V spans a smooth rank-1 distribution on M (see Example 10.33(a)). The image of any integral curve of V is an integral manifold of $D$ (b) In $\mathbb { R } ^ { n }$ , the vector fields $\partial / \partial x ^ { 1 } , \ldots , \partial / \partial x ^ { k }$ span a smooth distribution of rank k. The k-dimensional affine subspaces parallel to $\mathbb { R } ^ { k }$ are integral manifolds. (c) Let R be the distribution on $\mathbb { R } ^ { n } \setminus \{ 0 \}$ spanned by the unit radial vector field $x ^ { i } \partial / \partial x ^ { i }$ , and let $R ^ { \perp }$ be its orthogonal complement bundle (see Lemma 10.35). Then $R ^ { \perp }$ is a smooth rank- $( n - 1 )$ distribution on $\mathbb { R } ^ { n } \setminus \{ 0 \}$ . Through each point $x \in \mathbb { R } ^ { n } \setminus \{ 0 \}$ , the sphere of radius $| x |$ around 0 is an integral manifold of $R ^ { \perp }$ (d) Let D be the smooth distribution on $\mathbb { R } ^ { 3 }$ spanned by the following vector fields: \[ X = \frac {\partial}{\partial x} + y \frac {\partial}{\partial z}, \qquad Y = \frac {\partial}{\partial y}. \] (See Fig. 19.1.) It

Definition/convention — source terminology/construction

FC08-C19-U005 · Ch. 19, § Integral Manifolds and Involutivity; source L14780 · not formalized

The last example shows that in general, integral manifolds may fail to exist. Suppose D is a smooth distribution on M . We say that D is involutive if given any pair of smooth local sections of D (i.e., smooth vector fields X, Y defined on an open subset of M such that $X _ { p } , Y _ { p } \in D _ { p }$ for each $p )$ , their Lie bracket is also a local section of D. The next proposition shows that the involutivity condition can be expressed concisely in terms of lie algebras.

Proposition 19.2

FC08-C19-U006 · Ch. 19, § Integral Manifolds and Involutivity; source L14782 · not formalized

T M$ be a smooth distribution, and let $\Gamma ( D \mathfrak { X } } ( M )$ denote the space of smooth global sections of $D$ . Then D is involutive if and only if $\Gamma ( D )$ is a Lie subalgebra of X.M /. Proof. If D is involutive, the definition implies that $

Definition/convention — integrable

FC08-C19-U007 · Ch. 19, § Integral Manifolds and Involutivity; source L14788 · not formalized

A smooth distribution D on M is said to be integrable if each point of M is contained in an integral manifold of D.

Proposition 19.3

FC08-C19-U008 · Ch. 19, § Integral Manifolds and Involutivity; source L14790 · not formalized

Proposition 19.3. Every integrable distribution is involutive.

Lemma 19.4

FC08-C19-U009 · Ch. 19, § Integral Manifolds and Involutivity; source L14798 · not formalized

Lemma 19.4 (Local Frame Criterion for Involutivity). Let $D \subseteq T M$ be a distribution. If in a neighborhood of every point of M there exists a smooth local frame $( V _ { 1 } , \ldots , V _ { k } )$ for D such that $[ V _ { i } , V _ { j } ]$ is a section of D for each $i , j = 1 , \ldots , k$ , then D is involutive.

Lemma 19.5

FC08-C19-U010 · Ch. 19, § Involutivity and Differential Forms; source L14812 · not formalized

Lemma 19.5 (1-Form Criterion for Smooth Distributions). Suppose M is a smooth n-manifold and $D \subseteq T M$ is a distribution of rank k. Then D is smooth if and only if each point $p \in M$ has a neighborhood U on which there are smooth 1-forms $\omega ^ { 1 } , \ldots , \omega ^ { n - k }$ such that for each $q \in U$ \[ D _ {q} = \mathrm{Ker} \omega^ {1} \big | _ {q} \cap \dots \cap \mathrm{Ker} \omega^ {n - k} \big | _ {q}.\tag{19.1} \]

Definition/convention — local defining forms for D

FC08-C19-U011 · Ch. 19, § Involutivity and Differential Forms; source L14826 · not formalized

If $D$ is a rank-$k$ distribution on a smooth $n$-manifold $M$, any $n-k$ linearly independent 1-forms $\omega^{1},\dots,\omega^{n-k}$ defined on an open subset $U \subseteq M$ and satisfying (19.1) at each $q \in U$ are local defining forms for $D$. More generally, for $0 \leq p \leq n$, a $p$-form $\omega \in \Omega^{p}(M)$ annihilates $D$ if $\omega(X_{1},\dots,X_{p}) = 0$ whenever $X_{1},\dots,X_{p}$ are local sections of $D$; for $p = 0$ only the zero function annihilates $D$.

Not formalized. none; no complete checked declaration under strict bundle semantics — The row requires both a smooth distribution and manifold differential forms/exterior derivative; the former is absent in C19 search and the latter was established absent in FC08 C14–C17. Strict whole-row semantics reject proper subsets and unbridged reconstruction.

Lemma 19.6

FC08-C19-U012 · Ch. 19, § Involutivity and Differential Forms; source L14828 · not formalized

Lemma 19.6. Suppose M is a smooth n-manifold and D is a smooth rank-k distribution on M . Let $\omega ^ { 1 } , \ldots , \omega ^ { n - k }$ be smooth local defining forms for D over an open subset $U \subseteq M$ . A smooth p-form defined on U annihilates D if and only if it can be expressed in the form \[ \eta = \sum_ {i = 1} ^ {n - k} \omega^ {i} \wedge \beta^ {i}\tag{19.2} \] for some smooth $( p - 1 )$ -forms $\beta ^ { 1 } , \ldots , \beta ^ { n - k }$ on $U$ .

Theorem 19.7

FC08-C19-U013 · Ch. 19, § Involutivity and Differential Forms; source L14854 · not formalized

Theorem 19.7 (1-Form Criterion for Involutivity). Suppose $D \subseteq T M$ is a smooth distribution. Then D is involutive if and only if the following condition is satisfied: If is any smooth 1-form that annihilates D on an open subset $U \subseteq M$ ; then d also annihilates D on $U$ (19.3)

Proposition 19.8

FC08-C19-U014 · Ch. 19, § Involutivity and Differential Forms; source L14880 · not formalized

Proposition 19.8 (Local Coframe Criterion for Involutivity). Let D be a smooth distribution of rank k on a smooth n-manifold M; and let $\omega ^ { 1 } , \ldots , \omega ^ { n - k }$ be smooth defining forms for D on an open subset $U \subseteq M$ . The following are equivalent: (a) D is involutive on U . (b) $d \omega ^ { 1 } , \ldots , d \omega ^ { n - k }$ annihilate D. (c) There exist smooth 1-forms $\left\{ \alpha _ { j } ^ { i } : i , j = 1 , \ldots , n - k \right\}$ such that \[ d \omega^ {i} = \sum_ {j = 1} ^ {n - k} \omega^ {j} \wedge \alpha_ {j} ^ {i}, \quad f o r e a c h i = 1, \dots , n - k. \]

Definition/convention — source terminology/construction

FC08-C19-U015 · Ch. 19, § Involutivity and Differential Forms; source L14896 · not formalized

For a smooth distribution $D$ on a smooth $n$-manifold $M$, let $\mathcal{I}^{p}(D) \subseteq \Omega^{p}(M)$ be the space of smooth $p$-forms annihilating $D$, and let $\mathcal{I}(D) = \mathcal{I}^{0}(D) \oplus \cdots \oplus \mathcal{I}^{n}(D) \subseteq \Omega^{*}(M)$.

Definition/convention — Pfaffian system

FC08-C19-U016 · Ch. 19, § Involutivity and Differential Forms; source L14903 · not formalized

Any ideal of the form $\mathcal { A } ( D )$ for some smooth distribution D is sometimes called a Pfaffian system. An ideal A } ^ { * } ( M )$ is said to be a differential ideal if $ } } ) \subseteq { \mathcal { that is, if $\omega \in \mathcal { A }$

Proposition 19.11

FC08-C19-U017 · Ch. 19, § Involutivity and Differential Forms; source L14905 · not formalized

(Differential Ideal Criterion for Involutivity). Let $M$ be a smooth manifold. A smooth distribution $D \subseteq TM$ is involutive if and only if $\mathcal{I}(D)$ is a differential ideal in $\Omega^{*}(M)$.

Definition/convention — source terminology/construction

FC08-C19-U018 · Ch. 19, § The Frobenius Theorem; source L14911 · after FC08-C19-U004 · not formalized

Theorem In Example 19.1, all of the distributions we defined except the last one had the property that there was an integral manifold through each point. Moreover, locally these submanifolds all “fit together” nicely like parallel affine subspaces of R. Given a rank-k distribution $D \subseteq T M ,$ ; let us say that a smooth coordinate chart $( U , \varphi )$ on M is flat for D if $\varphi ( U )$ is a cube in $\mathbb { R } ^ { n }$ , and at points of U , D is spanned by the first k coordinate vector fields $\partial / \partial x ^ { 1 } , \ldots , \partial / \partial x ^ { k } \ \mathrm { ( F i g . \ 1 9 . 2 ) }$ . In any such chart, each slice of the form $x ^ { k + 1 } = c ^ { k + 1 } , . . . , x ^ { n } = c ^ { n }$ for constants $c ^ { k + 1 } , \ldots , c ^ { n }$ is an integral manifold of D. This is the nicest possible local situation for integral manifolds. We say that a distribution $D \subseteq T M$ is completely integrable if there exists a flat chart for $D$ in a neighborhood of each point of M . Obviously, every completely integrable distribution is integrable and therefore involutive. In summary, \[ \text { completely integrable } \Rightarrow \text { integrable } \Rightarrow \text { involutive }. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H/current/external search found no Frobenius theorem, flat-chart/completely-integrable distribution, foliation/leaves structure, maximal integral-manifold construction, or distribution–foliation correspondence. Strict whole-row semantics reject proper subsets and unbridged reconstruction.

Theorem 19.12

FC08-C19-U019 · Ch. 19, § The Frobenius Theorem; source L14923 · not formalized

Theorem 19.12 (Frobenius). Every involutive distribution is completely integrable.

Corollary 19.13

FC08-C19-U020 · Ch. 19, § The Frobenius Theorem; source L14964 · not formalized

Corollary 19.13. Suppose M is a smooth manifold, D is an involutive rank-k distribution on M; and $S \subseteq M$ is a codimension-k embedded submanifold. If $p \in S$ is a point such that $T _ { p } S$ is complementary to $D _ { p }$ , then there is a flat chart $\left( U , \left( s ^ { i } \right) \right)$ for $D$ centered at p in which $S \cap U$ is the slice $s ^ { 1 } = \cdots = s ^ { k } = 0$

Example 19.14

FC08-C19-U021 · Ch. 19, § The Frobenius Theorem; source L14970 · after FC08-C08-U038, FC08-C09-U065 · not formalized

Let $D \subseteq T\mathbb{R}^{3}$ be spanned by \[ X = x\frac{\partial}{\partial x} + \frac{\partial}{\partial y} + x(y+1)\frac{\partial}{\partial z}, \qquad Y = \frac{\partial}{\partial x} + y\frac{\partial}{\partial z}. \] Example 8.27 gives $[X,Y] = -\frac{\partial}{\partial x} - y\frac{\partial}{\partial z} = -Y$, so $D$ is involutive. Inverting $(x,y,z) = \Phi(u,v,w) = (u,\ v,\ w+uv)$ gives the flat coordinates $(u,v,w) = \Phi^{-1}(x,y,z) = (x,\ y,\ z-xy)$, so the integral manifolds of $D$ are the level sets of $w(x,y,z) = z - xy$; since this chart is global, these are all of them.

Proposition 19.16

FC08-C19-U022 · Ch. 19, § The Frobenius Theorem; source L15039 · not formalized

(Local Structure of Integral Manifolds). Let $D$ be an involutive distribution of rank $k$ on a smooth manifold $M$ and let $(U,(x^{i}))$ be a flat chart for $D$. If $H$ is any integral manifold of $D$, then $H \cap U$ is a union of countably many disjoint open subsets of parallel $k$-dimensional slices of $U$, each open in $H$ and embedded in $M$.

Theorem 19.17

FC08-C19-U023 · Ch. 19, § The Frobenius Theorem; source L15049 · not formalized

(See Chapter 5.) Theorem 19.17. Every integral manifold of an involutive distribution is weakly embedded.

Definition/convention — leaves of the foliation)

FC08-C19-U024 · Ch. 19, § Foliations; source L15063 · not formalized

To express more precisely what we mean by “fitting together,” we need to extend our notion of a flat chart slightly. Let M be a smooth n-manifold, and let $\mathcal { F }$ be any collection of k-dimensional submanifolds of M . A smooth chart $( U , \varphi )$ for M is said to be flat for if $\varphi ( U )$ is a cube in $\mathbb { R } ^ { n }$ , and each submanifold in $\mathcal { F }$ intersects $U$ in either the empty set or a countable union of k-dimensional slices of the form $x ^ { k + 1 } = c ^ { k + 1 } , . . . , x ^ { n } = c ^ { n }$ . We define a foliation of dimension k on M to be a collection $\mathcal { F }$ of disjoint, connected, nonempty, immersed k-dimensional submanifolds of M (called the leaves of the foliation), whose union is M; and such that in a neighborhood of each point $p \in M$ there exists a fl suppose $k \geq 2$ , and we have shown that there is a smooth map $\tilde { f _ { 0 } } \colon U \to M$ whose restriction to $U \cap \partial _ { i } \Delta _ { p }$ agrees with f for $i = 1 , \ldots , k - 1$ .

Example 19.18

FC08-C19-U025 · Ch. 19, § Foliations; source L15065 · after FC08-C04-U020 · not formalized

(Foliations). (a) The $k$-dimensional affine subspaces of $\mathbb{R}^{n}$ parallel to $\mathbb{R}^{k} \times \{0\}$ form a $k$-dimensional foliation of $\mathbb{R}^{n}$. (b) The open rays $\{\lambda x : \lambda > 0\}$, as $x$ ranges over $\mathbb{R}^{n} \setminus \{0\}$, form a 1-dimensional foliation of $\mathbb{R}^{n} \setminus \{0\}$. (c) The spheres centered at $0$ form an $(n-1)$-dimensional foliation of $\mathbb{R}^{n} \setminus \{0\}$. (d) For connected smooth manifolds $M$ and $N$, the sets $M \times \{q\}$, $q \in N$, foliate $M \times N$ with leaves diffeomorphic to $M$; the circles $\{p\} \times \mathbb{S}^{1}$ give a different foliation of $\mathbb{T}^{2}$. (e) For fixed $\alpha \in \mathbb{R}$, the images of the curves $\gamma_{\theta}(t) = (e^{it},\ e^{i(\alpha t + \theta)})$, $\theta \in \mathbb{R}$, form a 1-dimensional foliation of the torus, with every leaf an embedded circle when $\alpha$ is rational and every leaf dense when $\alpha$ is irrational. (f) The connected components of the curves in the $(y,z)$-plane given by $z = \sec y + c$ for $c \in \mathbb{R}$ and $y = \left(k + \tfrac{1}{2}\right)\pi$ for $k \in \mathbb{Z}$ foliate $\mathbb{R}^{2}$. (g) Revolving those curves about the $z$-axis gives a 2-dimensional foliation of $\mathbb{R}^{3}$ whose leaves are diffeomorphic to disks or to cylinders.

Proposition 19.19

FC08-C19-U026 · Ch. 19, § Foliations; source L15102 · not formalized

Proposition 19.19. Let be a foliation on a smooth manifold M . The collection of tangent spaces to the leaves of forms an involutive distribution on M . E

Theorem 19.21

FC08-C19-U027 · Ch. 19, § Foliations; source L15108 · not formalized

subgroups.) Theorem 19.21 (Global Frobenius Theorem). Let D be an involutive distribution on a smooth manifold M . The collection of all maximal connected integral manifolds of D forms a foliation of M . T

Lemma 19.22

FC08-C19-U028 · Ch. 19, § Foliations; source L15112 · not formalized

Suppose $D \subseteq TM$ is an involutive distribution and $\{N_{\alpha}\}_{\alpha \in A}$ is any collection of connected integral manifolds of $D$ with a point in common. Then $N = \bigcup_{\alpha} N_{\alpha}$ has a unique smooth manifold structure making it a connected integral manifold of $D$.

Definition/convention — distribution D

FC08-C19-U029 · Ch. 19, § Foliations; source L15151 · not formalized

Suppose $M$ is a smooth manifold and $\Phi \colon M \to M$ is a diffeomorphism. A distribution $D$ on $M$ is $\Phi$-invariant if $d\Phi(D) = D$, that is, if $d\Phi_{x}(D_{x}) = D_{\Phi(x)}$ for each $x \in M$. A foliation $\mathcal{F}$ on $M$ is $\Phi$-invariant if $\Phi(L)$ is a leaf of $\mathcal{F}$ for every leaf $L$ of $\mathcal{F}$.

Proposition 19.23

FC08-C19-U030 · Ch. 19, § Foliations; source L15153 · not formalized

Let M be a smooth manifold and ˚ M M be a diffeomorphism. Suppose D is an involutive distribution on M and F is the foliation it determines. Then D is ˚-invariant if and only if F is ˚-invariant.

Definition/convention — left-invariant

FC08-C19-U031 · Ch. 19, § Lie Subalgebras and Lie Subgroups; source L15159 · not formalized

Foliations have profound applications to the theory of Lie groups. Here we present two such applications; we will see many more in the next two chapters. Both rely on the following simple relationship between Lie subalgebras and distributions. A distribution $D$ on a Lie group G is said to be left-invariant if it is invariant under every left translation. (Recall that this means $d ( L _ { g } ) ( D ) = D$ for each $g \in G . )$

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has GroupLieAlgebra, left-invariant vector fields, and LieSubalgebra, but no checked integration of an arbitrary Lie subalgebra to Lee’s unique connected Lie subgroup or associated involutive distribution/weak embedding. Strict whole-row semantics reject proper subsets and unbridged reconstruction.

Lemma 19.24

FC08-C19-U032 · Ch. 19, § Lie Subalgebras and Lie Subgroups; source L15161 · not formalized

Lemma 19.24. Let G be a Lie group. $H { \mathfrak { h } }$ is a Lie subalgebra of Lie.G/, then the subset $\begin{array} { r } { D = \bigcup _ { g \in G } D _ { g } \subseteq T G } \end{array}$ , where \[ D _ {g} = \{X _ {g}: X \in \mathfrak {h} \} \subseteq T _ {g} G,\tag{19.7} \] is a left-invariant involutive distribution on $G$.

Theorem 19.25

FC08-C19-U033 · Ch. 19, § Lie Subalgebras and Lie Subgroups; source L15171 · not formalized

(Lie Subgroups Are Weakly Embedded). Every Lie subgroup is an integral manifold of an involutive distribution, and therefore is a weakly embedded submanifold.

Theorem 19.26

FC08-C19-U034 · Ch. 19, § Lie Subalgebras and Lie Subgroups; source L15175 · not formalized

embedded in $G$ Theorem 19.26 (The Lie Subgroup Associated with a Lie Subalgebra). Suppose G is a Lie group and g is its Lie algebra. If h is any Lie subalgebra of g, then there is a unique connected Lie subgroup of $G$ whose Lie algebra is $\mathfrak{h}$.

Theorem 19.27

FC08-C19-U035 · Ch. 19, § Overdetermined Systems of Partial Differential Equations; source L15218 · not formalized

Let $W \subseteq \mathbb{R}^{n}$ be open and $1 \leq m \leq n$. Suppose given an embedded codimension-$m$ submanifold $S \subseteq W$, a linearly independent $m$-tuple of smooth vector fields $(A_{1},\dots,A_{m})$ on $W$ whose span is complementary to $T_{p}S$ at each $p \in S$, functions $f_{1},\dots,f_{m} \in C^{\infty}(W)$, and smooth functions $c^{k}_{ij} \in C^{\infty}(W)$ satisfying the compatibility conditions \[ [A_{i},A_{j}] = c^{k}_{ij}A_{k}, \tag{19.9} \] \[ A_{i}f_{j} - A_{j}f_{i} = c^{k}_{ij}f_{k}, \tag{19.10} \] with $k$ summed from $1$ to $m$. Then each $p \in S$ has a neighborhood $U$ such that for every $\varphi \in C^{\infty}(S \cap U)$ there is a unique solution $u \in C^{\infty}(U)$ of the overdetermined Cauchy problem \[ A_{i}u = f_{i} \quad (i = 1,\dots,m), \tag{19.11} \] \[ u|_{S \cap U} = \varphi. \tag{19.12} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have local ODE theory but no multivariable Frobenius/Pfaffian integrability theorem realizing Lee’s stated overdetermined first-order PDE existence-and-uniqueness result. Strict whole-row semantics reject proper subsets and unbridged reconstruction.

Proposition 19.28

FC08-C19-U036 · Ch. 19, § Overdetermined Systems of Partial Differential Equations; source L15302 · not formalized

Suppose $\alpha$ and $\beta$ are smooth real-valued functions on an open subset $W \subseteq \mathbb{R}^{3}$ satisfying (19.14) there. For each $(x_{0},y_{0},z_{0}) \in W$ there are a neighborhood $U$ of $(x_{0},y_{0})$ in $\mathbb{R}^{2}$ and a unique smooth $u \colon U \to \mathbb{R}$ satisfying (19.13) and $u(x_{0},y_{0}) = z_{0}$.

Proposition 19.29

FC08-C19-U037 · Ch. 19, § Overdetermined Systems of Partial Differential Equations; source L15353 · not formalized

Suppose $W$ is an open subset of $\mathbb{R}^{n} \times \mathbb{R}^{m}$ and $\alpha = (\alpha^{i}_{j}) \colon W \to M(m \times n,\mathbb{R})$ is a smooth matrix-valued function satisfying \[ \frac{\partial \alpha^{i}_{j}}{\partial x^{k}} + \alpha^{l}_{k}\frac{\partial \alpha^{i}_{j}}{\partial z^{l}} = \frac{\partial \alpha^{i}_{k}}{\partial x^{j}} + \alpha^{l}_{j}\frac{\partial \alpha^{i}_{k}}{\partial z^{l}} \quad \text{for all } i,j,k, \] where a point of $\mathbb{R}^{n} \times \mathbb{R}^{m}$ is written $(x,z) = (x^{1},\dots,x^{n},z^{1},\dots,z^{m})$. Then for any $(x_{0},z_{0}) \in W$ there is a neighborhood $U$ of $x_{0}$ in $\mathbb{R}^{n}$ and a unique smooth $u \colon U \to \mathbb{R}^{m}$ with $u(x_{0}) = z_{0}$ whose Jacobian satisfies \[ \frac{\partial u^{i}}{\partial x^{j}}(x^{1},\dots,x^{n}) = \alpha^{i}_{j}\big(x^{1},\dots,x^{n},u^{1}(x),\dots,u^{m}(x)\big). \]