Theorems · Theorem · ordinary differential equations

dist_le_of_approx_trajectories_ODE_of_mem

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g f' g' : ℝ → E} {a b εf εg δ : ℝ},
  (∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (f' t) (Set.Ici t) t) →
        (∀ t ∈ Set.Ico a b, dist (f' t) (v t (f t)) ≤ εf) →
          (∀ t ∈ Set.Ico a b, f t ∈ s t) →
            ContinuousOn g (Set.Icc a b) →
              (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (g' t) (Set.Ici t) t) →
                (∀ t ∈ Set.Ico a b, dist (g' t) (v t (g t)) ≤ εg) →
                  (∀ t ∈ Set.Ico a b, g t ∈ s t) →
                    dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ gronwallBound δ (↑K) (εf + εg) (t - a)

If f and g are two approximate 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 some time-dependent set s t, and assumes that the solutions never leave this set.

Defined in

Mathlib.Analysis.ODE.Gronwall

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace