le_gronwallBound_of_liminf_deriv_right_le
theorem le_gronwallBound_of_liminf_deriv_right_le :
∀ {f f' : ℝ → ℝ} {δ K ε a b : ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), (z - x)⁻¹ * (f z - f x) < r) →
f a ≤ δ → (∀ x ∈ Set.Ico a b, f' x ≤ K * f x + ε) → ∀ x ∈ Set.Icc a b, f x ≤ gronwallBound δ K ε (x - a)
This theorem is a version of the Grönwall's inequality. It states that if a function `f : ℝ → ℝ` is continuous over the closed interval `[a, b]` and satisfies the two conditions: (1) `f a ≤ δ`, and (2) for all `x` in the half-open interval `[a, b)`, the lower limit as `z` approaches `x` from the right side of `(f z - f x)/(z - x)` is less than or equal to `K * f x + ε`, then `f x` is bounded by `gronwallBound δ K ε (x - a)` on the closed interval `[a, b]`.
The function `gronwallBound δ K ε (x - a)` is defined as `δ + ε * x` if `K = 0`, otherwise it is `(δ * exp(K * x) + ε / K * (exp(K * x) - 1))`.
This theorem is particularly useful in the analysis of differential equations and provides an upper bound for the solution of an ordinary differential equation.
More concisely: Given a continuous function `f : ℝ → ℝ` over the interval `[a, b]`, if `f(a) ≤ δ`, and for all `x` in `[a, b)`, `(f(z) - f(x))/(z - x) ≤ K * f(x) + ε`, then `f(x)` is bounded by `δ + ε*x` if `K = 0`, and `δ * exp(K * x) + ε / K * (exp(K * x) - 1)` otherwise on the interval `[a, b]`.
|
dist_le_of_approx_trajectories_ODE
theorem dist_le_of_approx_trajectories_ODE :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal}
{f g f' g' : ℝ → E} {a b εf εg δ : ℝ},
(∀ (t : ℝ), LipschitzWith K (v 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) →
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) →
dist (f a) (g a) ≤ δ →
∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ gronwallBound δ (↑K) (εf + εg) (t - a)
This theorem states that if `f` and `g` are two approximate solutions of the same ordinary differential equation, the distance between them does not grow faster than an exponential rate. To be precise, if for any real number `t`, the function `v t` is Lipschitz continuous with a nonnegative constant `K`, and `f` and `g` are both continuous on a closed interval `[a, b]`. Moreover, if for all `t` in the half-open interval `[a, b)`, `f` and `g` have derivatives `f' t` and `g' t` respectively within the set of all real numbers greater than or equal to `t`, and the distances of these derivatives from `v t (f t)` and `v t (g t)` are not more than `εf` and `εg` respectively. Lastly, if the initial distance between `f a` and `g a` is not more than a real number 'δ', then for any `t` in the closed interval `[a, b]`, the distance between `f t` and `g t` is not more than the upper bound given by Gronwall's inequality, which depends on `δ`, `K`, `εf`, `εg`, and `(t - a)`.
More concisely: If two approximate solutions `f` and `g` of an ordinary differential equation satisfy certain Lipschitz and continuity conditions, and their initial distance is bounded, then their distance at any given time is bounded by Gronwall's inequality.
|
norm_le_gronwallBound_of_norm_deriv_right_le
theorem norm_le_gronwallBound_of_norm_deriv_right_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → E} {δ K ε a b : ℝ},
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
‖f a‖ ≤ δ →
(∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ K * ‖f x‖ + ε) → ∀ x ∈ Set.Icc a b, ‖f x‖ ≤ gronwallBound δ K ε (x - a)
This theorem provides a Grönwall-like inequality in the context of real-valued normed space. Suppose we have a function `f` from real numbers to a normed additively commutative group `E`, which is continuous on a closed interval `[a, b]`. This function has a right derivative `f' x` at every point `x` in the half-open interval `[a, b)`. If the norm of `f a` is less than or equal to a real number `δ` and for all `x` in `[a, b)`, the norm of `f' x` is less than or equal to `K` times the norm of `f x` plus `ε`, then the norm of `f x` is bounded by the function `gronwallBound δ K ε (x - a)` on the closed interval `[a, b]`. Here, `gronwallBound` is a function defined on four real variables, which has a different value if `K` equals 0 or not.
More concisely: If a continuous function `f` on the closed interval `[a, b]` with right derivative `f'` satisfies `||f(a)|| ≤ δ` and `||f'(x)|| ≤ K||f(x)|| + ε` for all `x` in `[a, b)`, then `||f(x)|| ≤ gronwallBound δ K ε (x - a)` for all `x` in `[a, b]`.
|
ODE_solution_unique_of_mem_Ioo
theorem ODE_solution_unique_of_mem_Ioo :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E}
{K : NNReal} {f g : ℝ → E} {a b t₀ : ℝ},
(∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) →
t₀ ∈ Set.Ioo a b →
(∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) →
(∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) → f t₀ = g t₀ → Set.EqOn f g (Set.Ioo a b)
This theorem, `ODE_solution_unique_of_mem_Ioo`, states that for a given type `E` which forms a normed additive commutative group and a normed space over the real numbers, along with a function `v` mapping real numbers and elements of `E` to `E`, a pair of sets `s` mapping real numbers to sets of `E`, a non-negative real number `K`, two functions `f` and `g` mapping real numbers to `E`, and three real numbers `a`, `b`, and `t₀`, if every `v t` is Lipschitz continuous with constant `K` on the set `s t` and both `f` and `g` have the derivative `v t (f t)` and `v t (g t)`, respectively, at every point `t` in the open interval `(a, b)` (meaning `t` is strictly greater than `a` and strictly less than `b`) with `f t` and `g t` belonging to the set `s t`, and `f t₀ = g t₀`, then `f` and `g` are equal for all `t` in the open interval `(a, b)`. In other words, in the context of ordinary differential equations (ODEs), this theorem asserts the uniqueness of the solution to an ODE in an open interval.
More concisely: Given a normed additive commutative group `E`, a Lipschitz continuous function `v : ℝ × E → E`, sets `s : ℝ → sets E`, real numbers `a < b` and `K ≥ 0`, functions `f, g : ℝ → E` with `f 0 = g 0`, and assuming `f` and `g` have the same derivative `v t (f t)` and `v t (g t)` in the open interval `(a, b)` where `f t` and `g t` belong to `s t`, then `f = g` on `(a, b)`.
|
dist_le_of_trajectories_ODE
theorem dist_le_of_trajectories_ODE :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal} {f g : ℝ → E}
{a b δ : ℝ},
(∀ (t : ℝ), LipschitzWith K (v t)) →
ContinuousOn f (Set.Icc a b) →
(∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
ContinuousOn g (Set.Icc a b) →
(∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ δ * (↑K * (t - a)).exp
The theorem `dist_le_of_trajectories_ODE` states that if `f` and `g` are two exact solutions of the same ordinary differential equation, then the distance between them cannot grow faster than exponentially. The assumptions are that for all `t`, the function `v t` is Lipschitz continuous with constant `K`, that `f` and `g` are continuous on the closed interval [a, b], and that `f` and `g` have derivatives within the interval [a, b) that satisfy the differential equation. Furthermore, the initial distance between `f a` and `g a` is less than or equal to `δ`. Under these conditions, for all `t` in the closed interval [a, b], the distance between `f t` and `g t` is less than or equal to `δ` times `K` times the exponent of `(t - a)`. This theorem is a consequence of Grönwall's inequality.
More concisely: If two Lipschitz continuous exact solutions of an ordinary differential equation with initial distance less than or equal to δ, on a closed interval where their derivatives also satisfy the equation, have distance at most δ × K × exp((t - a)) for all t in the interval, where K is the Lipschitz constant.
|
ODE_solution_unique_of_mem_Icc_right
theorem ODE_solution_unique_of_mem_Icc_right :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E}
{K : NNReal} {f g : ℝ → E} {a b : ℝ},
(∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) →
ContinuousOn f (Set.Icc a b) →
(∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
(∀ t ∈ Set.Ico a b, f t ∈ s t) →
ContinuousOn g (Set.Icc a b) →
(∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
(∀ t ∈ Set.Ico a b, g t ∈ s t) → f a = g a → Set.EqOn f g (Set.Icc a b)
The theorem `ODE_solution_unique_of_mem_Icc_right` states that within a closed interval `[a, b]`, where `a` is the initial time, there exists a unique solution to an ordinary differential equation (ODE) of the form \(\dot x = v(t, x)\) that lies within a given set `s ⊆ ℝ × E` and has a specified initial value. This uniqueness is guaranteed under the conditions that the right-hand side function `v` is Lipschitz continuous with a nonnegative real constant `K` within `s` and that the solutions `f` and `g` we consider are continuous on the interval `[a, b]`, have derivatives within the set `s` that match the function `v` evaluated at `f` and `g`, and that `f` and `g` yield the same initial value. If these conditions are met, then the functions `f` and `g` are equal on the interval `[a, b]`.
More concisely: Given an ODE \(\dot x = v(t, x)\) with Lipschitz continuous right-hand side \(v\) on a closed interval \([a, b]\), and given two solutions \(f, g \colon [a, b] \to \mathbb{R} \times E\) with the same initial value and continuous derivatives matching \(v\), then \(f = g\) on \([a, b]\).
|
ODE_solution_unique_of_mem_Icc_left
theorem ODE_solution_unique_of_mem_Icc_left :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E}
{K : NNReal} {f g : ℝ → E} {a b : ℝ},
(∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) →
ContinuousOn f (Set.Icc a b) →
(∀ t ∈ Set.Ioc a b, HasDerivWithinAt f (v t (f t)) (Set.Iic t) t) →
(∀ t ∈ Set.Ioc a b, f t ∈ s t) →
ContinuousOn g (Set.Icc a b) →
(∀ t ∈ Set.Ioc a b, HasDerivWithinAt g (v t (g t)) (Set.Iic t) t) →
(∀ t ∈ Set.Ioc a b, g t ∈ s t) → f b = g b → Set.EqOn f g (Set.Icc a b)
The theorem `ODE_solution_unique_of_mem_Icc_left` establishes the uniqueness of solutions to a given ordinary differential equation (ODE). Given two functions `f` and `g` that are continuous on a closed interval `[a, b]` (with `b` being the initial time rather than the typical `a`), if both functions satisfy the ODE—meaning they have the same derivative with respect to time `t` at every point in the open interval `(a, b]` and the values of `f` and `g` lie in the set `s t` for every point in `(a, b]`—and they coincide at time `b`, then `f` and `g` are identical on the entire interval `[a, b]`. This shows that for this type of ODE and under these conditions, there can only be one unique solution that fits the given initial conditions and properties.
More concisely: If two continuous functions on a closed interval with the same derivative on the open interval and equal values at the right endpoint have overlapping definitions on the open interval, then they are equal on the entire closed interval.
|
ODE_solution_unique_of_mem_Icc
theorem ODE_solution_unique_of_mem_Icc :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E}
{K : NNReal} {f g : ℝ → E} {a b t₀ : ℝ},
(∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) →
t₀ ∈ Set.Ioo a b →
ContinuousOn f (Set.Icc a b) →
(∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t) →
(∀ t ∈ Set.Ioo a b, f t ∈ s t) →
ContinuousOn g (Set.Icc a b) →
(∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t) →
(∀ t ∈ Set.Ioo a b, g t ∈ s t) → f t₀ = g t₀ → Set.EqOn f g (Set.Icc a b)
This theorem states that for two functions `f` and `g` mapping real numbers to a normed space `E`, if both `f` and `g` satisfy the same ordinary differential equation (ODE), and their values at a certain point `t₀` in an open interval `(a, b)` are the same, then `f` and `g` are equal on the closed interval `[a, b]`. This ODE is given by the function `v`, which for every `t`, is Lipschitz continuous on the set `s(t)`. We also have that `f` and `g` are continuous on `[a, b]`, their derivatives at any `t` in `(a, b)` are given by `v(t, f(t))` and `v(t, g(t))` respectively, and their values at any `t` in `(a, b)` belong to the set `s(t)`. This theorem essentially says that under these conditions, the solution to the ODE is unique in the interval `[a, b]`.
More concisely: If two real-valued functions `f` and `g` defined on an open interval `(a, b)` satisfy the same Lipschitz continuous ordinary differential equation `v(t, x)` with the same initial condition `f(a) = g(a)`, and their derivatives belong to the domain of `v` at all points in `(a, b)`, then `f = g` on the closed interval `[a, b]`.
|
ODE_solution_unique
theorem ODE_solution_unique :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal} {f g : ℝ → E}
{a b : ℝ},
(∀ (t : ℝ), LipschitzWith K (v t)) →
ContinuousOn f (Set.Icc a b) →
(∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
ContinuousOn g (Set.Icc a b) →
(∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
f a = g a → Set.EqOn f g (Set.Icc a b)
This theorem states that there exists a unique solution for an ordinary differential equation (ODE) of the form \(\dot x = v(t, x)\) with a given initial value, provided that the right-hand side function 'v' is Lipschitz continuous in 'x'. More specifically, given two solutions 'f' and 'g' of the ODE, both continuously defined on a closed interval [a, b], with the derivative of each at 't' in the right-closed interval [a, b) being the value of 'v' evaluated at 't' and the function value, and both solutions having the same initial value at 'a', then 'f' and 'g' should be equal on the whole interval [a, b].
More concisely: Given a Lipschitz continuous right-hand side function 'v' for the ODE \(\dot x = v(t, x)\), and initial value 'x0' at 't=a', there exists a unique solution on the interval [a, b] such that any two solutions 'f' and 'g' of the ODE with the same initial value 'x0' at 't=a' are equal on the whole interval [a, b].
|
ODE_solution_unique_of_eventually
theorem ODE_solution_unique_of_eventually :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E}
{K : NNReal} {f g : ℝ → E} {t₀ : ℝ},
(∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) →
(∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) →
(∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) → f t₀ = g t₀ → (nhds t₀).EventuallyEq f g
The theorem states that solutions to an ordinary differential equation (ODE) are locally unique. Specifically, given a normed vector space `E` over the real numbers `ℝ`, a function `v : ℝ → E → E` that specifies the ODE, and a function `s : ℝ → Set E` that specifies the domain of `v` at each time point, together with a Lipschitz continuity condition on `v`, if two functions `f` and `g` have the same derivative `v t (f t)` and `v t (g t)` respectively at all points `t` near a point `t₀`, and also both `f t` and `g t` are in the set `s t` near `t₀`, then if `f t₀ = g t₀`, the two functions `f` and `g` are equal near `t₀`. In other words, two solutions to the ODE that match at a single point `t₀` must match at all points near `t₀`. This local uniqueness is a fundamental property of solutions to ODEs.
More concisely: Given an ordinary differential equation with Lipschitz continuous vector field, if two solutions agree at a point and are defined in a neighborhood of that point, then they are equal in that neighborhood.
|
dist_le_of_trajectories_ODE_of_mem
theorem dist_le_of_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 : ℝ → E} {a b δ : ℝ},
(∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) →
ContinuousOn f (Set.Icc a b) →
(∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
(∀ t ∈ Set.Ico a b, f t ∈ s t) →
ContinuousOn g (Set.Icc a b) →
(∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
(∀ t ∈ Set.Ico a b, g t ∈ s t) →
dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ δ * (↑K * (t - a)).exp
The theorem `dist_le_of_trajectories_ODE_of_mem` states the following:
Consider two functions `f` and `g` which are solutions of the same ordinary differential equation defined by a vector field `v`. Let `s` be a time-dependent set such that for every point of time `t`, the vector field `v` is Lipschitz continuous with some nonnegative constant `K` on `s(t)` and both `f(t)` and `g(t)` are in `s(t)`. Let `a` and `b` be two real numbers such that `f` and `g` are continuous on the closed interval `[a, b]` and both `f` and `g` have their derivatives at every point in the half-open interval `[a, b)` equal to `v(t)` evaluated at `f(t)` and `g(t)` respectively. Suppose the distance between `f(a)` and `g(a)` is less than or equal to some real number `δ`. Then, the theorem states that for every point `t` in the closed interval `[a, b]`, the distance between `f(t)` and `g(t)` is less than or equal to `δ` times the exponential of `K` times `(t - a)`. This is essentially a statement about the bound on the growth of the distance between two solutions of the same ODE, asserting that the distance cannot grow faster than exponentially. This is a consequence of Grönwall's inequality, and sometimes referred to as Grönwall's inequality as well.
More concisely: Given two solutions `f` and `g` of the same Lipschitz continuous ODE with initial points close enough, the distance between them on any interval where both are defined is bounded by the initial distance multiplied by the exponential of the Lipschitz constant times the length of the interval.
|
dist_le_of_approx_trajectories_ODE_of_mem
theorem 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 : ℝ), 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)
This theorem states that if we have two approximate solutions, `f` and `g`, of the same ordinary differential equation (ODE) defined by `v`, then the distance between them cannot grow faster than exponentially. This is a direct implication of Grönwall's inequality.
This theorem assumes that all the inequalities hold true within a time-dependent set `s t`, and that the solutions `f` and `g` never exit this set. It also assumes that `f` and `g` are Lipschitz continuous on `s t` with a nonnegative constant `K`. Both `f` and `g` are required to be continuous on the closed interval `[a, b]`. For every point `t` in the open interval `(a, b)`, `f` and `g` have respective derivatives `f'` and `g'` and both `f` and `g` do not deviate from the values given by `v` by more than `εf` and `εg` respectively. Lastly, the theorem assumes that the distance between `f` and `g` at the point `a` does not exceed `δ`.
Under these assumptions, the theorem shows that for every point `t` in the closed interval `[a, b]`, the distance between `f(t)` and `g(t)` is less than or equal to the Grönwall's bound of `δ`, `K`, `εf + εg`, and `t - a`. This essentially implies that the solutions `f` and `g` stay close to each other as specified by the Grönwall's bound.
More concisely: If two Lipschitz continuous approximate solutions of an ODE with a common time-dependent set, initial distance, and continuous derivatives never exceeding given errors, then their maximum distance is bounded by Grönwall's inequality using the constants involved.
|