Theorems · Theorem · ordinary differential equations

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)

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

Defined in

Mathlib.Analysis.ODE.Gronwall

Cited by

2 results in Mathlib

Foundations

Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace