The straightening theorem for vector fields on a normed space

Near a point where a C^n vector field w on a finite-dimensional real normed space E does not vanish, some C^n change of coordinates carries w to a constant field. Precisely, there is an open partial homeomorphism φ of E, C^n with C^n inverse, whose domain contains the point a and whose derivative sends w y to w a at every point y of its domain (TauCeti.exists_openPartialHomeomorph_fderiv_eq_const). This is the flow-box theorem: in the coordinates φ, the integral curves of w become parallel straight lines traversed with constant velocity w a.

Cut w off to a globally Lipschitz C^n field g that agrees with it near a, and let Φ be the global flow of g, which is C^n jointly in the initial condition and time. Choose a continuous linear functional ℓ with ℓ (w a) = 1 and set

ψ z = Φ (a + (z - ℓ z • w a)) (ℓ z).

The flow law gives ψ (z + s • w a) = Φ (ψ z) s, so differentiating in s shows that dψ z sends w a to g (ψ z). At z = 0 the derivative of ψ is the identity, so by the inverse function theorem with C^n inverse (ContDiffOn.exists_openPartialHomeomorph_fderiv_symm_apply_eq) ψ is a local diffeomorphism near 0 whose inverse sends g to w a; restricted to where g = w, that inverse is the required φ.

Main results

• TauCeti.exists_openPartialHomeomorph_fderiv_eq_const: a nonvanishing C^n vector field is constant in suitable C^n local coordinates.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Theorem 9.22 (canonical form near a regular point).

theorem TauCeti.exists_openPartialHomeomorph_fderiv_eq_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ∞} (hn : 1 ≤ n) {w : E → E} {s : Set E} {a : E} (hw : ContDiffOn ℝ (↑n) w s) (hs : s ∈ nhds a) (ha : w a ≠ 0) : ∃ (φ : OpenPartialHomeomorph E E), a ∈ φ.source ∧ (∀ y ∈ φ.source, ContDiffAt ℝ (↑n) (↑φ) y) ∧ (∀ z ∈ φ.target, ContDiffAt ℝ (↑n) (↑φ.symm) z) ∧ ∀ y ∈ φ.source, (fderiv ℝ (↑φ) y) (w y) = w a

The straightening theorem (flow-box theorem). A C^n vector field w, 1 ≤ n, defined near a point a of a finite-dimensional real normed space, with w a ≠ 0, is constant in suitable C^n coordinates: there is an open partial homeomorphism φ, C^n on its source with C^n inverse on its target, such that a ∈ φ.source and dφ_y (w y) = w a for every y ∈ φ.source.