Chaining RDE solutions across windows

Globalisation of the small-window well-posedness: given any partition 0 ≤ t₀ ≤ t₁ ≤ … ≤ t_N whose pieces satisfy the window conditions ω(tᵢ,tᵢ₊₁) ≤ 1 and ω(tᵢ,tᵢ₊₁)^α ≤ δα — no smallness of ω as a whole — there is a single path Y starting at y₀ that solves dY = f(Y)·dX on every window (rde_exists_chain).

The mechanism: on each window [a,b] the driver and control are pulled back along the clamp r ↦ min (max r a) b. The clamped control is dominated both by ω (so finiteness and fine partitions transport) and by the constant ω a b (so the window conditions hold globally for the clamped data), hence rde_wellposed applies. Clamped solutions are frozen outside [a,b] — their increments vanish where the clamp is constant — so the window solutions can be glued at the knots.

Clamping to a window

noncomputable def RoughPaths.clampIcc (a b r : ℝ) : ℝ

Clamp a real time to the window [a, b].

Equations

• RoughPaths.clampIcc a b r = min (max r a) b

theorem RoughPaths.clampIcc_mono (a b : ℝ) : Monotone (clampIcc a b)

theorem RoughPaths.le_clampIcc {a b : ℝ} (hab : a ≤ b) (r : ℝ) : a ≤ clampIcc a b r

theorem RoughPaths.clampIcc_le (a b r : ℝ) : clampIcc a b r ≤ b

theorem RoughPaths.clampIcc_of_le {a b r : ℝ} (hab : a ≤ b) (h : r ≤ a) : clampIcc a b r = a

theorem RoughPaths.clampIcc_of_ge {a b r : ℝ} (hab : a ≤ b) (h : b ≤ r) : clampIcc a b r = b

theorem RoughPaths.clampIcc_of_mem {a b r : ℝ} (h1 : a ≤ r) (h2 : r ≤ b) : clampIcc a b r = r

theorem RoughPaths.comap_clampIcc_le (ω : Control ℝ) {a b : ℝ} (hab : a ≤ b) ⦃s t : ℝ⦄ : s ≤ t → (ω.comap (clampIcc a b) ⋯).toFun s t ≤ ω.toFun s t

The clamped control is dominated by the original control.

theorem RoughPaths.comap_clampIcc_le_window (ω : Control ℝ) {a b : ℝ} (hab : a ≤ b) ⦃s t : ℝ⦄ (hst : s ≤ t) : (ω.comap (clampIcc a b) ⋯).toFun s t ≤ ω.toFun a b

The clamped control is globally dominated by the window value.

theorem RoughPaths.IsLevel2RoughPath.comap {d : ℕ} {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2RoughPath X ω α) (f : ℝ → ℝ) (hf : Monotone f) : IsLevel2RoughPath (AlgebraicRoughPath.comapTime f X) (ω.comap f hf) α

Level-2 bounds transport along monotone time changes.

Solutions are frozen where the clamped data is constant

theorem RoughPaths.RDEVectorField.IsRDESolution.const_of_zero {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {V' : RDEVectorField d E} {hX : IsLevel2RoughPath X ω α} {hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1} {Z : ControlledPath X ω α E} {I : ℝ → ℝ → E} (hsol : V'.IsRDESolution hX hω1 Z I) ⦃s t : ℝ⦄ (hst : s ≤ t) (hω0 : ω.toFun s t = 0) (hXu : X.increment s t = Word.unit (Fin d) ℝ) : Z.Y t = Z.Y s

A solution has constant path across any interval where the control vanishes and the driver increment is the unit: the germ and hence the increment are zero there.

theorem RoughPaths.RDEVectorField.IsRDESolution.frozen_of_clamp_eq {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {V' : RDEVectorField d E} {a b : ℝ} {hXc : IsLevel2RoughPath (AlgebraicRoughPath.comapTime (clampIcc a b) X) (ω.comap (clampIcc a b) ⋯) α} {hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → (ω.comap (clampIcc a b) ⋯).toFun s t ≤ 1} {Z : ControlledPath (AlgebraicRoughPath.comapTime (clampIcc a b) X) (ω.comap (clampIcc a b) ⋯) α E} {I : ℝ → ℝ → E} (hsol : V'.IsRDESolution hXc hω1 Z I) ⦃s t : ℝ⦄ (hst : s ≤ t) (hcl : clampIcc a b s = clampIcc a b t) : Z.Y t = Z.Y s

A solution of the clamped problem is frozen wherever the clamp is constant.

Solving on a single window

def RoughPaths.RDEVectorField3.SolvesOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (V : RDEVectorField3 d E) (hX : IsLevel2RoughPath X ω α) (Y : ℝ → E) (a b : ℝ) : Prop

Y solves dY = f(Y)·dX on the window [a,b]: the problem with driver and control clamped to [a,b] has a solution whose path agrees with Y throughout the window.

Equations

• One or more equations did not get rendered due to their size.

theorem RoughPaths.rde_solve_window {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (V : RDEVectorField3 d E) (hX : IsLevel2RoughPath X ω α) (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) (P : V.PicardParams α) {a b : ℝ} (hab : a ≤ b) (h0a : 0 ≤ a) (hwin1 : ω.toFun a b ≤ 1) (hwinα : ω.toFun a b ^ α ≤ ↑P.δα) (y : E) : ∃ (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → (ω.comap (clampIcc a b) ⋯).toFun s t ≤ 1) (Z : ControlledPath (AlgebraicRoughPath.comapTime (clampIcc a b) X) (ω.comap (clampIcc a b) ⋯) α E) (I : ℝ → ℝ → E), V.IsRDESolution ⋯ hω1 Z I ∧ Z.Y a = y

Solve on one window: if the single window [a,b] ⊆ [0,∞) satisfies the window conditions, the clamped problem has a box-certified solution whose value at a is the prescribed y.

The chain theorem

theorem RoughPaths.rde_exists_chain {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (V : RDEVectorField3 d E) (hX : IsLevel2RoughPath X ω α) (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) (P : V.PicardParams α) (N : ℕ) (t : Fin (N + 1) → ℝ) (y₀ : E) : 0 ≤ t 0 → (∀ (i : Fin N), t i.castSucc ≤ t i.succ) → (∀ (i : Fin N), ω.toFun (t i.castSucc) (t i.succ) ≤ 1) → (∀ (i : Fin N), ω.toFun (t i.castSucc) (t i.succ) ^ α ≤ ↑P.δα) → ∃ (Y : ℝ → E), Y (t 0) = y₀ ∧ ∀ (i : Fin N), V.SolvesOn hX Y (t i.castSucc) (t i.succ)

Globalisation by window chaining: for any partition 0 ≤ t₀ ≤ … ≤ t_N whose pieces satisfy the window conditions — no global smallness of ω — there is a single path Y with Y (t 0) = y₀ solving dY = f(Y)·dX on every window. Combined with exists_picardParams, every C³_b RDE is solvable along any sufficiently fine partition of an arbitrary horizon.

theorem RoughPaths.exists_window_chain {ω : Control ℝ} {α : ℝ} (hfine : Sewing.HasFinePartitions ω) (hα : 0 < α) {δα : NNReal} (hδα : 0 < δα) {s T : ℝ} (hsT : s ≤ T) : ∃ (N : ℕ) (t : Fin (N + 1) → ℝ), t 0 = s ∧ t (Fin.last N) = T ∧ (∀ (i : Fin N), t i.castSucc ≤ t i.succ) ∧ (∀ (i : Fin N), ω.toFun (t i.castSucc) (t i.succ) ≤ 1) ∧ ∀ (i : Fin N), ω.toFun (t i.castSucc) (t i.succ) ^ α ≤ ↑δα

Existence of window chains: fine partitions provide partitions satisfying the window conditions between any two times.

theorem RoughPaths.rde_exists_global {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (V : RDEVectorField3 d E) (hX : IsLevel2RoughPath X ω α) (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) {T₀ : ℝ} (h0T : 0 ≤ T₀) (y₀ : E) : ∃ (x : V.PicardParams α) (N : ℕ) (t : Fin (N + 1) → ℝ), t 0 = 0 ∧ t (Fin.last N) = T₀ ∧ (∀ (i : Fin N), t i.castSucc ≤ t i.succ) ∧ ∃ (Y : ℝ → E), Y 0 = y₀ ∧ ∀ (i : Fin N), V.SolvesOn hX Y (t i.castSucc) (t i.succ)

Global solvability along a fine partition: for every C³_b vector field, finite control with fine partitions, horizon T₀ ≥ 0 and initial value, there are Picard parameters, a partition of [0, T₀] satisfying the window conditions, and a path started at y₀ solving the RDE on every window.