Smooth dependence of the constructed flow on its initial position #
The actual Picard flow is a continuous family of paths. Its integral equation is inverted locally on the path Banach space: the derivative is the genuine Volterra operator, whose two-sided inverse was constructed from the linear ODE. This proves smooth label dependence at every order.
Construction of the flow and its continuous inverse from a genuine bounded continuous velocity on the prescribed finite time interval. Endpoint extension only defines the auxiliary velocity outside that interval; all stated ODE identities use the original velocity.
Of time interval, bundling velocity, continuous, lipschitzConstant, lipschitz and
the required compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The actual finite-time flow has an actual two-sided continuous inverse. No flow map, inverse map or ODE solution is assumed.
Flow data, given by ofTimeInterval T hT A.field ‖A.derivative.field‖₊ (velocity_lipschitz T A).
Equations
Instances For
Path family as an element of C(E, C(Icc (0 : ℝ) T, E)).
Equations
- EulerSmoothBanachFlow.pathFamily T hT A = { toFun := fun (p : E × ↑(Set.Icc 0 T)) => (EulerSmoothBanachFlow.flowData T hT A).forward (↑p.2) p.1, continuous_toFun := ⋯ }.curry
Instances For
Path operator, given by u - EulerContinuousTimeIntegral.integral T hT (A.superposition u).
Equations
- EulerSmoothBanachFlow.pathOperator T hT A u = u - (EulerContinuousTimeIntegral.integral T hT) (A.superposition u)
Instances For
The actual nonlinear flow has smooth dependence on its initial point, in the uniform path norm on the whole prescribed time interval.