mathlib3 documentation

analysis.ODE.gronwall

Grönwall's inequality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, 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 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 `gronwall_bound` #

noncomputable def gronwall_bound (δ K ε x : ℝ) :

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

Equations

gronwall_bound δ K ε x = ite (K = 0) (δ + ε * x) (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))

theorem gronwall_bound_K0 (δ ε : ℝ) :

gronwall_bound δ 0 ε = λ (x : ℝ), δ + ε * x

theorem gronwall_bound_of_K_ne_0 {δ K ε : ℝ} (hK : K ≠ 0) :

gronwall_bound δ K ε = λ (x : ℝ), δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)

theorem has_deriv_at_gronwall_bound (δ K ε x : ℝ) :

has_deriv_at (gronwall_bound δ K ε) (K * gronwall_bound δ K ε x + ε) x

theorem has_deriv_at_gronwall_bound_shift (δ K ε x a : ℝ) :

has_deriv_at (λ (y : ℝ), gronwall_bound δ K ε (y - a)) (K * gronwall_bound δ K ε (x - a) + ε) x

theorem gronwall_bound_x0 (δ K ε : ℝ) :

gronwall_bound δ K ε 0 = δ

theorem gronwall_bound_ε0 (δ K x : ℝ) :

gronwall_bound δ K 0 x = δ * rexp (K * x)

theorem gronwall_bound_ε0_δ0 (K x : ℝ) :

gronwall_bound 0 K 0 x = 0

theorem gronwall_bound_continuous_ε (δ K x : ℝ) :

continuous (λ (ε : ℝ), gronwall_bound δ K ε x)

Inequality and corollaries #

theorem le_gronwall_bound_of_liminf_deriv_right_le {f f' : ℝ → ℝ} {δ K ε a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → ∀ (r : ℝ), f' x < r → (∃ᶠ (z : ℝ) in nhds_within x (set.Ioi x), (z - x)⁻¹ * (f z - f x) < r)) (ha : f a ≤ δ) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → f' x ≤ K * f x + ε) (x : ℝ) (H : x ∈ set.Icc a b) :

f x ≤ gronwall_bound δ 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 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.

theorem norm_le_gronwall_bound_of_norm_deriv_right_le {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f f' : ℝ → E} {δ K ε a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at f (f' x) (set.Ici x) x) (ha : ‖f a‖ ≤ δ) (bound : ∀ (x : ℝ), x ∈ set.Ico a b → ‖f' x‖ ≤ K * ‖f x‖ + ε) (x : ℝ) (H : x ∈ set.Icc a b) :

‖f x‖ ≤ gronwall_bound δ 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 gronwall_bound δ K ε (x - a) on [a, b].

theorem dist_le_of_approx_trajectories_ODE_of_mem_set {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {v : ℝ → E → E} {s : ℝ → set E} {K : ℝ} (hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → has_dist.dist (v t x) (v t y) ≤ K * has_dist.dist x y) {f g f' g' : ℝ → E} {a b εf εg δ : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at f (f' t) (set.Ici t) t) (f_bound : ∀ (t : ℝ), t ∈ set.Ico a b → has_dist.dist (f' t) (v t (f t)) ≤ εf) (hfs : ∀ (t : ℝ), t ∈ set.Ico a b → f t ∈ s t) (hg : continuous_on g (set.Icc a b)) (hg' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at g (g' t) (set.Ici t) t) (g_bound : ∀ (t : ℝ), t ∈ set.Ico a b → has_dist.dist (g' t) (v t (g t)) ≤ εg) (hgs : ∀ (t : ℝ), t ∈ set.Ico a b → g t ∈ s t) (ha : has_dist.dist (f a) (g a) ≤ δ) (t : ℝ) (H : t ∈ set.Icc a b) :

has_dist.dist (f t) (g t) ≤ gronwall_bound δ 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} [normed_add_comm_group E] [normed_space ℝ E] {v : ℝ → E → E} {K : nnreal} (hv : ∀ (t : ℝ), lipschitz_with K (v t)) {f g f' g' : ℝ → E} {a b εf εg δ : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at f (f' t) (set.Ici t) t) (f_bound : ∀ (t : ℝ), t ∈ set.Ico a b → has_dist.dist (f' t) (v t (f t)) ≤ εf) (hg : continuous_on g (set.Icc a b)) (hg' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at g (g' t) (set.Ici t) t) (g_bound : ∀ (t : ℝ), t ∈ set.Ico a b → has_dist.dist (g' t) (v t (g t)) ≤ εg) (ha : has_dist.dist (f a) (g a) ≤ δ) (t : ℝ) (H : t ∈ set.Icc a b) :

has_dist.dist (f t) (g t) ≤ gronwall_bound δ ↑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} [normed_add_comm_group E] [normed_space ℝ E] {v : ℝ → E → E} {s : ℝ → set E} {K : ℝ} (hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → has_dist.dist (v t x) (v t y) ≤ K * has_dist.dist x y) {f g : ℝ → E} {a b δ : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at f (v t (f t)) (set.Ici t) t) (hfs : ∀ (t : ℝ), t ∈ set.Ico a b → f t ∈ s t) (hg : continuous_on g (set.Icc a b)) (hg' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at g (v t (g t)) (set.Ici t) t) (hgs : ∀ (t : ℝ), t ∈ set.Ico a b → g t ∈ s t) (ha : has_dist.dist (f a) (g a) ≤ δ) (t : ℝ) (H : t ∈ set.Icc a b) :

has_dist.dist (f t) (g t) ≤ δ * rexp (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} [normed_add_comm_group E] [normed_space ℝ E] {v : ℝ → E → E} {K : nnreal} (hv : ∀ (t : ℝ), lipschitz_with K (v t)) {f g : ℝ → E} {a b δ : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at f (v t (f t)) (set.Ici t) t) (hg : continuous_on g (set.Icc a b)) (hg' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at g (v t (g t)) (set.Ici t) t) (ha : has_dist.dist (f a) (g a) ≤ δ) (t : ℝ) (H : t ∈ set.Icc a b) :

has_dist.dist (f t) (g t) ≤ δ * rexp (↑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} [normed_add_comm_group E] [normed_space ℝ E] {v : ℝ → E → E} {s : ℝ → set E} {K : ℝ} (hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → has_dist.dist (v t x) (v t y) ≤ K * has_dist.dist x y) {f g : ℝ → E} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at f (v t (f t)) (set.Ici t) t) (hfs : ∀ (t : ℝ), t ∈ set.Ico a b → f t ∈ s t) (hg : continuous_on g (set.Icc a b)) (hg' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at g (v t (g t)) (set.Ici t) t) (hgs : ∀ (t : ℝ), t ∈ set.Ico a b → g t ∈ s t) (ha : f a = g a) (t : ℝ) (H : t ∈ set.Icc a b) :

f 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} [normed_add_comm_group E] [normed_space ℝ E] {v : ℝ → E → E} {K : nnreal} (hv : ∀ (t : ℝ), lipschitz_with K (v t)) {f g : ℝ → E} {a b : ℝ} (hf : continuous_on f (set.Icc a b)) (hf' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at f (v t (f t)) (set.Ici t) t) (hg : continuous_on g (set.Icc a b)) (hg' : ∀ (t : ℝ), t ∈ set.Ico a b → has_deriv_within_at g (v t (g t)) (set.Ici t) t) (ha : f a = g a) (t : ℝ) (H : t ∈ set.Icc a b) :

f 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.