Differential equations

TheoremCauchy-Lipschitz Theorem#

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local solution whose initial point x may be different from the centre x₀ of the closed ball within which the properties of the vector field hold.

IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) :
  ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t

Sources

• Mathlib documentation: IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt
• Source of IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt in Mathlib/Analysis/ODE/ExistUnique.lean
• Mathlib undergraduate list: Multivariable calculus › Differential equations
• 1000+ theorems list: Q530152
• 1000+ theorems project: Q530152
• Wikipedia: Picard–Lindelöf theorem
• Wikidata: Q530152

MathlibIsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt

Uses 10 · Used by 1

Statement usesCompleteness · Continuous linear map · Finite set · Normed vector space over a normed field · Topological module

Proof usesBochner integral · Carathéodory's theorem (measure theory) · Lebesgue measure (Measures and integral calculus) · Lipschitz continuity · Metric structure

Used byLocal existence of integral curves

TheoremGrönwall lemma#

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

norm_le_gronwallBound_of_norm_deriv_right_le.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {f 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)

Sources

• Mathlib documentation: norm_le_gronwallBound_of_norm_deriv_right_le
• Source of norm_le_gronwallBound_of_norm_deriv_right_le in Mathlib/Analysis/ODE/Gronwall.lean
• Mathlib undergraduate list: Multivariable calculus › Differential equations

Mathlibnorm_le_gronwallBound_of_norm_deriv_right_le

Uses 12

Statement usesContinuous linear map · Exponential · Normed vector space over a normed field · Topological module

Proof usesAssociative algebra over a commutative ring · Closure · Completeness · Derivative at a point · Euclidean affine space · Order topology · Ordered ring · Topological ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.