Maximal solutions and global existence

TheoremGluing solutions of an ODE#✓fully proved

Let \(E\) be a real normed space, let \(v : \mathbb{R} \times E \to E\), let \(I, J \subseteq \mathbb{R}\) be open, and let \(x, y : \mathbb{R} \to E\) satisfy \(x'(t) = v(t, x(t))\) for every \(t \in I\) and \(y'(t) = v(t, y(t))\) for every \(t \in J\), with \(x = y\) on \(I \cap J\). Then there is \(z : \mathbb{R} \to E\) with \(z = x\) on \(I\), \(z = y\) on \(J\) and \(z'(t) = v(t, z(t))\) for every \(t \in I \cup J\).

theorem hasDerivAt_piecewise_union_of_eqOn
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {v : ℝ → E → E} {x y : ℝ → E} {I J : Set ℝ}
    (hI : IsOpen I) (hJ : IsOpen J)
    (hx : ∀ t ∈ I, HasDerivAt x (v t (x t)) t)
    (hy : ∀ t ∈ J, HasDerivAt y (v t (y t)) t)
    (hxy : EqOn x y (I ∩ J)) :
    ∃ z : ℝ → E, EqOn z x I ∧ EqOn z y J ∧
      ∀ t ∈ I ∪ J, HasDerivAt z (v t (z t)) t

Used by 2

Used byGlobal existence and uniqueness for globally Lipschitz ODEs · Solutions of locally Lipschitz ODEs that leave every compact set

TheoremGlobal existence and uniqueness for globally Lipschitz ODEs#✓fully proved

Let \(E\) be a real Banach space, let \(f : \mathbb{R} \times E \to E\) be continuous, and let \(L \ge 0\) be such that \(f(t, \cdot)\) is \(L\)-Lipschitz for every \(t \in \mathbb{R}\). Then for every \(t_0 \in \mathbb{R}\) and \(x_0 \in E\) there is exactly one function \(x : \mathbb{R} \to E\) with \(x(t_0) = x_0\) and \(x'(t) = f(t, x(t))\) for every \(t \in \mathbb{R}\).

Proof: local Picard--Lindelöf solutions are continued using the Gronwall bound of Teschl's Theorem 2.17 and the extension criterion of Lemma 2.14. Time reversal supplies the negative-time solution, and global Gronwall uniqueness identifies every solution with the glued one.

theorem ode_global_exists_of_global_lipschitz
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (L : NNReal)
    (hfcont : Continuous (Function.uncurry f))
    (hlip : ∀ t, LipschitzWith L (f t)) :
    ∃! x : ℝ → E, x t₀ = x₀ ∧ ∀ t, HasDerivAt x (f t (x t)) t

Sources

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Section 2.2; stable ref https://en.wikipedia.org/wiki/Picard%E2%80%93Lindel%C3%B6f_theorem.

Uses 1 · Used by 3

Proof usesGluing solutions of an ODE

Used byFirst-order convergence of the explicit Euler method · Global existence and uniqueness for homogeneous linear ODEs · Existence for the Sturm–Liouville Dirichlet problem on the closed unit interval

TheoremSolutions of locally Lipschitz ODEs that leave every compact set#✓fully proved

Let \(E\) be a real Banach space, let \(U \subseteq \mathbb{R} \times E\) be open, let \((t_0, x_0) \in U\), and let \(f : \mathbb{R} \times E \to E\) be continuous on \(U\) and locally Lipschitz in the state variable, uniformly in time: every \(p \in U\) has a neighbourhood \(N\) and a constant \(C \ge 0\) such that \(\|f(t, u) - f(t, w)\| \le C \|u - w\|\) whenever \((t, u)\) and \((t, w)\) lie in \(N \cap U\). Then there are an open interval \(I\) (possibly unbounded) containing \(t_0\) and a function \(x : \mathbb{R} \to E\) with \(x(t_0) = x_0\) such that \((t, x(t)) \in U\) and \(x'(t) = f(t, x(t))\) for every \(t \in I\), and such that for every compact \(K \subseteq U\) there are \(c_1, c_2 \in I\) with \((t, x(t)) \notin K\) for every \(t \in I\) with \(t \ge c_1\) and for every \(t \in I\) with \(t \le c_2\).

Proof: local Picard--Lindelöf solutions are glued by uniqueness into Teschl's maximal solution (Theorem 2.13). A compactly recurrent finite endpoint extends by Lemma 2.14, giving the two exit statements of Corollaries 2.15--2.16.

theorem ode_maximal_solution_exit_compact
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (U : Set (ℝ × E)) (f : ℝ × E → E) (t₀ : ℝ) (x₀ : E)
    (hU : IsOpen U) (hmem : (t₀, x₀) ∈ U)
    (hf : ContinuousOn f U)
    (hlip : ∀ p ∈ U, ∃ C : NNReal, ∃ s ∈ nhds p,
      ∀ t : ℝ, ∀ x y : E, (t, x) ∈ s ∩ U → (t, y) ∈ s ∩ U →
        dist (f (t, x)) (f (t, y)) ≤ C * dist x y) :
    ∃ I : Set ℝ, ∃ x : ℝ → E, x t₀ = x₀ ∧ IsOpen I ∧ t₀ ∈ I ∧
      (∀ t₁ ∈ I, ∀ t₂ ∈ I, Set.Icc t₁ t₂ ⊆ I) ∧
      (∀ t ∈ I, (t, x t) ∈ U ∧ HasDerivAt x (f (t, x t)) t) ∧
      ∀ K : Set (ℝ × E), IsCompact K → K ⊆ U →
        (∃ c ∈ I, ∀ t ∈ I, c ≤ t → (t, x t) ∉ K) ∧
        ∃ c ∈ I, ∀ t ∈ I, t ≤ c → (t, x t) ∉ K

Sources

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Section 2.4.

Uses 1

Proof usesGluing solutions of an ODE

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.