The local Frobenius theorem

Let E and F be real normed spaces and f : E × F → (E →L[ℝ] F). The total differential equation D u x = f (x, u x) asks for a function u : E → F whose graph is tangent, at each of its points p, to the graph {(v, f p v) | v : E} of f p. Differentiating the equation once more shows that solutions can exist through all points near p₀ only if f satisfies the Frobenius integrability condition TauCeti.IsFrobeniusIntegrableAt near p₀: the bilinear map (v, w) ↦ fderiv ℝ f p (v, f p v) w is symmetric. The local Frobenius theorem says that the condition is also sufficient, and that the local solutions are unique.

The integrability condition is the involutivity of the distribution p ↦ {(v, f p v)}, written in coordinates: the vector fields p ↦ (v, f p v) span it, and the Lie bracket of the fields attached to v and w is (0, fderiv ℝ f p (v, f p v) w - fderiv ℝ f p (w, f p w) v), which is tangent to the distribution exactly when it vanishes. In a chart adapted to an involutive distribution on a manifold, the distribution takes this graph form, and the graphs of the local solutions are its integral manifolds. This is the analytic content of the Frobenius theorem for involutive distributions, which integrates a Lie subalgebra of the Lie algebra of a Lie group to a connected Lie subgroup.

Main definitions and results

• TauCeti.IsFrobeniusIntegrableAt f p: the Frobenius integrability condition at p.
• TauCeti.isFrobeniusIntegrableAt_of_eventually_hasFDerivAt: the condition holds along the graph of every solution.
• TauCeti.exists_eventually_hasFDerivAt_of_isFrobeniusIntegrableAt: the local Frobenius theorem, existence of a local solution through a point near which the condition holds.
• TauCeti.eventuallyEq_of_eventually_hasFDerivAt: local solutions with the same initial value agree.
• TauCeti.eventually_exists_hasFDerivAt_iff_eventually_isFrobeniusIntegrableAt: solutions exist through all points near p₀ exactly when the condition holds near p₀.

Implementation notes

Existence is proved in finite dimension, where a smooth germ has a globally Lipschitz smooth representative, so that the parameterized Picard theorem ODE.exists_contDiffAt_picard_solution_of_contDiff applies. The solution through (x₀, y₀) is built along rays: for a small parameter z, the ordinary differential equation b' = f (x₀ + t • z, b) z with b 0 = y₀ is solved on [0, 1], smoothly in z, and u (x₀ + z) = b 1. Rescaling time shows that b t = u (x₀ + t • z), so u solves the equation in the radial direction: D u x (x - x₀) = f (x, u x) (x - x₀). To upgrade the radial equation, fix w and a ray; then h t = t • (D u (x₀ + t • z) w - f (x₀ + t • z, u (x₀ + t • z)) w) solves a linear ordinary differential equation with h 0 = 0, so h vanishes. The derivative of h is computed without differentiating u twice: t • D u (x₀ + t • z) w is the derivative in s of u along the ray in the direction z + s • w, which is an integral of f along that ray by the radial equation, and it is differentiated under the integral sign. The integrability condition then turns this derivative into the linear equation. So f only needs to be C¹.

References

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

def TauCeti.IsFrobeniusIntegrableAt {𝕜 : 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) : Prop

The Frobenius integrability condition for the total differential equation D u x = f (x, u x) at the point p: the bilinear map obtained by differentiating f at p along the graph directions (v, f p v), namely (v, w) ↦ fderiv 𝕜 f p (v, f p v) w, is symmetric. The condition is meant for f differentiable at p: otherwise fderiv 𝕜 f p is zero and the condition holds trivially.

Equations

• TauCeti.IsFrobeniusIntegrableAt f p = ∀ (v w : E), ((fderiv 𝕜 f p) (v, (f p) v)) w = ((fderiv 𝕜 f p) (w, (f p) w)) v

theorem TauCeti.isFrobeniusIntegrableAt_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} {p : E × F} : IsFrobeniusIntegrableAt f p ↔ ∀ (v w : E), ((fderiv 𝕜 f p) (v, (f p) v)) w = ((fderiv 𝕜 f p) (w, (f p) w)) v

The defining property of the Frobenius integrability condition.

theorem Filter.EventuallyEq.isFrobeniusIntegrableAt_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E × F → E →L[𝕜] F} {p : E × F} (h : f =ᶠ[nhds p] g) : TauCeti.IsFrobeniusIntegrableAt f p ↔ TauCeti.IsFrobeniusIntegrableAt g p

The Frobenius integrability condition at p only depends on the germ of f at p.

theorem TauCeti.isFrobeniusIntegrableAt_of_eventually_hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IsRCLikeNormedField 𝕜] {f : E × F → E →L[𝕜] F} {u : E → F} {x : E} (hu : ∀ᶠ (y : E) in nhds x, HasFDerivAt u (f (y, u y)) y) (hf : DifferentiableAt 𝕜 f (x, u x)) : IsFrobeniusIntegrableAt f (x, u x)

The Frobenius integrability condition is necessary. If u solves the total differential equation D u y = f (y, u y) near x and f is differentiable at (x, u x), then f satisfies the Frobenius integrability condition at (x, u x): the condition is the symmetry of the second derivative of u at x.

theorem TauCeti.eventuallyEq_of_eventually_hasFDerivAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E × F → E →L[ℝ] F} {u₁ u₂ : E → F} {x₀ : E} {K : NNReal} {s : Set (E × F)} (hs : s ∈ nhds (x₀, u₁ x₀)) (hf : LipschitzOnWith K f s) (hu₁ : ∀ᶠ (x : E) in nhds x₀, HasFDerivAt u₁ (f (x, u₁ x)) x) (hu₂ : ∀ᶠ (x : E) in nhds x₀, HasFDerivAt u₂ (f (x, u₂ x)) x) (h₀ : u₁ x₀ = u₂ x₀) : u₁ =ᶠ[nhds x₀] u₂

Uniqueness in the local Frobenius theorem. Two solutions of the total differential equation D u x = f (x, u x) near x₀ taking the same value at x₀ agree near x₀, as soon as f is Lipschitz near (x₀, u₁ x₀). Neither integrability nor finite dimensionality is needed: along each ray from x₀ both solutions solve the same ordinary differential equation.

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

The local Frobenius theorem. Let E and F be finite-dimensional real normed spaces and let f : E × F → (E →L[ℝ] F) be C^(n+1) near (x₀, y₀), for instance C¹. If f satisfies the Frobenius integrability condition near (x₀, y₀), then the total differential equation D u x = f (x, u x) has a local solution u with u x₀ = y₀, which is C^(n+1) at x₀.

theorem TauCeti.eventually_exists_hasFDerivAt_iff_eventually_isFrobeniusIntegrableAt {E F : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {n : ℕ∞} {f : E × F → E →L[ℝ] F} {s : Set (E × F)} {p₀ : E × F} (hf : ContDiffOn ℝ (↑n + 1) f s) (hs : s ∈ nhds p₀) : (∀ᶠ (p : E × F) in nhds p₀, ∃ (u : E → F), u p.1 = p.2 ∧ ∀ᶠ (x : E) in nhds p.1, HasFDerivAt u (f (x, u x)) x) ↔ ∀ᶠ (p : E × F) in nhds p₀, IsFrobeniusIntegrableAt f p

The Frobenius theorem for total differential equations. Let E and F be finite-dimensional real normed spaces and let f : E × F → (E →L[ℝ] F) be C^(n+1) near p₀, for instance C¹. The total differential equation D u x = f (x, u x) has a local solution through every point near p₀ if and only if f satisfies the Frobenius integrability condition near p₀.