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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 30 definitions, 20 theorems, 7 propositions, 6 lemmas, 4 corollaries, 12 examples and 2 conventions.

Of the 81 statements checked against Lean, 2 are formalized somewhere and 79 are not.

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

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 9, FC08-C09-U001–FC08-C09-U081, exactly 81 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Search order followed the Sweep-II plan: project source first at A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean 4.33.0), current upstream Mathlib H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0, Lean 4.34.0-rc2), then targeted indexed/external Lean searches. No project-existing, package-import, or reference-port C09 owner survived strict whole-row checking.
C09 has 2 pinned mathlib rows and 79 dated unmatched rows. Positive rows are: U010, U011.
The controlling geometric boundary is inherited from promoted C03/C08. Lee’s tangent vectors are the point-derivation model; Mathlib’s manifold integral-curve theory (IntegralCurve/Basic, Transform, ExistUnique, UniformTime) is formulated with the separate standard TangentSpace model. Exact P/H searches again found no PointDerivation ≃ TangentSpace bridge. Consequently the otherwise-close integral-curve existence, uniqueness, translation/scaling, uniform-time, vector-field and Lie-bracket APIs cannot silently own Lee’s derivation-tangent rows.
This exclusion is substantive: pinned Mathlib now has a strong manifold integral-curve package. IsMIntegralCurveOn/At, exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless, isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless, the transform lemmas, and exists_isMIntegralCurve_of_isMIntegralCurveOn are all nearby. They establish adjacency only, because using them here would reverse the already-promoted C03 model decision.
U010 and U011 are independent of tangent vectors and do match exactly. Mathlib/Dynamics/Flow.lean::Flow ℝ M stores Lee’s global continuous ℝ-action. Its fixed-time continuity, group laws, toHomeomorph, and orbit_eq_range own U011’s topological clauses. For the smooth clause, after using Flow.toAddAction, ContMDiffVAdd and Diffeomorph.vadd give the fixed-time diffeomorphism. /tmp/fc08-c09-flow-witness.lean compiled the entire U010/U011 interface at P.
P/H have no local/partial-flow structure with a flow domain D ⊆ ℝ × M, no maximal-flow object, and no fundamental theorem producing Lee’s maximal partial flow. Dynamics.Flow is global only. This is the separate blocker for U017–U027, U035–U037, U048–U050, U057–U061 even aside from tangent semantics.
U017 and U018 are canonically truncated in the Sweep-I catalogue; U073 is also truncated before its coordinate formula. They were left unmatched from the canonical text and were not reconstructed from the book during Sweep II.
Current H was checked specifically for LocalFlow, flow-domain/maximal-flow constructions, collar neighborhoods, Lie derivatives, manifold time-dependent vector fields, and first-order characteristics; it contains none. Its relevant flow/integral-curve file set is materially the same as P on these interfaces.
Boundary geometry remains absent: P/H have no collar-neighborhood construction/theorem, boundary flowout theorem, smooth attachment-along-boundary theorem, connected-sum/double construction with Lee’s smooth properties, or boundary flow-box theorem. Geometry/Manifold/Bordism.lean only mentions the collar-neighborhood theorem in prose.
The Lie-derivative/commuting-fields section also has no direct owner. Mathlib has the standard-tangent manifold Lie bracket and global flow/invariant-set APIs, but no Lie derivative of vector fields defined via flow, no vector-field invariance-under-flow predicate, and no local-flow commutation theorem. Replacing Lee’s flow definition by the bracket using his later theorem would reverse the source dependency and cross the tangent-model boundary.
Time-dependent theory is presently Banach-space rather than manifold-level. Mathlib/Analysis/ODE formalizes time-dependent vector fields, integral curves, Picard–Lindelöf local flows, and uniqueness on normed spaces. No P/H theorem gives Lee’s arbitrary-manifold time-dependent flow with maximal domains, restart property, partial-time diffeomorphisms, and cocycle law.
Targeted indexed search found no Lean implementation of the missing collar/local-flow/Lie-derivative/method-of-characteristics results. The only method-of-characteristics hits were non-Lean numerical/symbolic projects and were irrelevant to routing.
No first-order linear/quasilinear Cauchy-problem or method-of-characteristics formalization matching U070–U081 was found in project source, P, H, or indexed Lean repositories.
N=2026-09-07 marks dated unmatched decisions after the prescribed search layers. Strict whole-row semantics apply uniformly.

Definition/convention — integral curve of V

FC08-C09-U001 · Ch. 9, § Integral Curves; source L5902 · not formalized

If $V$ is a vector field on $M$, an integral curve of $V$ is a differentiable curve $\gamma \colon J \to M$ whose velocity at each point equals the value of $V$ there: \[ \gamma'(t) = V_{\gamma(t)} \quad \text{for all } t \in J. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has a substantial manifold integral-curve API (IsMIntegralCurveOn, IsMIntegralCurveAt, local existence/uniqueness, and translation/scaling lemmas), but it is formulated entirely with Mathlib’s standard TangentSpace. Lee’s tangent vectors in FC08 were introduced via point derivations, and promoted C03 established that no checked PointDerivation ≃ TangentSpace bridge exists at P or H. Therefore this otherwise-close integral-curve row cannot be routed without crossing the same unproved model identification. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — starting point of γ

FC08-C09-U002 · Ch. 9, § Integral Curves; source L5908 · not formalized

(See Fig. 9.1.) $\operatorname { I f } 0 \in J$ , the point $\gamma ( 0 )$ is called the starting point of $\gamma .$ . (The reason for the term “integral curve” will be explained shortly. Note that this is one definition that requires some differentiability hypothesis, because the definition of an integra curve would make no sense for a curve that is merely conti e the one whose objects are finitedimensional Lie algebras and whose morphisms are Lie algebra homomorphisms.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has no source-facing “starting point” object/terminology for an interval-domain integral curve matching Lee’s convention. The raw expression γ 0 is only an ingredient, while the manifold integral-curve structures themselves are behind the unbridged tangent-model boundary. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 9.1

FC08-C09-U003 · Ch. 9, § Integral Curves; source L5910 · not formalized

(Integral Curves). (a) Let $(x,y)$ be standard coordinates on $\mathbb{R}^{2}$ and $V = \partial/\partial x$ the first coordinate vector field. There is a unique integral curve starting at each point of the plane, and the images of different integral curves are either identical or disjoint. (b) Let $W = x\,\partial/\partial y - y\,\partial/\partial x$ on $\mathbb{R}^{2}$. Since $\gamma(0) = (a,b)$, again there is a unique integral curve starting at each point $(a,b) \in \mathbb{R}^{2}$, and the images are either identical or disjoint.

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked declaration packages Lee’s two explicit planar integral-curve computations and their uniqueness/image conclusions as this example bundle. Generic ODE/integral-curve machinery would require reconstructing the examples, and the manifold version uses the unbridged standard tangent model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Convention/notation — system of ODEs

FC08-C09-U004 · Ch. 9, § Integral Curves; source L5953 · not formalized

(We use a dot to denote an ordinary derivative with respect to t when there are superscripts that would make primes hard to read.) The fundamental fact about such systems is the existence, uniqueness, and smoothness theorem, Theorem D.1. (This is the reason for the terminology “integral curves,” because solving a system of ODEs is often referred to as “integrating” the system.) We will derive detailed consequences of that theorem later; for now, we just note the following simple result. P

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib/Analysis/ODE formalizes time-dependent ODEs on normed vector spaces, but Lee’s row is a source convention tying local-coordinate vector-field equations to the Appendix-D ODE theorem. No complete declaration owns that notation/convention bundle. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 9.2

FC08-C09-U005 · Ch. 9, § Integral Curves; source L5955 · not formalized

Proposition 9.2. Let V be a smooth vector field on a smooth manifold M . For each point $p \in M$ ; there exist $\varepsilon > 0$ and a smooth curve $\gamma \colon ( - \varepsilon , \varepsilon ) \to M$ that is an integral curve of V starting at $p$.

Lemma 9.3

FC08-C09-U006 · Ch. 9, § Integral Curves; source L5964 · not formalized

Lemma 9.3 (Rescaling Lemma). Let V be a smooth vector field on a smooth manifold M; let $J \subseteq \mathbb { R }$ be an interval, and let $J \to M$ be an integral curve of V . For any $a \in \mathbb { R }$ , the curve $\widetilde \gamma \colon \widetilde J M$ defined by $\widetilde { \gamma } ( t ) = \gamma ( a t )$ is an integral curve of the vector field aV , where $\widetilde { J } = \{ t : a t \in J \}$

Lemma 9.4

FC08-C09-U007 · Ch. 9, § Integral Curves; source L5972 · not formalized

(Translation Lemma). Let $V$, $M$, $J$ and $\gamma$ be as in the preceding lemma. For any $b \in \mathbb{R}$, the curve $\widehat{\gamma} \colon \widehat{J} \to M$ defined by $\widehat{\gamma}(t) = \gamma(t+b)$ is also an integral curve of $V$, where $\widehat{J} = \{t : t + b \in J\}$.

Proposition 9.6

FC08-C09-U008 · Ch. 9, § Integral Curves; source L5976 · not formalized

(Naturality of Integral Curves). Suppose $M$ and $N$ are smooth manifolds and $F \colon M \to N$ is a smooth map. Then $X \in \mathfrak{X}(M)$ and $Y \in \mathfrak{X}(N)$ are $F$-related if and only if $F$ takes integral curves of $X$ to integral curves of $Y$, that is, $F \circ \gamma$ is an integral curve of $Y$ for each integral curve $\gamma$ of $X$.

Convention/notation — map

FC08-C09-U009 · Ch. 9, § Flows; source L6000 · not formalized

Here is another way to visualize the family of integral curves associated with a vector field. Let M be a smooth manifold and $V \in { \mathfrak { X } } ( M )$ , and suppose that for each point $p \in M .$ V has a unique integral curve starting at p and defined for all $t \in \mathbb { R }$ , which we denote by ${ \theta ^ { ( p ) } } \colon { \mathbb { R } } \to M .$ (It may not always be the case that every integral curve is defined for all t , but for purposes of illustration let us assume so for the time being.) For each $t \in \mathbb { R }$ , we can define a map $\theta _ { t } \colon M \to M$ by sending each $p \in M$ to the point obtained by following for time t the integral curve starting at p: \[ \theta_ {t} (p) = \theta^ {(p)} (t). \] Each map $\theta _ { t }$ “slides” the manifold along the integral curves for time t . The translation lemma implies that $t \mapsto \theta ^ { ( p ) } ( t + s )$ is an integral curve of $V$ starting at $q =$ $\theta ^ { ( p ) } ( s )$ ; since we are assuming uniqueness nite-dimensional Lie algebra, a (finitedimensional) representation of g is a Lie algebra homomorphism $\varphi \colon { \mathfrak { g } } \to { \mathfrak { g l } } ( V )$ for some finite-dimensional vector space V , where gl.V / denotes the Lie algebra of linear maps from V to itself.

Not formalized. none; no complete checked declaration under strict bundle semantics — This construction starts from unique global integral curves of Lee’s vector field and forms the time maps θ_t. Flow owns the resulting action once supplied, but Mathlib has no checked construction from Lee’s derivation-model integral curves; the standard-tangent manifold integral-curve theory is unbridged. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — one-parameter group action) to be a continuous left R-action

FC08-C09-U010 · Ch. 9, § Flows; source L6014 · in Mathlib

Motivated by these observations, we define a global flow on M (also called a one-parameter group action) to be a continuous left R-action on M ; that is, a continuous map $\theta \colon \mathbb { R } \times M \to M$ satisfying the following properties for all $s , t \in { \mathbb { R } }$ and $p \in M$ \[ \theta (t, \theta (s, p)) = \theta (t + s, p), \quad \theta (0, p) = p.\tag{9.2} \]

Formalized. Mathlib/Dynamics/Flow.lean::Flow — Flow ℝ M is exactly a continuous left ℝ-action: it stores joint continuity of (t,p) ↦ θ_t(p), the law θ_(t+s)(p)=θ_t(θ_s(p)), and θ_0(p)=p. This is Lee’s global-flow/one-parameter-group-action definition verbatim up to currying.

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

Definition/convention — two collections of maps as follows

FC08-C09-U011 · Ch. 9, § Flows; source L6020 · in Mathlib

Given a global flow $\theta$ on M; we define two collections of maps as follows: For each $t \in \mathbb { R }$ , define a continuous map $\theta _ { t } \colon M \to M$ by \[ \theta_ {t} (p) = \theta (t, p). \] The defining properties (9.2) are equivalent to the group laws \[ \theta_ {t} \circ \theta_ {s} = \theta_ {t + s}, \qquad \theta_ {0} = \mathrm{Id} _ {M}.\tag{9.3} \] As is the case for any continuous group action, each map $\theta _ { t } \colon M \to M$ is a homeomorphism, and if the flow is smooth, $\theta _ { t }$ is a diffeomorphism For each $p \in M$ ; define a curve $\theta ^ { ( p ) } \colon { \mathbb { R } } \to M$ by \[ \theta^ {(p)} (t) = \theta (t, p). \] The image of this curve is th presentation $\rho \colon { \mathfrak { g } } \to { \mathfrak { g l } } ( V )$ for some finite-dimensional real vector space V .

Formalized. Mathlib/Dynamics/Flow.lean::Flow.continuous_toFun, Flow.map_add, Flow.map_zero, Flow.toHomeomorph, Flow.toAddAction, Flow.orbit_eq_range; Mathlib/Geometry/Manifold/Algebra/SMul.lean::ContMDiffVAdd, Diffeomorph.vadd — For φ : Flow ℝ M, pinned Mathlib proves each fixed-time map φ t continuous, the composition/zero laws, and packages φ t as a homeomorphism with inverse φ (-t); orbit_eq_range identifies the orbit with the image of t ↦ φ t p. If the induced additive action is smooth (ContMDiffVAdd), Diffeomorph.vadd packages every fixed-time map as a diffeomorphism. /tmp/fc08-c09-flow-witness.lean compiles the complete Lee bundle at P.

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

Definition/convention — infinitesimal generator of θ

FC08-C09-U012 · Ch. 9, § Flows; source L6047 · not formalized

The next proposition shows that every smooth global flow is derived from the integral curves of some smooth vector field in precisely the way we described above. If $\theta \colon \mathbb { R } \times M \to M$ is a smooth global flow, for each $p \in M$ we define a tangent vector $V _ { p } \in T _ { p } M$ by \[ V _ {p} = \theta^ {(p) \prime} (0). \] The assignment $p \mapsto V _ { p }$ is a (rough) vector field on M; which is called the infinitesimal generator of , for reasons we will explain ).

Not formalized. none; no complete checked declaration under strict bundle semantics — The infinitesimal generator is defined by differentiating the flow curves into T_pM. Mathlib has standard manifold derivatives and smooth additive actions, but Lee’s T_pM is the point-derivation model and no explicit bridge to standard TangentSpace exists. No separate derivation-model infinitesimal-generator theorem was found. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 9.7

FC08-C09-U013 · Ch. 9, § Flows; source L6055 · not formalized

$\theta \colon \mathbb { R } \times M \to M$ be a smooth global flow on a smooth manifold M . The infinitesimal generator V of is a smooth vector field on M; and each curve $\theta ^ { ( p ) }$ is an integral cur t $f ( \lambda x ) = \lambda ^ { c } f ( x )$ for all $\lambda > 0$ and $x \in \mathbb { R } ^ { n } \setminus \{ 0 \}$ .

Example 9.8

FC08-C09-U014 · Ch. 9, § Flows; source L6079 · after FC08-C09-U003 · not formalized

Example 9.8 (Global Flows). The two vector fields on the plane described in Example 9.1 both had integral curves defined for all $t \in \mathbb { R }$ , so they generate global flows. Using the results of that example, we can write down the flows explici - x ^ {3} - x ^ {4} + x ^ {1} + x ^ {2} , \[ \] X _ {3} = - x ^ {4} + x ^ {3} - x ^ {2} + x ^ {1} .

Not formalized. none; no complete checked declaration under strict bundle semantics — This is an explicit flow/integral-curve example rather than a generic interface. No checked declaration packages the complete example and its maximality/nonextendability conclusions; rebuilding it from Euclidean ODE calculus would be new proof work. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 9.9

FC08-C09-U015 · Ch. 9, § The Fundamental Theorem on Flows; source L6103 · not formalized

Let $M = \mathbb{R}^{2} \setminus \{0\}$ with standard coordinates $(x,y)$ and let $V = \partial/\partial x$ on $M$. The unique integral curve of $V$ starting at $(-1,0) \in M$ is $\gamma(t) = (t-1,0)$. Composing with the inclusion $M \hookrightarrow \mathbb{R}^{2}$ shows $\gamma(t) \to (0,0)$ as $t \nearrow 1$; since limits in $\mathbb{R}^{2}$ are unique, this is a contradiction.

Example 9.10

FC08-C09-U016 · Ch. 9, § The Fundamental Theorem on Flows; source L6105 · not formalized

Let $M = \mathbb{R}^{2}$ and $W = x^{2}\,\partial/\partial x$. The unique integral curve of $W$ starting at $(1,0)$ is $\gamma(t) = \left(\frac{1}{1-t},\, 0\right)$, which cannot be extended past $t = 1$ because its $x$-coordinate is unbounded as $t \nearrow 1$.

Definition/convention — flow domain for M

FC08-C09-U017 · Ch. 9, § The Fundamental Theorem on Flows; source L6113 · not formalized

A flow domain for a manifold $M$ is an open subset $\mathcal{D} \subseteq \mathbb{R} \times M$ such that for each $p \in M$ the set $\mathcal{D}^{(p)} = \{t \in \mathbb{R} : (t,p) \in \mathcal{D}\}$ is an open interval containing $0$. A flow on $M$ is a continuous map $\theta \colon \mathcal{D} \to M$, with $\mathcal{D}$ a flow domain, satisfying the group laws \[ \theta(0,p) = p \tag{9.6} \] for all $p \in M$, and \[ \theta(t,\theta(s,p)) = \theta(t+s,p) \tag{9.7} \] for all $s \in \mathcal{D}^{(p)}$ and $t \in \mathcal{D}^{(\theta(s,p))}$ with $s + t \in \mathcal{D}^{(p)}$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned and current Mathlib have only global Flow and no local/partial-flow structure with an open flow domain and time-slice domains. The canonical source extraction for this row is also truncated, so Sweep II does not reconstruct the missing source formula from the book. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — source terminology/construction

FC08-C09-U018 · Ch. 9, § The Fundamental Theorem on Flows; source L6130 · not formalized

If θ is a flow, we define θ _t ( p ) = θ ^( p ) ( t ) = θ ( t , p ) whenever ( t , p ) ∈ D , just as for a global flow. For each t ∈ ℝ , we also define \[ M_{t} = \{p \in M : (t,p) \in \mathcal{D}\}, \tag{9.8} \] the domain of $\theta_{t}$.

Definition/convention — source terminology/construction

FC08-C09-U019 · Ch. 9, § The Fundamental Theorem on Flows; source L6142 · not formalized

If is smooth, the infinitesimal generator of $\pmb \theta$ is defined by $V _ { p } = \theta ^ { ( p ) \prime } ( 0 )$

Not formalized. none; no complete checked declaration under strict bundle semantics — Lee’s local-flow infinitesimal-generator construction requires both a partial-flow domain and tangent-valued differentiation. P/H have no local-flow object, and the available tangent calculus is the unbridged standard TangentSpace model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 9.11

FC08-C09-U020 · Ch. 9, § The Fundamental Theorem on Flows; source L6144 · not formalized

Proposition 9.11. If $\theta \colon { \mathcal { D } } M$ is a smooth flow, then the infinitesimal generator $V \ o f \theta$ is a smooth vector field, and each curve $\theta ^ { ( p ) }$ is an integral curve of $V$.

Definition/convention — maximal integral curve

FC08-C09-U021 · Ch. 9, § The Fundamental Theorem on Flows; source L6148 · not formalized

The next theorem is the main result of this section. A maximal integral curve is one that cannot be extended to an integral curve on any larger open interval, and a maximal flow is a flow that admits no extension to a flow on a larger flow domain.

Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned/current local maximal-flow object or fundamental theorem packages Lee’s maximal flow, maximal integral curves, translated time domains, and partial-time diffeomorphisms. Mathlib’s manifold integral-curve files prove local existence/uniqueness and a uniform-time global-existence lemma only, all in the standard tangent model; Dynamics.Flow is global rather than partial. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 9.12

FC08-C09-U022 · Ch. 9, § The Fundamental Theorem on Flows; source L6150 · not formalized

Theorem 9.12 (Fundamental Theorem on Flows). Let V be a smooth vector field on a smooth manifold M . There is a unique smooth maximal flow $\theta \colon { \mathcal { D } } M$ whose infinitesimal generator is V . This flow has the following properties: (a) For each $p \in M ,$ ; the curve $\boldsymbol { \theta ^ { ( p ) } } \colon \mathcal { D } ^ { ( p ) } \to M$ is the unique maximal integral curve of V starting at p. (b) $I f s \in \mathcal { D } ^ { ( p ) }$ , then $\bar { \mathcal { D } } ^ { ( \theta ( s , p ) ) }$ is the interval ${ \mathcal { D } } ^ { ( p ) } - s = \left\{ t - s : t \in { \mathcal { D } } ^ { ( p ) } \right\}$ (c) For each $t \in \mathbb { R }$ , the set $M _ { t }$ is open in M; and $\theta _ { t } \colon M _ { t } \to M _ { - t }$ is a diffeomorphism with inverse $\theta _ { - t } .$ Proof. Proposition 9.2 shows that there exists an integral curve starting at each point $p \in M$ . Suppose $\gamma , \widetilde { \gamma } \colon J \to M$

Definition/convention — flow generated by V

FC08-C09-U023 · Ch. 9, § The Fundamental Theorem on Flows; source L6185 · not formalized

The flow whose existence and uniqueness are asserted in the fundamental theorem is called the flow generated by V , or just the flow of V . The term “infinitesimal generator” comes from the following picture: in a smooth chart, a good approximation to an integral curve can be obtained by composing many small straight-line motions, with the direction and length of each motion determined by the value of the vector field at the point arrived at in the previous step. Intuitively, one can think of a flow as a sequence of infinitely many infinitesimally small linear steps.

Proposition 9.13

FC08-C09-U024 · Ch. 9, § The Fundamental Theorem on Flows; source L6189 · not formalized

Proposition 9.13 (Naturality of Flows). Suppose M and N are smooth manifolds, $F \colon M \to N$ is a smooth map, $X \in { \mathfrak { X } } ( M )$ , and $Y \in { \mathfrak { X } } ( N )$ . Let be the flow of X and the flow of Y . If X and Y are F -related, then for each $t \in \mathbb { R } , F ( M _ { t } ) \subseteq N _ { t }$ and $\eta _ { t } \circ F = F \circ \theta _ { t }$ on $M _ { t }$ : \[ \begin{array}{c} M _ {t} \xrightarrow {F} N _ {t} \\ \theta_ {t} \Big \downarrow \qquad \qquad \qquad \qquad \Big \downarrow \eta_ {t} \\ M _ {- t} \xrightarrow {F} N _ {- t}. \end{array} \]

Corollary 9.14

FC08-C09-U025 · Ch. 9, § The Fundamental Theorem on Flows; source L6211 · not formalized

Corollary 9.14 (Diffeomorphism Invariance of Flows). Let $F \colon M \to N$ be a diffeomorphism. If $X \in { \mathfrak { X } } ( M )$ and is the flow of X, then the flow of $F _ { * } X \ i s$ $\eta _ { t } = F \circ \theta _ { t } \circ F ^ { - 1 }$ , with domain $N _ { t } = F ( M _ { t } )$ for each $t \in \mathbb { R }$

Definition/convention — smooth vector field

FC08-C09-U026 · Ch. 9, § Complete Vector Fields; source L6215 · after FC08-C09-U014 · not formalized

Complete Vector Fields As we observed earlier in this chapter, not every smooth vector field generates a global flow. The ones that do are important enough to deserve a name. We say that a smooth vector field is complete if it generates a global flow, or equivalently if each of its maximal integral curves is defined for all t R. For example, both of the vector fields on the plane whose flows we computed in Example 9.8 are complete, whereas those of Examples 9.9

Not formalized. none; no complete checked declaration under strict bundle semantics — Lee’s completeness predicate is defined via the generated maximal local flow / maximal integral curves. P/H expose neither a local maximal-flow object nor a completeness predicate for manifold vector fields; standard-tangent integral-curve existence alone is not an equivalent interface. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Lemma 9.15

FC08-C09-U027 · Ch. 9, § Complete Vector Fields; source L6221 · not formalized

Lemma 9.15 (Uniform Time Lemma). Let V be a smooth vector field on a smooth manifold M; and let be its flow. Suppose there is a positive number ” such that for every $p \in M$ ; the domain of $\overset { \cdot } { \theta } ^ { ( p ) }$ contains $( - \varepsilon , \varepsilon )$ . Then V is complete.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean::exists_isMIntegralCurve_of_isMIntegralCurveOn is a very close standard-tangent analogue of the uniform-time lemma, but it talks about existence of global integral curves rather than Lee’s maximal-flow completeness predicate and still crosses the unbridged C03 tangent model. It therefore does not own the whole row. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 9.16

FC08-C09-U028 · Ch. 9, § Complete Vector Fields; source L6231 · not formalized

Theorem 9.16. Every compactly supported smooth vector field on a smooth manifold is complete.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H searches found no theorem giving Lee’s compact-support, compact-manifold, left-invariant completeness results or escape lemma. The available manifold integral-curve theory supplies local uniqueness/uniform-time ingredients in the standard tangent model, not these complete source theorems. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Corollary 9.17

FC08-C09-U029 · Ch. 9, § Complete Vector Fields; source L6235 · not formalized

On a compact smooth manifold, every smooth vector field is complete.

Theorem 9.18

FC08-C09-U030 · Ch. 9, § Complete Vector Fields; source L6239 · not formalized

Theorem 9.18. Every left-invariant vector field on a Lie group is complete.

Lemma 9.19

FC08-C09-U031 · Ch. 9, § Complete Vector Fields; source L6250 · not formalized

Lemma 9.19 (Escape Lemma). Suppose M is a smooth manifold and $V \in { \mathfrak { X } } ( M )$ $I f \gamma \colon J \to M$ is a maximal integral curve of V whose domain J has a finite leas upper bound b, then for any $t _ { 0 } \in J , \gamma \big ( [ t _ { 0 } , b ) \big )$ is not contained in any compact subset of $M$.

Theorem 9.20

FC08-C09-U032 · Ch. 9, § Flowouts; source L6258 · not formalized

(Flowout Theorem). Suppose $M$ is a smooth manifold, $S \subseteq M$ is an embedded $k$-dimensional submanifold, and $V \in \mathfrak{X}(M)$ is a smooth vector field nowhere tangent to $S$. Let $\theta \colon \mathcal{D} \to M$ be the flow of $V$, let $\mathcal{O} = (\mathbb{R} \times S) \cap \mathcal{D}$ and let $\Phi = \theta|_{\mathcal{O}}$. (a) $\Phi \colon \mathcal{O} \to M$ is an immersion. (b) $\partial/\partial t \in \mathfrak{X}(\mathcal{O})$ is $\Phi$-related to $V$. (c) There is a smooth positive function $\delta \colon S \to \mathbb{R}$ such that the restriction of $\Phi$ to \[ \mathcal{O}_{\delta} = \{(t,p) \in \mathcal{O} : |t| < \delta(p)\} \tag{9.9} \] is injective; thus $\Phi(\mathcal{O}_{\delta})$ is an immersed submanifold of $M$ containing $S$, and $V$ is tangent to it. (d) If $S$ has codimension $1$, then $\Phi|_{\mathcal{O}_{\delta}}$ is a diffeomorphism onto an open submanifold of $M$.

Not formalized. none; no complete checked declaration under strict bundle semantics — The flowout theorem requires the missing local-flow/fundamental-flow package and the general embedded/immersed submanifold layer already absent in C05. No checked whole-row flowout construction or named flowout object exists at P/H. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — flowout

FC08-C09-U033 · Ch. 9, § Flowouts; source L6274 · not formalized

The submanifold $\Phi(\mathcal{O}_{\delta}) \subseteq M$ is called a flowout from $S$ along $V$.

Definition/convention — a singular point of V

FC08-C09-U034 · Ch. 9, § Regular Points and Singular Points; source L6344 · not formalized

Points If V is a vector field on M; a point $p \in M$ is said to be a singular point of V if $V _ { p } = 0 $ , and a regular point otherwise. The next proposition shows that the integral curves starting at regular and singular points behave very differently from each other.

Not formalized. none; no complete checked declaration under strict bundle semantics — The equation V_p = 0 is expressible for Mathlib standard-tangent vector fields, but Lee’s vector fields use his derivation-defined tangent spaces. With no checked tangent-model equivalence, the source-facing singular/regular-point definition is not promoted from the raw zero predicate. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Proposition 9.21

FC08-C09-U035 · Ch. 9, § Regular Points and Singular Points; source L6346 · not formalized

Proposition 9.21. Let V be a smooth vector field on a smooth manifold M; and let $\theta \colon { \mathcal { D } } M$ be the flow generated by V . If $p \in M$ is a singular point of V , then $\mathcal { D } ^ { ( p ) } = \mathbb { R }$ and $\theta ^ { ( p ) }$ is the constant curve $\theta ^ { ( p ) } ( t ) \equiv p , I f$ p is a regular point, then $\boldsymbol { \theta ^ { ( p ) } } \colon \mathcal { D } ^ { ( p ) } \to M$ is a smooth immersion. Proof. If $V _ { p } = 0$ , then the constant curve $\gamma \colon \mathbb { R } \to M$ given by $\gamma ( t ) \equiv p$ is clearly an integral curve of $V$ starting at $p$.

Not formalized. none; no complete checked declaration under strict bundle semantics — This theorem depends on Lee’s maximal partial flow and derivation-model integral curves. P/H lack the local-flow object, and the standard-tangent integral-curve API is not bridged to the source tangent model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — equilibrium point of θ

FC08-C09-U036 · Ch. 9, § Regular Points and Singular Points; source L6358 · after FC08-C09-U035 · not formalized

If $\theta \colon \mathcal{D} \to M$ is a flow, a point $p \in M$ is an equilibrium point of $\theta$ if $\theta(t,p) = p$ for all $t \in \mathcal{D}^{(p)}$. Proposition 9.21 shows that the equilibrium points of a smooth flow are exactly the singular points of its infinitesimal generator.

Not formalized. none; no complete checked declaration under strict bundle semantics — AddAction.fixedPoints exactly captures equilibria for a global action, but Lee’s θ : D → M here is the preceding local/partial flow. P/H have no partial-flow action/fixed-point interface, so using global fixed points would cover only a proper special case. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 9.22

FC08-C09-U037 · Ch. 9, § Regular Points and Singular Points; source L6362 · not formalized

Theorem 9.22 (Canonical Form Near a Regular Point). Let V be a smooth vector field on a smooth manifold M; and let $p \in M$ be a regular point of V . There exist smooth coordinates $\left( s ^ { i } \right)$ on some neighborhood of p in which V has the coordinate representation $\partial / \dot { \partial } s ^ { \dot { 1 } } . I f S \subseteq M$ is any embedded hypersurface with $p \in S$ and $V _ { p } \notin T _ { p } S$ , then the coordinates can also be chosen so that $s ^ { 1 }$ is a local defining function also cannot be extended past $t = 1$ , because its x-coordinate is unbounded as $t \nearrow 1$ // For this reason, we make the following definitions.

Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned/current flow-box/canonical-form theorem or packaged polar-coordinate example matches this row. Standard-tangent local-frame/bracket/ODE ingredients do not assemble to the source theorem without substantial new proof and cross the C03 tangent boundary. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 9.23

FC08-C09-U038 · Ch. 9, § Regular Points and Singular Points; source L6381 · after FC08-C09-U014 · not formalized

Let $W = x\,\partial/\partial y - y\,\partial/\partial x$ on $\mathbb{R}^{2}$, whose flow was computed in Example 9.8(b). Define $\Psi \colon \mathbb{R}^{2} \to \mathbb{R}^{2}$ by $\Psi(t,s) = \theta_{t}(s,0) = (s\cos t,\ s\sin t)$ and solve locally for $(t,s)$ in terms of $(x,y)$ to obtain the coordinate map near $(1,0)$ \[ (t,s) = \Psi^{-1}(x,y) = \left(\tan^{-1}(y/x),\ \sqrt{x^{2}+y^{2}}\right). \tag{9.13} \] In these coordinates $W = \partial/\partial t$; they are polar coordinates under other names.

Theorem 9.24

FC08-C09-U039 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6406 · not formalized

Theorem 9.24 (Boundary Flowout Theorem). Let M be a smooth manifold with nonempty boundary, and let N be a smooth vector field on M that is inwardpointing at each point of @M . There exist a smooth function $\delta \colon \partial M \to \mathbb { R } ^ { + }$ and a smooth embedding $\Phi \colon { \mathcal { P } } _ { \delta } \to M$ ; where $\mathcal { P } _ { \delta } = \{ ( t , p ) : p \in \partial M , 0 \leq t < \delta ( p ) \} \subseteq$ $\mathbb { R } \times \partial M$ ; such that $\varPhi ( \mathcal { P } _ { \delta } )$ is a neighborhood of @M; and for each $p \in \partial M$ the map $t \mapsto \varPhi ( t , p )$

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have no formal collar-neighborhood construction or collar-neighborhood theorem; Bordism.lean only mentions the theorem in prose. The boundary flowout theorem additionally requires local flows and tangent-to-boundary/inward-pointing vector-field infrastructure in Lee’s unbridged tangent model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — collar neighborhood

FC08-C09-U040 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6410 · not formalized

Let M be a smooth manifold with boundary. A neighborhood of @M is called a collar neighborhood if it is the image of a smooth embedding $[ 0 , 1 ) \times \partial M \to M$ that restricts to the obvious identification $\{ 0 \} \times \partial M \to \partial M$ . (See Fig. 9.9.)

Theorem 9.25

FC08-C09-U041 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6412 · not formalized

9.9.) Theorem 9.25 (Collar Neighborhood Theorem). If M is a smooth manifold with nonempty boundary, then @M has a collar neighborhood.

Theorem 9.26

FC08-C09-U042 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6418 · not formalized

Theorem 9.26. Let M be a smooth manifold with nonempty boundary, and let Int $M \hookrightarrow M$ denote inclusion. There exists a proper smooth embedding $R \colon M \to$ Int M such that both R $M \to M$ and $R \circ \iota \colon$ Int $M $ Int M are smoothly homotopic to identity maps. Therefore, is a homotopy equivalence.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted searches found no smooth boundary retraction-to-interior theorem or the two Whitney-approximation/smooth-homotopy theorems in this generality. Existing Euclidean/manifold approximation results do not own these complete boundary-manifold statements. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 9.27

FC08-C09-U043 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6438 · not formalized

Theorem 9.27 (Whitney Approximation for Manifolds with Boundary). If M and N are smooth manifolds with boundary, then every continuous map from M to N is homotopic to a smooth map. F

Theorem 9.28

FC08-C09-U044 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6447 · not formalized

Theorem 9.28. Suppose M and N are smooth manifolds with or without boundary. $I f F , G \colon M \to N$ are homotopic smooth maps, then they are smoothly homotop _ {t} (p), & p U _ {1}, 0 t < t _ {1}, \ _ {t - t _ {1}} _ {t _ {1}} (p), & p U _ {1}, t _ {1} - < t < t _ {1} + .

Theorem 9.29

FC08-C09-U045 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6453 · not formalized

Theorem 9.29 (Attaching Smooth Manifolds Along Their Boundaries). Let M and N be smooth n-manifolds with nonempty boundaries, and suppose $h \colon \partial N \to$ @M is a diffeomorphism $( F i g . 9 . 1 0 )$ . Let $M \cup _ { h } N$ be the adjunction space formed by identifying each $x \in \partial N$ with $h ( x ) \in \partial M$ . Then M $\cup _ { h }$ N is a topological manifold (without boundary), and has a smooth structure such that there are regular domains $M ^ { \prime } , N ^ { \prime } \subseteq M \cup _ { h }$ N diffeomorphic to M and N , respectively, and satisfying \[ M ^ {\prime} \cup N ^ {\prime} = M \cup_ {h} N, \qquad M ^ {\prime} \cap N ^ {\prime} = \partial M ^ {\prime} = \partial N ^ {\prime}.\tag{9.14} \] If M and N are both compact, then M $\cup _ { h }$ N is compact, and if they are both connected, then M $\cup _ { h } N$ is co fundamental theorem is called the flow generated by V , or just the flow of V .

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked declaration constructs the smooth adjunction of manifolds along diffeomorphic boundaries, connected sums via that attachment, or the double with Lee’s stated regular-domain properties. Generic quotient/adjunction topology would require a substantial new smooth-structure proof. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 9.31

FC08-C09-U046 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6487 · not formalized

Example 9.31 (Connected Sums). Let $M _ { 1 } , M _ { 2 }$ be connected smooth manifolds of dimension n. For $i = 1 , 2$ , let $U _ { i }$ be a regular coordinate ball centered at some point $p _ { i } \in M _ { i }$ , and let $M _ { i } ^ { \prime } = M _ { i } \setminus U _ { i } ~ ( \mathrm { F i g . ~ 9 . 1 1 } )$ . Problem 5-8 shows that each $M _ { i } ^ { \prime }$ is a smooth manifold with boundary whose boundary is diffeomorphic to $\mathbb { S } ^ { n - 1 }$ A smooth connected sum of $M _ { 1 }$ and $M _ { 2 }$ , denoted by $M _ { 1 } \# M _ { 2 }$ , is a smooth manifold formed by choosing a diffeomorphism from $\partial M _ { 1 }$ to $\partial M _ { 2 }$ and attaching $M _ { 1 } ^ { \prime }$ and $M _ { 2 } ^ { \prime }$ along their boun nded below.) Let $b =$ sup $\mathcal { D } ^ { \left( p \right) }$ , let $t _ { 0 }$ be a positive number such that $b - \varepsilon < t _ { 0 } < b$ , and let $q = \theta ^ { ( p ) } ( t _ { 0 } )$ The hypothesis implies that $\theta ^ { ( q ) } ( t )$ is defined at least for $t \in ( - \varepsilon , \varepsilon )$ .

Example 9.32

FC08-C09-U047 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6494 · not formalized

Example 9.32 (The Double of a Smooth Manifold with Boundary). Let M be a smooth manifold with boundary. The double of M is the manifold $D ( M ) =$ $M \cup _ { \mathrm { I d } } M$ , where Id $\partial M \to \partial M$ is the identity map of $\partial M ;$ ; it is obtained from M M by identifying each boundary point in one copy of M with the same boundary point in the other. It is a smooth manifold without boundary, and contains two regular domains diffeomorphic to M . It is easy to check that $D ( M )$ is compact if and only if M is compact, and connected if and only if M is connected. (It is useful to extend the definition to manifolds without boundary by defining $D ( M ) = M$ M when $\partial M = \emptyset .$ 1

Lemma 9.33

FC08-C09-U048 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6498 · not formalized

Lemma 9.33. Suppose M is a smooth manifold and $D \subseteq M$ is a regular domain. If V is a smooth vector field on M that is tangent to @D, then every integral curve of V that starts in D remains in D as long as it is defined.

Not formalized. none; no complete checked declaration under strict bundle semantics — These boundary-flow statements require the missing partial/maximal-flow package, general regular-domain/submanifold boundary infrastructure, and tangent-to-boundary vector fields. No P/H theorem packages Lee’s invariant-domain lemma, boundary fundamental flow theorem, or boundary flow-box normal form. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 9.34

FC08-C09-U049 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6504 · after FC08-C09-U022 · not formalized

(Flows on Manifolds with Boundary). The conclusions of Theorem 9.12 remain true if M is a smooth manifold with boundary and V is a smooth vector field on M that is tangent to @M .

Theorem 9.35

FC08-C09-U050 · Ch. 9, § Flows and Flowouts on Manifolds with Boundary; source L6510 · not formalized

Theorem 9.35 (Canonical Form Near a Regular Point on the Boundary). Let M be a smooth manifold with boundary and let V be a smooth vector field on M that is tangent to @M . If $p \in \partial M$ is a regular point of V , there exist smooth boundary coordinates $\left( s ^ { i } \right)$ on some neighborhood of p in which V has the coordinate representation $\partial / \dot { \partial } s ^ { 1 }$ Proof. Problem 9-15. ## Lie Derivatives We know how to make sense of directional derivatives iction of ˚ to $\mathcal { O } _ { \delta }$ is injective, where $\mathcal { O } _ { \delta } \subseteq \mathcal { O }$ is the flow domain \[ \mathcal {O} _ {\delta} = \bigl \{(t, p) \in \mathcal {O}: | t | < \delta (p) \bigr \}.\tag{9.9} \] Thus, $\varPhi ( \mathcal { O } _ { \delta } )$ is an immersed submanifold of M containing S, and V is tangent to this submanifold.

Definition/convention — Lie derivative of W

FC08-C09-U051 · Ch. 9, § Lie Derivatives; source L6535 · not formalized

This problem can be circumvented if we replace the vector $v \in T _ { p } M$ with a vector field $V \in { \mathfrak { X } } ( M )$ , so we can use the flow of V to push values of W back to p and then differentiate. Thus we make the following definition. Suppose M is a smooth manifold, V is a smooth vector field on $M ,$ ; and is the flow of V . For any smooth vector field W on M; define a rough vector field on M; denoted by $\mathcal { L } _ { V } W$ and called the Lie derivative of W with respect to V , by \[ \begin{array}{l} (\mathcal {L} _ {V} W) _ {p} = \frac {d}{d t} \bigg | _ {t = 0} d (\theta_ {- t}) _ {\theta_ {t} (p)} \big (W _ {\theta_ {t} (p)} \big) \\ = \lim _ {t \to 0} \frac {d (\theta_ {- t}) _ {\theta_ {t} (p)} \big (W _ {\theta_ {t} (p)} \big) - W _ {p}}{t}, \end{array}\tag{9.16} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib has VectorField.mlieBracket and its naturality/product/Jacobi laws, but no Lie-derivative-via-flow construction for manifold vector fields. Defining the Lie derivative as the bracket would use Lee’s theorem U053 backwards rather than formalize his flow definition, and the standard-tangent bracket itself remains unbridged from Lee’s derivation tangent model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Lemma 9.36

FC08-C09-U052 · Ch. 9, § Lie Derivatives; source L6545 · not formalized

Suppose $M$ is a smooth manifold with or without boundary and $V, W \in \mathfrak{X}(M)$. If $\partial M \neq \emptyset$, assume in addition that $V$ is tangent to $\partial M$. Then $(\mathcal{L}_{V}W)_{p}$ exists for every $p \in M$, and $\mathcal{L}_{V}W$ is a smooth vector field.

Theorem 9.38

FC08-C09-U053 · Ch. 9, § Lie Derivatives; source L6568 · not formalized

If $M$ is a smooth manifold and $V, W \in \mathfrak{X}(M)$, then $\mathcal{L}_{V}W = [V,W]$.

Definition/convention — source terminology/construction

FC08-C09-U054 · Ch. 9, § Lie Derivatives; source L6590 · not formalized

other hand, $[ V , W ] _ { p } = 0$ by formula (8.8). This theorem allows us to extend the definition of the Lie derivative to arbitrary smooth vector fields on a smooth manifold M with boundary. Given V; $W \in { \mathfrak { X } } ( M )$ we define $( { \mathcal { L } } _ { V } W ) _ { p }$ for $p \in \partial M$ by embedding M in a smooth manifold $\widetilde { M }$ without boundary (such as the double of $M )$ , extending V and $W$ to smooth vector fields on $\widetilde { M }$ , and computing the Lie derivative there. By virtue of the preceding theorem, $( { \mathcal { L } } _ { V } W ) _ { p } = [ X , Y ] _ { p }$ is i

Corollary 9.39

FC08-C09-U055 · Ch. 9, § Lie Derivatives; source L6594 · not formalized

Corollary 9.39. Suppose M is a smooth manifold with or without boundary, and $V , W , X \in { \mathfrak { X } } ( M )$ (a) ${ \mathcal { L } } _ { V } W = - { \mathcal { L } } _ { W } V .$ (b) $\operatorname { \mathcal { L } } _ { V } [ W , X ] = [ \mathcal { L } _ { V } W , X ] + [ W , \mathcal { L } _ { V } X ] .$ (c) $\mathcal { L } _ { [ V , W ] } X = \mathcal { L } _ { V } \mathcal { L } _ { W } X - \mathcal { L } _ { W } \mathcal { L } _ { V } X .$ (d) $I f g \in C ^ { \infty } ( M )$ , then $\mathcal { L } _ { V } ( g W ) = ( V g ) W + g \mathcal { L } _ { V } W$ (e) If $F \colon M \to N$ is a diffeomorphism, then $F _ { * } ( \mathcal { L } _ { V } X ) = \mathcal { L } _ { F _ { * } V } F _ { * } X .$

Proposition 9.41

FC08-C09-U056 · Ch. 9, § Lie Derivatives; source L6612 · not formalized

Theorem 9.42 below. Proposition 9.41. Suppose M is a smooth manifold without boundary and $V , W \in \mathfrak { X } ( M ) . I f \partial M \not = \emptyset$ assume also that V is tangent to @M . Let be the flow of V . For 0 } , p )$ in the domain of , \[ \left. \frac {d}{d t} \right| _ {t = t _ {0}} d (\theta_ {- t}) _ {\theta_ {t} (p)} \left(W _ {\theta_ {t} (p)}\right) = d \left(\theta_ {- t _ {0}}\right) \left((\mathcal {L} _ {V} W) _ {\theta_ {t _ {0}} (p)}\right).\tag{9.17} \] Proof. Let $

Definition/convention — invariant under

FC08-C09-U057 · Ch. 9, § Commuting Vector Fields; source L6628 · not formalized

to the right-hand side of (9.17). ## Commuting Vector Fields Let M be a smooth manifold and V; $W \in { \mathfrak { X } } ( M )$ We say that V and W commute if $V W f = W V f$ for every smooth function $f$ , or equivalently if $[ V , W ] \equiv 0$ . If is a smooth flow, a vector field W is said to be invariant under if W is $\theta _ { t }$ -related to itself for each t ; more precisely, this means that $W | _ { M _ { t } }$ is t -related to $W | _ { M _ { - t } }$ for each t, or equivalently that $d ( \theta _ { t } ) _ { p } ( W _ { p } ) = W _ { \theta _ { t } ( p ) }$ for all $( t , p )$ in the domain of $\theta .$ The next proposition shows that these two concepts are intimately re lve locally for .t; s/ in terms of $( x , y )$ to obtain the following coordinate map in a neighborhood of .1; 0/: \[ (t, s) = \Psi^ {- 1} (x, y) = \left(\tan^ {- 1} (y / x), \sqrt {x ^ {2} + y ^ {2}}\right).\tag{9.13} \] It is easy to check that $W = \partial / \partial t$ in these coordinates.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has flow invariance for sets and standard-tangent Lie brackets separately, but no predicate saying a manifold vector field is invariant under a (local) flow and no theorem equating that invariance with vanishing bracket/commutation. The local-flow layer is absent and the bracket lives in the unbridged tangent model. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 9.42

FC08-C09-U058 · Ch. 9, § Commuting Vector Fields; source L6630 · not formalized

Theorem 9.42. For smooth vector fields V and W on a smooth manifold M; the following are equivalent: ## (a) V and W 9.41 ## (b) W is invariant under the flow of V . (c) V is invariant under the flow ed, just polar coordinates with different names.) // Fig.

Corollary 9.43

FC08-C09-U059 · Ch. 9, § Commuting Vector Fields; source L6643 · not formalized

Every smooth vector field is invariant under its own flow.

Definition/convention — source terminology/construction

FC08-C09-U060 · Ch. 9, § Commuting Vector Fields; source L6649 · not formalized

Thus we make the following definition. If and are flows on M; we say that and commute if the following condition holds for every $p \in M$ : whenever J and K are open intervals containing 0 such that one of the expressions $\theta _ { t } \circ \psi _ { s } ( p )$ or $\psi _ { s } \circ \theta _ { t } ( p )$ is defined for all $( s , t ) \in J \times K$ , both are defined and they are equal. For global flows, this is the same as saying that $\theta _ { t } \circ \psi _ { s } = \psi _ { s } \circ \theta _ { t }$ for all s and t . ##

Not formalized. none; no complete checked declaration under strict bundle semantics — For global flows one can state pointwise commutation using generic function equality/Function.Commute, but Lee defines commutation for local partial flows and then proves equivalence with commuting vector fields. P/H have no local-flow object or corresponding commuting-flow theorem, so the global special case is insufficient. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 9.44

FC08-C09-U061 · Ch. 9, § Commuting Vector Fields; source L6651 · not formalized

Theorem 9.44. Smooth vector fields commute if and only if their flows commute.

Definition/convention — commuting frame

FC08-C09-U062 · Ch. 9, § Commuting Frames; source L6689 · not formalized

Suppose M is a smooth n-manifold. Recall that a local frame for M is an n-tuple $( E _ { i } )$ of vector fields defined on an open subset $U \subseteq M$ such that $\left( E _ { i } | _ { p } \right)$ forms a basis for $T _ { p } M$ at each $p \in U$ . A smooth local frame $\left( E _ { i } \right)$ for M is called a commuting frame if $[ E _ { i } , E _ { j } ] = 0$ for all i and j . (Commuting frames are called holonomic frames by s

Not formalized. none; no complete checked declaration under strict bundle semantics — IsLocalFrameOn and VectorField.mlieBracket provide adjacent standard-tangent frame/bracket infrastructure, but no commuting-frame predicate or canonical-coordinate theorem matching Lee’s row. These APIs also remain behind the C03 point-derivation/standard-tangent bridge. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 9.45

FC08-C09-U063 · Ch. 9, § Commuting Frames; source L6691 · not formalized

Example 9.45 (Commuting and Noncommuting Frames). (a) The simplest examples of commuting frames are the coordinate frames. Given any smooth coordinate chart $\left( U , \left( x ^ { i } \right) \right)$ for a smooth manifold M; (8.10) shows that the coordinate frame $\left( { \partial } / { \partial x ^ { i } } \right)$ is a commuting frame. (b) The frame $( E _ { 1 } , E _ { 2 } )$ for $\mathbb { R } ^ { 2 }$ over $\mathbb { R } ^ { 2 } \setminus \{ 0 \}$ defined by (8.3) is not a commuting frame, because a straightforward computation shows that \[ [ E _ {1}, E _ {2} ] = \frac {y}{r ^ {2}} \frac {\partial}{\partial x} - \frac {x}{r ^ {2}} \frac {\partial}{\partial y} \neq 0.\tag{//} \] Because every coordinate frame is a commuting frame, and because Lie brackets are invariantly defined, it follows that a necessary condition for a smooth frame to be expressible as a coordinate frame in some smooth chart is that it be a commuting frame. Thus, the computation above shows that $( E _ { 1 } , E _ { 2 } )$ cannot be expressed as a coordinate frame for $\mathbb { R } ^ { 2 }$ with respect of.

Theorem 9.46

FC08-C09-U064 · Ch. 9, § Commuting Frames; source L6705 · not formalized

Theorem 9.46 (Canonical Form for Commuting Vector Fields). Let M be a smooth n-manifold, and let $( V _ { 1 } , \ldots , V _ { k } )$ be a linearly independent k-tuple of smooth commuting vector fields on an open subset $W \subseteq M$ . For each $p \in W$ , there exists a smooth coordinate chart $\left( U , \left( s ^ { i } \right) \right)$ centered at $p$ such that $V _ { i } = \partial / \partial s ^ { i }$ for $i = 1 , \dots , k . I f S \subseteq W$ is an embedded codimension-k submanifold and p is a point $o f S$ such that $T _ { p } S$ is complementary to the span of $\left( V _ { 1 } | _ { p } , \ldots , V _ { k } | _ { p } \right)$ , then the coordinates can also be chosen such that $S \cap U$ is the slice defined by $s ^ { 1 } = \cdots = s ^ { k } = 0$

Example 9.47

FC08-C09-U065 · Ch. 9, § Commuting Frames; source L6749 · after FC08-C09-U014 · not formalized

Consider the vector fields $V = x\,\frac{\partial}{\partial y} - y\,\frac{\partial}{\partial x}$ and $W = x\,\frac{\partial}{\partial x} + y\,\frac{\partial}{\partial y}$ on $\mathbb{R}^{2}$, for which $[V,W] = 0$. The flow of $V$ is $\theta_{t}(x,y) = (x\cos t - y\sin t,\ x\sin t + y\cos t)$ and the flow of $W$ is $\eta_{t}(x,y) = (e^{t}x,\ e^{t}y)$. Since $k = n = 2$, take $S = \{(1,0)\}$ and define $\Phi \colon \mathbb{R}^{2} \to \mathbb{R}^{2}$ by $\Phi(s,t) = \eta_{t} \circ \theta_{s}(1,0) = (e^{t}\cos s,\ e^{t}\sin s)$. Near $(1,0)$ this inverts explicitly to the coordinate map \[ (s,t) = \left(\tan^{-1}(y/x),\ \log\sqrt{x^{2}+y^{2}}\right). \]

Definition/convention — source terminology/construction

FC08-C09-U066 · Ch. 9, § Time-Dependent Vector Fields; source L6781 · not formalized

All of the systems of differential equations we have encountered so far have been autonomous ones, meaning that when they are written in the form (9.1), the functions $V ^ { i }$ on the right-hand sides do not depend explicitly on the independent variable t (see Appendix D). However, nonautonomous ODEs do arise in manifold theory, so it is worth exploring how the results of this chapter can be extended to cover this case. We will use this theory only in Chapter 22.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s Banach-space ODE files distinguish time-dependent vector fields in prose and APIs, but this source row is a manifold-theory convention contrasting autonomous and nonautonomous systems. No complete source-facing declaration owns that convention. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — time-dependent vector field

FC08-C09-U067 · Ch. 9, § Time-Dependent Vector Fields; source L6783 · not formalized

Let M be a smooth manifold. A time-dependent vector field on M is a continuous map $V \colon J \times M \to T M$ ; where $J \subseteq \mathbb { R }$ is an interval, such that $V ( t , p ) \in T _ { p }$ M for each $( t , p ) \in J \times M$ . This means that for each $t \in J$ , the map $V _ { t } \colon M \to T M$ defined by $V _ { t } ( p ) = V ( t , p )$ is a vector field on M . If V is a time-dependent vector field on M; an integral curve of V is a differentiable curve $\gamma \colon J _ { 0 } M$ ; where $J _ { 0 }$ is an interval contained in J , such that \[ \gamma^ {\prime} (t) = V \bigl (t, \gamma (t) \bigr) \quad \text { for all } t \in J _ {0}. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib/Analysis/ODE/Basic.lean defines time-dependent vector fields and integral curves only on normed vector spaces E; Mathlib’s manifold integral-curve API is autonomous. Lee’s row is a time-dependent tangent field on an arbitrary manifold and again uses the point-derivation tangent model. No whole-row manifold owner exists. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Theorem 9.48

FC08-C09-U068 · Ch. 9, § Time-Dependent Vector Fields; source L6793 · not formalized

Theorem 9.48 (Fundamental Theorem on Time-Dependent Flows). Let M be a smooth manifold, let $J \subseteq \mathbb { R }$ be an open interval, and let V $J \times M \to T M$ be a smooth time-dependent vector field on M . There exist an open subset ${ \mathcal { E } } \subseteq J \times$ $J \times M$ and a smooth map $\psi \colon \mathcal { E } \to M$ called the time-dependent flow of $V$ , with the following properties: (a) For each $t _ { 0 } \in J$ and $p \in M$ ; the set $\mathcal { E } ^ { ( t _ { 0 } , p ) } = \{ t \in J : ( t , t _ { 0 } , p ) \in \mathcal { E } \}$ is an open interval containing $t _ { 0 }$ , and the smooth curve $\psi ^ { ( t _ { 0 } , p ) } \colon \mathcal { E } ^ { ( t _ { 0 } , p ) } \to M$ defined by $\psi ^ { ( t _ { 0 } , p ) } ( t ) = \psi ( t , t _ { 0 } , p )$ is the unique maximal integral curve of V with initial condition $\psi ^ { ( t _ { 0 } , p ) } ( t _ { 0 } ) = p$ (b) $I f t _ { 1 } \in \mathcal { E } ^ { ( t _ { 0 } , p ) }$ and $q = \psi ^ { ( t _ { 0 } , p ) } ( t _ { 1 } )$ , then $\mathcal { E } ^ { ( t _ { 1 } , q ) } = \mathcal { E } ^ { ( t _ { 0 } , p ) }$ and $\psi ^ { ( t _ { 1 } , q ) } = \psi ^ { ( t _ { 0 } , p ) }$ (c) For each $( t _ { 1 } , t _ { 0 } ) \in J \times J$ , the set $M _ { t _ { 1 } , t _ { 0 } } = \{ p \in M : ( t _ { 1 } , t _ { 0 } , p ) \in \mathcal { E } \}$ is open in M; and the map $\psi _ { t _ { 1 } , t _ { 0 } } \colon M _ { t _ { 1 } , t _ { 0 } } \to M$ defined by $\psi _ { t _ { 1 } , t _ { 0 } } ( p ) = \psi ( t _ { 1 } , t _ { 0 } , p )$ is a diffeomorphism from $M _ { t _ { 1 } , t _ { 0 } }$ onto $M _ { t _ { 0 } , t _ { 1 } }$ with inverse $\psi _ { t _ { 0 } , t _ { 1 } }$ (d) If $p \in M _ { t _ { 1 } , t _ { 0 } }$ and $\psi _ { t _ { 1 } , t _ { 0 } } ( p ) \in M _ { t _ { 2 } , t _ { 1 } }$ , then $p \in M _ { t _ { 2 } , t _ { 0 } }$ and \[ \psi_ {t _ {2}, t _ {1}} \circ \psi_ {t _ {1}, t _ {0}} (p) = \psi_ {t _ {2}, t _ {0}} (p).\tag{9.18} \] Proof. This can be proved by following the outline of the proof of Theorem 9.12, using Theorem D.6 in place of Theorem D.1. However, it is much quicker to use the following trick to reduce it to the time-independent case. Consider the smooth vector field ent vectors $W _ { p + t v }$ and $W _ { p }$ can both be viewed as elements of $\mathbb { R } ^ { n }$ .

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has Picard–Lindelöf time-dependent flows on Banach spaces, but no manifold-level time-dependent flow theorem with Lee’s maximal domains, restart property, partial-time diffeomorphisms, and cocycle law. The Banach-space result is a proper specialization, not an owner for the manifold theorem. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 9.50

FC08-C09-U069 · Ch. 9, § Time-Dependent Vector Fields; source L6861 · not formalized

Define a time-dependent vector field $V$ on $\mathbb{R}^{n}$ by \[ V(t,x) = \frac{1}{t}x^{i}\left.\frac{\partial}{\partial x^{i}}\right|_{x}, \qquad (t,x) \in (0,\infty) \times \mathbb{R}^{n}. \] The maximal solution is $x^{i}(t) = tx_{0}^{i}/t_{0}$, defined for all $t > 0$, so the time-dependent flow of $V$ is $\psi(t,t_{0},x) = tx/t_{0}$ for $(t,t_{0},x) \in (0,\infty) \times (0,\infty) \times \mathbb{R}^{n}$.

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked declaration packages Lee’s explicit V(t,x)=x/t time-dependent manifold/vector-space example together with its maximal flow and solution formula. Reconstructing it from generic ODE calculus would be new example proof work. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — source terminology/construction

FC08-C09-U070 · Ch. 9, § First-Order Partial Differential Equations; source L6881 · not formalized

Differential Equations One of the most powerful applications of the theory of flows is to partial differential equations. In its most general form, a partial differential equation (PDE) is any equation that relates an unknown function of two or more variables with its partial derivatives up to some order and with the independent variables. The order of the PDE is the highest-order derivative of the unknown function that appears.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted project/P/H/indexed searches found no first-order PDE/Cauchy-problem/method-of-characteristics formalization matching Lee’s terminology and geometric setup. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — fully nonlinear

FC08-C09-U071 · Ch. 9, § First-Order Partial Differential Equations; source L6883 · not formalized

The number of specialized techniques that have been developed to solve partial differential equations is staggering. (For an introduction to the general theory, you can consult one of the many excellent introductory books on the subject, such as [Eva98, Fol95, Joh91].) However, it is a remarkable fact that real-valued first-order PDEs can be reduced to ordinary differential equations by means of the theory of flows, and thus can be solved using only ODEs and a little differential-geometric insight but no specialized PDE theory. In this section, we describe how this is done for two special classes of first-order equations: first, linear equations; and then, somewhat more generally, quasilinear equations (which we define below). A PDE that is not quasilinear is said to be fully nonlinear; we will show how to treat fully nonlinear first-order equations in Chapter 22.

Definition/convention — Cauchy problem

FC08-C09-U072 · Ch. 9, § First-Order Partial Differential Equations; source L6899 · not formalized

The problem of finding a solution to (9.20) in a neighborhood of S subject to the initial condition (9.21) is called a Cauchy problem.

Definition/convention — source terminology/construction

FC08-C09-U073 · Ch. 9, § Linear Equations; source L6905 · not formalized

The first type of equation we will treat is a first-order linear PDE, which is one that depends linearly or affinely on the unknown function and its derivatives. In coordinate form, the most general such equation can be written \[ a^{1}(x)\frac{\partial u}{\partial x^{1}}(x) + \cdots + a^{n}(x)\frac{\partial u}{\partial x^{n}}(x) + b(x)u(x) = f(x), \tag{9.22} \] with $a^{1},\dots,a^{n}$, $b$ and $f$ given functions.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted project/P/H/indexed searches found no first-order PDE/Cauchy-problem/method-of-characteristics formalization matching Lee’s terminology and geometric setup. The canonical extraction is truncated and was not reconstructed during Sweep II. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Definition/convention — noncharacteristic

FC08-C09-U074 · Ch. 9, § Linear Equations; source L6919 · not formalized

In terms of A , , we can rewrite (9.22) in the simple form A u + b u = f . In this form, it makes sense on any smooth manifold, and is no more difficult to solve in that generality, so we state our first theorem in that context. The Cauchy problem for A u + b u = f with initial hypersurface S is said to be noncharacteristic if A is nowhere tangent to S.

Theorem 9.51

FC08-C09-U075 · Ch. 9, § Linear Equations; source L6921 · not formalized

Theorem 9.51 (The Linear First-Order Cauchy Problem). Let M be a smooth manifold. Suppose we are given an embedded hypersurface $S \subseteq M$ } ( M )$ that is nowhere tangent to $S$ , and functions $ } ( S )$ . Then for some neighborhood U of S in M; there exists a unique solution $ } ( U )$ to the noncharacteristic Cauchy problem \[ A u + b u = f,\tag{9.24} \] \[ u | _ {S} = \varphi .\tag{9.25} \] Proof. The flowout theorem gives us a neighborhood $

Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Lean theorem/example was found for Lee’s linear or quasilinear first-order Cauchy problem and method-of-characteristics construction. Mathlib’s ODE theory does not supply these PDE existence/uniqueness statements as a packaged consequence. Strict whole-row semantics reject proper subsets, unbridged equivalent models, stronger-hypothesis substitutes, isolated ingredients, and reconstruction of the substantive source theorem.

Example 9.52

FC08-C09-U076 · Ch. 9, § Linear Equations; source L6947 · after FC08-C09-U038 · not formalized

Example 9.52 (A Linear Cauchy Problem). Suppose we wish to solve the following Cauchy problem for a smooth function $u ( x , y )$ in the plane: \[ x \frac {\partial u}{\partial y} - y \frac {\partial u}{\partial x} = x,\tag{9.27} \] \[ u (x, 0) = x \quad \text { when } x > 0.\tag{9.28} \] The vector field acting on u on the left-hand side of (9.27) is the vector field W of Example 9.23. The initial hypersurface S is the positive x-axis, and this problem is noncharacteristic because W is nowhere tangent to S. (Notice that this would not be the case if we took S to be the entire x-axis.) Using the computations of Example 9.23, we find that the transformation $( x , y ) = \varPsi ( t , s ) = ( s \cos t , s \sin t )$ pushes $\partial / \partial t$ forward to $W$ , and thus transforms (9.27)–(9.28) to the ODE initial value problem \[ \begin{array}{c} \frac {\partial \widehat {u}}{\partial t} (t, s) = s \cos t, \\ \widehat {u} (0, s) = s. \end{array} \] This is solved by ${ \widehat { u } } ( t , s ) = s \sin t + s$ . Substituting for $( t , s )$ in terms of $( x , y )$ using (9.13), we obtain the solution $u ( x , y ) = y + \sqrt { x ^ { 2 } + y ^ { 2 } }$ to the original problem. ## Quasilinear Equations The preceding results extend easily to certain nonlinear partial differential equations. A PDE is called quasilinear if it can be written as an affine function of the first derivatives of the unknown function.

Definition/convention — quasilinear

FC08-C09-U077 · Ch. 9, § Quasilinear Equations; source L6967 · not formalized

Equations The preceding results extend easily to certain nonlinear partial differential equations. A PDE is called quasilinear if it can be written as an affine equation in the highest-order derivatives of the unknown function, with coefficients that may depend on the function itself and its derivatives of lower order. Thus, in coordinates, a quasilinear first-order PDE is a differential equation of the form \[ a ^ {1} (x, u (x)) \frac {\partial u}{\partial x ^ {1}} + \dots + a ^ {n} (x, u (x)) \frac {\partial u}{\partial x ^ {n}} = f (x, u (x))\tag{9.29} \] for an unknown real-valued function $u ( x ^ { 1 } , \ldots , x ^ { n } )$ , where $a ^ { 1 } , \ldots , a ^ { n }$ and $f$ are smooth real-valued functions defined on some open subset $W \subseteq \mathbb { R } ^ { n + 1 }$ . (For simplicity, this time we concentrate only on the local problem, and restrict our attention to open subsets of Euclidean spa of flow domains, it must be defined for all t in some open interval containing 0 and $t _ { 0 }$ , but the analogous statement need not be true of s—there might be values of $s$ between 0 and $s _ { 0 }$ for which the integral curve of V starting at $\psi _ { s } ( p )$ does not extend all the way to $t = t _ { 0 }$ Thus we make the following definition.

Definition/convention — noncharacteristic

FC08-C09-U078 · Ch. 9, § Quasilinear Equations; source L6975 · not formalized

We wish to solve a Cauchy problem for this equation with initial condition \[ u | _ {S} = \varphi ,\tag{9.30} \] where $S \subseteq \mathbb { R } ^ { n }$ is a smooth, embedded hypersurface, and $\varphi \colon S \mathbb { R }$ is a smooth function whose graph is contained in W . A quasilinear Cauchy problem is said to be noncharacteristic if the vector field $A ^ { \varphi }$ along S defined by \[ \left. A ^ {\varphi} \right| _ {x} = a ^ {1} (x, \varphi (x)) \left. \frac {\partial}{\partial x ^ {1}} \right| _ {x} + \dots + a ^ {n} (x, \varphi (x)) \left. \frac {\partial}{\partial x ^ {n}} \right| _ {x}\tag{9.31} \] is nowhere tangent to $S$ . (Notice that in this case the noncharacteristic condition depends on the initial value $\varphi$ , not just on the initial hypersurface.) We will show that a noncharacteristic Cauchy problem always has local solutions. (As we will see below, finding global solutions can be probl ommute if and only if their flows commute.

Theorem 9.53

FC08-C09-U079 · Ch. 9, § Quasilinear Equations; source L6989 · not formalized

Theorem 9.53 (The Quasilinear Cauchy Problem). If the Cauchy problem (9.29)–(9.30) is noncharacteristic, then for each $p \in S$ there exists a neighborhood U of p in M on which there exists a unique solution u to (9.29)–(9.30).

Example 9.54

FC08-C09-U080 · Ch. 9, § Quasilinear Equations; source L7021 · not formalized

(A Quasilinear Cauchy Problem). Consider \[ (u+1)\frac{\partial u}{\partial x} + \frac{\partial u}{\partial y} = 0, \qquad u(x,0) = x, \] with initial hypersurface the $x$-axis and initial value $\varphi(x,0) = x$. Reparametrizing the graph in terms of $x$ and $y$ means inverting $\pi \circ \psi$, that is solving $(x,y) = (s+t+st,\ t)$ locally for $t$ and $s$, which gives $(t,s) = \left(y,\ \frac{x-y}{1+y}\right)$; so on the flowout manifold $z = s = (x-y)/(1+y)$ and the solution is $u(x,y) = (x-y)/(1+y)$, defined only where $y > -1$, not on the whole plane.

Definition/convention — characteristic curves (

FC08-C09-U081 · Ch. 9, § Quasilinear Equations; source L7049 · after FC08-C09-U076 · not formalized

The integral curves of $\xi$ in $\mathbb { R } ^ { n + 1 }$ are called the characteristic curves (or characteristics) of the PDE (9.29). This solution technique, which boils down to constructing the graph of $u$ as a union of characteristic curves, is called the method $\pmb { o f }$ characteristics. (For linear equations, the term characteristic curves is also sometimes applied to the integral curves of the vector field A defined by (9.23). Of course, the method described above for quasilinear equations can be applied to linear ones as well, but the technique of Example 9.52 is usually easier in the linear s ^ {k + 1}, , s ^ {n}) ).