Theorems · Theorem · ordinary differential equations

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)

A Grönwall-like inequality: if f : ℝ → ℝ is continuous on [a, b] and satisfies the inequalities f a ≤ δ and ∀ x ∈ [a, b), liminf_{z→x+0} (f z - f x)/(z - x) ≤ K * (f x) + ε, then f x is bounded by gronwallBound δ K ε (x - a) on [a, b]. See also norm_le_gronwallBound_of_norm_deriv_right_le for a version bounding ‖f x‖, f : ℝ → E.

Defined in

Mathlib.Analysis.ODE.Gronwall

Cited by

1 results in Mathlib

Foundations

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