Tangent distributions and involutivity

A distribution on a manifold M assigns to every point x a linear subspace D x of the tangent space T_x M. It is a C^n distribution of rank k when near every point it is spanned by k vector fields of class C^n whose values are linearly independent, that is, when it admits C^n local frames. It is involutive when the Lie bracket of two vector fields tangent to D is again tangent to D. Involutivity is the hypothesis of the Frobenius theorem, which is not proved here: on a real manifold modelled on a finite-dimensional space, it makes an involutive smooth distribution the tangent field of a foliation.

The distribution is recorded as the family of subspaces D : Π x, Submodule 𝕜 (TangentSpace I x), while its regularity and involutivity are predicates on that family.

Main definitions

• TauCeti.distributionModelFiber: a tangent-space fibre of a distribution on a normed space, transported to the model vector space.
• TauCeti.IsDistributionFrameOn I n D X U: the vector fields X i form a C^n local frame of D on U.
• TauCeti.IsDistributionFrameOn.extend: the extension of a vector of a fibre of D by a local frame, with constant coefficients.
• TauCeti.IsContMDiffDistribution I n k D: D is a C^n distribution of rank k.
• TauCeti.IsInvolutiveDistribution I D: D is involutive.
• TauCeti.IsInvolutiveDistributionOn I D s: D is involutive on s.
• TauCeti.standardContactDistribution 𝕜: the kernel of dz - x dy on 𝕜³.

Main results

• TauCeti.IsDistributionFrameOn.isSubbundleFrameOn: a C^n local frame of D is a continuous local frame of D as a family of subspaces of the tangent bundle, in the sense of TauCeti.IsSubbundleFrameOn.
• TauCeti.isDistributionFrameOn_top_iff: local frames of the whole tangent bundle, in the sense of IsLocalFrameOn, are the local frames of the distribution ⊤.
• TauCeti.IsContMDiffDistribution.finrank_eq: a distribution of rank k has k-dimensional fibres.
• TauCeti.IsContMDiffDistribution.exists_contMDiffOn_apply_eq: every vector of D x extends to a C^n vector field tangent to D near x.
• TauCeti.isContMDiffDistribution_top and TauCeti.isInvolutiveDistribution_top: the whole tangent bundle is a C^n involutive distribution.
• TauCeti.IsInvolutiveDistribution.isInvolutiveDistributionOn: an involutive distribution is involutive on every set.
• TauCeti.mlieBracket_sum_smul_mem: if vector fields differentiable at x have values and pairwise Lie brackets at x in a subspace D of the tangent space there, then so does the Lie bracket of any two of their combinations with coefficients differentiable at x. This is the computation behind the frame criterion for involutivity.
• TauCeti.isContMDiffDistribution_const and TauCeti.isInvolutiveDistribution_const: a fixed finite-dimensional (respectively closed) subspace S of a normed space E, taken at every point, is a C^n (respectively involutive) distribution on E.
• TauCeti.not_isInvolutiveDistribution_standardContactDistribution: the standard contact distribution is a smooth distribution of rank two that is not involutive.

Implementation notes

Involutivity quantifies over vector fields that are only differentiable on the open set where they are tangent to D: one derivative is all the Lie bracket uses. Every C^n vector field with 1 ≤ n is among them, so an involutive distribution in this sense satisfies the usual condition on smooth local sections.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 19 (distributions, local frames, involutivity, and the Frobenius theorem).
• A. Candel, L. Conlon, Foliations I, AMS GSM 23 (2000), Chapter 1.

noncomputable def TauCeti.distributionModelFiber {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (D : (x : E) → Submodule 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) x)) (p : E) : Submodule 𝕜 E

The fibre of a distribution on a normed space, transported from the tangent space to the model vector space by its canonical identification.

@[simp]

theorem TauCeti.mem_distributionModelFiber {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {D : (x : E) → Submodule 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) x)} {p v : E} : v ∈ distributionModelFiber D p ↔ (NormedSpace.fromTangentSpace p).symm v ∈ D p

Membership in distributionModelFiber, expressed in the original tangent-space fibre.

theorem TauCeti.distributionModelFiber_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {D : (x : E) → Submodule 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) x)} (p : E) : distributionModelFiber D p = D p

On a normed space, transporting a distribution fibre through the canonical tangent-model identification leaves the submodule unchanged.

structure TauCeti.IsDistributionFrameOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (n : WithTop ℕ∞) {ι : Type u_5} (D : (x : M) → Submodule 𝕜 (TangentSpace I x)) (X : ι → (x : M) → TangentSpace I x) (U : Set M) : Prop

The vector fields X i form a C^n local frame of the distribution D on the set U: each X i is C^n on U, and at every point x of U the values X i x form a basis of D x.

• contMDiffOn (i : ι) : ContMDiffOn I I.tangent n (fun (x : M) => ⟨x, X i x⟩) U

  Each member of the frame is a C^n vector field on U.

• linearIndependent {x : M} (hx : x ∈ U) : LinearIndependent 𝕜 fun (x_1 : ι) => X x_1 x

  The values of the frame at a point of U are linearly independent.

• span_eq {x : M} (hx : x ∈ U) : Submodule.span 𝕜 (Set.range fun (x_1 : ι) => X x_1 x) = D x

  The values of the frame at a point of U span the subspace of the distribution there.

theorem TauCeti.IsDistributionFrameOn.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U U' : Set M} (hX : IsDistributionFrameOn I n D X U) (hU : U' ⊆ U) : IsDistributionFrameOn I n D X U'

A local frame of D on U is a local frame of D on every subset of U.

theorem TauCeti.IsDistributionFrameOn.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n m : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} (hX : IsDistributionFrameOn I n D X U) (hmn : m ≤ n) : IsDistributionFrameOn I m D X U

A C^n local frame is a C^m local frame for every m ≤ n.

theorem TauCeti.IsDistributionFrameOn.isSubbundleFrameOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} (hX : IsDistributionFrameOn I n D X U) : IsSubbundleFrameOn E D X U

A C^n local frame of D is a continuous local frame of D, viewed as a family of subspaces of the fibres of the tangent bundle. Its algebraic consequences, such as the basis of each fibre hX.isSubbundleFrameOn.basis, are those of TauCeti.IsSubbundleFrameOn.

theorem TauCeti.IsDistributionFrameOn.contMDiffOn_trivOperator {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} [Fintype ι] [IsManifold I (n + 1) M] (hX : IsDistributionFrameOn I n D X U) (x : M) : ContMDiffOn I (modelWithCornersSelf 𝕜 ((ι → 𝕜) →L[𝕜] E)) n (IsSubbundleFrameOn.trivOperator 𝕜 E X x) (U ∩ (trivializationAt E (TangentSpace I) x).baseSet)

The operator of a C^n distribution frame, read in the tangent-bundle trivialization at x, is C^n where both the frame and the trivialization are defined.

noncomputable def TauCeti.IsDistributionFrameOn.extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} [Fintype ι] (hX : IsDistributionFrameOn I n D X U) {x : M} (hx : x ∈ U) (u : ↥(D x)) (y : M) : TangentSpace I y

The extension of a vector u of D x by a local frame X on a set U containing x: the vector field ∑ i, c i • X i, where the constants c i are the coordinates of u in the basis X · x of D x.

@[simp]

theorem TauCeti.IsDistributionFrameOn.extend_apply_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} [Fintype ι] (hX : IsDistributionFrameOn I n D X U) {x : M} (hx : x ∈ U) (u : ↥(D x)) : hX.extend hx u x = ↑u

The constant-coefficient extension of u by a local frame takes the value u at x.

theorem TauCeti.IsDistributionFrameOn.extend_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} [Fintype ι] (hX : IsDistributionFrameOn I n D X U) {x : M} (hx : x ∈ U) (u : ↥(D x)) {y : M} (hy : y ∈ U) : hX.extend hx u y ∈ D y

The constant-coefficient extension of a vector by a local frame on U is tangent to D on U.

theorem TauCeti.IsDistributionFrameOn.contMDiffOn_extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} [Fintype ι] (hX : IsDistributionFrameOn I n D X U) {x : M} (hx : x ∈ U) (u : ↥(D x)) : ContMDiffOn I I.tangent n (fun (y : M) => ⟨y, hX.extend hx u y⟩) U

The constant-coefficient extension of a vector by a C^n local frame on U is C^n on U.

@[simp]

theorem TauCeti.IsDistributionFrameOn.extend_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} [Fintype ι] (hX : IsDistributionFrameOn I n D X U) {x : M} (hx : x ∈ U) (u u' : ↥(D x)) : hX.extend hx (u + u') = hX.extend hx u + hX.extend hx u'

The constant-coefficient extension by a local frame is additive.

@[simp]

theorem TauCeti.IsDistributionFrameOn.extend_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} [Fintype ι] (hX : IsDistributionFrameOn I n D X U) {x : M} (hx : x ∈ U) (c : 𝕜) (u : ↥(D x)) : hX.extend hx (c • u) = c • hX.extend hx u

The constant-coefficient extension by a local frame commutes with scalar multiplication.

theorem TauCeti.IsDistributionFrameOn.exists_contDiffOn_clm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_6} [NormedAddCommGroup V] [NormedSpace 𝕜 V] {ι : Type u_7} [Fintype ι] {n : WithTop ℕ∞} {D : V → Submodule 𝕜 V} {X : ι → V → V} {U : Set V} (hX : IsDistributionFrameOn (modelWithCornersSelf 𝕜 V) n D X U) : ∃ (Φ : V → (ι → 𝕜) →L[𝕜] V), ContDiffOn 𝕜 n Φ U ∧ ∀ p ∈ U, Function.Injective ⇑(Φ p) ∧ (↑(Φ p)).range = D p

A C^n local frame X of a distribution on a normed space V, on a set U, gives a C^n family of continuous linear maps Φ p : (ι → 𝕜) →L[𝕜] V, namely c ↦ ∑ i, c i • X i p, which on U is injective with range D p.

theorem TauCeti.isDistributionFrameOn_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} {X : ι → (x : M) → TangentSpace I x} {U : Set M} : IsDistributionFrameOn I n (fun (x : M) => ⊤) X U ↔ IsLocalFrameOn I E n X U

The local frames of the distribution ⊤ are exactly the local frames of the tangent bundle.

def TauCeti.IsContMDiffDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (n : WithTop ℕ∞) (k : ℕ) (D : (x : M) → Submodule 𝕜 (TangentSpace I x)) : Prop

D is a C^n distribution of rank k: every point has an open neighbourhood on which D has a C^n local frame of k vector fields.

theorem TauCeti.isContMDiffDistribution_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} : IsContMDiffDistribution I n k D ↔ ∀ (x : M), ∃ (U : Set M), IsOpen U ∧ x ∈ U ∧ ∃ (X : Fin k → (y : M) → TangentSpace I y), IsDistributionFrameOn I n D X U

The defining property of a C^n distribution of rank k.

theorem TauCeti.IsContMDiffDistribution.of_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (h : ∀ (x : M), ∃ U ∈ nhds x, ∃ (X : Fin k → (y : M) → TangentSpace I y), IsDistributionFrameOn I n D X U) : IsContMDiffDistribution I n k D

A distribution has rank k and class C^n as soon as every point has a neighbourhood, not necessarily open, on which it has a C^n local frame of k vector fields.

theorem TauCeti.IsContMDiffDistribution.exists_contMDiffOn_apply_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsContMDiffDistribution I n k D) {x : M} (v : ↥(D x)) : ∃ (U : Set M), IsOpen U ∧ x ∈ U ∧ ∃ (V : (y : M) → TangentSpace I y), ContMDiffOn I I.tangent n (fun (y : M) => ⟨y, V y⟩) U ∧ (∀ y ∈ U, V y ∈ D y) ∧ V x = ↑v

Every vector of D x, for a C^n distribution D, is the value at x of a vector field which is C^n and tangent to D on an open neighbourhood of x.

theorem TauCeti.IsDistributionFrameOn.isContMDiffDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : Fin k → (x : M) → TangentSpace I x} (hX : IsDistributionFrameOn I n D X Set.univ) : IsContMDiffDistribution I n k D

A distribution with a global C^n frame of k vector fields is a C^n distribution of rank k.

theorem TauCeti.IsContMDiffDistribution.finrank_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsContMDiffDistribution I n k D) (x : M) : Module.finrank 𝕜 ↥(D x) = k

A distribution of rank k has k-dimensional subspaces.

theorem TauCeti.IsContMDiffDistribution.of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n m : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsContMDiffDistribution I n k D) (hmn : m ≤ n) : IsContMDiffDistribution I m k D

A C^n distribution is a C^m distribution for every m ≤ n.

theorem TauCeti.isContMDiffDistribution_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} [FiniteDimensional 𝕜 E] [IsManifold I (n + 1) M] : IsContMDiffDistribution I n (Module.finrank 𝕜 E) fun (x : M) => ⊤

On a manifold modelled on a finite-dimensional space, the whole tangent bundle is a C^n distribution whose rank is the dimension. The local frames are those of the trivializations of the tangent bundle.

theorem TauCeti.isContMDiffDistribution_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} (S : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥S] : IsContMDiffDistribution (modelWithCornersSelf 𝕜 E) n (Module.finrank 𝕜 ↥S) fun (x : E) => S

A finite-dimensional subspace S of E, taken at every point of E, is a C^n distribution on E whose rank is the dimension of S. Its local frames are constant.

def TauCeti.IsInvolutiveDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (D : (x : M) → Submodule 𝕜 (TangentSpace I x)) : Prop

D is involutive: whenever two vector fields are differentiable and tangent to D on an open set U, their Lie bracket is tangent to D on U.

def TauCeti.IsInvolutiveDistributionOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (D : (x : M) → Submodule 𝕜 (TangentSpace I x)) (s : Set M) : Prop

D is involutive on s: whenever two vector fields are differentiable and tangent to D on an open subset of s, their Lie bracket is tangent to D there.

theorem TauCeti.isInvolutiveDistribution_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} : IsInvolutiveDistribution I D ↔ ∀ ⦃U : Set M⦄, IsOpen U → ∀ ⦃V W : (x : M) → TangentSpace I x⦄, (MDiff[U] fun (x : M) => ⟨x, V x⟩) → (MDiff[U] fun (x : M) => ⟨x, W x⟩) → (∀ x ∈ U, V x ∈ D x) → (∀ x ∈ U, W x ∈ D x) → ∀ x ∈ U, VectorField.mlieBracket I V W x ∈ D x

The defining property of an involutive distribution.

theorem TauCeti.isInvolutiveDistributionOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {s : Set M} : IsInvolutiveDistributionOn I D s ↔ ∀ ⦃U : Set M⦄, IsOpen U → U ⊆ s → ∀ ⦃V W : (x : M) → TangentSpace I x⦄, (MDiff[U] fun (x : M) => ⟨x, V x⟩) → (MDiff[U] fun (x : M) => ⟨x, W x⟩) → (∀ x ∈ U, V x ∈ D x) → (∀ x ∈ U, W x ∈ D x) → ∀ x ∈ U, VectorField.mlieBracket I V W x ∈ D x

The defining property of a distribution that is involutive on a set.

theorem TauCeti.IsInvolutiveDistribution.mlieBracket_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsInvolutiveDistribution I D) {U : Set M} (hU : IsOpen U) {V W : (x : M) → TangentSpace I x} (hV : MDiff[U] fun (x : M) => ⟨x, V x⟩) (hW : MDiff[U] fun (x : M) => ⟨x, W x⟩) (hVD : ∀ x ∈ U, V x ∈ D x) (hWD : ∀ x ∈ U, W x ∈ D x) {x : M} (hx : x ∈ U) : VectorField.mlieBracket I V W x ∈ D x

The Lie bracket of two vector fields that are differentiable and tangent to an involutive distribution on an open set is tangent to it there.

theorem TauCeti.IsInvolutiveDistributionOn.mlieBracket_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {s U : Set M} (hD : IsInvolutiveDistributionOn I D s) (hU : IsOpen U) (hUs : U ⊆ s) {V W : (x : M) → TangentSpace I x} (hV : MDiff[U] fun (x : M) => ⟨x, V x⟩) (hW : MDiff[U] fun (x : M) => ⟨x, W x⟩) (hVD : ∀ x ∈ U, V x ∈ D x) (hWD : ∀ x ∈ U, W x ∈ D x) {x : M} (hx : x ∈ U) : VectorField.mlieBracket I V W x ∈ D x

The Lie bracket of two vector fields that are differentiable and tangent to a distribution on an open subset of its involutivity set is tangent to the distribution there.

theorem TauCeti.IsInvolutiveDistribution.isInvolutiveDistributionOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsInvolutiveDistribution I D) (s : Set M) : IsInvolutiveDistributionOn I D s

An involutive distribution is involutive on every set.

theorem TauCeti.IsInvolutiveDistributionOn.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {s t : Set M} (hD : IsInvolutiveDistributionOn I D s) (ht : t ⊆ s) : IsInvolutiveDistributionOn I D t

A distribution that is involutive on s is involutive on every subset of s.

@[simp]

theorem TauCeti.isInvolutiveDistributionOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} : IsInvolutiveDistributionOn I D Set.univ ↔ IsInvolutiveDistribution I D

Involutivity on the whole manifold is equivalent to involutivity.

theorem TauCeti.isInvolutiveDistribution_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] : IsInvolutiveDistribution I fun (x : M) => ⊤

The whole tangent bundle is involutive.

theorem TauCeti.isInvolutiveDistribution_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Submodule 𝕜 E} (hS : IsClosed ↑S) : IsInvolutiveDistribution (modelWithCornersSelf 𝕜 E) fun (x : E) => S

A closed subspace S of E, taken at every point of E, is an involutive distribution on E: the Lie bracket of two vector fields with values in S has values in S.

theorem TauCeti.mlieBracket_sum_smul_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {ι : Type u_5} {X : ι → (x : M) → TangentSpace I x} {x : M} [IsManifold I 2 M] [CompleteSpace E] {D : Submodule 𝕜 (TangentSpace I x)} {s : Finset ι} (hX : ∀ i ∈ s, (MDiffAt fun (x : M) => ⟨x, X i x⟩) x) (hXD : ∀ i ∈ s, X i x ∈ D) (hXX : ∀ i ∈ s, ∀ j ∈ s, VectorField.mlieBracket I (X i) (X j) x ∈ D) {f g : ι → M → 𝕜} (hf : ∀ i ∈ s, MDiffAt (f i) x) (hg : ∀ i ∈ s, MDiffAt (g i) x) : VectorField.mlieBracket I (∑ i ∈ s, f i • X i) (∑ j ∈ s, g j • X j) x ∈ D

Let the vector fields X i be differentiable at x, with values at x and pairwise Lie brackets at x in a subspace D of the tangent space there. Then the Lie bracket at x of two combinations ∑ i, f i • X i and ∑ j, g j • X j whose coefficients are differentiable at x also lies in D.

This is the pointwise computation behind the classical criterion for involutivity: a distribution whose local frames are closed under the Lie bracket is involutive.

def TauCeti.standardContactDistribution (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (p : 𝕜 × 𝕜 × 𝕜) : Submodule 𝕜 (𝕜 × 𝕜 × 𝕜)

The standard contact distribution on 𝕜³: at p = (x, y, z) it is the kernel of the contact form dz - x dy, consisting of the vectors (a, b, c) with c = x b.

@[simp]

theorem TauCeti.mem_standardContactDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {p v : 𝕜 × 𝕜 × 𝕜} : v ∈ standardContactDistribution 𝕜 p ↔ v.2.2 = p.1 * v.2.1

theorem TauCeti.isContMDiffDistribution_standardContactDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) : IsContMDiffDistribution (modelWithCornersSelf 𝕜 (𝕜 × 𝕜 × 𝕜)) n 2 (standardContactDistribution 𝕜)

The standard contact distribution is a C^n distribution of rank two.

theorem TauCeti.not_isInvolutiveDistribution_standardContactDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : ¬IsInvolutiveDistribution (modelWithCornersSelf 𝕜 (𝕜 × 𝕜 × 𝕜)) (standardContactDistribution 𝕜)

The standard contact distribution is not involutive: the Lie bracket of its frame fields (1, 0, 0) and (0, 1, x) is the vector field (0, 0, 1), which is nowhere tangent to it.