exists_isPicardLindelof_const_of_contDiffAt
theorem exists_isPicardLindelof_const_of_contDiffAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : E → E} (t₀ : ℝ) {x₀ : E},
ContDiffAt ℝ 1 v x₀ → ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
The theorem `exists_isPicardLindelof_const_of_contDiffAt` states the following: for any normed additive commutative group `E` equipped with a real normed space structure, any function `v` from `E` to `E`, any real number `t₀`, and any element `x₀` of `E`, if `v` is continuously differentiable at `x₀`, then there exist a positive real number `ε` and real numbers `L`, `R`, and `C` such that the function `v` satisfies the hypotheses of the Picard-Lindelöf theorem on the interval `(t₀ - ε, t₀ + ε)`.
In other words, a time-independent, continuously differentiable ordinary differential equation (ODE) is guaranteed to satisfy the conditions of the Picard-Lindelöf theorem, which is a key result in the existence and uniqueness theory of ODEs. This theorem allows us to assert the existence of a solution to the ODE in a small interval around `t₀`.
More concisely: Given a normed additive commutative group `E` with a real normed space structure, a continuously differentiable function `v` from `E` to `E`, a real number `t₀`, and an element `x₀` in `E`, there exist an ε > 0 and constants L, R, and C such that `v` satisfies the hypotheses of the Picard-Lindelöf theorem on the interval (t₀ - ε, t₀ + ε).
|
exists_forall_hasDerivAt_Ioo_eq_of_contDiff
theorem exists_forall_hasDerivAt_Ioo_eq_of_contDiff :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : E → E} (t₀ : ℝ) {x₀ : E}
[inst_2 : CompleteSpace E],
ContDiff ℝ 1 v → ∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t
This theorem states that for a time-independent, continuously differentiable ordinary differential equation (ODE), there is a solution in some open interval. More specifically, given a function `v` of a normed additively commutative group `E` where `E` is also a normed space over real numbers, and given a real number `t₀` and an element `x₀` of `E`, under the condition that `E` is a complete space and `v` is continuously differentiable, there exists a function `f` such that it passes through the point `(t₀, x₀)`, and there exists a positive `ε`, for all `t` in the open interval `(t₀ - ε, t₀ + ε)`, `f` has a derivative at `t` that equals `v(f(t))`. In essence, the theorem guarantees the existence of a local solution around `t₀` to the ODE defined by `v`.
More concisely: Given a time-independent, continuously differentiable ODE defined by a function `v` over a complete normed space `E`, there exists a locally defined solution `f` passing through `(t₀, x₀)` such that `f` is differentiable on an open interval containing `t₀` and `f'(t) = v(f(t))` for all `t` in that interval.
|
PicardLindelof.tMin_le_tMax
theorem PicardLindelof.tMin_le_tMax :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (v : PicardLindelof E), v.tMin ≤ v.tMax
The theorem `PicardLindelof.tMin_le_tMax` states that for all `E`, which is a type belonging to a Normed Additive Commutative Group and also a Normed Space over the real numbers ℝ, and for any `v` that is an instance of the Picard Lindelöf structure on `E`, the minimum time value `tMin` is less than or equal to the maximum time value `tMax`. This theorem is a basic property of the time interval in the Picard Lindelöf structure, which is often used in the study of ordinary differential equations.
More concisely: For any Normed Additive Commutative Group and Normed Space `E` over the real numbers, and for any Picard Lindelöf structure `v` on `E`, the minimum time `tMin` is less than or equal to the maximum time `tMax`.
|
IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq
theorem IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {v : ℝ → E → E}
{tMin t₀ tMax : ℝ} (x₀ : E) {C R : ℝ} {L : NNReal},
IsPicardLindelof v tMin t₀ tMax x₀ L R C →
∃ f, f t₀ = x₀ ∧ ∀ t ∈ Set.Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Set.Icc tMin tMax) t
The Picard-Lindelöf (or Cauchy-Lipschitz) theorem states that for a given normed additive commutative group `E` which is a normed space over the real numbers, and for which the space is complete, given a function `v` mapping real numbers to a function from `E` to `E`, and given real numbers `tMin`, `t₀`, and `tMax`, an element `x₀` of `E`, and real numbers `C` and `R`, along with a non-negative real number `L`, if these satisfy the conditions of the `IsPicardLindelof` property, then there exists a function `f` such that `f` of `t₀` equals `x₀` and for all `t` in the closed interval from `tMin` to `tMax`, the derivative of `f` at `t`, within this interval, equals `v` of `t` applied to `f` of `t`, where `v` of `t` is a function from `E` to `E`.
More concisely: Given a complete normed space `E` over the real numbers, if a function `v` satisfies the conditions of the Picard-Lindelöf theorem, then there exists a unique solution `f` to the initial value problem of the first-order ordinary differential equation `y'(t) = v(t, y(t))`, `y(t0) = x0`, where `t` ranges from `tMin` to `tMax` in the closed interval.
|
exists_forall_hasDerivAt_Ioo_eq_of_contDiffAt
theorem exists_forall_hasDerivAt_Ioo_eq_of_contDiffAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : E → E} (t₀ : ℝ) {x₀ : E}
[inst_2 : CompleteSpace E],
ContDiffAt ℝ 1 v x₀ → ∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t
This theorem states that for a continuously differentiable, time-independent ordinary differential equation (ODE), given a normed additive commutative group `E` over the real numbers, and a function `v` from `E` to `E`, there exists a solution in some open interval around any point `(t₀, x₀)`.
More specifically, if `v` is continuously differentiable at a point `x₀` in `E`, then there exists a function `f` such that `f(t₀) = x₀`, and there exists a positive number `ε` such that for all `t` in the open interval `(t₀ - ε, t₀ + ε)`, `f` has the derivative `v(f(t))` at the point `t`. Here, the open interval `(t₀ - ε, t₀ + ε)` is represented by `Set.Ioo (t₀ - ε) (t₀ + ε)`, where `Set.Ioo a b` denotes the set of all `x` such that `a < x < b`.
More concisely: If a continuously differentiable, time-independent ODE `v` over a normed additive commutative group `E` has a continuously differentiable solution `f` around `(t₀, x₀) ∈ E × E`, then there exists an open interval `(t₀ - ε, t₀ + ε)` such that `f` is the unique function satisfying `f(t₀) = x₀` and `f'(t) = v(f(t))` for all `t ∈ (t₀ - ε, t₀ + ε)`.
|
PicardLindelof.exists_solution
theorem PicardLindelof.exists_solution :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (v : PicardLindelof E)
[inst_2 : CompleteSpace E],
∃ f,
f ↑v.t₀ = v.x₀ ∧ ∀ t ∈ Set.Icc v.tMin v.tMax, HasDerivWithinAt f (v.toFun t (f t)) (Set.Icc v.tMin v.tMax) t
The Picard-Lindelöf (also known as Cauchy-Lipschitz) theorem states that for a given Picard-Lindelöf object `v` in a complete normed additive commutative group `E` endowed with a normed space structure over the real numbers, there exists a function `f` such that `f` at the initial time `v.t₀` equals to the initial state `v.x₀`, and furthermore, for each time `t` in the closed interval from `v.tMin` to `v.tMax`, `f` has a derivative within this interval equal to the function `v.toFun` applied to `t` and `f(t)`. This theorem is a fundamental result in the theory of ordinary differential equations, asserting the existence and uniqueness of solutions under certain conditions.
More concisely: The Picard-Lindelöf theorem guarantees the existence and uniqueness of a continuously differentiable function satisfying a given initial value problem of an ordinary differential equation in a complete normed additive commutative group.
|