Theorems · Theorem · real analysis

Convex.image_sub_le_mul_sub_of_deriv_le

∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          ∀ {C : ℝ}, (∀ x ∈ interior D, deriv f x ≤ C) → ∀ x ∈ D, ∀ y ∈ D, x ≤ y → f y - f x ≤ C * (y - x)

Let f be a function continuous on a convex (or, equivalently, connected) subset D of the real line. If f is differentiable on the interior of D and f' ≤ C, then f grows at most as fast as C * x on D, i.e., f y - f x ≤ C * (y - x) whenever x, y ∈ D, x ≤ y.

Defined in

Mathlib.Analysis.Calculus.Deriv.MeanValue

Cited by

2 results in Mathlib

Foundations

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