Graph distributions and the Frobenius theorem in coordinates

A family f : E × F → (E →L[𝕜] F) of linear maps defines a distribution on E × F, its graph distribution TauCeti.graphDistribution f: at p it is the graph {(v, f p v) | v : E} of f p. A smooth distribution on E × F whose subspace at a point p₀ is a complement of 0 × F is, near p₀, the graph distribution of a smooth family f, so graph distributions are the local normal form in which the Frobenius theorem is proved; that reduction is TauCeti.IsContMDiffDistribution.exists_eventually_eq_graphDistribution, in TauCeti/Geometry/Manifold/Distribution/Transverse.lean.

This file identifies involutivity of a graph distribution with the Frobenius integrability condition TauCeti.IsFrobeniusIntegrableAt of the total differential equation D u x = f (x, u x), whose solutions are the functions u : E → F with graphs tangent to the distribution. The computation behind it is TauCeti.snd_lieBracket_eq_of_eventually_mem_graphDistribution: if V and W are vector fields tangent to the graph distribution near p, their Lie bracket [V, W] at p fails to lie in the graph of f p exactly by

fderiv 𝕜 f p (V p) (W p).1 - fderiv 𝕜 f p (W p) (V p).1,

which vanishes when the integrability condition holds at p. Conversely, the vector fields q ↦ (v, f q v) are tangent to the distribution, and their brackets recover the integrability condition. Combined with the local Frobenius theorem for total differential equations (TauCeti.exists_eventually_hasFDerivAt_of_isFrobeniusIntegrableAt), this proves the Frobenius theorem for graph distributions: over finite-dimensional real spaces, a C¹ graph distribution is involutive exactly when through every point there passes the graph of a local solution, an integral manifold of the distribution.

Main definitions

• TauCeti.graphDistribution f: the distribution p ↦ {(v, f p v) | v : E} on E × F.

Main results

• TauCeti.isContMDiffDistribution_graphDistribution: for a C^n family f with finite-dimensional source, the graph distribution is a C^n distribution of rank dim E.
• TauCeti.lieBracket_mem_graphDistribution_iff: the Lie bracket at p of two vector fields tangent to the graph distribution near p is tangent to it exactly when fderiv 𝕜 f p (V p) (W p).1 = fderiv 𝕜 f p (W p) (V p).1.
• TauCeti.isInvolutiveDistribution_graphDistribution_iff: for differentiable f, the graph distribution is involutive exactly when the Frobenius integrability condition holds everywhere.
• TauCeti.IsInvolutiveDistribution.exists_eventually_hasFDerivAt: the Frobenius theorem in coordinates. Over finite-dimensional real spaces, an involutive graph distribution of a map f of class C^(n+1) near (x₀, y₀) has an integral manifold through (x₀, y₀): the graph of a local solution u with u x₀ = y₀.
• TauCeti.isInvolutiveDistribution_graphDistribution_iff_forall_exists: for C¹ maps f between finite-dimensional real spaces, the graph distribution is involutive exactly when the graph of a local solution passes through every point.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 19.
• S. Lang, Fundamentals of Differential Geometry, Springer GTM 191 (1999), Chapter VI, §1.
• J. Dieudonné, Foundations of Modern Analysis, Academic Press (1960), Section 10.9.

def TauCeti.graphDistribution {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E × F → E →L[𝕜] F) (p : E × F) : Submodule 𝕜 (E × F)

The graph distribution of a family f of linear maps E →L[𝕜] F indexed by E × F: at p it is the graph {(v, f p v) | v : E} of f p, a subspace of E × F.

theorem TauCeti.graphDistribution_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E × F → E →L[𝕜] F) (p : E × F) : graphDistribution f p = (↑(f p)).graph

@[simp]

theorem TauCeti.mem_graphDistribution {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E × F → E →L[𝕜] F} {p v : E × F} : v ∈ graphDistribution f p ↔ v.2 = (f p) v.1

theorem TauCeti.isContMDiffDistribution_graphDistribution {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [FiniteDimensional 𝕜 E] {n : WithTop ℕ∞} {f : E × F → E →L[𝕜] F} (hf : ContDiff 𝕜 n f) : IsContMDiffDistribution (modelWithCornersSelf 𝕜 (E × F)) n (Module.finrank 𝕜 E) (graphDistribution f)

For a C^n family f with finite-dimensional source E, the graph distribution of f is a C^n distribution of rank finrank 𝕜 E. A basis b of E gives the global frame q ↦ (b i, f q (b i)).

theorem TauCeti.snd_lieBracket_eq_of_eventually_mem_graphDistribution {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E × F → E →L[𝕜] F} {V W : E × F → E × F} {p : E × F} (hf : DifferentiableAt 𝕜 f p) (hV : DifferentiableAt 𝕜 V p) (hW : DifferentiableAt 𝕜 W p) (hVD : ∀ᶠ (q : E × F) in nhds p, V q ∈ graphDistribution f q) (hWD : ∀ᶠ (q : E × F) in nhds p, W q ∈ graphDistribution f q) : (VectorField.lieBracket 𝕜 V W p).2 = (f p) (VectorField.lieBracket 𝕜 V W p).1 + (((fderiv 𝕜 f p) (V p)) (W p).1 - ((fderiv 𝕜 f p) (W p)) (V p).1)

The Lie bracket of two vector fields tangent to a graph distribution. If V and W are differentiable at p and tangent to the graph distribution of f near p, and f is differentiable at p, then the second component of [V, W] at p is f p applied to its first component, plus the defect fderiv 𝕜 f p (V p) (W p).1 - fderiv 𝕜 f p (W p) (V p).1.

theorem TauCeti.lieBracket_mem_graphDistribution_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E × F → E →L[𝕜] F} {V W : E × F → E × F} {p : E × F} (hf : DifferentiableAt 𝕜 f p) (hV : DifferentiableAt 𝕜 V p) (hW : DifferentiableAt 𝕜 W p) (hVD : ∀ᶠ (q : E × F) in nhds p, V q ∈ graphDistribution f q) (hWD : ∀ᶠ (q : E × F) in nhds p, W q ∈ graphDistribution f q) : VectorField.lieBracket 𝕜 V W p ∈ graphDistribution f p ↔ ((fderiv 𝕜 f p) (V p)) (W p).1 = ((fderiv 𝕜 f p) (W p)) (V p).1

The Lie bracket at p of two vector fields tangent to the graph distribution of f near p is tangent to it at p exactly when fderiv 𝕜 f p (V p) (W p).1 = fderiv 𝕜 f p (W p) (V p).1.

theorem TauCeti.lieBracket_mem_graphDistribution {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E × F → E →L[𝕜] F} {V W : E × F → E × F} {p : E × F} (hf : DifferentiableAt 𝕜 f p) (hV : DifferentiableAt 𝕜 V p) (hW : DifferentiableAt 𝕜 W p) (hVD : ∀ᶠ (q : E × F) in nhds p, V q ∈ graphDistribution f q) (hWD : ∀ᶠ (q : E × F) in nhds p, W q ∈ graphDistribution f q) (hint : IsFrobeniusIntegrableAt f p) : VectorField.lieBracket 𝕜 V W p ∈ graphDistribution f p

Where the Frobenius integrability condition holds, the Lie bracket of two vector fields tangent to the graph distribution is tangent to it.

theorem TauCeti.IsInvolutiveDistributionOn.isFrobeniusIntegrableAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {D : E × F → Submodule 𝕜 (E × F)} {f : E × F → E →L[𝕜] F} {p : E × F} {s : Set (E × F)} (hD : IsInvolutiveDistributionOn (modelWithCornersSelf 𝕜 (E × F)) D s) (hs : s ∈ nhds p) (hDf : ∀ᶠ (q : E × F) in nhds p, D q = graphDistribution f q) (hf : ∀ᶠ (q : E × F) in nhds p, DifferentiableAt 𝕜 f q) : IsFrobeniusIntegrableAt f p

A distribution involutive on a neighbourhood of p that agrees near p with the graph distribution of f, where f is differentiable near p, makes f satisfy the Frobenius integrability condition at p. The condition is the tangency of the brackets of the vector fields q ↦ (v, f q v), which are tangent to the distribution near p.

theorem TauCeti.IsInvolutiveDistribution.isFrobeniusIntegrableAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {D : E × F → Submodule 𝕜 (E × F)} {f : E × F → E →L[𝕜] F} {p : E × F} (hD : IsInvolutiveDistribution (modelWithCornersSelf 𝕜 (E × F)) D) (hDf : ∀ᶠ (q : E × F) in nhds p, D q = graphDistribution f q) (hf : ∀ᶠ (q : E × F) in nhds p, DifferentiableAt 𝕜 f q) : IsFrobeniusIntegrableAt f p

An involutive distribution that agrees near p with the graph distribution of f, where f is differentiable near p, makes f satisfy the Frobenius integrability condition at p.

theorem TauCeti.isInvolutiveDistribution_graphDistribution_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E × F → E →L[𝕜] F} (hf : Differentiable 𝕜 f) : IsInvolutiveDistribution (modelWithCornersSelf 𝕜 (E × F)) (graphDistribution f) ↔ ∀ (p : E × F), IsFrobeniusIntegrableAt f p

Involutivity of a graph distribution is the Frobenius integrability condition. For a differentiable family f, the graph distribution of f is involutive exactly when f satisfies the Frobenius integrability condition at every point.

theorem TauCeti.IsInvolutiveDistribution.exists_eventually_hasFDerivAt {E F : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ∞} {f : E × F → E →L[ℝ] F} {s : Set (E × F)} {x₀ : E} {y₀ : F} (hD : IsInvolutiveDistribution (modelWithCornersSelf ℝ (E × F)) (graphDistribution f)) (hf : ContDiffOn ℝ (↑n + 1) f s) (hs : s ∈ nhds (x₀, y₀)) : ∃ (u : E → F), u x₀ = y₀ ∧ ContDiffAt ℝ (↑n + 1) u x₀ ∧ ∀ᶠ (x : E) in nhds x₀, HasFDerivAt u (f (x, u x)) x

The Frobenius theorem in coordinates. Let f be of class C^(n+1) near (x₀, y₀), with an involutive graph distribution. Then the distribution has an integral manifold through (x₀, y₀): the graph of a function u, of class C^(n+1) at x₀, with u x₀ = y₀ and D u x = f (x, u x) near x₀, so that the tangent space of the graph at (x, u x) is the graph of f (x, u x).

theorem TauCeti.isInvolutiveDistribution_graphDistribution_iff_forall_exists {E F : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E × F → E →L[ℝ] F} (hf : ContDiff ℝ 1 f) : IsInvolutiveDistribution (modelWithCornersSelf ℝ (E × F)) (graphDistribution f) ↔ ∀ (p : E × F), ∃ (u : E → F), u p.1 = p.2 ∧ ∀ᶠ (x : E) in nhds p.1, HasFDerivAt u (f (x, u x)) x

The Frobenius theorem for graph distributions. For a C¹ family f over finite-dimensional real spaces, the graph distribution of f is involutive exactly when through every point p there passes an integral manifold, the graph of a local solution u of D u x = f (x, u x) with u p.1 = p.2.