Theorems · Theorem · ordinary differential equations

eq_zero_of_abs_deriv_le_mul_abs_self_of_eq_zero_right

∀ {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 = 0 → (∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ K * ‖f x‖) → ∀ x ∈ Set.Icc a b, f x = 0

Let f : [a, b] → E be a differentiable function such that f a = 0 and ‖f'(x)‖ ≤ K ‖f(x)‖ for some constant K. Then f = 0 on [a, b].

Defined in

Mathlib.Analysis.ODE.Gronwall

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace