Theorems · Theorem · ordinary differential equations

dist_le_of_trajectories_ODE

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal} {f g : ℝ → E}
  {a b δ : ℝ},
  (∀ (t : ℝ), LipschitzWith K (v t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
        ContinuousOn g (Set.Icc a b) →
          (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
            dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ δ * Real.exp (↑K * (t - a))

If f and g are two exact solutions of the same ODE, then the distance between them can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some people call this Grönwall's inequality too. This version assumes all inequalities to be true in the whole space.

Defined in

Mathlib.Analysis.ODE.Gronwall

Cited by

0 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace