1.1. Local existence and uniqueness🔗

theorem

IsPicardLindelof.exists_forall_mem_closedBall_eq_isIntegralCurveOn.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal}
  (hf : IsPicardLindelof f t₀ x₀ a r L K) :
  ∃ α,
    ∀ x ∈ Metric.closedBall x₀ ↑r,
      α x ↑t₀ = x ∧ IsIntegralCurveOn (α x) f (Set.Icc tmin tmax)
IsPicardLindelof.exists_forall_mem_closedBall_eq_isIntegralCurveOn.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [CompleteSpace E]
  {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal}
  (hf :
    IsPicardLindelof f t₀ x₀ a r L K) :
  ∃ α,
    ∀ x ∈ Metric.closedBall x₀ ↑r,
      α x ↑t₀ = x ∧
        IsIntegralCurveOn (α x) f
          (Set.Icc tmin tmax)

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow.

theorem

IsIntegralCurveOn.eqOn_inter.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {t₀ : ℝ} {I J : Set ℝ}
  (hv : ∀ t ∈ I ∩ J, LipschitzOnWith K (v t) (s t))
  (hI : IsPreconnected I) (hJ : IsPreconnected J) (htI : t₀ ∈ I)
  (htJ : t₀ ∈ J) (hf : IsIntegralCurveOn f v I)
  (hfs : ∀ t ∈ I ∩ J, f t ∈ s t) (hg : IsIntegralCurveOn g v J)
  (hgs : ∀ t ∈ I ∩ J, g t ∈ s t) (heq : f t₀ = g t₀) :
  Set.EqOn f g (I ∩ J)
IsIntegralCurveOn.eqOn_inter.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {v : ℝ → E → E}
  {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {t₀ : ℝ} {I J : Set ℝ}
  (hv :
    ∀ t ∈ I ∩ J,
      LipschitzOnWith K (v t) (s t))
  (hI : IsPreconnected I)
  (hJ : IsPreconnected J) (htI : t₀ ∈ I)
  (htJ : t₀ ∈ J)
  (hf : IsIntegralCurveOn f v I)
  (hfs : ∀ t ∈ I ∩ J, f t ∈ s t)
  (hg : IsIntegralCurveOn g v J)
  (hgs : ∀ t ∈ I ∩ J, g t ∈ s t)
  (heq : f t₀ = g t₀) :
  Set.EqOn f g (I ∩ J)

If two integral curves of a Lipschitz vector field on connected sets I and J agree at a point t₀ ∈ I ∩ J, then they agree on all of I ∩ J.

1.1.1. Uniformly locally Lipschitz maps🔗

We define functions f : ℝ → E → E that are locally uniformly Lipschitz.

def

UniformlyLocallyLipschitzOn.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  (f : ℝ → E → E) (s : Set (ℝ × E)) : Prop
UniformlyLocallyLipschitzOn.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (f : ℝ → E → E) (s : Set (ℝ × E)) : Prop

A function is uniformly locally Lipschitz if for every t₀ and x₀ there exists a K such that f t is Lipschitz on a neighbourhood of x₀ for all t in a neighborhood of t₀.

The main use of this definition is that it gives a sufficent condition for local existence of ODEs using the Picard-Lindelöf theorem.

def

UniformlyLocallyLipschitz.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  (f : ℝ → E → E) : Prop
UniformlyLocallyLipschitz.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (f : ℝ → E → E) : Prop

A function is uniformly locally Lipschitz if for every t₀ and x₀ there exists a K such that f t is Lipschitz on a neighbourhood of x₀ for all t in a neighborhood of t₀.

The main use of this definition is that it gives a sufficent condition for local existence of ODEs using the Picard-Lindelöf theorem.

We prove that locally uniformly Lipschitz functions satisfy the Picard--Lindelöf conditions

theorem

UniformlyLocallyLipschitzOn.isPicardLindelof.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] {f : ℝ → E → E} {s : Set (ℝ × E)}
  (hf : UniformlyLocallyLipschitzOn f s)
  (hf' :
    ∀ (x : E),
      ContinuousOn (fun x_1 ↦ f x_1 x) ((fun x_1 ↦ (x_1, x)) ⁻¹' s))
  {t₀ : ℝ} {x₀ : E} (hs : s ∈ nhds (t₀, x₀)) :
  ∃ ε,
    ∃ (hε : 0 < ε),
      ∃ a r L K,
        ∃ (_ : 0 < a) (_ : 0 < r), IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
UniformlyLocallyLipschitzOn.isPicardLindelof.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {f : ℝ → E → E} {s : Set (ℝ × E)}
  (hf : UniformlyLocallyLipschitzOn f s)
  (hf' :
    ∀ (x : E),
      ContinuousOn (fun x_1 ↦ f x_1 x)
        ((fun x_1 ↦ (x_1, x)) ⁻¹' s))
  {t₀ : ℝ} {x₀ : E}
  (hs : s ∈ nhds (t₀, x₀)) :
  ∃ ε,
    ∃ (hε : 0 < ε),
      ∃ a r L K,
        ∃ (_ : 0 < a) (_ : 0 < r),
          IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a
            r L K

If f is continuous and uniformly locally Lipschitz, then the ODE d/dt x = f t x has a local solution for every initial condition x t₀ = x₀.