The maximal flow of a vector field #
This file presents Tau Ceti's maximal integral curves as a partial flow whose arguments are ordered
as time followed by initial point. The domain and value are adapters for
maximalIntegralCurveFlowDomain and maximalIntegralCurve, not independent constructions. The
domain-aware group law records both the value equation and the condition that the composite time
remains in the interval of existence.
For complete normed model spaces, the existing smooth-dependence theorem for maximal integral
curves gives joint openness of the domain and joint smoothness of the flow, so flowing a C^n
family of points for a C^n family of times is again C^n. At time zero, the derivative of the
flow is the field in the time direction and the identity in the space directions, so flowing for a
time τ vanishing at x has derivative w ↦ w + dτ_x(w) • v x at x. Along a trajectory, a
function changes at the rate of its derivative in the direction of the vector field. The escape
theorem says that a maximal trajectory approaching a finite right endpoint eventually leaves every
compact set.
Main declarations #
TauCeti.flowDomain: the domain of the maximal flow, in(time, point)order.TauCeti.flowOf: the maximal flow, total with junk values outsideflowDomain.TauCeti.isOpen_flowDomain: openness of the domain for complete model spaces.TauCeti.contMDiffOn_flowOf: joint regularity of the flow for complete model spaces.TauCeti.contMDiffAt_flowOf_comp: flowingC^nfamilies of points forC^nfamilies of times.TauCeti.mfderiv_flowOf_comp_apply: the differential of(t, s) ↦ φₜ(f s).TauCeti.hasDerivAt_comp_flowOf: the time derivative of a function along a trajectory.TauCeti.mfderiv_flowOf_zero_apply: the derivative of the flow at time zero.TauCeti.hasMFDerivAt_flowOf_comp_of_eq_zero: the derivative of flowing for a time that vanishes at the base point.TauCeti.mfderiv_flowOf_trajectory_apply,TauCeti.mfderiv_flowOf_trajectory_zero_apply: the derivative of a trajectory is the field.TauCeti.mfderiv_flowOf_apply_self: the differential of the time-tmap carries the field to itself.TauCeti.flowOf_add: the domain-aware group law.TauCeti.flowOf_neg_flowOf: flowing backwards undoes flowing forwards.TauCeti.eventually_flowOf_notMem: escape from compact sets at a finite right endpoint.
References #
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Chapter 9.
The domain of the maximal flow in (time, point) order. This is
maximalIntegralCurveFlowDomain transported by Prod.swap.
Instances For
The maximal flow of a vector field, total with the same junk values as
maximalIntegralCurve.
Instances For
The maximal-flow adapter evaluates to the existing maximal integral curve.
Membership in the maximal-flow domain is membership in the maximal interval through the initial point.
Time zero belongs to the maximal-flow domain of x as soon as some time does.
The maximal flow fixes every point at time zero.
The trajectory t ↦ flowOf v t x is an integral curve on its maximal interval of
existence.
Time zero belongs to the maximal-flow domain.
A global integral curve of a C¹ field is the maximal flow through its initial value.
No completeness hypothesis is needed on the field or the model space.
The velocity of a maximal-flow trajectory is the vector field at the current point, whenever the trajectory is in its domain.
A maximal-flow trajectory is differentiable at every time in its domain.
The derivative of a trajectory. At every time in its domain, the derivative of
s ↦ flowOf v s x sends a to a • v (flowOf v t x).
The derivative of a trajectory at time zero. The derivative of s ↦ flowOf v s x at
s = 0 sends a to a • v x.
On a complete normed model space, the domain of the maximal flow is jointly open in time and initial point.
On a complete normed model space, a C^n vector field has a jointly C^n maximal flow on
its domain.
On a complete normed model space, flowing a C^n family of initial points for a C^n family
of times is C^n, wherever the flow is defined.
The differential of a flow out of a map. On a complete normed model space, at a point
(t, s) where φₜ(f s) is defined, the differential of (t, s) ↦ φₜ(f s) sends a tangent vector
(r, w) to r v + dφₜ(df w).
Derivative along a flow line. The derivative in time of a function g along the
trajectory of v through x is the derivative of g in the direction of v.
The derivative of the flow at time zero. At (0, x), the derivative of
(t, y) ↦ flowOf v t y sends the time direction to the field at x and is the identity in the
space direction.
Flowing for a time that vanishes at a point. If τ x = 0, the map
z ↦ flowOf v (τ z) z has derivative w ↦ w + dτ_x(w) • v x at x.
The domain-aware group law for the maximal flow. If time s is defined at x and time t
is defined after flowing for s, then time s + t is defined at x and gives the same value.
The flow can be run backwards along a trajectory: if time t is defined at x, then time
-t is defined at flowOf v t x.
Flowing for time -t undoes flowing for time t.
If x returns to itself at time t, it does so at every natural multiple of t.
If x returns to itself at time s, then so does every point flowOf v t x of its
trajectory.
The flow preserves its generating field. If time t is defined at x, the derivative of
the time-t map of the flow carries v x to v (flowOf v t x).
At a finite right endpoint of a maximal interval, the trajectory eventually leaves every compact set.