An actual global flow for a bounded, uniformly Lipschitz velocity

Existence is the proved global Picard theorem in EulerPacketExistence. Uniqueness gives the two-time composition and inverse identities. The bounded velocity and Grönwall estimate will give joint continuity in both times and the initial point.

structure EulerBoundedLipschitzFlow.Data (E : Type u_1) [NormedAddCommGroup E] : Type u_1

Data, collecting velocity, continuous, lipschitzConstant, lipschitz, speedBound, speed.

• velocity : ℝ → E → E

  Velocity field of Data, of type ℝ → E → E.

• continuous : Continuous (Function.uncurry self.velocity)
• lipschitzConstant : NNReal

  Lipschitz constant of Data, of type ℝ≥0.

• lipschitz (t : ℝ) : LipschitzWith self.lipschitzConstant (self.velocity t)
• speedBound : NNReal

  Speed bound of Data, of type ℝ≥0.

• speed (t : ℝ) (x : E) : ‖self.velocity t x‖ ≤ ↑self.speedBound

theorem EulerBoundedLipschitzFlow.Data.curve_exists {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s : ℝ) (x : E) : ∃ (α : ℝ → E), α s = x ∧ ∀ (t : ℝ), HasDerivAt α (V.velocity t (α t)) t

noncomputable def EulerBoundedLipschitzFlow.Data.flow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s t : ℝ) (x : E) : E

Flow, given by (V.curve_exists s x).choose t.

Equations

• V.flow s t x = ⋯.choose t

@[simp]

theorem EulerBoundedLipschitzFlow.Data.flow_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s : ℝ) (x : E) : V.flow s s x = x

theorem EulerBoundedLipschitzFlow.Data.flow_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s t : ℝ) (x : E) : HasDerivAt (fun (r : ℝ) => V.flow s r x) (V.velocity t (V.flow s t x)) t

theorem EulerBoundedLipschitzFlow.Data.flow_continuous_time {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s : ℝ) (x : E) : Continuous fun (t : ℝ) => V.flow s t x

theorem EulerBoundedLipschitzFlow.Data.flow_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s : ℝ) (x : E) (α : ℝ → E) (hα : ∀ (t : ℝ), HasDerivAt α (V.velocity t (α t)) t) (hαs : α s = x) : α = fun (t : ℝ) => V.flow s t x

theorem EulerBoundedLipschitzFlow.Data.flow_cocycle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (r s t : ℝ) (x : E) : V.flow s t (V.flow r s x) = V.flow r t x

@[simp]

theorem EulerBoundedLipschitzFlow.Data.flow_inverse {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s t : ℝ) (x : E) : V.flow t s (V.flow s t x) = x

theorem EulerBoundedLipschitzFlow.Data.flow_lipschitz_time {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s : ℝ) (x : E) : LipschitzWith V.speedBound fun (t : ℝ) => V.flow s t x

theorem EulerBoundedLipschitzFlow.Data.trajectory_distance {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : Data E) (α β : ℝ → E) (hα : ∀ (t : ℝ), HasDerivAt α (V.velocity t (α t)) t) (hβ : ∀ (t : ℝ), HasDerivAt β (V.velocity t (β t)) t) (a b : ℝ) : dist (α b) (β b) ≤ dist (α a) (β a) * Real.exp (↑V.lipschitzConstant * |b - a|)

A two-sided Grönwall estimate for actual global trajectories.

theorem EulerBoundedLipschitzFlow.Data.flow_distance_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (s t : ℝ) (x y : E) : dist (V.flow s t x) (V.flow s t y) ≤ dist x y * Real.exp (↑V.lipschitzConstant * |t - s|)