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.

Equations

• gronwallBound δ K ε x = if K = 0 then δ + ε * x else δ * Real.exp (K * x) + ε / K * (Real.exp (K * x) - 1)

theorem gronwallBound_K0 (δ : ℝ) (ε : ℝ) : gronwallBound δ 0 ε = fun (x : ℝ) => δ + ε * x

theorem gronwallBound_of_K_ne_0 {δ : ℝ} {K : ℝ} {ε : ℝ} (hK : K ≠ 0) : gronwallBound δ K ε = fun (x : ℝ) => δ * Real.exp (K * x) + ε / K * (Real.exp (K * x) - 1)

theorem hasDerivAt_gronwallBound (δ : ℝ) (K : ℝ) (ε : ℝ) (x : ℝ) : HasDerivAt (gronwallBound δ K ε) (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 ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), (z - x)⁻¹ * (f z - f x) < r) (ha : f a ≤ δ) (bound : ∀ x ∈ Set.Ico a b, f' x ≤ K * f x + ε) (x : ℝ) : x ∈ Set.Icc a b → f 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} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {f' : ℝ → E} {δ : ℝ} {K : ℝ} {ε : ℝ} {a : ℝ} {b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) (ha : ‖f a‖ ≤ δ) (bound : ∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ K * ‖f x‖ + ε) (x : ℝ) : x ∈ Set.Icc a b → ‖f 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 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {f' : ℝ → E} {g' : ℝ → E} {a : ℝ} {b : ℝ} {εf : ℝ} {εg : ℝ} {δ : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (f' t) (Set.Ici t) t) (f_bound : ∀ t ∈ Set.Ico a b, dist (f' t) (v t (f t)) ≤ εf) (hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (g' t) (Set.Ici t) t) (g_bound : ∀ t ∈ Set.Ico a b, dist (g' t) (v t (g t)) ≤ εg) (hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t) (ha : dist (f a) (g a) ≤ δ) (t : ℝ) : 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.

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

theorem dist_le_of_trajectories_ODE_of_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {a : ℝ} {b : ℝ} {δ : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) (hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) (hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t) (ha : dist (f a) (g a) ≤ δ) (t : ℝ) : 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 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} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {a : ℝ} {b : ℝ} {δ : ℝ} (hv : ∀ (t : ℝ), LipschitzWith K (v t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) (ha : dist (f a) (g a) ≤ δ) (t : ℝ) : 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.

theorem ODE_solution_unique_of_mem_Icc_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {a : ℝ} {b : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) (hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) (hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t) (ha : f a = g a) : Set.EqOn f g (Set.Icc a b)

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 the RHS is Lipschitz continuous in x within s, and we consider only solutions included in s.

This version shows uniqueness in a closed interval Icc a b, where a is the initial time.

theorem ODE_solution_unique_of_mem_Icc_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {a : ℝ} {b : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ioc a b, HasDerivWithinAt f (v t (f t)) (Set.Iic t) t) (hfs : ∀ t ∈ Set.Ioc a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ioc a b, HasDerivWithinAt g (v t (g t)) (Set.Iic t) t) (hgs : ∀ t ∈ Set.Ioc a b, g t ∈ s t) (hb : f b = g b) : Set.EqOn f g (Set.Icc a b)

A time-reversed version of ODE_solution_unique_of_mem_Icc_right. Uniqueness is shown in a closed interval Icc a b, where b is the "initial" time.

theorem ODE_solution_unique_of_mem_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {a : ℝ} {b : ℝ} {t₀ : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (ht : t₀ ∈ Set.Ioo a b) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t) (hfs : ∀ t ∈ Set.Ioo a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t) (hgs : ∀ t ∈ Set.Ioo a b, g t ∈ s t) (heq : f t₀ = g t₀) : Set.EqOn f g (Set.Icc a b)

A version of ODE_solution_unique_of_mem_Icc_right for uniqueness in a closed interval whose interior contains the initial time.

theorem ODE_solution_unique_of_mem_Ioo {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {a : ℝ} {b : ℝ} {t₀ : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (ht : t₀ ∈ Set.Ioo a b) (hf : ∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : Set.EqOn f g (Set.Ioo a b)

A version of ODE_solution_unique_of_mem_Icc for uniqueness in an open interval.

theorem ODE_solution_unique_of_eventually {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {t₀ : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (hf : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : f =ᶠ[nhds t₀] g

Local unqueness of ODE solutions.

theorem ODE_solution_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal} {f : ℝ → E} {g : ℝ → E} {a : ℝ} {b : ℝ} (hv : ∀ (t : ℝ), LipschitzWith K (v t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) (ha : f a = g a) : Set.EqOn f g (Set.Icc a b)

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