# Documentation

Mathlib.Analysis.ODE.Gronwall

# Grönwall's inequality #

The main technical result of this file is the Grönwall-like inequality norm_le_gronwallBound_of_norm_deriv_right_le. It states that if f : ℝ → E satisfies ‖f a‖ ≤ δ and ∀ x ∈ [a, b), ‖f' x‖ ≤ K * ‖f x‖ + ε, then for all x ∈ [a, b] we have ‖f x‖ ≤ δ * exp (K * x) + (ε / K) * (exp (K * x) - 1).

Then we use this inequality to prove some estimates on the possible rate of growth of the distance between two approximate or exact solutions of an ordinary differential equation.

The proofs are based on [Hubbard and West, Differential Equations: A Dynamical Systems Approach, Sec. 4.5][HubbardWest-ode], where norm_le_gronwallBound_of_norm_deriv_right_le is called “Fundamental Inequality”.

## TODO #

• Once we have FTC, prove an inequality for a function satisfying ‖f' x‖ ≤ K x * ‖f x‖ + ε, or more generally liminf_{y→x+0} (f y - f x)/(y - x) ≤ K x * f x + ε with any sign of K x and f x.

### Technical lemmas about gronwallBound#

noncomputable def gronwallBound (δ : ) (K : ) (ε : ) (x : ) :

Upper bound used in several Grönwall-like inequalities.

Instances For
theorem gronwallBound_K0 (δ : ) (ε : ) :
= fun x => δ + ε * x
theorem gronwallBound_of_K_ne_0 {δ : } {K : } {ε : } (hK : K 0) :
= fun x => δ * Real.exp (K * x) + ε / K * (Real.exp (K * x) - 1)
theorem hasDerivAt_gronwallBound (δ : ) (K : ) (ε : ) (x : ) :
HasDerivAt () (K * gronwallBound δ K ε x + ε) x
theorem hasDerivAt_gronwallBound_shift (δ : ) (K : ) (ε : ) (x : ) (a : ) :
HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x
theorem gronwallBound_x0 (δ : ) (K : ) (ε : ) :
gronwallBound δ K ε 0 = δ
theorem gronwallBound_ε0 (δ : ) (K : ) (x : ) :
gronwallBound δ K 0 x = δ * Real.exp (K * x)
theorem gronwallBound_ε0_δ0 (K : ) (x : ) :
gronwallBound 0 K 0 x = 0
theorem gronwallBound_continuous_ε (δ : ) (K : ) (x : ) :
Continuous fun ε => gronwallBound δ K ε x

### Inequality and corollaries #

theorem le_gronwallBound_of_liminf_deriv_right_le {f : } {f' : } {δ : } {K : } {ε : } {a : } {b : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ), x Set.Ico a b∀ (r : ), f' x < r∃ᶠ (z : ) in nhdsWithin x (), (z - x)⁻¹ * (f z - f x) < r) (ha : f a δ) (bound : ∀ (x : ), x Set.Ico a bf' x K * f x + ε) (x : ) :
x Set.Icc a bf x gronwallBound δ K ε (x - a)

A Grönwall-like inequality: if f : ℝ → ℝ is continuous on [a, b] and satisfies the inequalities f a ≤ δ and ∀ x ∈ [a, b), liminf_{z→x+0} (f z - f x)/(z - x) ≤ K * (f x) + ε, then f x is bounded by gronwallBound δ K ε (x - a) on [a, b].

See also norm_le_gronwallBound_of_norm_deriv_right_le for a version bounding ‖f x‖, f : ℝ → E.

theorem norm_le_gronwallBound_of_norm_deriv_right_le {E : Type u_1} [] {f : E} {f' : E} {δ : } {K : } {ε : } {a : } {b : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (x : ), x Set.Ico a bHasDerivWithinAt f (f' x) () x) (ha : f a δ) (bound : ∀ (x : ), x Set.Ico a bf' x K * f x + ε) (x : ) :
x Set.Icc a bf x gronwallBound δ K ε (x - a)

A Grönwall-like inequality: if f : ℝ → E is continuous on [a, b], has right derivative f' x at every point x ∈ [a, b), and satisfies the inequalities ‖f a‖ ≤ δ, ∀ x ∈ [a, b), ‖f' x‖ ≤ K * ‖f x‖ + ε, then ‖f x‖ is bounded by gronwallBound δ K ε (x - a) on [a, b].

theorem dist_le_of_approx_trajectories_ODE_of_mem_set {E : Type u_1} [] {v : EE} {s : Set E} {K : } (hv : ∀ (t : ) (x : E), x s t∀ (y : E), y s tdist (v t x) (v t y) K * dist x y) {f : E} {g : E} {f' : E} {g' : E} {a : } {b : } {εf : } {εg : } {δ : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt f (f' t) () t) (f_bound : ∀ (t : ), t Set.Ico a bdist (f' t) (v t (f t)) εf) (hfs : ∀ (t : ), t Set.Ico a bf t s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt g (g' t) () t) (g_bound : ∀ (t : ), t Set.Ico a bdist (g' t) (v t (g t)) εg) (hgs : ∀ (t : ), t Set.Ico a bg t s t) (ha : dist (f a) (g a) δ) (t : ) :
t Set.Icc a bdist (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.

theorem dist_le_of_approx_trajectories_ODE {E : Type u_1} [] {v : EE} {K : NNReal} (hv : ∀ (t : ), LipschitzWith K (v t)) {f : E} {g : E} {f' : E} {g' : E} {a : } {b : } {εf : } {εg : } {δ : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt f (f' t) () t) (f_bound : ∀ (t : ), t Set.Ico a bdist (f' t) (v t (f t)) εf) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt g (g' t) () t) (g_bound : ∀ (t : ), t Set.Ico a bdist (g' t) (v t (g t)) εg) (ha : dist (f a) (g a) δ) (t : ) :
t Set.Icc a bdist (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 the whole space.

theorem dist_le_of_trajectories_ODE_of_mem_set {E : Type u_1} [] {v : EE} {s : Set E} {K : } (hv : ∀ (t : ) (x : E), x s t∀ (y : E), y s tdist (v t x) (v t y) K * dist x y) {f : E} {g : E} {a : } {b : } {δ : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt f (v t (f t)) () t) (hfs : ∀ (t : ), t Set.Ico a bf t s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt g (v t (g t)) () t) (hgs : ∀ (t : ), t Set.Ico a bg t s t) (ha : dist (f a) (g a) δ) (t : ) :
t Set.Icc a bdist (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 some time-dependent set s t, and assumes that the solutions never leave this set.

theorem dist_le_of_trajectories_ODE {E : Type u_1} [] {v : EE} {K : NNReal} (hv : ∀ (t : ), LipschitzWith K (v t)) {f : E} {g : E} {a : } {b : } {δ : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt f (v t (f t)) () t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt g (v t (g t)) () t) (ha : dist (f a) (g a) δ) (t : ) :
t Set.Icc a bdist (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.

theorem ODE_solution_unique_of_mem_set {E : Type u_1} [] {v : EE} {s : Set E} {K : } (hv : ∀ (t : ) (x : E), x s t∀ (y : E), y s tdist (v t x) (v t y) K * dist x y) {f : E} {g : E} {a : } {b : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt f (v t (f t)) () t) (hfs : ∀ (t : ), t Set.Ico a bf t s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt g (v t (g t)) () t) (hgs : ∀ (t : ), t Set.Ico a bg t s t) (ha : f a = g a) (t : ) :
t Set.Icc a bf t = g t

There exists only one solution of an ODE (\dot x=v(t, x)) in a set s ⊆ ℝ × E with a given initial value provided that RHS is Lipschitz continuous in x within s, and we consider only solutions included in s.

theorem ODE_solution_unique {E : Type u_1} [] {v : EE} {K : NNReal} (hv : ∀ (t : ), LipschitzWith K (v t)) {f : E} {g : E} {a : } {b : } (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt f (v t (f t)) () t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ (t : ), t Set.Ico a bHasDerivWithinAt g (v t (g t)) () t) (ha : f a = g a) (t : ) :
t Set.Icc a bf t = g t

There exists only one solution of an ODE (\dot x=v(t, x)) with a given initial value provided that RHS is Lipschitz continuous in x.