- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
Given a manifold \(M\) with a tangent distribution \(\mathcal{D} \hookrightarrow TM\) of rank \(r\) (as a vector bundle), a submanifold \(\iota \colon N \hookrightarrow M\) passing through \(x_0 \in M\) is called an integral submanifold of the distribution \(\mathcal{D}\) if it is everywhere tangent to \(\mathcal{D}\), \(T\iota (TN) \subseteq \mathcal{D}\), where naturally \(\dim N \le r\). In the case \(\dim N = r\), the integral submanifold is called maximal (in dimension).
A tangent distribution \(\mathcal{D} \hookrightarrow TM\) is involutive if, for any two vector field sections \(u\), \(v\) of \(\mathcal{D}\), the Lie bracket \([u,v]\) is also a section of \(\mathcal{D}\).
Let \(L_i = \sum _{k=1}^m f_i^k(x) \partial /\partial x^j\), \(i=1,\ldots ,r\le m\), be first order differential operators, such that the vector fields \(v_i(x) = (f_i^k(x))_{k=1}^m\) are linearly independent. They are said to be in involution when there exist functions \(c^k_{ij}(x)\) such that
On a manifold \(M\), given two vector fields \(u\), \(v\) (sections of the tangent bundle \(TM\)), their Lie bracket \(w = [u,v]\) is the vector field that satisfies the identity \(w(f) = u(v(f)) - v(u(f))\), where vector fields act as first order differential operators on a smooth function \(f\). In coordinate form, if \(u = u^i\partial _i\), \(v = v^i\partial _i\), \(w = w^i\partial _i\), then \(w^j = u^i \partial _i v^j - v^i \partial _i u^i\). The vector fields \(u\), \(v\) commute (or are in involution in the sense of Def. 1) if \([u,v] = 0\).
A tangent distribution on a manifold \(M\) is a vector sub-bundle \(\mathcal{D}\hookrightarrow TM\) (equivalently, an embedding of vector bundles).
Consider the operators \(L'_{i'}\) and the split neighborhood \(U\ni x_0\) as in Lem. 5. Let \(Z^k(y,z)\) and \(\bar{Z}^k(y,z)\) satisfy the inversion identity \(\bar{Z}^k(y, Z(y, z)) = z^k\), for all \(z\) on a sufficiently small neighborhood of \(z=0\), and for all \(y\) on a sufficiently small neighborhood of \(y=0\). Suppose that \(Z^j(y,z)\) satisfies (a) \(Z^j(0,z) = z^j\) and (b)
Then
and vice versa.
Let \(Z^j(y,z)\) be as in Lem. 6. Then, \(\zeta ^j(t,y,z) = Z^j(ty,z)\) satisfies \(\zeta ^j(0,y,z) = z^j\) and the equations
Conversely, if \(\zeta ^j(t,y,z)\) satisfies the initial value problem above, then there exists a sufficiently small neighborhood of \((y,z)=(0,0)\) for which \(Z^j(ty,z)\) exists up to at least \(t=1\). Then \(Z^j(y,z) = \zeta ^j(1,y,z)\) satisfies the conditions in the hypotheses of Lem. 6.
An ODE initial value problem (a sufficiently general one to cover the one for \(\zeta ^j(t,y,z)\) in Lem. 7 and the one for \(\eta _{i'}^j(t,y,z)\) in the proof of Lem. 7) (a) has a solution that is jointly smooth in \((t,y,z)\), which (b) is unique, and (c) exists (at least) up to time \(t=1\) on a sufficiently small neighborhood of \((y,z) = (0,0)\).
For the operators \(L_i\) from Def. 1, given \(x_0 \in M\), there exists an open coordinate neighborhood \(U\ni x_0\) such that (a) there an exists invertible \(\alpha _{i'}^i\) as in Lem. 3, (b) there exists a split local chart \((y,z)\colon M \supset U' \cong \mathbb {R}^r \times \mathbb {R}^{m-r}\), with (c) \((y(x_0),z(x_0)) = (0,0)\), (d)
and (e) \([L'_{i'}, L'_{j'}] = 0\), for \(i',j'=1,\ldots ,r\), which expressed in terms of \(f_{i'}^j\) means (f)
If \(\alpha _i\), \(i=1,\ldots k\le m-k\) are 1-forms on \(M\) that generate a closed differential ideal. Then there exist smooth scalar functions \(u_i(x)\), \(i=1,\ldots ,m-k\) such that the exact 1-forms \(du_i\), \(i=1,\ldots ,m-k\) generate the same differential ideal.
If the first order differential operators \(L_i\), \(i=1,\ldots ,r \le m\), are in involution, then there exist \(m-r\) smooth functions \(u^k(x)\) that satisfy the equations \(L_i u^k(x) = 0\) and such that their gradients \(\nabla u^k(x)\), \(k=1,\ldots ,m-r\) are linearly independent.
Let \(\mathcal{D} \subseteq TM\) be an involutive tangent space distribution of rank \(r\le m = \dim M\). Then, for every \(x_0\in M\), there exists a maximal integral submanifold \(\iota \colon \mathbb {R}^n \hookrightarrow M\) of \(\mathcal{D}\) such that \(\iota (0) = x_0\). Moreover, these integral submanifolds collect into a \(r\)-dimensional foliation of \(M\) whose leaves are everywhere tangent to the distribution \(\mathcal{D}\).