Grönwall's inequality
The main technical result of this file is the Grönwall-like inequality
norm_le_gronwall_bound_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_gronwall_bound_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 generallyliminf_{y→x+0} (f y - f x)/(y - x) ≤ K x * f x + εwith any sign ofK xandf x.
Technical lemmas about gronwall_bound
Inequality and corollaries
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 gronwall_bound δ K ε (x - a) on [a, b].
See also norm_le_gronwall_bound_of_norm_deriv_right_le for a version bounding ∥f x∥,
f : ℝ → E.
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 gronwall_bound δ K ε (x - a)
on [a, b].
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.
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.
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.
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.
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.
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.