Local smooth flows on Banach spaces

A locally C^(n+1) vector field on a real Banach space admits a local flow of the same joint regularity in time and initial condition. The flow has initial value the identity, satisfies the flow law, and solves the original differential equation near the chosen initial point at time zero.

The global flow used to totalize this local object comes from a Lipschitz extension of the field by radial retraction. This extension agrees with the field on a ball, but need not be smooth outside that ball. Local smooth parameter dependence of the Picard equation suffices; no smooth bump functions on the Banach space are assumed.

References

• J. Dieudonné, Foundations of Modern Analysis, Academic Press, 1969, Chapter X.

theorem ODE.exists_contDiffAt_localFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {n : ℕ∞} (v : E → E) {a : E} {s : Set E} (hv : ContDiffOn ℝ (↑n + 1) v s) (hs : s ∈ nhds a) : ∃ (Φ : E → ℝ → E), ContDiffAt ℝ (↑n + 1) (fun (p : E × ℝ) => Φ p.1 p.2) (a, 0) ∧ (∀ (x : E), Φ x 0 = x) ∧ (∀ (x : E) (t u : ℝ), Φ x (t + u) = Φ (Φ x t) u) ∧ ∀ᶠ (p : E × ℝ) in nhds (a, 0), HasDerivAt (Φ p.1) (v (Φ p.1 p.2)) p.2

The local flow of a smooth Banach-space vector field. A field that is C^(n+1) near a admits a flow jointly C^(n+1) near (a, 0), solving the equation there. Its initial value and flow law hold for all points and times. Away from this neighbourhood it is the global flow of a Lipschitz extension, rather than necessarily a solution of the original field.